NL semantics, soundness, and completeness (the Lean-aligned version)
Below is a self-contained presentation of the semantics that exactly matches the structures and clauses in the Lean files you listed (Semantics.lean, ProofSystem.lean, Lindenbaum.lean, Canonical.lean). It reads ~ as intuitionistic (Kripke) negation, interprets → via world-relative selections, and keeps ◦ as a primitive compatibility predicate. The frame conditions are the ones encoded in NL.Frame; the canonical construction and Truth Lemma follow Canonical.lean and Lindenbaum.lean.
Throughout, the language has atoms \(p,q,\dots\), conjunction \(\wedge\), negation \(\sim\), implication \(\to\), and a primitive binary connective \(\circ\). The intended abbreviations are
\[
\begin{aligned}
A\mid B \ &:=\ \sim(A\circ B), \\
A = B \ &:=\ (A\to B)\wedge(B\to A), \\
A\ne B \ &:=\ \sim(A=B),
\end{aligned}
\]
and \(A\ne B\ne C\) abbreviates \((A\ne B)\wedge(B\ne C)\wedge(A\ne C)\).
1. Frames and models
Up-set and intuitionistic negation at the set level
Let \((W,\le)\) be a preorder (reflexive and transitive). For \(X\subseteq W\), write
\[
\begin{aligned}
\uparrow w \ &:=\ {v\in W: w\le v},\\
\mathrm{iNeg}_\le(X) \ &:=\ {w\in W : \uparrow w\cap X=\varnothing}.
\end{aligned}
\]
Thus \(w\in \mathrm{iNeg}_\le(X)\) iff every \(v\ge w\) fails to be in \(X\). This is the Kripke/intuitionistic complement of \(X\) relative to \(\le\).
NL-frames
An NL-frame is a tuple
\[
\mathcal F=\langle W,\ \le,\ f,\ C\rangle
\]
with:
- \((W,\le)\) a nonempty preorder (intuitionistic accessibility).
- a selection map \(f: W\times\mathcal P(W)\to\mathcal P(W)\), written \(f_w(X)\);
- a compatibility predicate \(C: W\times\mathcal P(W)\times\mathcal P(W)\to{\mathsf{true},\mathsf{false}}\), written \(C_w(X,Y)\).
These satisfy, for all (w,x\in W) and (X,Y,Z\subseteq W):
Conditional laws
-
Id: \(f_w(X)\subseteq X\).
-
Her (heredity in the world): if \(w\le x\) then \(f_x(X)\subseteq f_w(X)\).
-
Succ (local detachment): if \(w\in X\) then \(w\in f_w(X)\).
-
Contra (set-level counterpart of axiom 1.7):
if \(f_w(X\cap Y)\subseteq Z\) then \(f_w!\big(X\cap \mathrm{iNeg}_\le(Z)\big)\subseteq \mathrm{iNeg}_\le(Y)\).
-
f-up (selections stay above the current world):
if \(x\in f_w(X)\) then \(w\le x\).
Compatibility laws
6. C-sym: \(C_w(X,Y)\iff C_w(Y,X)\).
7. C-coh (coherence with \(\to\)): if \(f_w(X)\subseteq Y\) then \(C_w(X,Y)\).
8. C-her (persistence of \(\circ\)): if \(w\le x\) and \(C_w(X,Y)\) then \(C_x(X,Y)\).
Guarded syllogism (matching axiom 1.5)
9. Tr≠ (at world \(w\)): define \(X\equiv_w Y\) iff \(f_w(X)\subseteq Y\) and \(f_w(Y)\subseteq X\); write \(X\not\equiv_w Y\) for its negation. Then
\[
\begin{aligned}
&X\not\equiv_w Y,\ \ Y\not\equiv_w Z,\ \ X\not\equiv_w Z,\ \\
&f_w(X)\subseteq Y,\ \ f_w(Y)\subseteq Z\ \ \Rightarrow\ \ f_w(X)\subseteq Z.
\end{aligned}
\]
Remarks.
• f_up makes the implication’s witnesses live at or above the current world (a Kripke-style guard), and—together with Her—yields persistence of truth for (\to).
• C_her ensures \(\circ\) is also upward persistent.
• Tr≠ validates precisely the guarded version 1.5; you may strengthen it to unconditional hypothetical syllogism if desired, but the logic only requires the guarded form.
NL-models and truth
An NL-model is \(\mathcal M=\langle \mathcal F, V\rangle\) where \(V\) assigns each atom \(p\) an up-set \(V(p)\subseteq W\) (i.e., \(w\in V(p)\le x\Rightarrow x\in V(p)\)).
Given a formula \(A\), write \(⟦ A⟧={w\in W: \mathcal M,w\models A}\). Let \(X=⟦ A⟧\), \(Y=⟦ B⟧\). Truth is defined by:
- \(w\models p \iff w\in V(p)\).
- \(w\models A\wedge B \iff w\models A\) and \(w\models B\) (so \(⟦ A\wedge B⟧=X\cap Y\)).
-
Intuitionistic negation: \(w\models \sim A \iff \forall v\ge w,\ v\not\models A\) (so \(⟦\sim A⟧=\mathrm{iNeg}_\le(X)\)).
-
Implication: \(w\models A\to B \iff f_w(X)\subseteq Y\).
-
Consistency: \(w\models A\circ B \iff C_w(X,Y)\).
Abbreviations \(A\mid B\), \(=\), \(\ne\) are interpreted from these clauses.
2. Immediate meta-properties
Persistence. For every formula \(A\), if \(w\models A\) and \(w\le x\), then \(x\models A\).
Sketch. Atoms persist by valuation; \(\wedge\) and \(\sim\) are standard Kripke cases; for \(\to\) use Her; for \(\circ\) use C_her.
Symmetry of inconsistency. \(⟦ A\mid B⟧=⟦ B\mid A⟧\) by C-sym and the Kripke clause for \(\sim\).
Kripke double negation. \(⟦ A⟧\subseteq⟦\sim\sim A⟧\) always holds, hence \(A\to\sim\sim A\) is valid.
3. Soundness for the Hilbert presentation of NL
All schemes 1.1–1.7 and rules R1–R2 are valid on every NL-frame.
-
1.1 \(A\to A\): by Id, \(f_w(X)\subseteq X\).
-
1.2 \((A\mid B)\to(B\mid A)\): \(⟦ A\circ B⟧=⟦ B\circ A⟧\) by C-sym, hence \(⟦\sim(A\circ B)⟧\subseteq ⟦\sim(B\circ A)⟧\) by the Kripke clause for \(\sim\).
-
1.3 \(A\to\sim\sim A\): \(X\subseteq \mathrm{iNeg}_\le(\mathrm{iNeg}_\le(X))\) in any Kripke structure; combine with Id.
-
1.4 \((A\to B)\to(A\circ B)\): immediate from C-coh.
-
1.5 \( (A\ne B\ne C)\to(((A\to B)\wedge(B\to C))\to(A\to C))\): at a world \(w\), the antecedent \(A\ne B\ne C\) says \(X\not\equiv_w Y\), \(Y\not\equiv_w Z\), \(X\not\equiv_w Z\). If also \(f_w(X)\subseteq Y\) and \(f_w(Y)\subseteq Z\), Tr≠ yields \(f_w(X)\subseteq Z\).
-
1.6 \((A\wedge B)=(B\wedge A)\): \(⟦ A\wedge B⟧=⟦ B\wedge A⟧\) set-theoretically, so each direction of \(=\) is an instance of 1.1.
-
1.7 \(((A\wedge B)\to C)\to((A\wedge\sim C)\to\sim B)\): write \(X=⟦ A⟧\), \(Y=⟦ B⟧\), \(Z=⟦ C⟧\). From \(f_w(X\cap Y)\subseteq Z\), Contra gives \(f_w(X\cap \mathrm{iNeg}_\le(Z))\subseteq \mathrm{iNeg}_\le(Y)\), i.e. the consequent.
-
R1 (modus ponens): if \(w\in X\) and \(f_w(X)\subseteq Y\), then by Succ \(w\in f_w(X)\subseteq Y\), so \(w\models B\).
-
R2 (adjunction): by the clause for \(\wedge\).
Nonclassicality. Using a 2-world chain \(w<v\) with \(V(p)={v}\), any selection of the form \(f_w(X)\subseteq X\cap\uparrow w\) and any symmetric, coherent \(C\) validates the axioms and rules while refuting \(\sim\sim p\to p\) at \(w\). Thus the negation is genuinely intuitionistic.
4. Canonical semantics and completeness
The completeness proof in the Lean development proceeds via canonical worlds built from the Hilbert interface NL.ProofSystem.NLProofSystem (with rules mp, adj and axioms 1.1–1.7).
Canonical worlds and accessibility
A world is a set \(\Gamma\) of formulas that is:
- closed under theorems and under
mp, adj (closure notion Closed), and
- (schematically) consistent (
Consistent in Lindenbaum.lean).
Write \(\mathrm{World}(\Gamma)\) for this property. Canonical worlds are packaged as
\[
\mathbf{W}_{\mathrm{can}}=\{\Gamma : \mathrm{World}(\Gamma)\},
\]
with canonical preorder \(\Gamma\le_C\Delta\) iff \(\Gamma\subseteq\Delta\).
Canonical detachment family
For a world \(\Gamma\) and formula \(A\), set
\[
F_\Gamma(A)\ :=\ \{\Delta\ \big|\ \mathrm{World}(\Delta),\ \Gamma\subseteq\Delta,\ \text{and}\ \forall B,\ (A\to B)\in\Gamma\ \Rightarrow\ B\in\Delta\}.
\]
In Canonical.lean we use \(F_\Gamma(A)\) to define the selection:
\[
F^{\mathrm{can}}(\Gamma,A)\ :=\ \{\Delta\in\mathbf{W}_{\mathrm{can}} : \Delta\in F_\Gamma(A)\}.
\]
The Lindenbaum apparatus (Lindenbaum.lean) provides the standard intuitionistic extension lemmas needed for negation and implication:
-
extend_to_world: extend a closed consistent base to a world.
-
neg_density: if \(\neg A\notin\Gamma\), there exists \(\Delta\supseteq\Gamma\) with \(A\in\Delta\).
-
neg_blocks: if \(\neg A\in\Gamma\subseteq\Delta\), then \(A\notin\Delta\).
-
F_nonempty: \(F_\Gamma(A)\) is nonempty.
-
detachment_witness: if \((A\to B)\notin\Gamma\), some \(\Delta\in F_\Gamma(A)\) omits \(B\).
Canonical truth and validity
Define canonical truth sets by recursion on \(A\):
\[
\begin{aligned}
⟦ p⟧_{\mathrm{can}} &:= {\Gamma: p\in\Gamma},\\
⟦ A\wedge B⟧_{\mathrm{can}} &:= {\Gamma:(A\wedge B)\in\Gamma},\\
⟦ \sim A⟧_{\mathrm{can}} &:= {\Gamma:\ \forall\Delta\ (\Gamma\subseteq\Delta\Rightarrow \Delta\notin ⟦ A⟧_{\mathrm{can}})},\\
⟦ A\to B⟧_{\mathrm{can}} &:= {\Gamma:\ F^{\mathrm{can}}(\Gamma,A)\subseteq ⟦ B⟧_{\mathrm{can}}},\\
⟦ A\circ B⟧_{\mathrm{can}} &:= {\Gamma:(A\circ B)\in\Gamma}.
\end{aligned}
\]
Write \(\Gamma\models_{\mathrm{can}} A\) for \(\Gamma\in⟦ A⟧_{\mathrm{can}}\), and say \(A\) is canonically valid if \(\Gamma\models_{\mathrm{can}} A\) for all canonical worlds \(\Gamma\).
Truth Lemma (canonical)
For every \(A\) and canonical world \(\Gamma\),
\[
\Gamma\models_{\mathrm{can}} A\quad\Longleftrightarrow\quad A\in\Gamma.
\]
Proof sketch. Induction on \(A\). Atoms, \(\wedge\), and \(\circ\) are by definition.
For \(A\to B\):
- If \((A\to B)\in\Gamma\), then by the definition of \(F_\Gamma(A)\), every \(\Delta\in F^{\mathrm{can}}(\Gamma,A)\) contains \(B\); by IH, \(\Delta\models_{\mathrm{can}} B\).
- Conversely, if \(F^{\mathrm{can}}(\Gamma,A)\subseteq ⟦ B⟧_{\mathrm{can}}\) but \((A\to B)\notin\Gamma\),
detachment_witness yields \(\Delta\in F^{\mathrm{can}}(\Gamma,A)\) with \(B\notin\Delta\), contradicting the subset condition.
For \(\sim A\):
- If \(\Gamma\models_{\mathrm{can}}\sim A\) and \(\sim A\notin\Gamma\),
neg_density gives \(\Delta\supseteq\Gamma\) with \(A\in\Delta\); by IH, \(\Delta\models_{\mathrm{can}}A\), contradicting the negation clause.
- If \(\sim A\in\Gamma\) and \(\Gamma\subseteq\Delta\), then
neg_blocks ensures \(A\notin\Delta\); by IH, \(\Delta\not\models_{\mathrm{can}}A\).
Completeness
Let Provable be the Hilbert notion from ProofSystem.lean. If \(A\) is canonically valid, then \(A\) is provable:
\[
\forall\Gamma,\ \Gamma\models_{\mathrm{can}}A\quad\Longrightarrow\quad \mathrm{Provable}(A).
\]
Proof. Suppose \(A\) is not provable. Extend the set of all theorems with \(\neg A\) to a world \(\Delta\) using extend_with_neg. By the Truth Lemma, \(\Delta\models_{\mathrm{can}}\neg A\), hence \(\Delta\not\models_{\mathrm{can}}A\), contradicting canonical validity.
From canonical to frame completeness. The canonical structure above is built to validate all NL axioms and rules and to satisfy the Truth Lemma; it serves as the usual Lindenbaum–Kripke model. Since the frame conditions used in §1 are precisely the ones enforced in the canonical construction (via the closure/extension lemmas and the way \(F_\Gamma(A)\) is used), validity over all NL-frames entails canonical validity, hence provability. Thus NL is strongly complete for the class of NL-frames of §1.
5. One concrete instance
As a concrete (and very simple) instance, put \(f_w(X)=X\cap\uparrow w\) (which satisfies Id, Her, Succ, f-up, and Contra) and let \(C_w\) be any symmetric, upward-persistent predicate with C-coh (e.g. the always-true relation). This validates 1.1–1.7 and R1–R2, but \(\sim\sim p\to p\) fails in general (take a 2-node chain \(w<v\) with \(V(p)={v}\)).
6. What differs from the earlier (informal) sketch
-
Selections are anchored:
f_up ensures \(f_w(X)\subseteq \uparrow w\).
-
\(\circ\) is persistent:
C_her builds upward monotonicity into the semantics of consistency.
-
Axiom 1.5 is matched exactly: we enforce the guarded syllogism
Tr≠ (not the unconditional one).
- The canonical route to completeness uses the Kripke negation lemmas (
neg_density, neg_blocks) and the detachment family \(F_\Gamma(A)\) to handle \(\to\) exactly as encoded in the Lean files.
This presentation is the human-readable counterpart of the Lean development and can be read independently of the code, while lining up one-for-one with the definitions and lemmas actually used.
