How to determine the probability of an "existence" question

Question

I am having a go at creating a program that does math like a human. By inventing statements, assigning probabilities to statements (to come back and think more deeply about later). But I'm stuck at the first hurdle.

If it is given the proposition

   ∃x∈ℕ: x==123

So, like a human it might test this proposition for a hundred or so numbers and then assign this proposition as "unlikely to be true". In other words it has concluded that all natural numbers are not equal to 123. Clearly ludicrous!

On the other hand this statement it decides is probably false which is good:

 ∃x∈ℕ: x+3 ≠ 3+x

Any ideas how to get round this hurdle? How does a human "know" for example that all natural numbers are different from the number 456. What makes these two cases different?

I don't want to give it too many axioms. I want it to find out things for itself.

Answer 1

A human has an abstract concept of numbers in mind. So 456 is a unique entity which is by definition unlike any other number because that are other unique entities. If you give ∃x ∈ ℕ: x==123 to your system it could check the property of natural numbers by counting from 0 to 123 to conclude that the statement is true. A human does it in another way. A human would "see" that it is a natural number because it has no decimal point. Because of the concept of natural numbers the statement is immediately clear. To get a faster result here the machine could check just the decimal point.

In your second case you have to apply the commutative property of addition and you are done because the syntax is equal then.

The second problem is more syntactic while the first is semantic. Your machine may "know" the commutative property of addition but not the concept of natural numbers. Therefore, it has to count.

Answer 2

You need some sort of interpretation abstraction before your mathematical reasoning. While the text might read "123", you need to parse this into a literal of type Natural Number or Integer. Similarly, "x" could be a member variable. Then your deduction becomes, is literal 123 a Natural Number? Yes.

As for the second statement, you should hopefully be able to reason to definitely false. Your internal representation of a sum should not be order dependent since addition is commutative. Then, the check for equality must handle this unordered property.