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

Question

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?

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.