Hilbert's style sysytem without deductive theorem.

Question

How to prove ¬P∨¬Q → ¬(P∧Q)

using the following axioms?

a1. A→(B→A)

a2. (A→(B→C))→((A→B)→(A→C))

a3.(A∧B)→A

a3'.(A∧B)→B

a4.A→(B→(A∧B))

a5. A→A∨B

a5'. B→A∨B

a6.(A→C)→((B→C)→(A∨B→C))

a7. ¬¬A→A

and only role is Modus Ponens.

a tried with a6, with A=¬P, B=¬Q, and C=¬(P∧Q), but it doesn't work.

Answer 1

Quite correct. You have to prove Contraposition: $(A \to B ) \to (\lnot B \to \lnot A)$.

Then apply it to (Ax.3) and (Ax.3') to get, respectively:

$\lnot P \to \lnot (P \land Q)$ and $\lnot Q \to \lnot (P \land Q)$.

---

We need "auxiliary lemmas" like the first one: $\vdash A \to A$, needed to prove, with (Ax.1) and (Ax.2) the Dedution Theorem.

A second one is the "auxiliary rule" of Hypothetical Syllogism:

$A \to B, B \to C \vdash A \to C$.

Proof

1) $B \to C \vdash A \to (B \to C)$ --- from (Ax.1)

2) $A \to B, B \to C \vdash A \to (B \to C)$ --- from 1)

3) $A \to B, B \to C \vdash A \to C$ --- from (Ax.2) and 2) by Modus Ponens twice.

Using the Deduction Th we can conclude with:

$\vdash (A \to B) \to ((B \to C) \to (A \to C)).$

In the post: proving $(p \to q) \to ((q \to r) \to (p \to r))$, you can find a Deduction Theorem-free derivation of it.

---

Now for the final step.

As per you Lectures Notes, $\lnot \varphi$ is an abbreviation of $\varphi \to \bot$.

Thus, we have to use HS in the form: $\vdash (A \to B) \to ((B \to \bot) \to (A \to \bot))$ to get, without abbreviation:

$A \to B \vdash \lnot B \to \lnot A$.

---

---

Now for the the proof.

1) $\vdash (P \land Q) \to P$ --- (Ax.3)

2) $\vdash \lnot P \to \lnot (P \land Q)$ --- from 1)

3) $\vdash (P \land Q) \to Q$ --- (Ax.3')

4) $\vdash \lnot Q \to \lnot (P \land Q)$ --- from 3)

5) $\vdash (\lnot P → \lnot (P \land Q)) → ((\lnot Q → \lnot (P \land Q)) → ((\lnot P \lor \lnot Q) → \lnot (P \land Q)))$ --- (Ax.6)

6) $\vdash (\lnot P \lor \lnot Q) → \lnot (P \land Q)$ --- from 2), 4) and 5) by MP twice.