Analytic Entailment and Consequence Relations @cite{jago-2026}

Truthmaker semantics distinguishes several inequivalent notions of consequence (@cite{jago-2026}):

• Exact entailment p ⊨ₑ q: every exact verifier of p also exactly verifies q. Hyperintensional — sensitive to subject-matter.
• Inexact entailment p ⊨ᵢ q: every inexact verifier of p also inexactly verifies q. Coarser than exact entailment. On basic models @cite{jago-2026} reports a coincidence with FDE (@cite{vanfraassen-1969}); FDE is not formalized in linglib, so this bridge is documented externally rather than proved here.
• Analytic / Angellic entailment (AC) p ≼ q: corresponds to content containment — p's content contains q's content. This is the system of @cite{jago-2026} (Fine 2016 Angellic content) and is the natural truthmaker home for the law of conjunction elimination without disjunction introduction (p ∧ q ⊢ p but ⊬ p ⊢ p ∨ q).

This file:

• defines analytic entailment via the bilateral conjunctive parthood IsContentPart (Up + Down) on TMProp;
• proves the basic chain (p ⊨ₑ q ∧ q ⊨ₑ p) → (p ≼ q) → (p ⊨ᵢ q);
• exhibits the conjunction-elimination / disjunction-introduction asymmetry that distinguishes truthmaker logic from classical/intuitionistic/relevant.

Cross-framework convergence

Phenomena.Conditionals.Studies.Santorio2018.IsTruthmaker p S is the world-extensional truthmaker of @cite{santorio-2018}. It is now defined as an abbrev for ExactEntails on the Bool extension: IsTruthmaker p S := (p · = true) ⊨ₑ (S · = true). It does not correspond to IsContentPart (= AnalyticEntails); the Up clause and mereological parthood are exactly what the world-extensional notion drops. This non-equivalence is theorematised in santorio_truthmaker_neq_fine_content_part in the same study file.

Theories/Semantics/Attitudes/Doxastic.lean's Hintikka boxAt is ∀-over-accessible-worlds; truthmaker attHolds (Basic.lean) is ∃-verifier-part-of-info-state. The empirical heart of @cite{bondarenko-elliott-2026} is exactly this divergence: attHolds distinguishes hyperintensional content (witness: the headline theorem subjectMatter_distinguishes_classically_equivalent in Basic.lean), which boxAt cannot.

def Semantics.Truthmaker.AnalyticEntails {S : Type u_1} [Preorder S] (p q : TMProp S) : Prop

Analytic entailment (AC, @cite{jago-2026} after Fine 2016): p ≼ q iff q is a content part of p — the Down clause says every verifier of p has a part verifying q, and the Up clause says every verifier of q is part of some verifier of p. This is IsContentPart q p (Up + Down).

Equations

• Semantics.Truthmaker.AnalyticEntails p q = Semantics.Truthmaker.IsContentPart q p

def Semantics.Truthmaker.«term_≼_» : Lean.TrailingParserDescr

Notation: p ≼ q for analytic entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem Semantics.Truthmaker.AnalyticEntails.refl {S : Type u_1} [Preorder S] (p : TMProp S) : AnalyticEntails p p

theorem Semantics.Truthmaker.AnalyticEntails.trans {S : Type u_1} [Preorder S] {p q r : TMProp S} (hpq : AnalyticEntails p q) (hqr : AnalyticEntails q r) : AnalyticEntails p r

theorem Semantics.Truthmaker.InexactEntails.of_analytic {S : Type u_1} [Preorder S] {p q : TMProp S} (h : AnalyticEntails p q) : InexactEntails p q

Inexact entailment from analytic entailment: p ≼ q → p ⊨ᵢ q.

From the Down clause of IsContentPart q p (= p ≼ q): every p-verifier has a q-part. So an inexact p-verifier s (with some u ≤ s such that p u) yields a q-part t ≤ u ≤ s, witnessing the inexact verification of q.

theorem Semantics.Truthmaker.AnalyticEntails.of_exact_of_subset {S : Type u_1} [Preorder S] {p q : TMProp S} (hpq : ExactEntails p q) (hqp : ExactEntails q p) : AnalyticEntails p q

Mutual exact entailment lifts to analytic entailment. The Up clause needs the converse direction q ⊨ₑ p to find an extension witness inside p for each q-verifier; with both directions the relation becomes essentially propositional equality on verifier-sets, which trivially satisfies both clauses with self as witness.

theorem Semantics.Truthmaker.isSubsumedBy_tmAnd_left_AC {S : Type u_1} [SemilatticeSup S] (p q : TMProp S) : IsSubsumedBy p (tmAnd p q)

Conjunction elimination holds at the IsSubsumedBy (Down) level unconditionally: p ∧ q is subsumed by p. (Re-export of IsSubsumedBy.tmAnd_left for clarity in the entailment context.)

theorem Semantics.Truthmaker.not_isSubsumedBy_tmOr_intro_general : ¬∀ (S : Type) (x : SemilatticeSup S) (p q : TMProp S), IsSubsumedBy p (tmOr p q)

Disjunction introduction is NOT a content-part relation: p does not in general subsume p ∨ q. A verifier of p ∨ q that only verifies q need not have a part verifying p.

This is the @cite{jago-2026} headline distinction: classical, intuitionistic, and relevant logics all collapse p ∨ (p ∧ q) ≡ p in some directions, conflating containment-respecting and containment-violating consequence. Truthmaker semantics keeps the asymmetry — enabling a logic of containment that supports conjunction elimination without supporting disjunction introduction.

Witness: S = Bool with p = (· = true) and q = (· = false). false verifies tmOr p q (via the right disjunct), but the only p-state is true, and true ≰ false in the Bool ordering.

NB: this differs from isSubsumedBy_or_not_general in Basic.lean (which tested whether q is subsumed by tmOr p q); here we test the introduction direction.