Skip to main content
added 260 characters in body
Source Link
DanielV
  • 24.6k
  • 5
  • 41
  • 70

$$ \frac{a\rightarrow b, \quad a\rightarrow \neg b}{\neg a}$$

This axiom doesn't prevent defining $\lnot X = \top$ . So you won't be able to prove any theorem that distinguishes $\top$ from $\lnot$. For example,

$$P \to \lnot P \to Q$$

holds under the intended meaning of $\lnot$, but $P \to \top \to Q$ is not going to be provable from sound axioms.


Another way of putting it is that any theorem provable from the given axioms will also be soundly true when any expression $\lnot X$ is replaced by $\top$ (true). So any tautology, which is not a tautology after a replacement, will not be provable.

$$ \frac{a\rightarrow b, \quad a\rightarrow \neg b}{\neg a}$$

This axiom doesn't prevent defining $\lnot X = \top$ . So you won't be able to prove any theorem that distinguishes $\top$ from $\lnot$. For example,

$$P \to \lnot P \to Q$$

holds under the intended meaning of $\lnot$, but $P \to \top \to Q$ is not going to be provable from sound axioms.

$$ \frac{a\rightarrow b, \quad a\rightarrow \neg b}{\neg a}$$

This axiom doesn't prevent defining $\lnot X = \top$ . So you won't be able to prove any theorem that distinguishes $\top$ from $\lnot$. For example,

$$P \to \lnot P \to Q$$

holds under the intended meaning of $\lnot$, but $P \to \top \to Q$ is not going to be provable from sound axioms.


Another way of putting it is that any theorem provable from the given axioms will also be soundly true when any expression $\lnot X$ is replaced by $\top$ (true). So any tautology, which is not a tautology after a replacement, will not be provable.

Source Link
DanielV
  • 24.6k
  • 5
  • 41
  • 70

$$ \frac{a\rightarrow b, \quad a\rightarrow \neg b}{\neg a}$$

This axiom doesn't prevent defining $\lnot X = \top$ . So you won't be able to prove any theorem that distinguishes $\top$ from $\lnot$. For example,

$$P \to \lnot P \to Q$$

holds under the intended meaning of $\lnot$, but $P \to \top \to Q$ is not going to be provable from sound axioms.