# Proof of soundness of the rule of implication introduction in natural deduction calculus

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?

• 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 at 7:18