Is there a way to define classical implication in this logic?

Question

I’m asking this question so that I may provide my own answer to it and share what I’ve discovered.

I’ve already posted about a logic that results from modifying the Gödel-McKinsey-Tarski translation from Intuitionistic Propositional Logic to classical S4 modal logic here: Has this logic already been studied?. The basic idea is to take the Gödel-McKinsey-Tarski translation and add in a new operator $\neg$. The translation is as follows:

• $tr(p)=\Box p$ for positive literals
• $tr(\bot)=\bot$
• $tr(A \land B)=(tr(A) \land tr(B))$
• $tr(A \lor B)=(tr(A) \lor tr(B))$
• $tr(\neg A)= \neg \Box tr(A)$
• $tr(A \to B)= \Box (tr(A) \to tr(B))$

Intuitionistic negation $\sim$ may be defined in terms of $\to$ and $\bot$. The accessibility relation between states is reflexive and transitive as in Intuitionistic Logic.

Given that all formulas in this logic are “modalized” in their propositional atoms, i.e. every translation from a formula in this logic to S4 results in an S4 formula modalized in all of its propositional atoms, is it possible to define a classical negation and/or implication operator?

Answer 1

The answer is in the affirmative. Note that $\neg A$ is equivalent to the classical negation of $\top \to A$ and $\sim \neg A$ is the classical negation of $\neg A$. Also, I use the term “Condition 1” to refer to wffs $A$ such that $tr(A)=\Box B$. Let $\overline A$ denote the classical negation of $A$ and $\supset$ classical implication. Then:

• $\overline A:= \neg A$ for Condition 1 $A$
• $\overline A:= \sim A $ for $A=\neg B$
• $\overline {(A \land B)}:=(\overline A \lor \overline B)$
• $\overline {(A \lor B)}:=(\overline A \land \overline B)$
• $(A ⊃ B):=(\overline A \lor B)$