We know that $P \to Q$ is equivalent to $\neg P \lor Q$, as can be verified easily in truth table. Now suppose we have proof for self-implication below [the axiom system is Lukasiewicz's, with L1: $P \to (Q \to P)$, L2: $(P \to (Q \to R) \to ((P \to Q) \to (P \to R))$]:

(1) $P \to ((P \to P) \to P)$ --- (L1)

(2) $(P \to ((P \to P) \to P)) \to ((P \to (P \to P)) \to (P \to P))$ --- (L2)

(3) $(P \to (P \to P)) \to (P \to P)$ --- (1,2 MP)

(4) $P \to (P \to P)$ --- (L1)

(5) $P \to P$ --- (3,4 MP)

This proof establishes that $P \to P$. It is at this point that I realized two things:

First, since we know that $P \to P$ is equivalent to $\neg P \lor P$ and since $\neg P \lor P$ is the Law of Excluded Middle (or more precisely $P \lor \neg P$, but the order of negation don't matter), can it be said that the two are the same? That is, LEM is self-implication. If so, then a logic without LEM (intuitionistic logic) is a logic without self-implication. In other words, in a logic where LEM is not a theorem, self-implication is also not a theorem. Is my reasoning correct?

Second, as a corrolary of the first, can we concludes that the above proof is also (albeit in a disguised form, given semantic reading of equivalence between propositions) proof of LEM?

  • $\begingroup$ I am not an expert on intuitionist logic, but the Wikipedia page seems to indicate that the two axioms you are using to derive $P \to P$ are axioms of intuitionist logic as well. So, $P \to P$ would seem to be a theorem of intuitionist logic. And if $P \lor \neg P$ is not, then the equivalence of $P \to P$ and $P \lor \neg P$ must be something that does not hold for intuitionist logic. $\endgroup$ – Bram28 May 23 '19 at 19:25

Self-implication is true in intuitionistic logic as well. It really should be: if we assume $P$, we really should be able to derive $P$.

The point is that $P \to Q$ and $\neg P \lor Q$ are not equivalent in intuitionistic logic. The direction: $P \to Q$ implies $\neg P \lor Q$ uses LEM (and cannot be proved without LEM).

As pointed out in the comments, it may be worth noting that truth tables do not work for intuitionistic logic. That is, if a truth table says two formulas are equivalent, then they are classically equivalent, but not necessarily intuitionistically equivalent. There are similar semantics for intuitionistic logic, called Heyting algebras, but this is more complicated.

  • 3
    $\begingroup$ As a bonus, another way of defining $P\to Q$ in classical logic is $\neg(P\land\neg Q)$. In intuitionistic logic, we end up with $\neg P\lor Q\implies P\to Q\implies\neg(P\land\neg Q)$ but neither of the reverse entailments. $\endgroup$ – Derek Elkins left SE May 23 '19 at 20:24
  • $\begingroup$ I'd recommend mentioning that truth tables is a semantics for classical propositional logic, and as such is not complete for intuitionistic propositional logic, i.e. that something is a classical tautology doesn't mean it's provable/valid intuitionistically. Different semantics are required for intuitionistic logic. $\endgroup$ – Derek Elkins left SE May 23 '19 at 20:32
  • $\begingroup$ @Derek I avoided semantics on purpose, because I do not know what OP is familiar with and it might just cause confusion. $\endgroup$ – Mark Kamsma May 23 '19 at 20:50
  • $\begingroup$ The OP references truth tables. Stating that truth tables already presuppose classical logic and therefore don't "work" for intuitionistic logic seems reasonable. My previous comment is more technical than I'd recommend formulating it in the answer because it was directed at you rather than the OP. Nevertheless, the source of the OP's confusion was an equivalence justified by truth tables, so it seems important to directly address that. In my experience, an incorrect belief along the lines that truth tables are the final arbiter of any logical question seems very common. $\endgroup$ – Derek Elkins left SE May 23 '19 at 20:58
  • $\begingroup$ @Derek Ah, I see. I added a bit about truth tables. Thank you for the suggestion. $\endgroup$ – Mark Kamsma May 23 '19 at 21:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.