Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

After reading about Curry-Howard corrsepondence and looking at some proofs written in coq i've thinked about meaning of proof of a proof.

  1. We can express proofs as a computer program
  2. Proof is correct when program compiles
  3. We can test compiled program or even write correctness proof for it.

So, what test of a proof checks? What correctness proof of a computer-program-proof will prove? Proof correctness is ensured on compilation stage, what is the meaning of proof of a proof? Is there any meaning?

share|cite|improve this question
After that, if we automate proofs of proofs, we can worry about proofs of proofs of proofs. This could go on forever, unless proving something actually means understanding something, which is what the automated part omits. – Michael Hardy Aug 30 '13 at 18:12
Understanding something doesn't really have a concrete meaning, so there is actually no "unless". – Mlazhinka Shung Gronzalez LeWy Aug 30 '13 at 18:27
Is this not actually extremely deep, essentially playing on the fact that one has to leave an axiom system in order to prove that it is consistent? – user1729 Aug 30 '13 at 18:52
Proof is socially constructed concept. You will never have an 'objectively' bulletproof proof. – Potato Aug 30 '13 at 19:52
I think "understanding something" does have an important meaning, but not one that admits of mathematical definition. – Michael Hardy Aug 31 '13 at 3:52
up vote 2 down vote accepted

Lewis Carroll, in 1895, recognized the infinite regress possible.

See "What the Tortoise Said to Achilles" here:

share|cite|improve this answer

I think your description of Curry-Howard correspondance is not precise enough:

  1. The proof is correct if the program is well-typed and has as type the formula to be proved.

Any well-typed program of the right type is a correct proof of this formula, you don't need to check 'correctness'.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.