How to get LNC as a theorem using Frege's Prop Calculus?

67 Views Asked by At

So Im using axioms from,Frege propositional calculus and is there any way to derive Law of non contradiction as theorem from them.

The axioms

  1. A → (B → A) | THEN-1

  2. (A → (B → C)) → ((A → B) → (A → C)) | THEN-2

  3. (A → (B → C)) → (B → (A → C)) | THEN-3

  4. (A → B) → (¬B → ¬A) | FRG-1

  5. ¬¬A → A | FRG-2

  6. A → ¬¬A | FRG-3

And one inference rule, MP

1

There are 1 best solutions below

1
On

I am not sure what you would regard as an expresion of the Law of Non-COntradiction (would be good to add to your post!), but Wikipedia states the Law of Contradiction as $\neg (P \land \neg P)$

As is, that statement cannot be derived from Frege's axioms, simply because Frege's system does not work with conjunctions... it only uses $\neg$'s and $\to$'s.

So, we could try and state the Law of Non-contradiction using $\neg$'s and $\to$'s by using certain elementary equivalences from Classical Logic.

For example, if we use the classical logic equivalence that $P \to Q \Leftrightarrow \neg (P \land \neg Q)$, then $\neg (P \land \neg P)$ could be written simply as $P \to P$ .. which is a theorem you can derive from Aixoms THEN-1 and THEN-2 fairly easily (most texts on axiom systems will have this proof ... it appears on the second page of this document)

But we can also use $\neg (P \to Q) \Leftrightarrow P \land \neg Q$, in which case we get that $\neg (P \land \neg P)$ becomes $\neg \neg (P \to P)$. Well, we already know that you can get $P \to P$ from THEN-1 and THEN-2, so using FRG-3 you'll then get $\neg \neg (P \to P)$.

FInally, we can say that $\neg(P \land Q) \Leftrightarrow \neg P \lor \neg Q$, and that $P \to Q \Leftrightarrow \neg P \lor Q$. So with that: $\neg(P \land \neg P) \Leftrightarrow \neg P \lor \neg \neg P \Leftrightarrow P \to \neg \neg P$ .. which simply is FRG-3.

This third suggestion is Noah's suggestion from Comments, and it would be my preferred choice as well: it says “if you have $P$, then you cannot (also) have $\neg P$ … which really seems to capture the spirit of the Law of Non-Contradiction, unlike $P \to P$, or $\neg \neg (P \to P)$.

And what about FRG-2, which is $\neg \neg P \to P$? Well, it is saying “if you don’t have $\neg P$, then at least you still have $P$”. In other words, this formula nicely captures the Law of Excluded Middle idea that at least one of $P$ and $\neg P$ is true, which we normally capture using $P \lor \neg P$. But that idea, as the Wikipedia page points out, isn’t quite the idea of the Law of Non-Contradiction … the Law of Non-Contrsdiction says that at most one of them is true, i.e. that they are not both true. For that $P \to \neg \neg P$ seems to fit the bill just right.