Epistemic Types — Standpoint-Indexed Modalities and Proof Transport

Constructive Agda prototype for standpoint-indexed epistemic modalities, separating knowledge, belief, and warrant, with proof transport sound relative to an explicit claim meaning.

Contents

• Overview
• The modality spectrum
• Warrants
• Accessibility and surreal standpoints
  • The surreal bridge
• Store-coherent reads and certified residues
• Applications: the RapidNJ Q-criterion
• Proof transport across trust boundaries
• What is standard and what is ours
• What remains intentionally unformalized
• Build
• Documentation
• License

Overview

When an agent observes a fact, the type of their access matters. Knowledge is factive; belief is not. A warrant records evidence without assuming soundness. Proof transported across a boundary becomes a receipt; a receiving proof requires a successful sound check of the receiver’s claim meaning.

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.

The modality spectrum

The base interface treats E as an indexed endofunctor. Stronger structure is added incrementally, each as a separate record:

Interface	Structure added	Intended reading
Modality	E, map	Plain indexed endofunctor
LawfulModality	Functor identity + composition laws	map respects structure
FactiveModality	reflect : E κ A → A	Knowledge (veridical: what is available is true)
BeliefModality	Intentionally no reflect	Belief (non-factive: available does not imply true)
ReturnModality	return : A → E κ A	Strong introduction (internal observation)

Monadic (bind) and comonadic (extract) structure are not provided by default. They are future commitments, not hidden assumptions.

Warrants

A warrant records the type of evidence for a claim without assuming the evidence is valid:

• Warrant κ A — the type of evidence tokens for A from standpoint κ.

• Epi κ A — an evidence token paired with its warrant type.

• SoundWarrant — a separate interface adding a soundness map (evidence → A). Not assumed by default.

This separates "I have a receipt for A" from "A is true."

Accessibility and surreal standpoints

Standpoint access is modelled by a preorder κ ≤κ κ' (read: κ' is at least as informed as κ). Transport increase moves epistemic availability along this order.

The surreal bridge

SurrealBridge enriches the preorder with an instance-supplied access grade. Its laws specify composition; they do not establish a physical cost or an information-loss measure:

magnitude-loss : x ≤♯ y → Grade
loss-refl      : magnitude-loss refl ≡ finite zero
loss-trans     : magnitude-loss (trans p q) ≡ gradePlus (magnitude-loss p) (magnitude-loss q)

Its concrete Echo adapter relaxes a proved upper bound on a residue measure along p : x ≤♯ y, while preserving the retained value:

E x (BoundedEcho C measure r visible)
  → E y (BoundedEcho C measure (gradePlus r (magnitude-loss p)) visible)

The concrete daySurrealAccess instance models the finite birthday tower using Nat standpoints, where the grade is the number of refinement steps. This is a set-sized fragment, not the full Conway proper class of surreals.

Store-coherent reads and certified residues

ReadConsistency now models finite store histories. A ReadView s proves its value equals contents s; a cached read records its source history and ancestry. Writes make existing caches stale. synchronize reads current contents in the model, while preserving evidence across a change requires an explicit proof. The former version-only relabelling and free Sync witness have been removed.

Echo C y carries a residue satisfying the relation specified by Retention C. Source compatibility is explicit in MatchesSource; exact recovery and migration need their respective round-trip and adequacy laws. A checked counterexample shows that discarded distinctions cannot support a migration requiring those distinctions. Resource grades are separate, measured upper bounds.

See the breaking API correction and proof boundaries. An optional integration gate proves correspondence with the actual sibling EchoResidue.EchoR; the core remains dependency-free.

Applications: the RapidNJ Q-criterion

The Applications/ tree is where the core interfaces are exercised against algorithmic claims that arrive with their own arithmetic. Its first example is the per-row branch-and-bound rule used by RapidNJ (Simonsen, Mailund, Pedersen 2008) when searching for the neighbour-joining minimum: while scanning a row of distances in increasing order, the row is abandoned as soon as

qBound = (r - 2) * d(i,next) - t(i) - t_max

is at least the incumbent q_min, because no unexamined entry can beat it.

The development is order-generic: Applications.QCriterion.qBound-≤-Q proves the bound for any carrier with monotone addition, antitone negation and a transitive order — no multiplication or division of carrier elements occurs anywhere, and the coefficient (r - 2) enters only as a Nat-indexed repeated sum. A skip certificate carries the sorted-row invariant, the running-maximum invariant and an accepted executable check; Applications.RapidNJSkip then generates a warrant for the skipped quadrant, and its soundness map is exactly the reflect of a FactiveModality:

run data -> skipWarrant -> skip-sound (the bound lemma) -> reflect -> the claim

So skipping a quadrant yields knowledge only through a proved bound, never by assumption, and the same run held without the soundness map is belief. The integer model is discharged in full (Applications.IntegerModel, Applications.RapidNJExamples); the rational case is a stated obligation, not a claim — see the applications note for the rescaling argument and the exact-arithmetic seam.

Proof transport across trust boundaries

ProofTransport is parameterised by agents, claim labels, artefacts, Meaning : Agent → Artifact → Claim → Set, and a certificate Payload : Artifact → Claim → Set. The caller states the meaning being proved.

A CertificateCheck contains an executable Boolean check and a proof that acceptance entails that exact meaning. Evidence carries a payload; possessing it alone proves nothing. A proof constructor also requires runChecker checker evidence ≡ true.

proofSound : View holder a Proof c -> Meaning holder a c

verify evaluates the checking function and returns InvalidEvidence on rejection. transmit produces a receipt at the receiving holder. publicIsPortable requires an explicit implication between the two holders' meanings; it does not silently relabel holder-dependent truths.

The example checks Boolean artefacts and certificates, proves legitimate acceptance, and refutes false claims. It does not claim that a physical action occurred. The older token-only model lacked semantic soundness; the strengthened interface is a breaking correction documented in docs/proof-transport.adoc.

What is standard and what is ours

Concept	Status	Home in this repo
Indexed endofunctor / modality	Standard	EpistemicTypes.Base
Knowledge (factivity) vs. Belief distinction	Standard (modal logic S5 vs. KD45)	EpistemicTypes.Base
Warrant types without assumed soundness	Project-specific emphasis	EpistemicTypes.Warrant
Preorder accessibility with transport	Standard	EpistemicTypes.Access
Resource-bound transport on surreal-like standpoints	Project-specific composition; no novelty theorem	EpistemicTypes.SurrealBridge
Proof transport with explicit semantic soundness	Novel formalisation	EpistemicTypes.ProofTransport
Order-generic RapidNJ Q-criterion bound and skip warrants	Transcription of a documented algorithm; no novelty theorem	EpistemicTypes.Applications.QCriterion

What remains intentionally unformalized

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

• Graded comonad for echo-type composition

• Proof irrelevance or decidability

• Global soundness of 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

• Cross-iteration reuse of a skip bound, and the row-insertion update that maintains the scan invariants (Applications.RapidNJSkip.WeakeningObligation)

• Confidentiality labels, secret types, declassification, and noninterference; see the information-flow proposal for the two-level baseline, non-claims, and repository boundary

Build

just check  # positive proofs and expected rejection controls

Or directly:

agda --no-libraries -i src src/EpistemicTypes/All.agda

Documentation

• EXPLAINME — claim-by-claim receipts and known gaps

• Continuity foundations — store coherence, retained information, bounds, and next obligations

• Proof transport — semantic verification across boundaries

• Applications: the RapidNJ Q-criterion — the bound, the skip warrant, the exact-arithmetic obligation

• Secret types — a proposed two-level information-flow model, its noninterference target, and the repository boundary; no API is implemented

License

SPDX-License-Identifier: MPL-2.0 — see LICENSE.