kripke-2026-10-12

README.adoc

@@ -15,7 +15,7 @@ When an agent observes a fact, the type of their access matters. Knowledge is fa
 
 Epistemic types provide a mechanised vocabulary for these distinctions. Given a type of standpoints `K` (agents, observers, evidence states), the modality `E : K → Set ℓ → Set ℓ` reads: `E κ A` is the type of `A` as epistemically available from standpoint `κ`.
 
-This repo does not define a complete epistemic logic or Kripke semantics. It provides the minimal interfaces — factive vs. non-factive modalities, warrants, accessibility preorder, and compositional proof transport — and proves the structural laws that hold generically, while making explicit what must be assumed.
+This repo does not define a complete epistemic logic. It provides Kripke semantics and the minimal interfaces — factive vs. non-factive modalities, warrants, accessibility preorder, and compositional proof transport — and proves the structural laws that hold generically, while making explicit what must be assumed.
 
 == The modality spectrum
 
@@ -188,15 +188,20 @@ interface is a breaking correction documented in link:docs/proof-transport.adoc[
 
 == What remains intentionally unformalized
 
+[NOTE]
+====
+2026-10-12: Kripke semantics, the frame-condition correspondences, a non-factive model (`Warrant ≠ SoundWarrant` witnessed), the residual-evidence frame and the dependence test now live under `src/EpistemicTypes/Kripke/`; see link:docs/kripke-status-2026-10-12.adoc[]. Global warrant soundness for type-determined warrants is reported externally in choreographic-types but remains open pending an immutable external revision containing the theorem and its import and a successful type-check (E-6). Soundness for data-dependent warrants remains an assumption.
+====
+
 [CAUTION]
 ====
 This is a prototype, not a complete epistemic logic. The following are **intentionally omitted** as future commitments, not hidden assumptions:
 ====
 
-* Complete epistemic logic or Kripke semantics
+* Complete epistemic logic
 * Graded comonad for echo-type composition
 * Proof irrelevance or decidability
-* Global soundness of warrants
+* Soundness for data-dependent warrants
 * Monadic (`bind`) or comonadic (`extract`) structure for `E`
 * A rational (ℚ) instance of the applications layer, and the rescaling
   transport that would lift the integer certificate to rational input

docs/kripke-status-2026-10-12.adoc

@@ -0,0 +1,35 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+= Kripke semantics and warrant soundness — status 2026-10-12
+
+The modules under `src/EpistemicTypes/Kripke/` formalise Kripke semantics
+and the results below. Complete epistemic logic and soundness for
+data-dependent warrants remain outstanding; E-6 records the open external
+verification for type-determined warrants.
+
+[cols="1,3,1",options="header"]
+|===
+| ID | Claim | Status
+| E-1 | `Modality` cannot express Kripke knowledge: its carrier has no world index. `IndexedModality`/`IndexedFactive`/`IndexedAccessible` are `Base`/`Access` field for field with `E : K → (W → Set) → (W → Set)`; the originals are the `W = ⊤` case (`toModality`) | PROVEN (`Kripke/Indexed.agda`)
+| E-2 | Frames and `Box`; `Box` is an `IndexedModality` | PROVEN (`Kripke/Frame.agda`)
+| E-3 | Correspondences, constructively: reflexive ⇔ factive (T, both directions); transitive ⇔ positively introspective (4, both directions); Euclidean ⇒ 5; serial ⇒ D. The converses of 5 and D need classical reasoning and are not claimed | PROVEN / OPEN as stated
+| E-4 | A reflexive frame yields an `IndexedFactive` (`factive`) | PROVEN
+| E-5 | *The non-factive model*: two worlds, access only w₀ → w₁; at w₀ there is a `Warrant` (evidence: a `Box` proof) for a false proposition, and no `sound` field can exist for it. `Warrant ≠ SoundWarrant`, witnessed | PROVEN (`Kripke/Belief.agda`: `believed`, `false-at-w₀`, `no-sound-warrant`); TESTED (`tests/reject/BeliefIsKnowledge`: factivity refused on this frame)
+| E-6 | Global soundness of warrants in a reflexive frame — every type-determined warrant sound — is reported externally in choreographic-types (`Choreographic.Kripke`, citing this repo's `Warrant` at `495db9c`) | OPEN (an immutable external revision containing the theorem and its import, and a successful type-check, are not recorded here)
+|===
+
+Separation (family bar, criterion 2): the belief model is a modality with
+evidence and no extraction, which no grade algebra and no secret label can
+express; the factive/non-factive split is the family's own.
+
+Builtins only; checked with the repo's own flags (`--safe --without-K
+--double-check -W error`).
+
+== Residual-evidence, read in the frame (`Kripke/Residual.agda`)
+
+[cols="1,3,1",options="header"]
+|===
+| ID | Claim | Status
+| E-7 | residual-evidence-types' `Holds c P` is `Box` over the accessibility "is a candidate" (same reading, satisfies the evidence): the Echo fibre cut down by evidence. Its four verdicts are the joint cases of `Box P`, `Box (¬ P)` | PROVEN by definition (`residualFrame`, `Holds`)
+| E-8 | "Presence without identification" is de dicto without de re: `Box (∃ x. Is x)` with no `Box (Is x)`; witnessed on a three-world model | PROVEN (`presence`, `no-identification`)
+| E-9 | DECISION-002 test 1 (dependence is not a function of the candidate set), run in a faithful mirror of residual-evidence's `Dependent`: contexts `[P]` and `[P, P]` have the same candidates pointwise, yet a claim can rest on a *proper* sub-context in the second and not the first. A box sees worlds; dependence sees assumptions | PROVEN in the mirror (`Kripke/Dependence.agda`); re-proof against residual-evidence's own record OPEN (same kernel, same shape)
+|===

src/EpistemicTypes/All.agda

@@ -5,6 +5,11 @@ module EpistemicTypes.All where
 open import EpistemicTypes.Base public
 open import EpistemicTypes.Warrant public
 open import EpistemicTypes.Access public
+import EpistemicTypes.Kripke.Indexed
+import EpistemicTypes.Kripke.Frame
+import EpistemicTypes.Kripke.Belief
+import EpistemicTypes.Kripke.Residual
+import EpistemicTypes.Kripke.Dependence
 open import EpistemicTypes.EchoBridge public
 -- Imported (checked) but NOT re-exported publicly: ReadConsistency keeps
 -- its own self-contained ⊥/¬_ (matching the Examples.agda convention),

src/EpistemicTypes/Kripke/Belief.agda

@@ -0,0 +1,49 @@
+{-# OPTIONS --safe --without-K #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+--
+-- The non-factive model.  Two worlds, one standpoint, access only from w₀
+-- to w₁.  At w₀ the standpoint has a warrant (a Box proof) for "we are at
+-- w₁", and it is false.  So Warrant and SoundWarrant genuinely differ:
+-- there is no soundness field for this evidence, provably.
+module EpistemicTypes.Kripke.Belief where
+
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import Agda.Builtin.Sigma using (Σ; _,_)
+open import Agda.Builtin.Unit using (⊤; tt)
+open import EpistemicTypes.Warrant
+open import EpistemicTypes.Kripke.Frame
+
+data W : Set where
+  w₀ w₁ : W
+
+data _∼_ : W → W → Set where
+  w₀∼w₁ : w₀ ∼ w₁
+
+F : Frame ⊤ W
+F = record { _∼[_]_ = λ w _ w' → w ∼ w' }
+
+AtW₁ : W → Set
+AtW₁ w₀ = ⊥
+AtW₁ w₁ = ⊤
+
+-- Warranted at w₀ ...
+believed : Box F tt AtW₁ w₀
+believed w₁ w₀∼w₁ = tt
+
+-- ... and false at w₀.
+false-at-w₀ : ¬ AtW₁ w₀
+false-at-w₀ ()
+
+-- epistemic-types' Warrant with this evidence exists; a SoundWarrant with
+-- this evidence cannot.
+warrant : Warrant ⊤ tt (AtW₁ w₀)
+warrant = mkWarrant (Box F tt AtW₁ w₀)
+
+no-sound-warrant : ¬ (Warrant.Evidence warrant → AtW₁ w₀)
+no-sound-warrant sound = false-at-w₀ (sound believed)
+
+-- The frame is not reflexive — which is the whole explanation.
+not-reflexive : ¬ Reflexive F
+not-reflexive r with r tt w₀
+... | ()

src/EpistemicTypes/Kripke/Dependence.agda

@@ -0,0 +1,77 @@
+{-# OPTIONS --safe --without-K #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+--
+-- DECISION-002 test 1, run in a faithful mirror of residual-evidence-types'
+-- Dependent (support ⊆ Γ, claim over the thinned context): dependence is
+-- NOT a function of the candidate set.  Two contexts with the same worlds
+-- differ in what a claim can be made to rest on — the duplicated
+-- assumption can be dropped in one and not the other.  A box sees worlds;
+-- dependence sees assumptions.  That is structure the frame forgets, and
+-- the family half of the test passes here; it remains to re-prove it
+-- against residual-evidence's own record (same kernel, same shape).
+module EpistemicTypes.Kripke.Dependence where
+
+open import Agda.Builtin.Sigma using (Σ; _,_)
+open import Agda.Builtin.Unit using (⊤; tt)
+open import EpistemicTypes.Kripke.Frame using (⊥)
+
+infixr 5 _∷_
+data Ctx (W : Set) : Set₁ where
+  []  : Ctx W
+  _∷_ : (W → Set) → Ctx W → Ctx W
+
+⟦_⟧ : ∀ {W} → Ctx W → W → Set
+⟦ [] ⟧    w = ⊤
+⟦ P ∷ Γ ⟧ w = Σ (P w) (λ _ → ⟦ Γ ⟧ w)
+
+infix 4 _⊆_
+data _⊆_ {W : Set} : Ctx W → Ctx W → Set₁ where
+  done : [] ⊆ []
+  keep : ∀ {P Γ Δ} → Γ ⊆ Δ → (P ∷ Γ) ⊆ (P ∷ Δ)
+  drop : ∀ {P Γ Δ} → Γ ⊆ Δ → Γ ⊆ (P ∷ Δ)
+
+-- A claim under Γ: P at every world satisfying Γ (the candidates).
+HoldsUnder : ∀ {W} → Ctx W → (W → Set) → Set
+HoldsUnder Γ P = ∀ w → ⟦ Γ ⟧ w → P w
+
+record Dependent {W : Set} (Γ : Ctx W) (P : W → Set) : Set₁ where
+  constructor rests-on
+  field
+    support : Ctx W
+    thin    : support ⊆ Γ
+    claim   : HoldsUnder support P
+
+-- A support is proper when it drops at least one assumption of Γ.
+Proper : ∀ {W} {Γ Δ : Ctx W} → Δ ⊆ Γ → Set
+Proper done     = ⊥
+Proper (keep t) = Proper t
+Proper (drop t) = ⊤
+
+ProperlyDependent : ∀ {W} → Ctx W → (W → Set) → Set₁
+ProperlyDependent Γ P = Σ (Dependent Γ P) (λ d → Proper (Dependent.thin d))
+
+----------------------------------------------------------------------
+-- The witness.
+data W : Set where u v : W
+
+P : W → Set
+P u = ⊤
+P v = ⊥
+
+Γ₁ Γ₂ : Ctx W
+Γ₁ = P ∷ []
+Γ₂ = P ∷ P ∷ []
+
+-- Same candidates, pointwise.
+same-candidates : ∀ w → Σ (⟦ Γ₁ ⟧ w → ⟦ Γ₂ ⟧ w) (λ _ → ⟦ Γ₂ ⟧ w → ⟦ Γ₁ ⟧ w)
+same-candidates w = (λ { (p , tt) → p , p , tt }) , (λ { (p , _ , tt) → p , tt })
+
+-- Under Γ₂ the claim can rest on strictly less than Γ₂ ...
+properly-in-Γ₂ : ProperlyDependent Γ₂ P
+properly-in-Γ₂ = rests-on (P ∷ []) (drop (keep done)) (λ { w (p , tt) → p }) , tt
+
+-- ... under Γ₁ it cannot: the only proper support is empty, and P fails at v.
+not-properly-in-Γ₁ : ProperlyDependent Γ₁ P → ⊥
+not-properly-in-Γ₁ (rests-on _ (keep done) _     , ())
+not-properly-in-Γ₁ (rests-on _ (drop done) claim , _) = claim v tt

src/EpistemicTypes/Kripke/Frame.agda

@@ -0,0 +1,62 @@
+{-# OPTIONS --safe --without-K #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+--
+-- Kripke frames, the box modality, and the frame-condition correspondences
+-- the README lists as unformalised.  Constructive throughout; where a
+-- converse needs classical reasoning (5, D) it is not claimed.
+module EpistemicTypes.Kripke.Frame where
+
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import Agda.Builtin.Sigma using (Σ; _,_)
+open import EpistemicTypes.Kripke.Indexed
+
+data ⊥ : Set where
+¬_ : Set → Set
+¬ A = A → ⊥
+
+record Frame (K W : Set) : Set₁ where
+  field
+    _∼[_]_ : W → K → W → Set        -- w ∼[ κ ] w' : κ cannot tell w from w'
+
+module _ {K W : Set} (F : Frame K W) where
+  open Frame F
+
+  -- Box: true at every world the standpoint cannot distinguish.
+  Box : K → (W → Set) → W → Set
+  Box κ φ w = ∀ w' → w ∼[ κ ] w' → φ w'
+
+  box : IndexedModality K W
+  box = record { E = Box ; map = λ f w b w' r → f w' (b w' r) }
+
+  ----------------------------------------------------------------------
+  -- Frame conditions
+  Reflexive  = ∀ κ w → w ∼[ κ ] w
+  Transitive = ∀ κ {w w' w''} → w ∼[ κ ] w' → w' ∼[ κ ] w'' → w ∼[ κ ] w''
+  Euclidean  = ∀ κ {w w' w''} → w ∼[ κ ] w' → w ∼[ κ ] w'' → w' ∼[ κ ] w''
+  Serial     = ∀ κ w → Σ W (λ w' → w ∼[ κ ] w')
+
+  -- T: reflexive frames are exactly the factive ones (both directions).
+  T : Reflexive → ∀ κ φ w → Box κ φ w → φ w
+  T r κ φ w b = b w (r κ w)
+
+  T⁻¹ : (∀ κ φ w → Box κ φ w → φ w) → Reflexive
+  T⁻¹ t κ w = t κ (λ w' → w ∼[ κ ] w') w (λ w' r → r)
+
+  factive : Reflexive → IndexedFactive K W
+  factive r = record { modality = box ; reflect = λ {κ} {φ} w b → T r κ φ w b }
+
+  -- 4: transitive frames are exactly the positively introspective ones.
+  Four : Transitive → ∀ κ φ w → Box κ φ w → Box κ (Box κ φ) w
+  Four t κ φ w b w' r w'' r' = b w'' (t κ r r')
+
+  Four⁻¹ : (∀ κ φ w → Box κ φ w → Box κ (Box κ φ) w) → Transitive
+  Four⁻¹ f κ {w} {w'} {w''} r r' = f κ (λ v → w ∼[ κ ] v) w (λ v s → s) w' r w'' r'
+
+  -- 5 and D, one direction (the converses are classical).
+  Five : Euclidean → ∀ κ φ w → ¬ Box κ φ w → Box κ (λ w' → ¬ Box κ φ w') w
+  Five e κ φ w nb w' r b' = nb (λ w'' r' → b' w'' (e κ r r'))
+
+  D : Serial → ∀ κ φ w → Box κ φ w → ¬ Box κ (λ w' → ¬ φ w') w
+  D s κ φ w b nb with s κ w
+  ... | w' , r = nb w' r (b w' r)

src/EpistemicTypes/Kripke/Indexed.agda

@@ -0,0 +1,49 @@
+{-# OPTIONS --safe --without-K #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+--
+-- World-indexed modalities.  Base.Modality carries E : K -> Set -> Set,
+-- which cannot express Kripke knowledge (truth at every accessible world
+-- is a statement about world-indexed propositions; over a single implicit
+-- world it collapses to the proposition itself).  The records below are
+-- Base/Access field for field, with E indexed by a world type W.  The
+-- originals are the W = ⊤ special case (toModality).
+module EpistemicTypes.Kripke.Indexed where
+
+open import Agda.Primitive using (lzero)
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import Agda.Builtin.Unit using (⊤; tt)
+open import EpistemicTypes.Base using (Modality)
+open import EpistemicTypes.Access using (Preorder)
+
+record IndexedModality (K W : Set) : Set₁ where
+  field
+    E   : K → (W → Set) → (W → Set)
+    map : ∀ {κ A B} → (∀ w → A w → B w) → ∀ w → E κ A w → E κ B w
+
+-- Factive: extraction at the world itself.  Belief-like modalities omit it.
+record IndexedFactive (K W : Set) : Set₁ where
+  field
+    modality : IndexedModality K W
+  open IndexedModality modality public
+  field
+    reflect : ∀ {κ A} w → E κ A w → A w
+
+record IndexedAccessible (K W : Set) : Set₁ where
+  field
+    modality : IndexedModality K W
+    access   : Preorder K
+  open IndexedModality modality public
+  open Preorder access public
+  field
+    increase       : ∀ {κ κ' A} → κ ≤κ κ' → ∀ w → E κ A w → E κ' A w
+    increase-refl  : ∀ {κ A} w (x : E κ A w) → increase refl≤ w x ≡ x
+    increase-trans : ∀ {κ₀ κ₁ κ₂ A} (p : κ₀ ≤κ κ₁) (q : κ₁ ≤κ κ₂) w (x : E κ₀ A w)
+                   → increase q w (increase p w x) ≡ increase (trans≤ p q) w x
+
+-- The unindexed record is the one-world case.
+toModality : ∀ {K} → IndexedModality K ⊤ → Modality K lzero
+toModality M = record
+  { E   = λ κ A → IndexedModality.E M κ (λ _ → A) tt
+  ; map = λ f → IndexedModality.map M (λ _ → f) tt
+  }

src/EpistemicTypes/Kripke/Residual.agda

@@ -0,0 +1,61 @@
+{-# OPTIONS --safe --without-K #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+--
+-- residual-evidence-types' Holds, read as a Kripke box.
+--
+-- There, a Case is an observation `observe : W → O`, a reading `r`, and
+-- evidence `E : W → Set`; a Candidate is a world with that reading that
+-- satisfies the evidence; `Holds c P` says P at every candidate.  That is
+-- Box over the accessibility "w' is a candidate" — the Echo fibre over the
+-- reading, cut down by the evidence.  So the four verdicts (entailed,
+-- refuted, unresolved, inconsistent) are the four joint cases of
+-- Box P and Box (¬ P), and "presence without identification" is de dicto
+-- without de re: Box (∃ a. P a) with no Box (P a).  Witnessed below.
+module EpistemicTypes.Kripke.Residual where
+
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import Agda.Builtin.Sigma using (Σ; _,_)
+open import Agda.Builtin.Unit using (⊤; tt)
+open import EpistemicTypes.Kripke.Frame
+
+-- The residual frame: one standpoint; w' accessible iff it is a candidate.
+residualFrame : {W O : Set} (observe : W → O) (r : O) (E : W → Set) → Frame ⊤ W
+residualFrame observe r E = record { _∼[_]_ = λ _ _ w' → Σ (observe w' ≡ r) (λ _ → E w') }
+
+-- Holds c P, by definition, is Box at any world (the base world is inert).
+Holds : {W O : Set} (observe : W → O) (r : O) (E : W → Set) → (W → Set) → W → Set
+Holds observe r E = Box (residualFrame observe r E) tt
+
+----------------------------------------------------------------------
+-- Presence without identification.  Three worlds; the observation cannot
+-- tell a from b; the evidence excludes c.  Something is present (de dicto),
+-- but no particular thing is (de re).
+data W : Set where a b c : W
+data O : Set where seen unseen : O
+
+observe : W → O
+observe a = seen
+observe b = seen
+observe c = unseen
+
+E : W → Set
+E _ = ⊤
+
+-- "Thing x is here": true only at world x.
+Is : W → W → Set
+Is a a = ⊤
+Is b b = ⊤
+Is _ _ = ⊥
+
+Present : W → Set
+Present w = Σ W (λ x → Is x w)
+
+presence : ∀ w → Holds observe seen E Present w
+presence _ a (refl , _) = a , tt
+presence _ b (refl , _) = b , tt
+
+no-identification : ∀ x w → ¬ Holds observe seen E (Is x) w
+no-identification a w h = h b (refl , tt)
+no-identification b w h = h a (refl , tt)
+no-identification c w h = h a (refl , tt)

tests/check-rejections.sh

@@ -6,7 +6,7 @@ cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.."
 # unrelated parse failures must fail this gate rather than count as rejection.
 fixtures=(LyingVerifier ForgedAcceptance ReplayedArtifact ReplayedHolder \
   StaleSample FakeFreshness ForkedHistory ForgedResidue MismatchedSource \
-  UnderstatedBound InventedMigration UncheckedSkip)
+  UnderstatedBound InventedMigration UncheckedSkip BeliefIsKnowledge)
 expected_files=$(printf 'tests/reject/%s.agda\n' "${fixtures[@]}" | sort)
 actual_files=$(rg --files tests/reject -g '*.agda' | sort)
 [[ "$actual_files" == "$expected_files" ]] || { echo 'FAIL: rejection manifest differs from files'; exit 1; }
@@ -27,6 +27,7 @@ for fixture in "${fixtures[@]}"; do
     FakeFreshness) expected='initial .*false !=' ;;
     UnderstatedBound) expected='1 != 0' ;;
     InventedMigration) expected='true != .*false' ;;
+    BeliefIsKnowledge) expected='w₁ != .*w₀' ;;
   esac
   if [[ "$status" -ne 42 ]] || ! rg -q "$expected" <<< "$diagnostic" || \
       ! rg -q 'when checking' <<< "$diagnostic"; then