0

Can we prove using intuitionist logic that $\neg \exists r: \forall x: [P(x,r) \iff \neg P(x,x)]$ where $P$ is a binary logical predicate?

Dan Christensen
  • 14,529
  • 2
    Yes, negation introduction is intuitionistically valid, and the formula under $\neg$ leads to contradictory propositions (taking $x=r$) fulfilling its antecedent. – Conifold Dec 17 '19 at 04:20
  • @Conifold Thanks. I thought intuitionistic logic would not allow the required proof by contradiction since they reject LEM. – Dan Christensen Dec 18 '19 at 05:12
  • 1
    Yes, this is a common loose formulation. They allow proofs by contradiction with negative conclusions. But if you derive a contradiction from $¬p$, as is usually done, you can not infer $p$ intuitionistically (double negation is not removable). – Conifold Dec 18 '19 at 05:15
  • The usual intuitionistic proof of $\lnot(P \leftrightarrow \lnot P)$ is: suppose $P \leftrightarrow \lnot P$. Then if you suppose $P$, then you also have $\lnot P$, giving a contradiction; by $\lnot I$, this overall implies $\lnot P$. But then you also have $P$, giving a contradiction; so by $\lnot I$, $\lnot(P \leftrightarrow \lnot P)$. – Daniel Schepler Feb 06 '20 at 22:03

0 Answers0