Hilbert Proof System Instance 2 Independence Results/Independence of A3

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\mathscr H_2$ be Instance 2 of the Hilbert proof systems.

Then:


Axiom $(A3)$ is independent from $(A1)$, $(A2)$, $(A4)$.


Proof

Denote with $\mathscr H_2 - (A3)$ the proof system resulting from $\mathscr H_2$ by removing axiom $(A3)$.

Consider $\mathscr C_4$, Instance 4 of constructed semantics.

We will prove that:

  • $\mathscr H_2 - (A3)$ is sound for $\mathscr C_4$;
  • Axiom $(A3)$ is not a tautology in $\mathscr C_4$

which leads to the conclusion that $(A3)$ is not a theorem of $\mathscr H_2 - (A3)$.


Soundness of $\mathscr H_2 - (A3)$ for $\mathscr C_4$

Starting with the axioms:

\((A1)\)   $:$   Rule of Idempotence    \(\ds (p \lor p) \implies p \)      Proof of Tautology
\((A2)\)   $:$   Rule of Addition    \(\ds q \implies (p \lor q) \)      Proof of Tautology
\((A4)\)   $:$   Factor Principle    \(\ds (q \implies r) \implies \left({ (p \lor q) \implies (p \lor r)}\right) \)      Proof of Tautology


Next it needs to be shown that the rules of inference of $\mathscr H_2$ preserve $\mathscr C_4$-tautologies.


Rule $RST \, 1$: Rule of Uniform Substitution

By definition, any WFF is assigned a value from $\set{ 0,1,2,3 }$.

Thus, in applying Rule $RST \, 1$, we are introducing $0$, $1$, $2$ or $3$ in the position of a propositional variable.

But all possibilities of assignments to such propositional variables were shown not to affect the resulting values of the axioms.

Hence Rule $RST \, 1$ preserves $\mathscr C_4$-tautologies.


Rule $RST \, 2$: Rule of Substitution by Definition

Because the definition of $\mathscr C_4$ was given in terms of Rule $RST \, 2$, it cannot affect any of its results.


Rule $RST \, 3$: Rule of Detachment

Suppose $\mathbf A$ and $\mathbf A \implies \mathbf B$ both take value $0$.

Then using Rule $RST \, 2$, definition $(2)$, we get:

$\neg \mathbf A \lor \mathbf B$

taking value $0$ by assumption.

But $\neg \mathbf A$ takes value $1$ by definition of $\neg$.

So from the definition of $\lor$, it must be that $\mathbf B$ takes value $0$.

Hence Rule $RST \, 3$ also produces only WFFs of value $0$.


Rule $RST \, 4$: Rule of Adjunction

Suppose $\mathbf A$ and $\mathbf B$ take value $0$.

Then using the definitional abbreviations:

$\mathbf A \land \mathbf B =_{\text{def}} \neg ( \neg \mathbf A \lor \neg \mathbf B )$

We compute:

\(\ds \mathbf A \land \mathbf B\) \(=\) \(\ds 0 \land 0\)
\(\ds \) \(=\) \(\ds \neg ( \neg 0 \lor \neg 0 )\) Rule $RST \, 2 \, (1)$
\(\ds \) \(=\) \(\ds \neg ( 1 \lor 1 )\)
\(\ds \) \(=\) \(\ds \neg 1\)
\(\ds \) \(=\) \(\ds 0\)

proving that Rule $RST \, 4$ also produces only $0$s from $0$s.


Hence $\mathscr H_2 - (A3)$ is sound for $\mathscr C_4$.


$(A3)$ is not a $\mathscr C_4$-tautology

Recall axiom $(A3)$, the Rule of Commutation:

$(p \lor q) \implies (q \lor p)$

Under $\mathscr C_4$, we apply a single definitional abbreviation and have the following:

$\begin{array}{|cccc|c|ccc|} \hline

\neg & (p & \lor & q) & \lor & (q & \lor & p) \\ \hline 1 & 0 & 0 & 0 & 0 & 0 & 0 & 0 \\ 1 & 0 & 0 & 1 & 0 & 1 & 0 & 0 \\ 1 & 0 & 0 & 2 & 0 & 2 & 0 & 0 \\ 1 & 0 & 0 & 3 & 0 & 3 & 0 & 0 \\ 1 & 1 & 0 & 0 & 0 & 0 & 0 & 1 \\ 0 & 1 & 1 & 1 & 0 & 1 & 1 & 1 \\ 0 & 1 & 2 & 2 & 0 & 2 & 2 & 1 \\ 2 & 1 & 3 & 3 & 0 & 3 & 3 & 1 \\ 1 & 2 & 0 & 0 & 0 & 0 & 0 & 2 \\ 0 & 2 & 2 & 1 & 0 & 1 & 2 & 2 \\ 0 & 2 & 2 & 2 & 0 & 2 & 2 & 2 \\ 1 & 2 & 0 & 3 & 3 & 3 & 3 & 2 \\ 1 & 3 & 0 & 0 & 0 & 0 & 0 & 3 \\ 2 & 3 & 3 & 1 & 0 & 1 & 3 & 3 \\ 2 & 3 & 3 & 2 & 0 & 2 & 0 & 3 \\ 2 & 3 & 3 & 3 & 0 & 3 & 3 & 3 \\ \hline \end{array}$

Hence according to the definition of $\mathscr C_4$, $(A3)$ is not a tautology.


Therefore $(A3)$ is independent from $(A1)$, $(A2)$, $(A4)$.

$\blacksquare$


Sources

Retrieved from "https://proofwiki.org/w/index.php?title=Hilbert_Proof_System_Instance_2_Independence_Results/Independence_of_A3&oldid=572906"