Consider the following system, $S$ above $\{\lnot, \to, \lor \}$:
Axioms (1-3 are HPC's original ones):
- $a\to (b\to a)$
- $(a\to (b\to c))\to ((a\to b)\to (a\to c))$
- $(\lnot a\to \lnot b)\to (b\to a)$
- $(a\lor b)\to (\lnot a\to b)$
Deduction Rules:
- MP
- $\frac{a}{a\lor b}$
- $\frac{b}{a\lor b}$
It's given that $S$ is sound - Prove that $S$ isn't complete.
My Try:
Let's look at $\varphi = p\lor \lnot p$. $\varphi$ is a tautology. Therefore, if $S$ is complete then $\vdash_S p\lor\lnot p$. Therefore, there's a proof for $\varphi$: $l_1, \ldots, l_n\equiv p\lor\lnot p$. Hence, WLOG for some $k<n$, $l_k \equiv p$. Therefore, $\vdash_S p$.
Since $S$ is sound, $\vDash p$ - but obviously that is not true that $p$ is a tautology (considering the interpretation $v(p) = f$)
I'd be glad to get a proof-verification
Thanks!