3

Consider the formal axiomatic theory, whose axioms are

$$(B \implies (A \implies B))$$ $$((B \implies (A \implies C)) \implies ((B \implies A) \implies (B \implies C)))$$ $$(((\neg A \implies (\neg B)) \implies (((\neg A) \implies B) \implies A )) $$

for all well-formed formulas $A, B, C$. The only rule of inference for this system is MP: $A$ is a direct consequence of $B$ and $B \implies A$. If we define $A \wedge B$ to be $\neg(B \implies \neg A)$, how would we prove in this system that

$$\vdash (A \wedge B) \implies A$$

We can use the deduction theorem.

user98606
  • 31
  • 1

1 Answers1

2

You don't actually use The Deduction Theorem, but the derivable rule of inference of conditional introduction, abbreviated Ci, that The Deduction Theorem allows for. At least so long as you keep theorems distinct from rules of inference, which if you don't, you've collapsed the meta-logic/object-logic distinction, since rules of inference come as belonging the meta-logic, while axioms and theorems belong to the object logic. Your book might call what I call detachment "modus ponens". You can basically make substitutions in the first axiom, or axiom scheme, and then use the third axiom scheme. What might you substitute in the first axiom? What might you substitute in the third axiom? I won't write the application of the definition for you in the following.

hypothesis       1  ¬(B⟹¬A)

1st axiom scheme 2 [¬A⟹(B⟹¬A)]

1st axiom scheme 3 {¬(B⟹¬A)⟹[¬A⟹¬(B⟹¬A)]}

3, 1 detachment  4 [¬A⟹¬(B⟹¬A)]

3rd axiom scheme 5 [¬A⟹¬(B⟹¬A)]⟹{[¬A⟹(B⟹¬A)]⟹A}

5, 4 detachment  6 {[¬A⟹(B⟹¬A)]⟹A}

6, 2 detachment  7 A

1-7 Ci           8 [¬(B⟹¬A)⟹A]
Doug Spoonwood
  • 11,211