How to prove a proof is correct

Question

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?)

Answer 1

I am not sure if the question is on topic here, it seems to contain basic misunderstandings about logic and mathematics (e.g. "This seems ridiculous because 1+1=2 is commonly known as correct, which doesn't need a complicated proof."), and therefore seems more appropriate for Math.SE.

Nonetheless, there is something interesting and related to it in proof complexity:

I assume that you are familiar with the notion of a Cook-Reckhow propositional proof system. Jan Krajicek has studied something similar to what you describe in the context of proof complexity named Implicit Proofs.

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.