0
$\begingroup$

Wikipedia's article on the deduction theorem states:

Although the deduction theorem could be taken as primitive rule of inference in [Hilbert-style] systems, this approach is not generally followed; instead, the deduction theorem is obtained as an admissible rule using the other logical axioms and modus ponens. In other formal proof systems, the deduction theorem is sometimes taken as a primitive rule of inference.

The article then cites natural deduction as an example of the latter case.

So I am wondering: in what other formal proof systems, besides natural deduction, is the deduction theorem taken as a primitive rule of inference?

EDIT: In particular, I am interested in Hilbert-like systems for which this is the case (or any formal proof system that, in general, prefers axioms over rules of inference, with the exception of using the deduction theorem rather than, e.g., Łukasiewicz's axioms CpCqp and CCpCqrCCpqCpr).

$\endgroup$
  • $\begingroup$ does it really make some difference that it is a primitive rule or the composition of $2$ or $3$ primitive rules ? $\endgroup$ – reuns Apr 15 '16 at 0:43
  • $\begingroup$ @user1952009 Yes, because if the deduction theorem is taken as a primitive rule, then the axioms of positive implicational logic become superfluous. $\endgroup$ – Hans Brende Apr 15 '16 at 1:19
  • 3
    $\begingroup$ Of course, in Gentzen's sequent calculus LK: $\to$-R. $\endgroup$ – Mauro ALLEGRANZA Apr 15 '16 at 6:05
  • 2
    $\begingroup$ @DougSpoonwood taking the deduction theorem as a primitive rule of inference in a Hilbert System could potentially allow one to eliminate the axioms CpCqp and CCpCqrCCpqCpr, so no dependencies would occur. That would be the goal. $\endgroup$ – Hans Brende Apr 16 '16 at 0:48
  • 1
    $\begingroup$ @DougSpoonwood Any rules of inference that must be reformulated to accommodate the deduction theorem as a primitive rule of inference is fine with me! I'm merely asking which, if any, Hilbert-like systems are successful in this reformulation. Judging by wikipedia's example of one such reformulation, I doubt this is impossible. $\endgroup$ – Hans Brende Apr 16 '16 at 19:44

Your Answer

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

Browse other questions tagged or ask your own question.