In what formal proof systems is the deduction theorem taken as a primitive rule of inference?

191 Views Asked by At

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