173k views
1 vote
From the definition of a sound calculus we can infer that a sound implication introduction has to have the form: Γ ⊢ A → Γ ⊨ A.

The rule for implication introduction goes (Γ ∪ {A} ⊢ B) ⊢ (Γ ⊢ A → B).
The rule of 2. translates into the natural deduction calculus as (Γ ∪ {A} ∪ {B}) ⊢ (Γ ∪ {A → B}).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.So we finally get ((Γ ∪ {A} ∪ {B}) ⊢ (Γ ∪ {A → B})) → (Γ ∪ {A} ∪ {B}) ⊨ (Γ ∪ {A → B}). Correct proof? If NO, why not?

1 Answer

5 votes

Final answer:

The proof is incorrect because it fails to apply the implication introduction rule properly and makes an erroneous leap in logic from syntactic entailment to semantic entailment without justification.

Step-by-step explanation:

The proof presented has a fundamental misunderstanding of the implication introduction rule in logical calculus. The rule is typically stated as if Γ ∧ {A} ⊢ B then Γ ⊢ A → B. However, the proof attempts to expand this rule incorrectly by adding {B} to both sides of the inference which is not how the rule works. Furthermore, the transition from the syntactical entailment (⊢) to the semantic entailment (⊘), and the assumption that A → B follows from A and B being assumed true, skips several necessary steps. To be correct, the proof must demonstrate that given A and the truth of A → B, then B must also be true. However, this has not been correctly shown. The part “because if we assume A and B as true then A ∧ ~B can never happen which means A → B has to be true” confuses the nature of the implication, as implications are not justified solely by the truth of their antecedent and consequent.

User Gumowy Kaczak
by
7.7k points
Welcome to QAmmunity.org, where you can ask questions and receive answers from other members of our community.