Infrastructure

1{-# OPTIONS --safe --without-K #-}
2
3-- T-FAILURE: Non-Factivity of the Consistency Operator
4-- Proving that ∘ is a Doxastic (Belief) modality, not Alethic (Knowledge)
5--
6-- The key insight is that the REFLECTION AXIOM (Axiom T):
7--     □A → A    ("If A is necessary, then A is true")
8-- FAILS for the consistency operator ∘:
9--     ∘A → A    ("If A is consistent, then A is true")  -- NOT VALID
10--
11-- This failure creates the "Valley of Death" between:
12--   - What is CONSISTENT (permitted by ∘)
13--   - What is TRUE (designated in evaluation)
14
15module Core.TFailure where
16
17open import Core.Val
18open import Core.DNF