5
$\begingroup$

I'm interested in formal proof verification, and one of the surprisingly difficult parts of this is dealing with proofs by contradiction. The issue is that the final step of such proofs is typically "if not P is a theorem, then false is a theorem," an inference rule in a Hilbert-like system, and Hilbert systems typically do not have "second order inference rules". To make this work, we need some version of the deduction theorem to derive "not P entails false", from which we can then derive P. This can be a pain in the neck if not done at the meta level (see http://us.metamath.org/mpegif/mmdeduction.html, for example).

Now, the deduction theorem is an admissible metatheorem; it proves that proofs exist, though the construction of the proofs is unwieldy. My question is: are there other such metatheorems (for standard first order, second order, or ZFC) whose addition is known to make proofs in Hilbert-like systems more flexible?

$\endgroup$
3
  • 3
    $\begingroup$ What are some examples of proofs that work like that? In my experience most proofs by contradiction don't involve assuming the existence of a proof. How is that used? Is it somehow needed to formalize ohter steps of the proof that informally does not assume a proof? $\endgroup$
    – Will Sawin
    Oct 3, 2015 at 23:36
  • $\begingroup$ en.wikipedia.org/wiki/… ? $\;$ $\endgroup$
    – user5810
    Oct 4, 2015 at 0:53
  • 5
    $\begingroup$ The first example that comes to mind is eliminability of definitions. You can extend the language of ZFC (or indeed of any first-order theory) by adding new defined relation and function symbols, along with their definitions. Any statement in the original language that is provable in the enlarged theory is also provable in the original theory (though possibly with a far longer and messier proof). This is used all the time. We don't do mathematics in the primitive language of ZFC (with $\in$ as the only nonlogical symbol); we work in a massive definitional extension. $\endgroup$ Oct 4, 2015 at 7:14

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.