I’ve asked this same question on math.stackexchange.com, but haven’t received any answers. I ask this question in good faith, so I hope it meets this site’s standards.
I have been spending the better part of a year thinking about the subtleties involved in balancing natural language intuitions for logic with the power and efficacy that Classical Logic and Intuitionsitic Logic provide. In so doing, I believe that I’ve discovered/invented a logic that is very similar to Bi-Intuitionistic Logic. The operators are defined the same way they usually are for a Kripke semantics for Intuitionistic Logic except that
$w \Vdash \neg A$ iff there is a $v$ s.t. $w \le v$ and $v \not \Vdash A$ where $\le$ is the accessibility relation between states.
For reference, the semantics for Bi-Intuitionistic Logic defines its weak negation $\sim$ as
$w \Vdash \sim A$ iff there is a $v$ s.t. $v \le w$ and $v \not \Vdash A$.
Below is an axiomatization for the altered semantics. Note that strong negation, $\top$, and $\bot$ may be defined in terms of $\neg$ and $\to$.
A1. $(B→C)→A→B→C$
A2. $(A→B)→(A→(B→C)) \to A→C$
B1. $(A→B)→¬B→¬A$
B2. $\neg (A \to A) \to C$
B3. $\neg(A \to B) \to ¬B$
B4. $(\neg(A→B)→B)→A→B$
$\lor$I. $A_i \to (A_1 \lor A_2)$ $\ $ where $i=1$ or $i=2$
$\land$E. $(A_1 \land A_2) \to A_i$ $\ $ where $i=1$ or $i=2$
$\land$I. $(A \to B) \to (A \to C) \to A \to (B \land C)$
$\lor$E$. ((A \land B) \to D) \to ((A \land C) \to D) \to (A \land (B \lor C)) \to D$
MP$:$ From $\vdash A$ and $\vdash A \to B$ infer $\vdash B$
NI$:$ From $\Gamma \vdash A$ infer $\Gamma \vdash A’$ where $A’$ results from the substitution $[(\top \to B)/B]$ for any Condition 1 formula $B$ occurring in $A$.
Condition 1 is defined for wffs $A$ as follows:
- If $A$ is a positive literal, then $A$ is Condition 1.
- If $A=(B \to C)$, then $A$ is Condition 1
- If $A=(B \land C)$ or $A=(B \lor C)$, and both $B$ and $C$ are Condition 1, then $A$ is as well.
- All and only Condition 1 formulas are constructed with finitely-many applications of these rules.
If NI is removed, the resulting logic is the same except that formulas built from only positive literals do not retain the Heredity Condition of Intuitionistic logic.
I know that there is a lot of recent research in this area of logic, but I haven’t been able to find any works by professional logicians on it. I am curious since this logic shares many similarities with both Relevance Logics, Intuitionistic Logic, and Classical Logic. Specifically, the implication in this logic is still the Intuitionistic implication, i.e.
$w\Vdash (A \to B)$ iff for any $v$ s.t. $wRv$, if $v \Vdash A$ then $v \Vdash B$.
But, the weak negation simultaneously validates semi-classical results like $(\neg A \to A) \to A$ and invalidates much of positive implicational logic, e.g. $A \to B \to A$.
Further, the full logic including the rule NI validates these analogues to some lesser-known modal logic axioms
$((A \to (\top \to A)) \to A) \to A$ [Grz. Axiom]
$- -A \to \neg \neg A$ [Mckinsey Axiom]
where $-$ is strong negation. These hold for the entire propositional portion of the logic and much of the first order portion.
When $\bot$ is defined, the pair of axiom schemata
$\neg (A \to B) \to \neg B$
$(\neg (A \to B) \to B) \to A \to B$
may be replaced by the axiom schema
$((A \to B’) \to (A \to C)) \to (A \to (\neg B \to C)) \to A \to C$
where $B’=B$ or $B’=\neg B \to \bot$.
Though unconventional, it is most natural to define $\bot:=\neg(A \to A)$ and $\top:=(\bot \to \bot)$.
