# How to prove a proof is correct

A one-line proposition $A$ can generate a 100-page proof $p(A)$. Since the proof is very long, it's highly suspectable that there is a mistake in it, which cannot be found out even after careful proofread by many people.

So we should write a proof $p(p(A))$ to make sure $p(A)$ is correct. By a similar argument, we should have $p(p(p(A))), p(p(p(p(A)))), \dots$.

This seems ridiculous because $1+1=2$ is commonly known as correct, which doesn't need a complicated proof. So (from my own point of view) it's better to regard a proof as a decomposition of a proposition into a series of axioms. But there are two problems:

• How many axioms do we need? Are they consistent?

• What is the structure of this decomposition (that makes it hard for a machine to do automatic proof)?

It seems the first problem has something to do with Gödel's Incompleteness Theorem. I'd sincerely thank those who recommend me very clear and illustrative materials about it. I'd also like to know what background will be needed to understand it. I tried to read the original paper but didn't quite understand what are the more fundamental facts that we can rely on to prove this theorem. (Maybe Peano Arithmetic and ZFC?)

• I think that A and p(A) have different types, and therefore your notation p(p(A)) does not make sense to me. – Tsuyoshi Ito Nov 2 '11 at 12:41
• I am reminded of Lewis Carroll "What the Tortoise Said to Achilles" [ en.wikipedia.org/wiki/What_the_Tortoise_Said_to_Achilles ]. – Ohad Kammar Nov 2 '11 at 13:25
• It's not meant to be about first order logic. I'm trying to understand the ambiguity of natural language, which seems to be more fundamental and difficult than (first order) logic. I want to decompose natural language in a structural way, and I'd like to know what ideas CS theorists and mathematicians may have. You can see mainstream natural language processing techniques are almost all about statistics and machine learning, which is not a structural way. And no practial machine translation system has ever worked decently. Anyway, I'm just interested in how other people think about it. – Cyker Nov 2 '11 at 14:11
• A considerable number of researchers in NLP, CL (Computational Linguistics), and KR (Knowledge Representation and Reasoning) work on non-statistical computational linguistics. Check the AI Q&A sites mentioned in the FAQ, I think they can be useful for what you want to know. – Kaveh Nov 2 '11 at 15:16
• ps: I would suggest that you also check Torkel Franzen's book, Godel's incompleteness has been quite prone to misuse. – Kaveh Nov 2 '11 at 15:25

The idea is that sometimes we can give a proof of a tautology succinctly by providing a small circuit that generates the bits of a proof in a propositional proof system $Q$. The problem is how can we know the bits generated by the circuit really represent a proof? The size of the circuit can be small (polynomial in $n$) with $n$ inputs and can describe an object of size $2^n$, so constructing the complete proof and checking its correctness can be an unfeasible task. The solution is to give a proof of correctness of the succinctly represented proof in $Q$ in a proof system $Q'$. This new proof system is called $[Q,Q']$ (note the $Q$ and $Q'$ can be the same system). Furthermore, Krajicek shows that for reasonable behaving propositional proof systems $Q$, the resulting system $[Q,Q]$ can p-simulate the $Q$. And you can repeat this processes and obtain potentially stronger and stronger systems (note that if there is optimal proof system then this construction will not give a stronger system, but just another optimal one), and then you can take union of these systems and continue.