5
$\begingroup$

I'm looking at Wikipedia's article on Intuitionist logic, and I can't figure out how it would prove $(p \rightarrow p)$.

Does it prove $(p \rightarrow p)$? If yes, how?

If no, is there a correct (or reasonable, if there is no "correct") axiomatization of intuitionistic logic available anywhere online?

  • 0
    As you can see from the answer below, the "standard" derivation, in an *Hilbert-style* proof system, of $p \rightarrow p$ use only the propositional axioms THEN-1 and THEN-2. They are both intuitionistically available. In classical logic, where $p \rightarrow q$ is equivalent to $\lnot p \lor q$, the *tautology* $p \rightarrow p$ is equivalent to $\lnot p \lor p$, i.e. to *Excluded Middle*; this does not work in *intuitionistic logic*, where the connectives are not interdefinable.2014-03-29

1 Answers 1

8
  1. $p→(p→p)$ (THEN-1)
  2. $p→((p→p)→p)$ (THEN-1)
  3. $(p→((p→p)→p))→((p→(p→p))→(p→p))$ (THEN-2)
  4. $(p→(p→p))→(p→p)$ (MP from lines 2,3)
  5. $(p→p)$ (MP from lines 1,4)