diff --git a/README.adoc b/README.adoc index 96df244..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 @@ -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 diff --git a/docs/kripke-status-2026-10-12.adoc b/docs/kripke-status-2026-10-12.adoc new file mode 100644 index 0000000..56612fb --- /dev/null +++ b/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) +|=== 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/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 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₁