Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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|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". –  ABC 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

1 Answer 1

up vote 2 down vote accepted

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

See "What the Tortoise Said to Achilles" here: http://www.ditext.com/carroll/tortoise.html

share|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.