2
$\begingroup$

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

$\endgroup$
6
  • $\begingroup$ What are the axioms you're using? Specifically, is $\vee$ an abbreviation or do your axioms define it? $\endgroup$
    – B. Mehta
    Commented Apr 20, 2018 at 4:19
  • $\begingroup$ 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$ $\endgroup$ Commented Apr 22, 2018 at 3:19
  • $\begingroup$ Isn't $P\leftrightarrow Q$ an abbreviation for $(P\rightarrow Q)\land(Q\rightarrow P)$? $\endgroup$
    – bof
    Commented Apr 28, 2018 at 6:22
  • $\begingroup$ ↔ 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/… $\endgroup$ Commented Apr 29, 2018 at 23:27
  • $\begingroup$ 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. $\endgroup$
    – hardmath
    Commented Aug 28, 2018 at 14:07

1 Answer 1

2
$\begingroup$

$\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.

$\endgroup$

Not the answer you're looking for? Browse other questions tagged .