Inexact Truthmaking and Entailment @cite{jago-2026}

Jago Def 3: A state s inexactly makes A true iff some part of s exactly verifies A. Inexact truthmaking obeys the standard extensional clauses for conjunction and disjunction (unlike exact truthmaking, which uses fusion).

This file:

• defines inexact verification (▷) and inexact falsification (◁) for unilateral and bilateral propositions;
• proves the bridge s ⊩ A → s ▷ A (exact implies inexact);
• defines exact and inexact entailment for unilateral propositions;
• shows the extensional clauses for inexact under tmAnd / tmOr and bilateral conj / disj.

The exact-vs-inexact distinction is what lets truthmaker semantics distinguish the logic of content from the logic of consequence (@cite{jago-2026}): exact entailment characterizes hyperintensional content (e.g., AC analytic entailment), while inexact entailment is the truthmaker analogue of familiar consequence relations.

NOTE: @cite{vanfraassen-1969}'s FDE is the canonical historical target — Jago notes that on basic models inexact consequence coincides with FDE. We do not formalize FDE here, so the correspondence is documented as an external claim, not verified inside linglib.

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

Inexact verification (@cite{jago-2026} Def 3): s ▷ p iff some part of s exactly verifies p.

Equations

• Semantics.Truthmaker.inexactVer p s = ∃ u ≤ s, p u

def Semantics.Truthmaker.«term_⊩ᵢ_» : Lean.TrailingParserDescr

Notation: s ⊩ᵢ p for "s inexactly verifies p".

Equations

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

theorem Semantics.Truthmaker.inexactVer_of_exact {S : Type u_1} [Preorder S] {p : TMProp S} {s : S} (hp : p s) : inexactVer p s

Exact verification implies inexact: a verifier is its own part.

theorem Semantics.Truthmaker.inexactVer_mono {S : Type u_1} [Preorder S] {p : TMProp S} {s t : S} (hs : inexactVer p s) (hle : s ≤ t) : inexactVer p t

Inexact verification is downward... wait — actually inexact verification is upward closed: if s inexactly verifies p and s ≤ t, then t inexactly verifies p (the same part of s is also a part of t).

theorem Semantics.Truthmaker.inexactVer_tmOr {S : Type u_1} [Preorder S] (p q : TMProp S) (s : S) : inexactVer (tmOr p q) s ↔ inexactVer p s ∨ inexactVer q s

Inexact verification of disjunction is the union of inexact verifications: s ▷ (p ∨ q) ↔ s ▷ p ∨ s ▷ q.

theorem Semantics.Truthmaker.inexactVer_tmAnd_imp {S : Type u_1} [SemilatticeSup S] (p q : TMProp S) (s : S) (h : inexactVer (tmAnd p q) s) : inexactVer p s ∧ inexactVer q s

Inexact verification of conjunction implies inexact verification of each conjunct: s ▷ (p ∧ q) → s ▷ p ∧ s ▷ q.

The reverse implication does NOT hold in general: s ▷ p and s ▷ q only give us a part of s for each, which need not fuse to a part of s (without further structural assumptions). This is why truthmaker conjunction is hyperintensional even at the inexact level.

def Semantics.Truthmaker.BilProp.inexactVer {S : Type u_1} [Preorder S] (A : BilProp S) (s : S) : Prop

Bilateral inexact verification: some part of s exactly verifies A.

Equations

• A.inexactVer s = Semantics.Truthmaker.inexactVer A.ver s

def Semantics.Truthmaker.BilProp.inexactFal {S : Type u_1} [Preorder S] (A : BilProp S) (s : S) : Prop

Bilateral inexact falsification: some part of s exactly falsifies A.

Equations

• A.inexactFal s = Semantics.Truthmaker.inexactVer A.fal s

@[simp]

theorem Semantics.Truthmaker.BilProp.inexactVer_neg {S : Type u_1} [Preorder S] (A : BilProp S) (s : S) : A.neg.inexactVer s ↔ A.inexactFal s

Negation swaps inexact verification and falsification.

@[simp]

theorem Semantics.Truthmaker.BilProp.inexactFal_neg {S : Type u_1} [Preorder S] (A : BilProp S) (s : S) : A.neg.inexactFal s ↔ A.inexactVer s

@[reducible, inline]

abbrev Semantics.Truthmaker.ExactEntails {S : Type u_1} (p q : TMProp S) : Prop

Exact entailment of unilateral propositions IS the pointwise ≤ on TMProp S = S → Prop (lifted via Pi.instPreorder from Prop's preorder, where P ≤ Q ↔ P → Q).

Equations

• Semantics.Truthmaker.ExactEntails p q = (p ≤ q)

def Semantics.Truthmaker.«term_⊨ₑ_» : Lean.TrailingParserDescr

Notation: p ⊨ₑ q for exact entailment.

Equations

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

theorem Semantics.Truthmaker.ExactEntails.iff_forall {S : Type u_1} {p q : TMProp S} : ExactEntails p q ↔ ∀ (s : S), p s → q s

ExactEntails unfolds to its pointwise definition.

@[reducible, inline]

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

Inexact entailment IS the pointwise ≤ on inexactVer-extensions of the propositions. Reflexivity and transitivity come from the Preorder on TMProp S.

Equations

• Semantics.Truthmaker.InexactEntails p q = (Semantics.Truthmaker.inexactVer p ≤ Semantics.Truthmaker.inexactVer q)

def Semantics.Truthmaker.«term_⊨ᵢ_» : Lean.TrailingParserDescr

Notation: p ⊨ᵢ q for inexact entailment.

Equations

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

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

Exact entailment implies inexact entailment. Pointwise lift of h along inexactVer.