From 25f351d7281a2e8d069b08a7e3457495a63ecc46 Mon Sep 17 00:00:00 2001 From: Aaron Stainback Date: Thu, 23 Apr 2026 17:36:40 -0400 Subject: [PATCH 1/2] =?UTF-8?q?linguistic-seed:=20first=20term=20=E2=80=94?= =?UTF-8?q?=20truth=20(Tarski-grounded;=20root=20of=20prereq=20DAG)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Per docs/linguistic-seed/README.md §Growth-discipline + backwards-chain from current-project needs. First term earns its existence: every factory vocabulary item grounds through 'truth' eventually (assertion, claim, invariant, property, proof, correctness all cite it). Content: - Plain English: correspondence definition (apple-is-red + witness-oath as operational anchor) - Mathematical sketch: T-schema + metalanguage discipline (Tarski 1933/1944) - Lean4 formalisation: deferred placeholder with sketch note (full formalisation requires syntax/reflection encoding; Mathlib has partial substrate) - Grounding point: witness-stand oath (tell-truth / whole-truth / nothing-but-truth operationalises the correspondence) - What this DOES NOT mean: not certainty / not agreement / not pragmatic-usefulness / not coherence-alone / not provability - Citations: Tarski 1933/1944 + Gödel 1931 - Factory usage: 6 cross-refs to how other factory terms ground through truth Dependencies: [] (root of DAG; axiomatic per Tarski) Gap #2 status: skeleton (Otto-23) → FIRST TERM LANDED. Full population multi-round follow-on; next-term candidates per skeleton (implication / equality / set / function / axiom / definition / retraction). Preemptive MD032 '+' scan clean. Attribution: Otto (loop-agent PM hat) authored v0; future Soraya (formal-verification-expert) on Lean4 formalisation cadence; applied-mathematics-expert on definitional review. Co-Authored-By: Claude Opus 4.7 --- docs/linguistic-seed/terms/truth.md | 154 ++++++++++++++++++++++++++++ 1 file changed, 154 insertions(+) create mode 100644 docs/linguistic-seed/terms/truth.md diff --git a/docs/linguistic-seed/terms/truth.md b/docs/linguistic-seed/terms/truth.md new file mode 100644 index 00000000..3948ddb9 --- /dev/null +++ b/docs/linguistic-seed/terms/truth.md @@ -0,0 +1,154 @@ +--- +name: truth +defined-by: Tarski's semantic definition of truth (1933/1944) +formalised: plain-English + mathematical sketch; Lean4 formalisation deferred +dependencies: [] +--- + +# truth + +## Plain English + +**Truth** is the property an assertion has when what it +says matches what is the case. + +"The apple is red" is true when the apple being referred +to is, in fact, red. "2 + 2 = 4" is true when the +arithmetic operation genuinely yields 4. Truth is not a +property of words alone; it is the correspondence +between the assertion and the situation the assertion +is about. + +When we say something is **true**, we are claiming the +assertion has this correspondence property. When we say +something is **false**, we are claiming the assertion's +negation has this property. + +## Mathematical definition + +Following Tarski's 1933/1944 formalisation: + +Given a language `L` with sentences `φ, ψ, ...`, a +**truth-definition** for `L` is a predicate `T` in a +richer metalanguage `M ⊃ L` such that for every sentence +`φ` of `L`: + +``` +T("φ") if and only if φ +``` + +The left side uses `T` applied to a *name* (quoted +string) of the sentence; the right side uses the sentence +itself as asserted in the metalanguage. + +This is the **T-schema** (or Convention T). A truth- +definition is adequate when every instance of the T-schema +is a theorem of the metalanguage. + +**Crucial Tarski theorem**: `L` cannot define its own +truth predicate (under mild assumptions). Truth is +definable only *about* `L`, only *in* a richer `M`. This +is what blocks the liar paradox: *"this sentence is +false"* cannot be self-consistently expressed in a +language that defines its own truth. + +## Lean4 formalisation + +```lean4 +-- Deferred. First-pass sketch: +-- In Lean4, `Prop` plays the role of sentences; the +-- metalanguage is Lean's type theory itself. The T-schema +-- is built into the proof assistant: +-- theorem T_schema : ∀ (p : Prop), (p = p) ↔ p +-- Formalising Tarski's hierarchy (object-language L ⊂ M ⊂ ...) +-- requires encoding syntax + quotation + reflection. Mathlib +-- has partial substrate (Tarski-Vaught test, elementary +-- substructure) but no closed "Tarski's truth" theorem +-- module as of writing. +-- Full formalisation: follow-on work per +-- `docs/linguistic-seed/README.md` §growth-discipline. +``` + +## Grounding point (per Otto-21 Craft discipline) + +**The witness-stand oath.** When a witness swears to "tell +the truth, the whole truth, and nothing but the truth," +the oath names three aspects of truth: + +- **Tell the truth** — say only assertions that correspond + to what is the case (no false statements) +- **The whole truth** — say all relevant assertions that + correspond (no omissions that mislead) +- **Nothing but the truth** — say only truth-correspondent + assertions (no unrelated material mixed in) + +The oath does not define truth in a philosophical sense; +it operationalises it for legal testimony. The factory +uses truth the same way — operationally, as a +correspondence between assertion and the-case-as-it-is. + +## What this term DOES NOT mean + +- **Not certainty** — we can assert truth without being + certain; certainty is a confidence measure, truth is + a correspondence property. +- **Not agreement** — a claim can be true even if no one + agrees with it (the universe of facts is not + determined by human agreement). +- **Not pragmatic-usefulness** — we are not defining + truth as "what works in practice" (pragmatist + redefinition); Tarski's correspondence is the seed's + anchor. +- **Not coherence-alone** — we are not defining truth as + "what fits with other beliefs" (coherentist + redefinition); internal consistency is necessary but + not sufficient. +- **Not provability** — a statement can be true without + being provable in a given formal system (Gödel's + incompleteness). Truth and provability are distinct + predicates. + +## Citations + +- **Tarski, Alfred.** *"The Concept of Truth in + Formalized Languages."* 1933 (Polish); 1956 (English + translation in *Logic, Semantics, Metamathematics*). + The seed's primary source for the correspondence / + T-schema formalisation. +- **Tarski, Alfred.** *"The Semantic Conception of Truth + and the Foundations of Semantics."* Philosophy and + Phenomenological Research 4 (1944). The accessible + English reformulation. +- **Gödel, Kurt.** *"On Formally Undecidable Propositions + of Principia Mathematica and Related Systems I"* + (1931). Establishes that truth and provability can + diverge — motivating why the seed distinguishes them. + +## Factory usage + +Other factory vocabulary grounds through `truth`: + +- **Assertion** (when landed) — something that can be + true or false +- **Claim** — an assertion proposed for acceptance +- **Invariant** — a claim whose truth is preserved + through state transitions +- **Property** (in property-based testing) — an assertion + about all instances of a type that should be true for + every instance +- **Proof** — a demonstration that a claim is true in a + given formal system +- **Correctness** — the property of software that its + outputs truly match its specification + +Every factory claim of the form "X is true" / "X is +correct" / "X holds" grounds through this term's +correspondence definition. + +## What this term IS (summary) + +The correspondence property of an assertion with what is +the case, definable only in a richer metalanguage +(Tarski). The factory uses it operationally, not +philosophically: an assertion is true when the-thing-it- +asserts is what's actually happening. From 904729d6591facac1c27d41e539b95c9cc97a108 Mon Sep 17 00:00:00 2001 From: Aaron Stainback Date: Sat, 25 Apr 2026 01:35:48 -0400 Subject: [PATCH 2/2] =?UTF-8?q?drain(#202=20P1=C3=973=20+=20P1+P2=C3=973?= =?UTF-8?q?=20Codex):=20Lean=20T-schema=20correction=20+=20frontmatter=20e?= =?UTF-8?q?num=20+=20hyphenation=20fixes?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit P1 (line 62, three threads on the same finding) — Lean T-schema: The sketch `theorem T_schema : ∀ (p : Prop), (p = p) ↔ p` is logically incorrect: `(p = p)` is provable for every p (by `rfl`), so the equivalence reduces to `True ↔ p` which is false for unprovable p. Replaced with a correct framing: Lean4's `Prop` directly embodies the T-schema (a proposition IS its own truth condition; producing a proof of p IS the truth-witness, no separate T-predicate needed). Added explanatory note about why the original attempt was wrong — for the reader who learns from the corrected error. P1 (line 9) — formalised: front-matter enum mismatch: The README schema specifies `formalised: `. The doc had a verbose prose value 'plain-English + mathematical sketch; Lean4 formalisation deferred'. Updated to `draft` per the schema enum. P2 (line 46) — manual hyphenation across line break: 'A truth-\ndefinition' would render as 'A truth- definition' in some Markdown renderers. Reflowed so the hyphenated compound stays on a single line. P2 (line 153/170) — same hyphenation issue: 'the-thing-it-\nasserts' would render as 'the-thing-it- asserts'. Reflowed. --- docs/linguistic-seed/terms/truth.md | 49 +++++++++++++++++++---------- 1 file changed, 33 insertions(+), 16 deletions(-) diff --git a/docs/linguistic-seed/terms/truth.md b/docs/linguistic-seed/terms/truth.md index 3948ddb9..a4257823 100644 --- a/docs/linguistic-seed/terms/truth.md +++ b/docs/linguistic-seed/terms/truth.md @@ -1,7 +1,7 @@ --- name: truth defined-by: Tarski's semantic definition of truth (1933/1944) -formalised: plain-English + mathematical sketch; Lean4 formalisation deferred +formalised: draft dependencies: [] --- @@ -41,9 +41,9 @@ The left side uses `T` applied to a *name* (quoted string) of the sentence; the right side uses the sentence itself as asserted in the metalanguage. -This is the **T-schema** (or Convention T). A truth- -definition is adequate when every instance of the T-schema -is a theorem of the metalanguage. +This is the **T-schema** (or Convention T). A +truth-definition is adequate when every instance of the +T-schema is a theorem of the metalanguage. **Crucial Tarski theorem**: `L` cannot define its own truth predicate (under mild assumptions). Truth is @@ -55,18 +55,35 @@ language that defines its own truth. ## Lean4 formalisation ```lean4 --- Deferred. First-pass sketch: --- In Lean4, `Prop` plays the role of sentences; the --- metalanguage is Lean's type theory itself. The T-schema --- is built into the proof assistant: --- theorem T_schema : ∀ (p : Prop), (p = p) ↔ p --- Formalising Tarski's hierarchy (object-language L ⊂ M ⊂ ...) --- requires encoding syntax + quotation + reflection. Mathlib --- has partial substrate (Tarski-Vaught test, elementary --- substructure) but no closed "Tarski's truth" theorem --- module as of writing. +-- Deferred — draft sketch only. +-- +-- In Lean4, `Prop` directly embodies the T-schema: +-- a proposition `p : Prop` IS its own truth condition. +-- You don't prove "T(p) ↔ p" in Lean's logic; you prove +-- `p` itself, and the act of producing a proof IS the +-- truth-witness. This is why Lean's type theory works +-- as a metalanguage for this term — Tarski's hierarchy +-- (object-language L ⊂ metalanguage M ⊂ ...) collapses +-- to a single layer when the object-language is Prop and +-- the metalanguage is the type theory above it. +-- +-- A *reflective* truth predicate that talks about a +-- closed object-language (separate syntax, separate +-- quotation, separate evaluation) requires explicit +-- syntactic encoding in Lean. Mathlib has partial +-- substrate (Tarski-Vaught test, elementary substructure) +-- but no closed "Tarski's truth" theorem module as of +-- 2026-04-23. +-- -- Full formalisation: follow-on work per -- `docs/linguistic-seed/README.md` §growth-discipline. +-- Deliberately NOT included here: the earlier draft +-- attempted `theorem T_schema : ∀ (p : Prop), (p = p) ↔ p` +-- which is logically incorrect — `(p = p)` is provable +-- for every p, so the equivalence reduces to "True ↔ p" +-- which is false for unprovable p. The error is fixed +-- by recognising that Lean's Prop already IS the +-- T-schema; no theorem needs to be proven about it. ``` ## Grounding point (per Otto-21 Craft discipline) @@ -150,5 +167,5 @@ correspondence definition. The correspondence property of an assertion with what is the case, definable only in a richer metalanguage (Tarski). The factory uses it operationally, not -philosophically: an assertion is true when the-thing-it- -asserts is what's actually happening. +philosophically: an assertion is true when +the-thing-it-asserts is what's actually happening.