Truth-bearer (proposition as section)

A truth-bearer, in the τ-framework, is a section of a presheaf — a structural object, not a linguistic entity. Propositions are sections of the truth-functor over the worlds-presheaf; sentences and beliefs become truth-bearers only by representing such a section. Truth-makers (VII.D27, VII.D60) are the structures that make sections exist — and four canonical types are identified: inclusion, section, diagram, invariant.

Categorical invariant. p is a truth-bearer ⟺ p ∈ Sect(F) for some presheaf F : World^op → Type in K_τ.

Primary registry anchor: VII.D61

Supporting items: VII.D60, VII.D27, VII.D62

1. VII.D27 — Truth-Maker in Ontological — four types of truth-makers: inclusion, section, diagram, invariant.
2. VII.D60 — Truth-Maker in Logical — structures that make sections exist; the ground of truth.
3. VII.D61 — Truth-Bearer as Section — propositions are sections of presheaves; truth-bearers are structural, not linguistic.
4. VII.D62 — Modal Frame in τ — possible worlds as internal objects, providing the base over which the truth-bearing presheaf is defined.

Lean modules referenced: TauLib.BookVII.Ethics.CIProof

A truth-bearer is instantiated wherever something is evaluable as true or false: an empirical claim, a normative judgement, a proof-statement, a commitment-attribution. Each such evaluable item is a section over a presheaf — empirical truth-bearers over the observation-presheaf, normative over the norm-presheaf, proof-theoretic over the proof-presheaf, commitment-theoretic over the stance-presheaf. The sentence we utter is not the truth-bearer; it represents the section.

Examples:

• Empirical: 'the cat is on the mat' — represents a section of the empirical-truth presheaf assigning configurations in which 'cat-on-mat' holds.
• Mathematical: 'every prime greater than 2 is odd' — a section of the proof-truth presheaf, with truth-makers of the diagram-and-invariant types.
• Normative: 'this verdict is just' — a section of the norm-presheaf in Reg_P, with truth-makers of the section type (legitimate justificatory glue).
• Commitment-theoretic: 'the agent is committed to F' — a section of the stance-presheaf in Reg_C, with truth-makers of the inclusion type (the stance-content includes F).

Register codomain: Cross-register (each register has its own truth-presheaf; the section-structure is uniform).

Manuscript reference: manuscript-sources/book-07/part06/ch72.tex

Status: Formalized

Module: TauLib.BookVII.Ethics.CIProof

Lean kind: structure

Lean symbol: Tau.BookVII.Ethics.CIProof.TruthBearerAsSection

Related glossary entries

• MG-O01-being Being (categorical existence)
• MG-O03-modality Modality (necessity, possibility, contingency)
• MG-O13-reality Reality (recoverable kernel field)

Referenced by

• MG-O13-reality Reality (recoverable kernel field)