From a93c4e55fe45155adbb16cb68022b91e78856fdb Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Mon, 12 Oct 2026 15:21:32 +0000 Subject: [PATCH 1/3] Kripke semantics: indexed modalities, frame correspondences, the non-factive model Kripke/Indexed: Base/Access field for field with E indexed by worlds (the originals are the one-world case). Kripke/Frame: Box as an indexed modality; reflexive <=> factive and transitive <=> positively introspective, both directions, constructively; Euclidean => 5, serial => D. Kripke/Belief: a two-world non-reflexive frame where a Warrant exists for a false proposition and no soundness field can, witnessing Warrant /= SoundWarrant. Expected rejection: factivity on the belief frame. Builtins only; repo flags incl. -W error. --- README.adoc | 5 ++ docs/kripke-status-2026-10-12.adoc | 34 ++++++++++ src/EpistemicTypes/All.agda | 5 ++ src/EpistemicTypes/Kripke/Belief.agda | 49 +++++++++++++++ src/EpistemicTypes/Kripke/Dependence.agda | 77 +++++++++++++++++++++++ src/EpistemicTypes/Kripke/Frame.agda | 62 ++++++++++++++++++ src/EpistemicTypes/Kripke/Indexed.agda | 49 +++++++++++++++ src/EpistemicTypes/Kripke/Residual.agda | 61 ++++++++++++++++++ tests/reject/BeliefIsKnowledge.agda | 11 ++++ 9 files changed, 353 insertions(+) create mode 100644 docs/kripke-status-2026-10-12.adoc create mode 100644 src/EpistemicTypes/Kripke/Belief.agda create mode 100644 src/EpistemicTypes/Kripke/Dependence.agda create mode 100644 src/EpistemicTypes/Kripke/Frame.agda create mode 100644 src/EpistemicTypes/Kripke/Indexed.agda create mode 100644 src/EpistemicTypes/Kripke/Residual.agda create mode 100644 tests/reject/BeliefIsKnowledge.agda diff --git a/README.adoc b/README.adoc index 96df244..21bae54 100644 --- a/README.adoc +++ b/README.adoc @@ -188,6 +188,11 @@ 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[]. The items below are updated accordingly: Kripke semantics is no longer unformalised; global warrant soundness is discharged for type-determined warrants (externally, choreographic-types) and remains an assumption for data-dependent ones. +==== + [CAUTION] ==== This is a prototype, not a complete epistemic logic. The following are **intentionally omitted** as future commitments, not hidden assumptions: diff --git a/docs/kripke-status-2026-10-12.adoc b/docs/kripke-status-2026-10-12.adoc new file mode 100644 index 0000000..bc5e6ba --- /dev/null +++ b/docs/kripke-status-2026-10-12.adoc @@ -0,0 +1,34 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += Kripke semantics and warrant soundness — status 2026-10-12 + +README lists *complete epistemic logic / Kripke semantics* and *global +soundness of warrants* as intentionally unformalised. The three modules +under `src/EpistemicTypes/Kripke/` change that status as follows. + +[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 discharged externally in choreographic-types (`Choreographic.Kripke`, which imports this repo's `Warrant` at 495db9c) | PROVEN there; 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) +|=== diff --git a/src/EpistemicTypes/All.agda b/src/EpistemicTypes/All.agda index 021ff97..11812c5 100644 --- a/src/EpistemicTypes/All.agda +++ b/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), diff --git a/src/EpistemicTypes/Kripke/Belief.agda b/src/EpistemicTypes/Kripke/Belief.agda new file mode 100644 index 0000000..8c256e3 --- /dev/null +++ b/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₀ +... | () diff --git a/src/EpistemicTypes/Kripke/Dependence.agda b/src/EpistemicTypes/Kripke/Dependence.agda new file mode 100644 index 0000000..3ced10e --- /dev/null +++ b/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 diff --git a/src/EpistemicTypes/Kripke/Frame.agda b/src/EpistemicTypes/Kripke/Frame.agda new file mode 100644 index 0000000..c407d5b --- /dev/null +++ b/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) diff --git a/src/EpistemicTypes/Kripke/Indexed.agda b/src/EpistemicTypes/Kripke/Indexed.agda new file mode 100644 index 0000000..ec9d6be --- /dev/null +++ b/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 + } diff --git a/src/EpistemicTypes/Kripke/Residual.agda b/src/EpistemicTypes/Kripke/Residual.agda new file mode 100644 index 0000000..22596ca --- /dev/null +++ b/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) diff --git a/tests/reject/BeliefIsKnowledge.agda b/tests/reject/BeliefIsKnowledge.agda new file mode 100644 index 0000000..43d5e17 --- /dev/null +++ b/tests/reject/BeliefIsKnowledge.agda @@ -0,0 +1,11 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +module BeliefIsKnowledge where +open import Agda.Builtin.Unit using (⊤; tt) +open import EpistemicTypes.Kripke.Frame +open import EpistemicTypes.Kripke.Belief + +-- Must fail: the belief frame is not reflexive, so no factivity. +invalid : Reflexive F +invalid _ w₀ = w₀∼w₁ From ada15b45f75ca13c4c446a5cd64f1f898ac6b3a0 Mon Sep 17 00:00:00 2001 From: "coderabbitai[bot]" <136622811+coderabbitai[bot]@users.noreply.github.com> Date: Mon, 12 Oct 2026 20:13:27 +0000 Subject: [PATCH 2/3] docs(docs): clarify formalised Kripke semantics and pending external warrant soundness verification --- README.adoc | 8 ++++---- docs/kripke-status-2026-10-12.adoc | 9 +++++---- 2 files changed, 9 insertions(+), 8 deletions(-) diff --git a/README.adoc b/README.adoc index 21bae54..1747c84 100644 --- a/README.adoc +++ b/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 @@ -190,7 +190,7 @@ interface is a breaking correction documented in link:docs/proof-transport.adoc[ [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[]. The items below are updated accordingly: Kripke semantics is no longer unformalised; global warrant soundness is discharged for type-determined warrants (externally, choreographic-types) and remains an assumption for data-dependent ones. +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] @@ -198,10 +198,10 @@ interface is a breaking correction documented in link:docs/proof-transport.adoc[ 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 diff --git a/docs/kripke-status-2026-10-12.adoc b/docs/kripke-status-2026-10-12.adoc index bc5e6ba..56612fb 100644 --- a/docs/kripke-status-2026-10-12.adoc +++ b/docs/kripke-status-2026-10-12.adoc @@ -1,9 +1,10 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 = Kripke semantics and warrant soundness — status 2026-10-12 -README lists *complete epistemic logic / Kripke semantics* and *global -soundness of warrants* as intentionally unformalised. The three modules -under `src/EpistemicTypes/Kripke/` change that status as follows. +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"] |=== @@ -13,7 +14,7 @@ under `src/EpistemicTypes/Kripke/` change that status as follows. | 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 discharged externally in choreographic-types (`Choreographic.Kripke`, which imports this repo's `Warrant` at 495db9c) | PROVEN there; recorded here +| 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 From c14f0385788d027e7a6ba7c69256efe215714690 Mon Sep 17 00:00:00 2001 From: "coderabbitai[bot]" <136622811+coderabbitai[bot]@users.noreply.github.com> Date: Mon, 12 Oct 2026 20:14:11 +0000 Subject: [PATCH 3/3] fix(tests): include BeliefIsKnowledge in the rejection gate and check its expected diagnostic --- tests/check-rejections.sh | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/tests/check-rejections.sh b/tests/check-rejections.sh index fa77907..a7b2bbd 100644 --- a/tests/check-rejections.sh +++ b/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