Help needed with axiomatic deductions

Question

Proof axiomatically:

$\vdash \forall x (\neg (Ax \rightarrow Bx) \rightarrow (\neg Ax \rightarrow \neg Bx))$

You can use in your deduction as step the equivalence of $\varphi$ with $\neg\neg\varphi$:

$\varphi\vdash\neg\neg\varphi$ and $\neg\neg \varphi \vdash \varphi$

Also used are the following axioms:

1 $(∀x(φ→ψ)) \rightarrow (\forall x \varphi \rightarrow \forall x \psi)$
2 $\varphi \rightarrow \forall x \varphi$ ($x$ not free in $\varphi$)
3 $\forall x \varphi \rightarrow [t/x]\varphi$
a $\varphi \rightarrow (\psi \rightarrow \varphi)$
b $\varphi \rightarrow (\psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi)\rightarrow(\varphi \rightarrow \chi))$
c $(\neg \varphi \rightarrow \neg \psi) \rightarrow (\psi \rightarrow \varphi)$

So starting out on this question, I had hopes of delivering an answer. But alas, my plans were foiled, I could not get a deduction. So, I decided to have a peek at the answer, and it baffled me completely:

1. $\vdash Bx \rightarrow (Ax \rightarrow Bx)$ (a)
2. $\neg\neg Bx\vdash Bx$ ($\neg\neg\varphi\vdash\varphi$)
3. $\neg\neg Bx \vdash Ax \rightarrow Bx$ (MP, 1, 2)
4. $Ax \rightarrow Bx \vdash \neg\neg(Ax \rightarrow Bx)$ ($\varphi\vdash\neg\neg\varphi$)
5. $\vdash (Ax \rightarrow Bx) \rightarrow \neg\neg(Ax \rightarrow Bx)$ (deduction theorem on 4)
6. $\neg\neg Bx \vdash \neg\neg(Ax \rightarrow Bx)$ (MP, 3, 5)
7. $\vdash \neg\neg Bx \rightarrow \neg\neg(Ax \rightarrow Bx)$ (deduction theorem on 6)
8. $\vdash (\neg\neg Bx \rightarrow \neg\neg(Ax \rightarrow Bx)) \rightarrow (\neg(Ax \rightarrow Bx) \rightarrow \neg Bx)$ (c)
9. $\vdash \neg(Ax \rightarrow Bx) \rightarrow \neg Bx$ (MP, 7, 8)
10. $\neg(Ax \rightarrow Bx) \vdash \neg(Ax \rightarrow Bx)$ (assumption)
11. $\neg(Ax \rightarrow Bx) \vdash \neg Bx$ (MP, 9, 10)
12. $\vdash \neg Bx \rightarrow (\neg Ax \rightarrow \neg Bx)$ (a)
13. $\neg(Ax \rightarrow Bx) \vdash (\neg Ax \rightarrow \neg Bx)$ (MP, 11, 12)
14. $\vdash \neg(Ax \rightarrow Bx) \rightarrow (\neg Ax \rightarrow \neg Bx)$ (deduction theorem on 13)
15. $\vdash \forall x (\neg(Ax \rightarrow Bx) \rightarrow (\neg Ax \rightarrow \neg Bx))$ (universal generalization on 14)

Starting from 1, I immediately run into a wall. I have absolutely no idea how it got here. Where does $Bx$ come from? So, I start from the bottom. This goes a bit easier, but backtracking it is still not easy. This goes well up until 10/9-ish, again, I run into a wall. No ideas on how to get to the following statement, let alone to 1.

My question is this: can someone guide me through this deduction, with the simplest of explanation?

Answer 1

This is a long comment ...

The above proof is "complicated" and difficult to grasp because the axiomatic (or Hilbert-style) proof-system is very "opaque", in terms of euristic (finding how to build up the required proof).

Natural deduction is far better for this.

A possible way to "simplify" the search of a proof in a case like that above, which is basically a "propositional" proof (the only "quantifier" rule is invoked in the last step), is to "enlarge" the set of rules available.

How ? Starting from the propositional axioms a)-c) and proving their completeness for the tautologies, i.e.proving the meta-theorem which states that all tautologies are provable from the above axioms with modus ponens.

In this way, we may use in our proofs every instance of a tautology.

Assuming having done this, we may build another proof of the theorem using the following tautologies :

$\vDash_{TAUT} (\varphi \rightarrow \psi) \lor (\psi \rightarrow \varphi)$ --- $(TAUT_1)$

and :

$\vDash_{TAUT} \lnot \sigma \rightarrow [ (\sigma \lor \tau) \rightarrow \tau) ]$ --- $(TAUT_2)$

and :

$\vDash_{TAUT} (\varphi \rightarrow \psi) \rightarrow (\lnot \psi \rightarrow \lnot \varphi)$ --- $(TAUT_3)$.

Now for the proof.

(1) Instantiate $TAUT_1$ with $Ax$ in place of $\varphi$ and $Bx$ in place of $\psi$ :

$\vdash (Ax \rightarrow Bx) \lor (Bx \rightarrow Ax)$

(2) Instantiate $TAUT_2$ with $(Ax \rightarrow Bx)$ in place of $\sigma$ and $(Bx \rightarrow Ax)$ in place of $\tau$ :

$\vdash \lnot (Ax \rightarrow Bx) \rightarrow ( [ (Ax \rightarrow Bx)\lor (Bx \rightarrow Ax) ] \rightarrow (Bx \rightarrow Ax) )$

(3) Assume :

$ \lnot (Ax \rightarrow Bx)$

(4) $\lnot (Ax \rightarrow Bx) \vdash [ (Ax \rightarrow Bx)\lor (Bx \rightarrow Ax) ] \rightarrow (Bx \rightarrow Ax)$ --- from 2) and 3) by modus ponens

(5) $\lnot (Ax \rightarrow Bx) \vdash (Bx \rightarrow Ax)$ --- from 1) and 4) by modus ponens

(6) Instantiate $TAUT_3$ with $Bx$ in place of $\varphi$ and $Ax$ in place of $\psi$ :

$ \vdash (Bx \rightarrow Ax) \rightarrow (\lnot Ax \rightarrow \lnot Bx)$

(7) $\lnot (Ax \rightarrow Bx) \vdash (\lnot Ax \rightarrow \lnot Bx)$ --- from 5) and 6) by modus ponens

(8) $\vdash \lnot (Ax \rightarrow Bx) \rightarrow (\lnot Ax \rightarrow \lnot Bx)$ --- from 7) by Deduction Theorem.

Now the "hard" work is done.

We have only to apply the Generalization Theorem :

if $\Gamma \vdash \varphi$ and $x$ does not occur free in any formula in $\Gamma$, then $\Gamma \vdash \forall x \varphi$,

with $\Gamma = \emptyset$, to conclude from 8) :

$\vdash \forall x [\lnot (Ax \rightarrow Bx) \rightarrow (\lnot Ax \rightarrow \lnot Bx) ]$.

Answer 2

Axioms a)-c) are a complete set of axioms for propositional logic and thus we are allowed to use in your proofs every instance of tautologies (like $\varphi \leftrightarrow \lnot \lnot \varphi$).

In addition, axioms a)-b) are enough to prove the Deduction Theorem.

Please, note that axiom 1) is wrongly stated. It must be (see your previous post ) :

$\forall x(\varphi \rightarrow \psi) \rightarrow (\forall x \varphi \rightarrow \forall x \psi)$.

In axiom 2), we have to add the proviso that $x$ is not free in $\varphi$, otherwise the formula $φ→∀xφ$ is not valid: thus, it cannot be an axiom.

Whit these corrections, axioms a)-c) plus 1)-3) form a complete set of axioms for first-order logic.

I assume that the only inference rule is modus ponens.

Having said that, the proof looks fine to me, except for the last step : what is the invoked "universal generalization" ?

Do you have also the inference rule :

$${\varphi \over \forall x \varphi}$$

If so, there are some "interference" with the deduction theorem to be checked.

Otherwise, with only modus ponens as rule, we must use the Generalization Theorem :

if $\Gamma \vdash \varphi$ and $x$ does not occur free in any formula in $\Gamma$, then $\Gamma \vdash \forall x \varphi$.

Added

Now the proof. We start using an instance of axiom a); the axiom is a schema. i.e. we may assert every instance of it, that is every formula obtained from the schema putting formulas whatever in place of $\varphi$ and $\psi$, provided that we substitute all occurrence of $\varphi$ (and $\psi$, and so on) with the same formula.

Thus, from :

$\vdash φ→(ψ→φ)$

putting $Bx$ in place of $\varphi$ and $Ax$ in place of $\psi$, we get 1) :

$\vdash Bx→(Ax→Bx)$.

Until 9) there are some easy steps. Then 10) is a new assumption; the "rule" is :

$\Gamma \vdash \varphi$, when $\varphi \in \Gamma$;

in our case : $\Gamma = \{ ¬(Ax→Bx) \}$.

Thus we state the temporary assumption : $\lnot (Ax \rightarrow Bx)$. We will "discharge" it in step 14) using the DT, in the same way as in step 7) we have "discharged" the temporary assumption $¬¬Bx$ introduced in step 2).

Having derived 9) :

$⊢¬(Ax→Bx)→¬Bx$

with 10) we use modus ponens to derive : $\lnot Bx$, under the above temporary assumption 10); that is 11) :

$\lnot (Ax \rightarrow Bx) \vdash \lnot Bx$.

Now we use a new instance of axiom a) : $\vdash φ→(ψ→φ)$, putting $\lnot Bx$ in place of $\varphi$ and $\lnot Ax$ in place of $\psi$. Thus, we get 12) :

$⊢¬Bx→(¬Ax→¬Bx)$.

Finally, we use modus ponens with 11) and 12) to "detach" : $(¬Ax→¬Bx)$.

But $\lnot Bx$ (we have used it in the last application of mp) "depends on" the temporary assumption 10); thus also the conclusion of mp depends on it, and we have 13) :

$¬(Ax→Bx) \vdash (¬Ax→¬Bx)$.

The last steps are easy.

---

Note about axiom schemata [from : Peter Smith, Types of Proof System (2010)].

Let's have an example of an axiomatic system to be going on with. In this system $\mathsf M$, to be found e.g. in Mendelson's classic Introduction to Mathematical Logic, the only propositional connectives built into the basic language of the theory are '$\rightarrow$' and '$\lnot$' ('if ... then ...' and 'not', the same choice of basic connectives as in Frege's Begrisschrift).

The axioms are then all wffs [wee-formed formulas] which are instances of the schemata [see footnote] :

Ax1. $(A \rightarrow (B \rightarrow A))$

Ax2. $((A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow)))$

Ax3. $((\lnot B \rightarrow \lnot A) \rightarrow ((\lnot B \rightarrow A) \rightarrow B))$.

$\mathsf M$'s one and only rule of inference is modus ponens, the rule from $A$ and $(A \rightarrow C)$ infer $C$.

In this axiomatic system, a proof from the given premisses $A_1, A_2, ...A_n$ to conclusion $C$ is a linear sequence of wffs such that each wff is either :

(i) a premiss $A_i$,

(ii) a logical axiom, i.e. an instance of Ax1, Ax2 or Ax3, or

(iii) follows from two previous wffs in the sequence by modus ponens, and

(iv) the final wff in the sequence is $C$.

When there is such a proof we will write :

$A_1, A_2, ... A_n \vdash_{\mathsf M} C$.

If we can prove $C$ from the axioms alone without additional premisses, we'll say that $C$ is a theorem, and write simply $\vdash_{\mathsf M} C$.

Footnote. 3`Instances of the schemata'? An wff is an instance of a schema (plural: schemata) if it results for systematically replacing schematic letters $A, B, C$ etc. in the schema by particular wffs - with, in a given case, the same schematic letter always being substituted by the same wff.

Going back to our example (see : step 1), from the schemata a) :

$φ→(ψ→φ)$

[which is the same as Ax1 of Peter Smith's paper] we may "generate" as many instances as we want. To do this, we need two formulas whatever to be substituded in place of shematic letters $\varphi$ and $\psi$.

Example 1) : $p$ in place of $\varphi$ and $q$ in place of $\psi$ :

$p→(q→p)$.

Example 2) : $0 = 0$ in place $\varphi$ and $1 = 0$ in place of $\psi$ :

$(0=0)→[(1=0)→(0=0)]$.

Example 3) : $Bx$ in place $\varphi$ and $Ax$ in place of $\psi$ :

$Bx→(Ax→Bx)$.

We have not "derived" $Bx$; we are using "instruction" n° (ii) of the above definition of proof :

a linear sequence of wffs such that each wff is [...] a logical axiom, i.e. an instance of Ax1, Ax2 or Ax3.