I have asked about similar logics before, but this one is different.

The logics that I’ve asked about in the past take the Gödel-McKinsey-Tarski translation for Intuitionistic Propositional Logic to classical $S4$, but change the translation of negation to

$t(\neg A)=\neg \Box t(A)$.

If you define the translation thus:

$t(p)=\Box p$

$t(\neg A)=\neg \Box t(A)$

$t(A \to B)=\Box (t(A) \to t(B))$

$t(A \leftrightarrow B)=\Box (t(A) \leftrightarrow t(B))$,

it holds that one can define the rest of the Intuitionsitic operators that respect their BHK definitions. For example,

$\bot:=\neg (p \to p)$

$\top:=(\bot \to \bot)$

$(A \land B):=(A \leftrightarrow (A \to B))$

$(A \lor B):=(\neg A \to (\neg B \to B))$ etc.

The negation is still non-constructive; any axiomatization for it needs at least one non-constructive axiom. However, the definable disjunction has the disjunction property, re Gödel’s results about $S4$. Is the following axiomatization understandable as constructive?

Lowercase letters are propositional atoms, and uppercase letters are arbitrary formulas.

$p \to (A \to p)$

$(A \to (B \to C)) \to ((A \to B) \to (A \to C))$

$\neg (A \to A) \to B$

$((A \to B) \to C) \to (\neg C \to \neg B)$

$(\neg (A \to B) \to B) \to (A \to B)$

$(A \leftrightarrow B) \to (A \to B)$

$(A \leftrightarrow B) \to (B \to A)$

$(A \to B) \to ((B \to A) \to (A \leftrightarrow B))$

From $\vdash A$ and $\vdash A \to B$, infer $B$.

From $\vdash A(p)$, infer $\vdash A(B \to C)$, where $B \to C$ is uniformly substituted for $p$ in $A$.

P.S., I ask because I wonder whether this logic would be suitable for constructive mathematical theories, given similar definitions for $\exists$ and $\forall$ so that they would satisfy the BHK interpretation. In such a case, formulas like $A \to \exists x A$ would be invalid for arbitrary formulas, but would hold for quantified formulas and unquantified positive literals like $x \in y$. Thanks.

  • $\begingroup$ $(\neg (A \to B) \to B) \to (A \to B)$ for true $A$ looks like consequentia mirabilis, so I'd start by, investigating if malicious consequences of that prevail in your system. $\endgroup$
    – Nikolaj-K
    Commented Jun 14 at 16:37
  • $\begingroup$ @Nikolaj-K yes, and the standard consequentia mirabilis is provable in this system. However, since $\neg A \to (B \to \neg A)$ is invalid, the semi-classical results are strongly mitigated. $\endgroup$
    – PW_246
    Commented Jun 14 at 16:40


You must log in to answer this question.