Consider the following system, $S$ above $\{\lnot, \to, \lor \}$:

Axioms (1-3 are HPC's original ones):

  1. $a\to (b\to a)$
  2. $(a\to (b\to c))\to ((a\to b)\to (a\to c))$
  3. $(\lnot a\to \lnot b)\to (b\to a)$
  4. $(a\lor b)\to (\lnot a\to b)$

Deduction Rules:

  1. MP
  2. $\frac{a}{a\lor b}$
  3. $\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


  • $\begingroup$ It seems to be broadly correct, but that "WLOG" hides a lot of important details. $\endgroup$ Jan 31, 2017 at 10:45
  • $\begingroup$ Basically, this WLOG means $l_k$ could be $p$ or $\lnot p$. Either way, one could prove $p\lor\lnot p$ from it (using the deduction rule). So that was my intention here. $\endgroup$ Jan 31, 2017 at 10:49
  • $\begingroup$ and obviously, if $l_k\equiv \lnot p$ then the proof stays the same since $\lnot p$ isn't a tautology either. $\endgroup$ Jan 31, 2017 at 10:50
  • 2
    $\begingroup$ Ah, then I misunderstood. My point is that you have to rule out that you can derive $\phi$ by MP somehow. $\endgroup$ Jan 31, 2017 at 10:51
  • $\begingroup$ Oh I see.. That's quite a challenge $\endgroup$ Jan 31, 2017 at 10:56

2 Answers 2


One approach is is as follows. First, note that all your axioms are tautologies under the normal (boolean) interpretation of propositional logic. Hence, just from the axioms it is impossible to prove, for a propositional letter $p$, either $p$ or $\neg p$, since tautologies need to hold regardless of the truth value of $p$.

Now, fix your formula $\phi$. We recursively define what it means for $\psi$ to be good (for $\phi$) as follows:

  • $\phi$ itself is good,
  • if $\psi$ and $\chi$ are good, then so is $\psi \lor \chi$,
  • if $\psi$ is good, and $\chi$ is not good, then $\chi \to \psi$ is good,
  • if $\psi$ is not good, then $\neg \psi$ is good,
  • all formulas whose goodness is not set by the above rules are not good.

Now, suppose towards a contradiction that we have a proof of $\phi$. Since $\phi$ is good, there must be a first good formula in the proof -- let us say that it is $\psi$. Now, $\psi$ cannot be an axiom, since none of the axioms are good. It also cannot follow by modus ponens, since if $\psi$ is good, then at least one of $\chi$ and $\chi \to \psi$ must be good. Finally, it cannot follow by your rules 2 or 3: if $\psi$ is $\phi$ itself, then it must follow from $p$ or $\neg p$, but we had established that your axioms cannot prove those. If $\psi = \psi_0 \lor \psi_1$ is good but not equal to $\phi$, then both $\psi_0$ and $\psi_1$ must be good; but $\psi$ must be derived from one of them.

All in all, this gives a contradiction. Hence your axioms do not prove $\phi$.

  • $\begingroup$ Why did you set "$\psi$ is not good, then $\lnot\psi$ is good"? Is that because semantically, $\lnot (p\lor \lnot p) \equiv p\lor \lnot p$? $\endgroup$ Feb 5, 2017 at 9:51
  • $\begingroup$ Also, if $a\equiv p$ then you can derive $p\lor \lnot p$ so it isn't true that "the rules of inference can only prove good formulas". $\endgroup$ Feb 5, 2017 at 9:53
  • $\begingroup$ The useless answer is "I use this definition because it works". More to the point: I designed the "good" formulas to be a class including those formulas from which you can prove $\phi$, and so you can't prove any good formulas. Hence it might be important to have formulas like $\neg\neg\phi$ be "good". Note that you crucially use the goodness clause for negated formulas when showing that the third axiom is not good. $\endgroup$ Feb 5, 2017 at 14:40
  • $\begingroup$ To your second point, you're quite right. I made an error in my answer. The clause for disjunctions should be that both formulas in it are good. Will correct it now. $\endgroup$ Feb 5, 2017 at 22:31
  • 1
    $\begingroup$ @blueplusgreen, I'm sorry, I didn't initially read your comment correctly. Your objection is very much right. I have edited my answer yet again, and am fairly confident that it is now correct. This question was much more subtle than I thought. $\endgroup$ Feb 6, 2017 at 13:36

There is a standard, but tedious way to prove that the law of excluded middle does not hold in some system. Let us have three truth values: $T,F$ and $U$, standing for "true", "false" and "unknown". Then we can define $\vee$ as maximum of the values ($F<U<T$), $\wedge$ as mininum (there is no $\wedge$ in this system though), $\neg A$ as $F$ unless it is known for sure that $A$ is false (that is, we add $\neg U=F$ to the usual laws $\neg F=T$ and $\neg T=F$), and $\rightarrow$ is rather tricky: false implies anything ($F\rightarrow x=T$), $T\rightarrow x$ is equivalent to $x$ and $U\rightarrow x$ is $T$ unless $x=F$, in the latter case $U\rightarrow F=F$. Now we can check with some brute-forcing that for all axioms the value is $T$ for any values of variables, and any deduction rule makes true out of true, but $p\vee\neg p$ turns into $U$ on $p=U$, so it is not derivable.

  • $\begingroup$ Actually, on second thought, I don't think this works: axiom 3 does not always evaluate to T (and it shouldn't, as under a normal axiom system, it is equivalent to LEM). $\endgroup$ Feb 5, 2017 at 14:44
  • $\begingroup$ @MeesdeVries On which input it doesn't? $\endgroup$
    – Wolfram
    Feb 5, 2017 at 15:37
  • $\begingroup$ On $b=T, a=U $. $\endgroup$ Feb 5, 2017 at 16:48

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .