关于将适用于直觉主义片段{¬,∨,∧}的经典-克林组合逻辑扩展至包含→算子的技术问询

Great question—let's break down your current work, the problem you're facing, and some actionable directions to address it:

背景回顾：你的经典-克林组合逻辑方案 #

Over a year ago, you developed a classical-Kleene combination logic that preserves intuitionistic tautologies for the ${ \neg, \vee, \wedge }$ fragment. Here's a quick recap of how it operates:

• You use ${0, 1, 2}$ to represent false, unsure, and true respectively. Since Kleene logic has no tautologies on its own, you introduced a "Gilvenko switch" (named for Gilvenko's lemma) to restrict it to only intuitionistic tautologies.
• Propositional variables get unique truth-value columns following standard classical truth-table rules. When a proposition leads to a classical contradiction, the unsure value $1$ can switch to $0$.
• The system is compositional: every formula has a "head" Kleene value paired with a "tail" truth-table column for each unique atomic proposition.

示例推导：$\neg \neg (A \vee \neg A)$ #

To illustrate, here's your step-by-step derivation of $\neg \neg (A \vee \neg A)$ (a double-negated LEM, which is an intuitionistic tautology):

$\neg \neg ([1,20] \vee \neg [1,20])$  # Initial assignment
$\neg \neg ([1,20] \vee [1,02])$
$\neg \neg [1,22]$  # Preserves that LEM itself is not an intuitionistic tautology
$\neg \neg [1,2]$  # Halving step
$\neg [1,0]$
$\neg [0,0]$  # Gilvenko switch (1 → 0 for contradictions)
$[2,2]$  # Aligns with Gilvenko's theorem: double-negated LEM is an intuitionistic tautology

当前困境：蕴含算子→的局限性 #

Your core issue is that this framework can't prove $P \rightarrow P$ unless you translate $\rightarrow$ to $\neg (P \wedge \neg P)$. But this translation introduces an unwanted side effect: it validates double negation elimination (DNE)—$(\neg \neg P \rightarrow P)$, which translates to $\neg (\neg \neg P \wedge \neg P)$.

This isn't surprising: in intuitionistic logic, $\rightarrow$ is independent of ${ \neg, \vee, \wedge }$ (unless you define $\neg A$ as $A \rightarrow \bot$, where $\bot$ is $[0,0]$ in your system). Translating $\rightarrow$ to negation/conjunction collapses this independence, leading to classical principles like DNE that you don't want.

You also noted that most existing intuitionistic decision procedures are emergent (composite-to-atomic) rather than compositional, and many are full theorem provers—overkill for your goal of building a programming language with an "unsure" value that follows intuitionistic rules.

核心问题与解决方案思路 #

Your key questions are: can we amend an algorithm to perform an inverse of the Gilvenko switch (turning $[1,2]$ to $[2,2]$), and is there literature on similar ideas? Here are targeted approaches:

1. Define a compositional rule for → instead of translating it #

Instead of reducing $\rightarrow$ to other operators, create a Kleene-style evaluation rule for $P \rightarrow Q$ that matches intuitionistic semantics:

• Intuitionistically, $P \rightarrow Q$ holds if whenever $P$ is provable, $Q$ is also provable. For your 3-valued system:
  • If $P$'s head is $2$ (true), then $Q$'s head must be $2$ for the implication to be $2$; if $Q$ is $0$, implication is $0$; if $Q$ is $1$, implication is $1$.
  • If $P$'s head is $0$, implication is $2$ (intuitionistic "ex falso quodlibet").
  • If $P$'s head is $1$, check the truth-table tail: if every classical assignment where $P$ is true forces $Q$ to be true, switch the implication's head from $1$ to $2$; otherwise keep it $1$.

This would let you prove $P \rightarrow P$ directly: no matter what $P$'s value is, the implication evaluates to $2$, without validating DNE.

2. Implement a "positive Gilvenko switch" #

Your current Gilvenko switch handles contradictions by turning $1$ to $0$. For the inverse (validating intuitionistic tautologies with $\rightarrow$), add a positive Gilvenko switch:

• If a formula's truth-table tail shows that every classical assignment makes the formula true (i.e., it's a classical tautology that's also an intuitionistic tautology), the unsure head value $1$ can switch to $2$.

For $P \rightarrow P$, the truth-table tail is $[2,2]$ (all classical assignments make it true). The head starts as $1$, but the positive switch turns it to $2$, since there's no classical counterexample. This avoids validating DNE because DNE's tail would have assignments where it fails (from an intuitionistic perspective), so the switch wouldn't trigger.

3. Adapt lightweight compositional intuitionistic decision procedures #

For your programming language use case, look into:

• Compositional intuitionistic tableaux systems: These build proofs bottom-up and can be adapted to your 3-valued framework.
• BDD-based IPL decision procedures: Binary Decision Diagrams offer $O(n \log n)$ performance and are inherently compositional, making them a good fit for a programming language tool.
• Kripke semantics mappings: Map your 3 values to Kripke worlds: $0$ = false in all worlds, $1$ = true in some but not all worlds, $2$ = true in all worlds. The positive Gilvenko switch would correspond to collapsing worlds where a formula is universally true.

相关文献参考 #

For existing work related to your proposal:

• Search for 3-valued intuitionistic logics (e.g., Heyting algebras with intermediate values or intuitionistic Kleene logics).
• Look into compositional semantics for IPL with partial/uncertain values—this is an active area for programming language applications (e.g., lazy evaluation, partial correctness).
• Explore generalizations of Gilvenko's lemma to fragments with implication; some papers extend the result to cover $\rightarrow$ and could formalize your positive switch rule.

备注：内容来源于stack exchange，提问作者Joshua Harwood