1
$\begingroup$

Is there a proof of the following statement: you cannot prove with natural deduction theorems that are unprovable in a Hilbert-style proof system? The logic in discussion is either propositional logic or FOL.

$\endgroup$
1
$\begingroup$

Yes. You have to follow a "typical" proof of "equivalence" between Natural Deduction and Hilbert-style.

See :

Sara Negri & Jan von Plato, Structural Proof Theory (2001), page 41-on.

An alternative approach is through soundness and completeness.

Both proof systems are sound and complete regarding valid formulae; thus, a formula unprovable in ND, being not valid, in not provable in H-s, and vice versa.

$\endgroup$
  • $\begingroup$ Thanks for the reference, but the alternative approach is quite ingenious, such a shame I haven't thought of it myself. $\endgroup$ – user132181 Jun 22 '14 at 12:32
  • $\begingroup$ @user132181 - This is the "key" for all different prooof systems; they works in a lot of different ways but we want that all agree exactly on the "class" of valid formulae (or tautology for prop logic). $\endgroup$ – Mauro ALLEGRANZA Jun 22 '14 at 12:37
  • $\begingroup$ Yeah, model theory here serves as a "bridge", so to speak. Very nice. $\endgroup$ – user132181 Jun 22 '14 at 12:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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