# Would this logic be considered constructive?

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.

• $(\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. Commented Jun 14 at 16:37
• @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. Commented Jun 14 at 16:40