Here, $\psi$ is some arbitrary formula.

The proof I've come up with is as follows.

Assume $\lnot \lnot (\psi \lor \lnot \psi)$ is not a theorem of IPL, which means there exists some Kripke model where

$$\exists w: w \not\models \lnot \lnot (\psi \lor \lnot \psi),$$

which, by definition of negation being truthful in Kripke models, is equivalent to

$$\exists w: \exists u \geq w: u \models \lnot (\psi \lor \lnot \psi).$$

This, again by definition of negation truthfulness, implies for this $u$ that

$$\forall v \geq u : v \not \models \psi \lor \lnot \psi.$$

By definition of truthfulness of $\lor$ in Kripke models, this, in turn, implies

$$\forall v \geq u : v \not \models \psi, v \not \models \lnot \psi.$$

But if $\forall v \geq u : v \not \models \psi$, then $u \models \lnot\psi$, which contradicts $\forall v \geq u : v \not \models \lnot \psi$.

Hence, the original assumption is false, and $\lnot \lnot (\psi \lor \lnot \psi)$ is a theorem of IPL.

Is this reasoning correct?

  • $\begingroup$ Or you could use syntax instead of semantics. $\endgroup$ – Kenny Lau Jun 2 '18 at 19:33
  • $\begingroup$ I haven't got that far in my self-studies yet. $\endgroup$ – 0xd34df00d Jun 2 '18 at 19:33
  • $\begingroup$ I find syntax easier than semantics, to be frank. $\endgroup$ – Kenny Lau Jun 2 '18 at 19:34
  • $\begingroup$ Just curious, how would you use syntax in this case? $\endgroup$ – 0xd34df00d Jun 2 '18 at 19:37
  • $\begingroup$ Which style of proof do you use? $\endgroup$ – Kenny Lau Jun 2 '18 at 19:38

To prove $\lnot \lnot (P \lor \lnot P)$, assume $\lnot (P \lor \lnot P)$ and show that it leads to a contradiction.

Under that assumption, you can show both $\lnot P$ holds by contradiction as well as $\lnot \lnot P$ holds, which is the desired contradiction. In long form:

$$ \begin{array} {rl} % Markup \begin{array} {r} \begin{array} {r|} \text{Assumption } \\ \hline \begin{array} {r|} \text{Assumption } \\ \hline \text{Or Intro } \\ \text{Contradiction } \\ \end{array} \\ \text{Negation Intro } \\ \begin{array} {r|} \text{Assumption } \\ \hline \text{Or Intro } \\ \text{Contradiction } \\ \end{array} \\ \text{Negation Intro } \\ \text{Contradiction } \\ \end{array} \\ \text{Negation Intro } \end{array} & % Proof \begin{array} {l} \begin{array} {|l} \lnot (P \lor \lnot P) \\ \hline \begin{array} {|l} P \\ \hline P \lor \lnot P \\ \bot \\ \end{array} \\ \lnot P \\ \begin{array} {|l} \lnot P \\ \hline P \lor \lnot P \\ \bot \\ \end{array} \\ \lnot \lnot P \\ \bot \\ \end{array} \\ \lnot \lnot (P \lor \lnot P) \end{array} % End Proof \end{array}$$

  • $\begingroup$ That's an interesting alternative to using the correspondence with Kripke models, thanks! $\endgroup$ – 0xd34df00d Jun 3 '18 at 17:52

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.