# Does the equivalence ($P \rightarrow Q$) $\iff$ ($\lnot P \lor Q$) hold in intuitionistic logic? [closed]

Does it maybe hold in one direction but not the other?

• What are the axioms you're using? Specifically, is $\vee$ an abbreviation or do your axioms define it? Commented Apr 20, 2018 at 4:19
• The answer will be the same for any usually-accepted axiomatization of intuitionistic propositional calculus. In none of these axiom-sets is much of any connective treated as an abbreviation, except that $\lnot P$ is (arguably) defined as an abbreviation for $P\rightarrow\bot$ Commented Apr 22, 2018 at 3:19
• Isn't $P\leftrightarrow Q$ an abbreviation for $(P\rightarrow Q)\land(Q\rightarrow P)$?
– bof
Commented Apr 28, 2018 at 6:22
• ↔ needn't occur at all in those axiomatizations. There is a difference between a definition and an axiom, usually. An occurrence of a term that has a definition that is an abbreviation can be eliminated (the left/short side of the definition can be eliminated in favor of the right/long one). ↔ is more syntactic icing than cake. It makes some things easier to say but it's truly optional. Negation is a little more critically basic than that. Here is an example: encyclopediaofmath.org/index.php/… Commented Apr 29, 2018 at 23:27
• Please avoid stating the problem you want help with only in the title. The body of a Question provides ample space for the specific details you've been asked to provide, and adding a series of Comments is less desirable than making a full self-contained problem statement in the body of the Question. Commented Aug 28, 2018 at 14:07

$\Leftarrow$ holds but $\Rightarrow$ does not hold.
To show that $\Leftarrow$ holds, suppose $\neg P \vee Q$ holds. Then if $P$, I claim that $P \to Q$ holds. In the first case, $\neg P$ and $P$ form a contradiction, so $Q$. If $Q$, then clearly $Q$. Thus $P \to Q$.
To show that $\Rightarrow$ does not hold, find a model of intuitionistic logic where $P \to Q$ holds but $\neg P \vee Q$ does not hold. Intutionistic logics are modeled by Heyting algebras, so to prove that $P \to Q$ does not imply $\neg P \vee Q$, it suffices to find a Heyting algebra where $((P \to Q) \Rightarrow (\neg P \vee Q))$ is not 1. An Heyting algebra where this is true is given by the third example on this Wikipedia page. Let $P = ½$, $Q = ½$. Then $P \to Q = 1$ but $\neg P \vee Q = ½$. Then $((P \to Q) \Rightarrow (\neg P \vee Q)) = 0$, which is not 1, so we are done.