## Proof and Computation

In my last post, I mentioned that I wanted to write about automated theorem proving. As it turns out, finding quality blog posts about this subject is very difficult due to it being a relatively new and confusing field. I did however come across a community blog of scientists, Less Wrong, that gave me a good starting place for thinking about the problem. There is a general method using first order logic that would allow us to construct a proof for any provable proposition and the author Jonah Sinick mentions this, but there are also downsides noted.

“It’s easy to give an algorithm that generates a proof of a mathematical theorem that’s provable: choose a formal language with definitions and axioms, and for successive values of n, enumerate all sequences of mathematical deductions of length n, halting if the final line of a sequence is the statement of the desired theorem. But the running time of this algorithm is exponential in the length of the proof, and the algorithm is infeasible to implement except for theorems with very short proofs.”

It’s certainly interesting that a general algorithm exists for provable propositions but the algorithm is awful. All we can guarantee in this algorithm is that a deduction will be returned in some finite amount of time (the universe may die before it can be returned). I suppose a kind of ultimate question is if there is some algorithm that necessarily runs in less time than the enumeration technique and produces the same proof? I think the fact that the author raises the obvious connection between theorem proving and general artificial intelligence is interesting, since it seems likely that new advances in “deep-learning” techniques will create better algorithms in the future. Furthermore, there is the question of what currently is provable in a general sense. The blog post mentions that only trivial theorems seem provable. Sinick writes, “I don’t know of any computer programs that have been able to prove theorems outside of the class ‘very routine and not requiring any ideas,’ without human assistance (and without being heavily specialized to an individual theorem).”

Sinick then mentions an example of theorems that if provable would hugely increase his confidence in the prospect of a true general AI. To him this could mean deriving the Sylow subgroup theorems. Since the Sylow subgroup theorems are constructed from the group axioms, we necessarily need to prove the Sylow subgroup theorems from the group axioms. I’ve had experience constructing these proofs myself, and the bizarre thing is that often some idea not in the axioms or derived from the axioms must be adapted to prove the theorems. These ideas themselves can be thought of as giving the justification for a deduction. Modus ponens or logical inference is an idea that sits behind some deduction in first order logic for instance or even the law of contradiction.

An efficient method for finding a correct deduction must then be able to illuminate the ideas that sit behind deductions from axioms. One would naturally think that the time to find a deduction would be based, at least partially, on the “complexity” of the set of ideas, which would be difficult to define concretely since two sets of separate ideas may be able to prove the same theorem. Perhaps something like Kolmogorov complexity (something that measures the complexity of a given string – for instance the string 0000 is less complex than 1214) would be a good starting place to look at complexity as a legitimate mathematical construct.

Ultimately, I think this problem has been very interesting to think about. The notion of a trivial set of theorems is interesting as well as the complexity of a set of ideas to required guarantee a deduction. Perhaps next time we can look at ways of defining the complexity of a set of axioms and an associated theorem T.

http://lesswrong.com/lw/hvv/progress_on_automated_mathematical_theorem_proving

Edit: It seems that Chaitin’s incompleteness theorem will guarantee that some string is unprovably complex past some level of complexity. Likely, this will be a huge problem.

## Provability and Truth

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.

## What Makes a Mathematician

I recently came across an article by the highly respected Cal Tech mathematician Terence Tao titled, “Does one have to be a genius to do maths?”