Is it always the case that if $\emptyset \vdash A \iff B$ in classical logic then at least one of $\emptyset \vdash A \to B$ or $\emptyset \vdash B \to A$ in constructive logic? Does it depend on if you are restricted to propositional logic vs predicate logic?

  • $\begingroup$ Well it's always both. $\endgroup$ – Kenny Lau Sep 23 '17 at 6:22
  • $\begingroup$ $A \iff B$ is defined as $A \to B \land B \to A$, right? $\endgroup$ – Kenny Lau Sep 23 '17 at 6:26
  • $\begingroup$ @KennyLau Classical logic has different rules than constructive logic. $\endgroup$ – DanielV Sep 23 '17 at 6:47
  • $\begingroup$ Then how is $A \iff B$ defined? $\endgroup$ – Kenny Lau Sep 23 '17 at 7:08
  • 2
    $\begingroup$ @KennyLau That's how $A\iff B$ is defined, but the question is about situations like, for example, $\varphi\iff\neg\neg\varphi$ which is provable classically but only $\varphi\implies\neg\neg\varphi$ is provable constructively. $\endgroup$ – Derek Elkins Sep 23 '17 at 7:33

The answer is "no" even in intuitionistic propositional logic, which is what I assume you mean by "constructive logic". $ \def\imp{\Rightarrow} \def\eq{\Leftrightarrow} \def\from{\leftarrow} $

Let $P \overset{def}\equiv ( A \lor \neg A ) \eq ( B \lor \neg B )$. Then $P$ is a classical tautology. But let $K$ be a Kripke frame with worlds $0 \to 1$ and $2 \to 3$ where $A$ holds at only $1$ while $B$ holds at only $3$. Then the implication $( A \lor \neg A ) \imp ( B \lor \neg B )$ is false in $K$ because at $2$ we have that $\neg A$ (which denotes "$A \to \bot$") holds but neither $B$ nor $\neg B$ hold. By symmetry, $( B \lor \neg B ) \imp ( A \lor \neg A )$ is false in $K$ too. Thus for atoms $A,B$ neither of the implications be proven.

  • $\begingroup$ Would you make your frame connected? $\endgroup$ – Kenny Lau Sep 23 '17 at 8:48
  • $\begingroup$ @KennyLau: I could, but must I? =) I like the explicit disconnect here, so that it is clear that both sides have nothing to do with each other. =) $\endgroup$ – user21820 Sep 23 '17 at 8:49

For a somewhat different example, let $P$ and $Q$ be propositional variables. Then intuitionistic propositional logic does not prove $(P \land \lnot\lnot Q) \to (\lnot\lnot P \land Q)$ (and hence, by symmetry, it does not prove $(Q \land \lnot\lnot P) \to (\lnot\lnot Q \land P)$). To see this note that if intuitionistic logic could prove $(P \land \lnot\lnot Q) \to (\lnot\lnot P \land Q)$, it could also prove $(\top \land \lnot\lnot Q) \to (\lnot\lnot \top \land Q)$, which it can prove equivalent to the law of double negation elimination, $\lnot\lnot Q \to Q$, which is not intuitionistically valid.


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.