From the source https://iep.utm.edu/natural-deduction/ :

Natural Deduction (ND) is a common name for the class of proof systems composed of simple and self-evident inference rules based upon methods of proof and traditional ways of reasoning that have been applied since antiquity in deductive practice.

What is it that makes them all ND systems despite the differences in the selection of rules, construction of proof, and other features? First of all, in contrast to proofs in axiomatic systems, proofs in ND systems are based on the use of assumptions which are freely introduced but discharged under some conditions.

What does it mean to say that an assumption is "freely introduced" and how does that contrast to "axiomatic systems"? I would think that if there is a certain introduction rule, one could always make use of it, provided the requirements of the rule were present. For example, for (∧I)φ,ψ⊢φ∧ψ, this can be made use of given no other precondition except essentially the existence of at least one formula, say φ. In what way is this not the case, in "Hilbert-style axiomatic systems"?

  • 2
    There are no introduction rules in Hilbert-style axiomatic systems, only axioms and modus ponens. Accordingly, you cannot introduce and discharge assumptions "freely", that is, formally, at all. The workaround is to fold them into implications, which makes derivations rather cumbersome.
    – Conifold
    Commented Feb 3 at 14:16
  • @Conifold, I think you are misusing the word "introduction" here. A Hilbert-style system could have an axiom "From A, B infer A/\B" and that would allow and-introduction. What you mean to say (I assume) is that there are no rules for adding an assumption, which can then be discharged. Commented Feb 3 at 17:14
  • @DavidGudeman No, it could not. Hilbert systems typically use only implication and negation, and a rule of this form is not first order even if other connectives were included. It can be a meta-rule in some conservative extension, but it can only be used in meta-language, not in the system itself.
    – Conifold
    Commented Feb 3 at 17:29
  • @Conifold Thank you, would you like to post that as an answer? I also can, if you prefer. Thank you. Commented Feb 3 at 19:49
  • 1
    ND system inference rules can be too free to introduce conditionals to become the formal system of automated theorem provers or more theoretical purpose which needs systematic encoding schemes. Classic Hilbert system with only modus ponens rule emphasizes axioms only on which any deduction is based without any other free assumptions on the object language level may seems inflexible and unnatural but is better suited for above cases. Sequent calculus lies in between and may not be so free to introduce conditionals via its right implication intro rule or the cut rule... Commented Feb 4 at 5:17

1 Answer 1


A simple answer to your question is that not all axiomatic systems have the Deduction Theorem, which is essentially the same as Conditional Proof, except that it is proven as a meta-theorem for a proof calculus instead of taken as a basic rule.

In particular, axiomatic systems that fail at least one of the following also fail the full Deduction Theorem:

  • A→(B→A) (A form of weakening the antecedent)
  • (A→(B→C))→((A→B)→(A→C)) (Distribution of implication over implication)
  • Modus Ponens

What the Deduction Theorem specifically says is that if a formula C is derivable from a set of sentences and an additional assumption A, then that set of sentences can already derive A→C without the extra assumption.

There are modified versions of the Deduction Theorem that can get proven for logics too weak to satisfy the three requirements, but these are not the full Deduction Theorem that reflects the Conditional Proof inference rule in Natutal Deduction for logics that prove the full Deduction Theorem.

  • 1
    "(A→(B→C))→((A→B)→(A→C)) (Distribution of implication over implication)" What about the converse, viz. ((A → B) → (A → C)) → (A → (B → C)). True? False? I can't find it through a search engine. Commented Feb 4 at 16:48
  • Yes, as long as the full DT is provable/valid, the converse is also provable/valid.
    – PW_246
    Commented Feb 4 at 17:06
  • It should be noted that for first order logic the proof of deduction theorem is a bit more complicated since you need to deal with new inference rules
    – Poscat
    Commented Mar 28 at 2:16
  • @Poscat not necessarily, since Generalization doesn’t need to be an inference rule. In those systems, it is provable for formulas A where the variable being quantified over does not occur free in the set of assumptions that prove A. This can also be seen from sequent calculus presentations of FOL wherein, so long as the other rules are followed, the deduction theorem/implies-right rule is always valid.
    – PW_246
    Commented Mar 28 at 2:24
  • Hmm, you still need to treat eigenvariables cautiously right?
    – Poscat
    Commented Mar 28 at 3:09

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .