I find myself very disappointed with my initial formulation of mathematical intelligence in my first blog post, or rather I should say I am unsatisfied with it. Essentially, the premise that there should be some set of ideas that can be used to construct a desired proof seems obvious in all but the most exceptional cases – that is the existence of some fuzzy set like L[T,A] is to be taken granted for all provably true propositions and doesn’t require any unnecessary mathematical formulation. If we wanted to add a little bit of rigor we can at least say that L[T,A] can be populated with elements of a deduction chain based on modus ponens which ends with the theorem T. This idea of a deduction chain can be formalized within first-order logic, but it is beyond the scope of this blog to discuss it in detail. However, the concept of a deduction can lead to a more well-defined L[T,A]. Define L[T,A] as follows – a set of propositions B is included in L[T,A] if and only if B is a deduction from A to T. An actual example would be useful. Suppose we wanted to prove the proposition that Bob is an animal, and suppose we had axioms that Bob is a cat and that a cat is an animal. Quite clearly there is a deduction – bob is a cat and all cats are animals, therefore bob is a cat, so we include all of those propositions in L[T,A].

Now, this seems useless unless there is something to be gained from analyzing L[T,A]. I should instead focus on the properties of L[T,A]. Take the following question. Suppose B and C are valid deductions from A to T and with B not equal to C. Is there necessarily some deduction D such that D is not equal to B or C? Put another way, if we have two different deductions, can we find another not equal to the first two? Thought it doesn’t matter for our purposes, the answer returns in the affirmative if there is some common deductive element of B and C different from the axioms themselves and the desired theorem. Ultimately, the fact that L[T,A] has something like definite structural properties is interesting. A more interesting question is as follows: when does L[T,A] contain nothing? Well clearly, if T doesn’t follow from A or if T is false, then L[T,A] is empty. However, what if T does follow from A, and L[T,A] is empty? That is, T is true but undeducible or unprovable.

One would wisely consider whether such a situation is possible, but as Kurt Godel proved in the first part of the twentieth century, it most certainly is. Godel’s brilliant insight was to realize and show mathematically that the notions of provability and truth are not the same by showing that there are true yet unprovable statements. Perhaps more radically, Godel showed that truth was not only “that which can be justified.” The resulting theorems were called Godel’s incompleteness theorems, and the first of them can be stated as follows. “Any consistent formal system F within which a certain amount of elementary arithmetic can be carried out is incomplete such that there are statements of the language of F which can neither be proved nor disproved in F.”

Godel himself uses a language example that hits at the heart of the matter. Take the following proposition T, “T is not provable in F” and note that the statement T makes a claim about itself (that is, it is self-referential). Now if T is true, then by definition T is not provable in F. Under this assumption, T is not provable, but it is certainly true on the basis that we assumed T is true, and we deduce that T is true but unprovable. If T is not true, then it must be false and we have that T is not not provable in F, or T is provable in F. If T is provable in F, then T is true in F and hence we arrive at a contradiction. That is T cannot both be true and false. Hence, the proposition “T is not provable in F” is true. This discovery was monumental – not only did it have profound mathematical implications, it also had profound philosophical implications by challenging the type of rationalism that seeks explanations for all things.

As for the figurative holy grail, it would be most useful to find a method for illuminating deductions. In my next post, I will look at automated theorem proving and the methods currently being used to find deductions autonomously.