1. From the definition of a sound calculus we can infer that a sound implication introduction has to have the form: Γ ⊢ A → Γ ⊨ A.
  2. The rule for implication introduction goes (Γ ∪ {A} ⊢ B) ⊢ (Γ ⊢ A → B).
  3. The rule of 2. translates into the natural deduction calculus as (Γ ∪ {A} ∪ {B}) ⊢ (Γ ∪ {A → B}).
  4. From there it follows trivially (Γ ∪ {A} ∪ {B}) ⊨ (Γ ∪ {A → B}), because if we assume A and B as true then A ∧ ~B can never happen which means A → B has to be true.
  5. So we finally get ((Γ ∪ {A} ∪ {B}) ⊢ (Γ ∪ {A → B})) → (Γ ∪ {A} ∪ {B}) ⊨ (Γ ∪ {A → B}).

Correct proof? If NO, why not?

  • 1
    Soundness of ND calculus is easily proved wholesale (not just for your rule) rigorously with the semantic entailment closure property of the naive set of all the (background, result) ordered pair sequent of any generic derivation as an invariance property under all rules via mathematical induction on the length of the entire derivation. And your proof is mixing sequent with object language. →-intro rule is just the syntactic form of the obvious semantic deduction theorem which holds intuitionistically too. More interesting perhaps is in what kind of logic this rule is not sound at all? Sep 14, 2023 at 7:18
  • If you are satisfied with the answer received, please accept it. Sep 14, 2023 at 7:23

1 Answer 1


Your notation is a bit difficult to read: you freely move between using → for both the object and metalanguage, likewise with ⊢. Heres the typical proof:

Suppose we are given a proof, such that implication introduction was the last rule applied. So the proof prior to ->I was a proof of B, with open assumptions amongst Gamma, A. By induction hypothesis (IH), we have that this proof is sound, ie every valuation that makes Gamma, A true makes B true.

We need now to show that every valuation that makes Gamma true, makes "if a then b" true. Suppose for contradiction there is a valuation makes Gamma true, but the implication false. Then, by viewing truth tables, A must be true, Gamma true, and B false. But by IH there is not such valuation. Hence proved.

Since proofs are essentially combinatorial objects built by inductive laws, you'll almost certainly need to mention an induction hypothesis. The fact that you didn't suggests to me that your proof can be made clearer.

You must log in to answer this question.

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