Type Theory with Records — Discourse State & Pragmatics

[Coo23] [Par73]

Discourse-level infrastructure for TTR ([Coo23], Chapters 2, 4, 5):

Signs & Illocutionary Force: TTRSign, ForcedSign (§2.5–2.6) — the illocutionary force component reuses Semantics.Mood.IllocutionaryMood rather than [Coo23]'s parallel four-way IllocForce enum (the surface distinction assertion | query | command | acknowledgement is the declarative/interrogative/imperative slice plus a backchannel constructor; true backchannels live in Pragmatics/Dialogue/Gameboard/).

Information States: InfoState (gameboard), agenda operations, bridge to CommonGround (§2.6).

Parametric Content: Parametric bg/fg, PPpty, PQuant, PQuantDet, PRel2 (§4.2–4.3). Bridge to Semantics.Presupposition.PartialProp.

Reference & Mental States: HasNamed, NameContext, semPropNameP, TotalInfoState, AccommodationKind, Paderewski puzzle, Assgnmnt/Cntxt, semPron, parametric verb semantics, Parametric.combine (§4.3–4.7).

Frames & Descriptions: AmbTempFrame, Scale, RiseEvent, IndPpty/FramePpty, Bot, unique, semDefArt, semUniversal, FixedPtType, FrameType, restrictPpty, TravelFrame/PassengerFrame, semBeID, semBeScalar (§5.2–5.8).

§ 2.6 Illocutionary force (Cooper ex 91)

Signs may carry illocutionary force. [Coo23]'s ex (91) introduces a four-way TTR-internal enum assertion | query | command | acknowledgement. We collapse assertion/query/command into Semantics.Mood.IllocutionaryMood's declarative/interrogative/imperative (the same Searlean cuts) and let backchannel acknowledgements be handled where dialogue moves live (Pragmatics/Dialogue/Gameboard/). The result: TTR signs share the rest of the library's mood vocabulary rather than re-stipulating it.

structure Semantics.TypeTheoretic.ForcedSign (Phon Cont : Type) extends Semantics.TypeTheoretic.TTRSign Phon Cont : Type

A sign with illocutionary force. [Coo23] ex (91), with IllocForce replaced by Semantics.Mood.IllocutionaryMood.

• phon : Phon
• cont : Cont
• illoc : Mood.IllocutionaryMood

@[implicit_reducible]

instance Semantics.TypeTheoretic.instCoeForcedSignTTRSign (Phon Cont : Type) : Coe (ForcedSign Phon Cont) (TTRSign Phon Cont)

ForcedSign ⊑ TTRSign (adding illoc = more fields = subtype).

Equations

• Semantics.TypeTheoretic.instCoeForcedSignTTRSign Phon Cont = { coe := Semantics.TypeTheoretic.ForcedSign.toTTRSign }

def Semantics.TypeTheoretic.IllocutionaryMood.toClauseForm? : Mood.IllocutionaryMood → Option Features.ClauseForm

Bridge: IllocutionaryMood → form-level ClauseForm. The two question form distinctions (matrix vs embedded) are not visible from illocutionary force alone, so we project to the matrix variant.

Imperatives, promissives, and exclamatives have no ClauseForm form-counterpart in Features.ClauseForm (which only enumerates the declarative/question word-order distinctions); they map to none.

Equations

• Semantics.TypeTheoretic.IllocutionaryMood.toClauseForm? Semantics.Mood.IllocutionaryMood.declarative = some Features.ClauseForm.declarative
• Semantics.TypeTheoretic.IllocutionaryMood.toClauseForm? Semantics.Mood.IllocutionaryMood.interrogative = some Features.ClauseForm.matrixQuestion
• Semantics.TypeTheoretic.IllocutionaryMood.toClauseForm? Semantics.Mood.IllocutionaryMood.imperative = none
• Semantics.TypeTheoretic.IllocutionaryMood.toClauseForm? Semantics.Mood.IllocutionaryMood.promissive = none
• Semantics.TypeTheoretic.IllocutionaryMood.toClauseForm? Semantics.Mood.IllocutionaryMood.exclamative = none

def Semantics.TypeTheoretic.IllocutionaryMood.fromClauseForm : Features.ClauseForm → Mood.IllocutionaryMood

Bridge: form-level ClauseForm → IllocutionaryMood. The form distinction between matrix and embedded questions collapses on the force side.

Equations

• Semantics.TypeTheoretic.IllocutionaryMood.fromClauseForm Features.ClauseForm.declarative = Semantics.Mood.IllocutionaryMood.declarative
• Semantics.TypeTheoretic.IllocutionaryMood.fromClauseForm Features.ClauseForm.matrixQuestion = Semantics.Mood.IllocutionaryMood.interrogative
• Semantics.TypeTheoretic.IllocutionaryMood.fromClauseForm Features.ClauseForm.embeddedQuestion = Semantics.Mood.IllocutionaryMood.interrogative

theorem Semantics.TypeTheoretic.illoc_declarative_roundtrip : IllocutionaryMood.toClauseForm? (IllocutionaryMood.fromClauseForm Features.ClauseForm.declarative) = some Features.ClauseForm.declarative

Round-trip: fromClauseForm preserves the declarative slot.

theorem Semantics.TypeTheoretic.illoc_question_roundtrip : IllocutionaryMood.toClauseForm? (IllocutionaryMood.fromClauseForm Features.ClauseForm.matrixQuestion) = some Features.ClauseForm.matrixQuestion

Round-trip: fromClauseForm preserves the matrix-question slot.

§ 2.6 Information states and gameboards (Cooper ex 88–90)

An information state (gameboard) has two parts:

• Private: the agent's agenda (plan of upcoming type acts)
• Shared: latest utterance + shared commitments

structure Semantics.TypeTheoretic.InfoState (SignT CommT : Type) : Type

An agent's information state (gameboard). §2.6, ex (88).

• agenda : List SignT

  The agent's agenda: sign types planned for realization

• latestUtterance : Option SignT

  The most recent utterance sign

• commitments : CommT

  Shared commitments (accumulated accepted content)

def Semantics.TypeTheoretic.InfoState.initial {SignT CommT : Type} (baseComm : CommT) : InfoState SignT CommT

Initial information state: empty agenda, no utterance, base commitments.

Equations

• Semantics.TypeTheoretic.InfoState.initial baseComm = { agenda := [], latestUtterance := none, commitments := baseComm }

def Semantics.TypeTheoretic.InfoState.execTopAgenda {SignT CommT : Type} (s : InfoState SignT CommT) : Option (SignT × InfoState SignT CommT)

Pop the top agenda item (ExecTopAgenda). §2.6, ex (120).

Equations

• s.execTopAgenda = match s.agenda with | [] => none | top :: rest => some (top, { agenda := rest, latestUtterance := s.latestUtterance, commitments := s.commitments })

def Semantics.TypeTheoretic.InfoState.downDateAgenda {SignT CommT : Type} (s : InfoState SignT CommT) : InfoState SignT CommT

Remove top agenda item after observation (DownDateAgenda).

Equations

• s.downDateAgenda = { agenda := List.drop 1 s.agenda, latestUtterance := s.latestUtterance, commitments := s.commitments }

def Semantics.TypeTheoretic.InfoState.integrate {SignT CommT : Type} (s : InfoState SignT CommT) (utt : SignT) (newComm : CommT) : InfoState SignT CommT

Record a new utterance and update commitments.

Equations

• s.integrate utt newComm = { agenda := s.agenda, latestUtterance := some utt, commitments := newComm }

def Semantics.TypeTheoretic.InfoState.pushAgenda {SignT CommT : Type} (s : InfoState SignT CommT) (signType : SignT) : InfoState SignT CommT

Push a new sign type onto the front of the agenda (PlanAckAss).

Equations

• s.pushAgenda signType = { agenda := signType :: s.agenda, latestUtterance := s.latestUtterance, commitments := s.commitments }

Bridge to CommonGround

def Semantics.TypeTheoretic.InfoState.toCG {W SignT : Type} (s : InfoState SignT (List (Set W))) : CommonGround W

Bridge: a Set W-based information state's commitments form a CommonGround.

Equations

• s.toCG = { propositions := s.commitments }

@[implicit_reducible]

instance Semantics.TypeTheoretic.instHasContextSetInfoStateListSet {W SignT : Type} : CommonGround.HasContextSet (InfoState SignT (List (Set W))) W

InfoState with Set W commitments projects to a context set via CommonGround.

Equations

• Semantics.TypeTheoretic.instHasContextSetInfoStateListSet = { toContextSet := fun (s : Semantics.TypeTheoretic.InfoState SignT (List (Set W))) => s.toCG.contextSet }

theorem Semantics.TypeTheoretic.infoState_initial_eq_empty_cg (W SignT : Type) : (InfoState.initial []).toCG = CommonGround.empty

Bridge theorem: initial state maps to empty common ground.

theorem Semantics.TypeTheoretic.integrate_comm_eq_cg_add {W SignT : Type} (s : InfoState SignT (List (Set W))) (utt : SignT) (p : Set W) : (s.integrate utt (p :: s.commitments)).toCG = s.toCG.add p

Bridge: integrating a commitment = adding to common ground.

Bridge to Semantics.Dynamic.Core.InfoState

def Semantics.TypeTheoretic.InfoState.toCoreInfoState {W E SignT : Type} (s : InfoState SignT (List (Set W))) : Set (Dynamic.Core.Possibility W E)

TTR's InfoState tracks discourse state via agenda/commitments. Semantics.Dynamic.Core.InfoState tracks possibilities (world + assignment). Bridge: a TTR InfoState with Set W commitments induces a Core InfoState by filtering possibilities that satisfy all commitments.

Equations

• s.toCoreInfoState = {p : Semantics.Dynamic.Core.Possibility W E | List.Forall (fun (x : Set W) => p.world ∈ x) s.commitments}

inductive Semantics.TypeTheoretic.FetchEvent : Type

String type example: a fetch game decomposes into sub-events.

• pickUp : FetchEvent
• throw : FetchEvent
• runAfter : FetchEvent
• pickUpReturn : FetchEvent
• return_ : FetchEvent

def Semantics.TypeTheoretic.instReprFetchEvent.repr : FetchEvent → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.TypeTheoretic.instReprFetchEvent : Repr FetchEvent

Equations

• Semantics.TypeTheoretic.instReprFetchEvent = { reprPrec := Semantics.TypeTheoretic.instReprFetchEvent.repr }

@[implicit_reducible]

instance Semantics.TypeTheoretic.instDecidableEqFetchEvent : DecidableEq FetchEvent

Equations

• Semantics.TypeTheoretic.instDecidableEqFetchEvent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.TypeTheoretic.fetchGame : StringType FetchEvent

Equations

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

def Semantics.TypeTheoretic.fetchThrow : StringType FetchEvent

Equations

• Semantics.TypeTheoretic.fetchThrow = Semantics.TypeTheoretic.StringType.singleton Semantics.TypeTheoretic.FetchEvent.throw

def Semantics.TypeTheoretic.fetchRunAfter : StringType FetchEvent

Equations

• Semantics.TypeTheoretic.fetchRunAfter = Semantics.TypeTheoretic.StringType.singleton Semantics.TypeTheoretic.FetchEvent.runAfter

theorem Semantics.TypeTheoretic.typeAct_covers_illoc (ta : TypeAct) : ∃ (i : Mood.IllocutionaryMood), ta = TypeAct.judge ∧ i = Mood.IllocutionaryMood.declarative ∨ ta = TypeAct.query ∧ i = Mood.IllocutionaryMood.interrogative ∨ ta = TypeAct.create ∧ i = Mood.IllocutionaryMood.imperative

The three type acts map to the three Searlean basic illocutionary moods (declarative, interrogative, imperative).

theorem Semantics.TypeTheoretic.exec_empty_agenda {SignT CommT : Type} (c : CommT) : (InfoState.initial c).execTopAgenda = none

ExecTopAgenda returns None on empty agenda.

theorem Semantics.TypeTheoretic.push_then_exec {SignT CommT : Type} (s : InfoState SignT CommT) (item : SignT) : (s.pushAgenda item).execTopAgenda = some (item, s)

PushAgenda then ExecTopAgenda recovers the pushed item.

§ 4.2–4.3 Parametric content

§4.3 introduces parametric content: semantic content that depends on a context (a presupposition). A parametric content has:

• bg (background): a context type — the presupposition
• fg (foreground): a function from satisfying contexts to content

structure Semantics.TypeTheoretic.Parametric (Content : Type u_1) : Type (max u_1 (u_2 + 1))

Parametric content: a background type (presupposition) paired with a foreground function from satisfying contexts to content. §4.3, (14).

• Bg : Type u_2

  Background type — what the context must provide (presupposition)

• fg : self.Bg → Content

  Foreground — content given a context satisfying the background

@[reducible, inline]

abbrev Semantics.TypeTheoretic.PPpty (E : Type) : Type (u_1 + 1)

Parametric property: context-dependent property.

Equations

• Semantics.TypeTheoretic.PPpty E = Semantics.TypeTheoretic.Parametric (Semantics.TypeTheoretic.Ppty E)

@[reducible, inline]

abbrev Semantics.TypeTheoretic.PQuant (E : Type) : Type (u_1 + 1)

Parametric quantifier: context-dependent quantifier.

Equations

• Semantics.TypeTheoretic.PQuant E = Semantics.TypeTheoretic.Parametric (Semantics.TypeTheoretic.Quant E)

@[reducible, inline]

abbrev Semantics.TypeTheoretic.PQuantDet (E : Type) : Type (u_1 + 1)

Parametric quantifier determiner: context-dependent Det meaning.

Equations

• Semantics.TypeTheoretic.PQuantDet E = Semantics.TypeTheoretic.Parametric (Semantics.TypeTheoretic.Ppty E → Semantics.TypeTheoretic.Quant E)

@[reducible, inline]

abbrev Semantics.TypeTheoretic.PRel2 (E : Type) : Type (u_1 + 1)

Parametric binary relation: context-dependent transitive verb meaning.

Equations

• Semantics.TypeTheoretic.PRel2 E = Semantics.TypeTheoretic.Parametric (Semantics.TypeTheoretic.Quant E → Semantics.TypeTheoretic.Ppty E)

def Semantics.TypeTheoretic.Parametric.trivial {Content : Type u_1} (c : Content) : Parametric Content

A trivial parametric content: no presupposition (bg = Unit).

Equations

• Semantics.TypeTheoretic.Parametric.trivial c = { Bg := Unit, fg := fun (x : Unit) => c }

theorem Semantics.TypeTheoretic.Parametric.trivial_fg {Content : Type u_1} (c : Content) (u : Unit) : (trivial c).fg u = c

A trivial parametric content yields the same value for any context.

Bridge: Parametric ↔ PartialProp (presupposition/assertion)

noncomputable def Semantics.TypeTheoretic.Parametric.toPartialProp {W : Type u_1} (p : Parametric (W → Prop)) (presupTest : W → Prop) [DecidablePred presupTest] (bgWitness : (w : W) → presupTest w → p.Bg) : Presupposition.PartialProp W

Convert a Parametric (W → Prop) to a PartialProp.

Equations

• p.toPartialProp presupTest bgWitness = { presup := presupTest, assertion := fun (w : W) => if h : presupTest w then p.fg (bgWitness w h) w else False }

def Semantics.Presupposition.PartialProp.toParametric {W : Type u_1} (p : PartialProp W) : TypeTheoretic.Parametric (Set W)

Convert a PartialProp back to a Parametric.

Equations

• p.toParametric = { Bg := { w : W // p.presup w }, fg := fun (x : { w : W // p.presup w }) => p.assertion }

theorem Semantics.TypeTheoretic.toParametric_toPartialProp_assertion {W : Type u_1} (p : Presupposition.PartialProp W) (w : W) (hp : p.presup w) : p.toParametric.fg ⟨w, hp⟩ w ↔ p.assertion w

Parametric ↔ PartialProp roundtrip: the assertion component survives when the presupposition holds.

noncomputable def Semantics.TypeTheoretic.Parametric.toPartialPropSimple {W : Type u_1} (presup : W → Prop) [DecidablePred presup] (assertion : (w : W) → presup w → Prop) : Presupposition.PartialProp W

When a Parametric has a Prop-valued background, it directly maps to PartialProp.

Equations

• Semantics.TypeTheoretic.Parametric.toPartialPropSimple presup assertion = { presup := presup, assertion := fun (w : W) => if h : presup w then assertion w h else False }

§ 4.3 Named predicate and parametric proper names

class Semantics.TypeTheoretic.HasNamed (E : Type) : Type

The named predicate: Named a n means individual a bears name n.

• named : E → String → Prop

structure Semantics.TypeTheoretic.NameContext (E : Type) [HasNamed E] (name : String) : Type

Context for a proper name: an individual bearing the right name.

• individual : E
• isNamed : HasNamed.named self.individual name

def Semantics.TypeTheoretic.semPropNameP {E : Type} [HasNamed E] (name : String) : PQuant E

Parametric proper name content (revised from Ch3).

Equations

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

theorem Semantics.TypeTheoretic.semPropNameP_resolved {E : Type} [HasNamed E] (name : String) (ctx : NameContext E name) : (semPropNameP name).fg ctx = semPropName ctx.individual

Bridge: parametric proper name reduces to Ch3 semPropName when the context is resolved to a specific individual.

§ 4.4 Total information state and accommodation

structure Semantics.TypeTheoretic.TotalInfoState (Memory Board : Type) : Type

A total information state: long-term memory + dialogue gameboard.

• ltm : Memory

  Long-term memory: persistent knowledge about individuals

• gb : Board

  Dialogue gameboard: dependent on ltm for anchoring

inductive Semantics.TypeTheoretic.AccommodationKind : Type

The three accommodation strategies for presupposition resolution. §4.4, (74).

• gameboard : AccommodationKind
• longTermMemory : AccommodationKind
• noMatch : AccommodationKind

def Semantics.TypeTheoretic.instReprAccommodationKind.repr : AccommodationKind → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.TypeTheoretic.instReprAccommodationKind : Repr AccommodationKind

Equations

• Semantics.TypeTheoretic.instReprAccommodationKind = { reprPrec := Semantics.TypeTheoretic.instReprAccommodationKind.repr }

@[implicit_reducible]

instance Semantics.TypeTheoretic.instDecidableEqAccommodationKind : DecidableEq AccommodationKind

Equations

• Semantics.TypeTheoretic.instDecidableEqAccommodationKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.TypeTheoretic.AccommodationKind.preference : AccommodationKind → ℕ

Accommodation preference: gameboard > long-term memory > no match.

Equations

• Semantics.TypeTheoretic.AccommodationKind.gameboard.preference = 0
• Semantics.TypeTheoretic.AccommodationKind.longTermMemory.preference = 1
• Semantics.TypeTheoretic.AccommodationKind.noMatch.preference = 2

theorem Semantics.TypeTheoretic.gameboard_preferred_over_ltm : AccommodationKind.gameboard.preference < AccommodationKind.longTermMemory.preference

theorem Semantics.TypeTheoretic.ltm_preferred_over_noMatch : AccommodationKind.longTermMemory.preference < AccommodationKind.noMatch.preference

§ 4.5 Paderewski puzzle

structure Semantics.TypeTheoretic.TwoConcept (E : Type) (pianist statesman : E → Prop) : Type

Two-concept state: an agent has two memory entries for "Paderewski".

• asMusician : E
• asPolitician : E
• isPianist : pianist self.asMusician
• isStatesman : statesman self.asPolitician

structure Semantics.TypeTheoretic.OneConcept (E : Type) (pianist statesman : E → Prop) : Type

One-concept state: after learning the identity.

• person : E
• isPianist : pianist self.person
• isStatesman : statesman self.person

def Semantics.TypeTheoretic.TwoConcept.merge {E : Type} {pianist statesman : E → Prop} (tc : TwoConcept E pianist statesman) (identity : tc.asMusician = tc.asPolitician) : OneConcept E pianist statesman

Merging two concepts when they turn out to be the same individual.

Equations

• tc.merge identity = { person := tc.asMusician, isPianist := ⋯, isStatesman := ⋯ }

theorem Semantics.TypeTheoretic.merge_person_eq {E : Type} {pianist statesman : E → Prop} (tc : TwoConcept E pianist statesman) (h : tc.asMusician = tc.asPolitician) : (tc.merge h).person = tc.asMusician

theorem Semantics.TypeTheoretic.merge_preserves_both {E : Type} {pianist statesman : E → Prop} (tc : TwoConcept E pianist statesman) (h : tc.asMusician = tc.asPolitician) : pianist (tc.merge h).person ∧ statesman (tc.merge h).person

theorem Semantics.TypeTheoretic.paderewski_nonrigid_identity {E : Type} (musician_concept politician_concept : Fin 2 → E) (w : Fin 2) (_hAgree : musician_concept w = politician_concept w) (hDisagree : ∃ (w' : Fin 2), musician_concept w' ≠ politician_concept w') : ¬Intensional.Intension.CoExtensional musician_concept politician_concept

Bridge to Intensional.Intension: the Paderewski puzzle is an instance of non-rigid identity.

§ 4.6 Unbound pronouns

@[reducible, inline]

abbrev Semantics.TypeTheoretic.Assgnmnt (E : Type) : Type

Variable assignment: maps natural-number indices to individuals. Equal to Core.PartialAssign E; the alias name is retained because Bekki/Asher's TYS prose uses 𝔰/𝔩/𝔯/𝔴/𝔤 as named "assignments" rather than as partial functions, and the inheritance carries the valued/valued_update_at simp set into this file's consumers.

Equations

• Semantics.TypeTheoretic.Assgnmnt E = Core.PartialAssign E

def Semantics.TypeTheoretic.Assgnmnt.hasBindings {E : Type} (g : Assgnmnt E) (n : ℕ) : Prop

An assignment with at least n bindings (all indices < n defined). Novel relative to Core.PartialAssign; not promoted (single consumer).

Equations

• g.hasBindings n = ∀ i < n, (g i).isSome = true

def Semantics.TypeTheoretic.Assgnmnt.merge {E : Type} (g₁ g₂ : Assgnmnt E) : Assgnmnt E

Merge two assignments (left-biased). Novel relative to Core.PartialAssign; Core.PartialAssign.empty, Core.PartialAssign.update, and the update-lookup lemmas are inherited via the Assgnmnt := PartialAssign abbrev and used directly by consumers.

Equations

• g₁.merge g₂ i = (g₁ i).orElse fun (x : Unit) => g₂ i

theorem Semantics.TypeTheoretic.Assgnmnt.merge_empty_left {E : Type} (g : Assgnmnt E) : merge Core.PartialAssign.empty g = g

Merge with empty on the left returns the right assignment.

@[reducible, inline]

abbrev Semantics.TypeTheoretic.PropCntxt : Type 1

Propositional context.

Equations

• Semantics.TypeTheoretic.PropCntxt = Type

structure Semantics.TypeTheoretic.Cntxt (E C : Type) : Type

Full context: assignment + propositional context.

• assignment : Assgnmnt E
• propCtx : C

def Semantics.TypeTheoretic.semPron {E : Type} : PQuant E

Pronoun semantics as a parametric quantifier.

Equations

• Semantics.TypeTheoretic.semPron = { Bg := E, fg := fun (a : E) => Semantics.TypeTheoretic.semPropName a }

theorem Semantics.TypeTheoretic.semPron_resolved {E : Type} (a : E) : semPron.fg a = semPropName a

Bridge: pronoun semantics reduces to semPropName when resolved.

Parametric verb semantics

def Semantics.TypeTheoretic.semIntransVerbP {E : Type} (Bg : Type) (p : E → Type) : PPpty E

Parametric intransitive verb content.

Equations

• Semantics.TypeTheoretic.semIntransVerbP Bg p = { Bg := Bg, fg := fun (x : Bg) => Semantics.TypeTheoretic.semCommonNoun p }

def Semantics.TypeTheoretic.semTransVerbP {E : Type} (Bg : Type) (p : E → E → Type) : Parametric (Quant E → Ppty E)

Parametric transitive verb content.

Equations

• Semantics.TypeTheoretic.semTransVerbP Bg p = { Bg := Bg, fg := fun (x : Bg) (Q : Semantics.TypeTheoretic.Quant E) (x_1 : E) => Q fun (y : E) => p x_1 y }

theorem Semantics.TypeTheoretic.semTransVerbP_trivial {E : Type} (p : E → E → Type) (u : Unit) (Q : Quant E) (x : E) : (semTransVerbP Unit p).fg u Q x = Q fun (y : E) => p x y

Bridge: transitive verb with trivial context reduces to Montague pattern.

S-combinator for parametric content (α@β)

def Semantics.TypeTheoretic.Parametric.combine {A : Type u_1} {B : Type u_2} (f : Parametric (A → B)) (x : Parametric A) : Parametric B

Combine two parametric contents via function application.

Equations

• f.combine x = { Bg := f.Bg × x.Bg, fg := fun (x_1 : f.Bg × x.Bg) => match x_1 with | (bf, bx) => f.fg bf (x.fg bx) }

theorem Semantics.TypeTheoretic.Parametric.combine_trivial {A : Type u_1} {B : Type u_2} (f : A → B) (a : A) : (trivial f).combine (trivial a) = { Bg := Unit × Unit, fg := fun (x : Unit × Unit) => match x with | (fst, snd) => f a }

Combining trivial parametric contents is trivial.

inductive Semantics.TypeTheoretic.Ind4 : Type

Extended individuals for Ch4.

• dudamel : Ind4
• beethoven : Ind4
• uchida : Ind4
• sam : Ind4

@[implicit_reducible]

instance Semantics.TypeTheoretic.instReprInd4 : Repr Ind4

Equations

• Semantics.TypeTheoretic.instReprInd4 = { reprPrec := Semantics.TypeTheoretic.instReprInd4.repr }

def Semantics.TypeTheoretic.instReprInd4.repr : Ind4 → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.TypeTheoretic.instDecidableEqInd4 : DecidableEq Ind4

Equations

• Semantics.TypeTheoretic.instDecidableEqInd4 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Semantics.TypeTheoretic.Conductor4 : Ind4 → Type

• mk : Conductor4 Ind4.dudamel

inductive Semantics.TypeTheoretic.Composer4 : Ind4 → Type

• mk : Composer4 Ind4.beethoven

inductive Semantics.TypeTheoretic.Pianist4 : Ind4 → Type

• mk : Pianist4 Ind4.uchida

inductive Semantics.TypeTheoretic.Leaves4 : Ind4 → Type

• mk : Leaves4 Ind4.sam

@[implicit_reducible]

instance Semantics.TypeTheoretic.instHasNamedInd4 : HasNamed Ind4

Equations

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

def Semantics.TypeTheoretic.samContext : NameContext Ind4 "Sam"

Equations

• Semantics.TypeTheoretic.samContext = { individual := Semantics.TypeTheoretic.Ind4.sam, isNamed := trivial }

def Semantics.TypeTheoretic.samPQuant : PQuant Ind4

Equations

• Semantics.TypeTheoretic.samPQuant = Semantics.TypeTheoretic.semPropNameP "Sam"

theorem Semantics.TypeTheoretic.sam_resolves : samPQuant.fg samContext = semPropName Ind4.sam

def Semantics.TypeTheoretic.leavePPpty : PPpty Ind4

Equations

• Semantics.TypeTheoretic.leavePPpty = Semantics.TypeTheoretic.semIntransVerbP Unit Semantics.TypeTheoretic.Leaves4

def Semantics.TypeTheoretic.samLeaves : Parametric Type

Equations

• Semantics.TypeTheoretic.samLeaves = Semantics.TypeTheoretic.Parametric.combine Semantics.TypeTheoretic.samPQuant Semantics.TypeTheoretic.leavePPpty

theorem Semantics.TypeTheoretic.samLeaves_resolved : samLeaves.fg (samContext, ()) = Leaves4 Ind4.sam

def Semantics.TypeTheoretic.samLeavesTrue : samLeaves.fg (samContext, ())

Equations

• Semantics.TypeTheoretic.samLeavesTrue = Semantics.TypeTheoretic.Leaves4.mk

Paderewski puzzle in the fragment

inductive Semantics.TypeTheoretic.PadInd : Type

• paderewski : PadInd

@[implicit_reducible]

instance Semantics.TypeTheoretic.instReprPadInd : Repr PadInd

Equations

• Semantics.TypeTheoretic.instReprPadInd = { reprPrec := Semantics.TypeTheoretic.instReprPadInd.repr }

def Semantics.TypeTheoretic.instReprPadInd.repr : PadInd → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.TypeTheoretic.instDecidableEqPadInd : DecidableEq PadInd

Equations

• Semantics.TypeTheoretic.instDecidableEqPadInd x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Semantics.TypeTheoretic.IsPianist : PadInd → Prop

• mk : IsPianist PadInd.paderewski

inductive Semantics.TypeTheoretic.IsStatesman : PadInd → Prop

• mk : IsStatesman PadInd.paderewski

def Semantics.TypeTheoretic.peterTwoConcept : TwoConcept PadInd IsPianist IsStatesman

Equations

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

def Semantics.TypeTheoretic.peterOneConcept : OneConcept PadInd IsPianist IsStatesman

Equations

• Semantics.TypeTheoretic.peterOneConcept = Semantics.TypeTheoretic.peterTwoConcept.merge Semantics.TypeTheoretic.peterOneConcept._proof_1

theorem Semantics.TypeTheoretic.paderewski_both : IsPianist peterOneConcept.person ∧ IsStatesman peterOneConcept.person

Pronoun resolution

def Semantics.TypeTheoretic.samAssignment : Assgnmnt Ind4

Equations

• Semantics.TypeTheoretic.samAssignment 0 = some Semantics.TypeTheoretic.Ind4.sam
• Semantics.TypeTheoretic.samAssignment i = none

theorem Semantics.TypeTheoretic.pronoun_resolves_to_sam : semPron.fg Ind4.sam = semPropName Ind4.sam

§5.2–5.3 Common nouns, individual concepts, and the Partee puzzle

§5.4 Frames as records

structure Semantics.TypeTheoretic.AmbTempFrame (Loc : Type) (temp : Loc → ℕ → Prop) : Type

Ambient temperature frame. §5.4, (14).

• x : ℕ
• loc : Loc
• constraint : temp self.loc self.x

@[reducible, inline]

abbrev Semantics.TypeTheoretic.Scale (Frame : Type) : Type

A scale maps frames to natural numbers.

Equations

• Semantics.TypeTheoretic.Scale Frame = (Frame → ℕ)

def Semantics.TypeTheoretic.ζ_temp {Loc : Type} {temp : Loc → ℕ → Prop} : Scale (AmbTempFrame Loc temp)

The canonical temperature scale.

Equations

• Semantics.TypeTheoretic.ζ_temp r = r.x

Rise events

structure Semantics.TypeTheoretic.RiseEvent (Frame : Type) (scale : Scale Frame) : Type

A rise event for a given frame type and scale.

• before : Frame
• after : Frame
• rises : scale self.before < scale self.after

@[reducible, inline]

abbrev Semantics.TypeTheoretic.TempRiseEvent {Loc : Type} {temp : Loc → ℕ → Prop} : Type

Equations

• Semantics.TypeTheoretic.TempRiseEvent = Semantics.TypeTheoretic.RiseEvent (Semantics.TypeTheoretic.AmbTempFrame Loc temp) Semantics.TypeTheoretic.ζ_temp

§5.5 Individual-level vs frame-level properties

@[reducible, inline]

abbrev Semantics.TypeTheoretic.IndPpty (E : Type) : Type 1

Individual-level property.

Equations

• Semantics.TypeTheoretic.IndPpty E = Semantics.TypeTheoretic.Ppty E

@[reducible, inline]

abbrev Semantics.TypeTheoretic.FramePpty (Frame : Type) : Type 1

Frame-level property.

Equations

• Semantics.TypeTheoretic.FramePpty Frame = (Frame → Type)

@[reducible, inline]

abbrev Semantics.TypeTheoretic.Bot : Type

The bottom type: no witnesses.

Equations

• Semantics.TypeTheoretic.Bot = Empty

def Semantics.TypeTheoretic.framePptyOnInd {E Frame : Type} (_p : FramePpty Frame) (_x : E) : Type

Applying a frame-level property to a non-frame yields ⊥.

Equations

• Semantics.TypeTheoretic.framePptyOnInd _p _x = Semantics.TypeTheoretic.Bot

theorem Semantics.TypeTheoretic.partee_blocked {Loc : Type} {temp : Loc → ℕ → Prop} (n : ℕ) (rising : FramePpty (AmbTempFrame Loc temp)) : framePptyOnInd rising n = Bot

Partee puzzle resolution: "ninety is rising" is type-inappropriate.

§5.6 Definite descriptions as dynamic generalized quantifiers

def Semantics.TypeTheoretic.unique {E : Type} (P : Ppty E) : Prop

Uniqueness predicate: exactly one witness of type P.

Equations

• Semantics.TypeTheoretic.unique P = ∃ (x : E), Nonempty (P x) ∧ ∀ (y : E), Nonempty (P y) → y = x

def Semantics.TypeTheoretic.semUniversal {E : Type} (restr scope : Ppty E) : Type

Universal quantifier as a type.

Equations

• Semantics.TypeTheoretic.semUniversal restr scope = ((x : E) → restr x → scope x)

def Semantics.TypeTheoretic.semDefArt {E : Type} (restr scope : Ppty E) : Type

The definite article as a type.

Equations

• Semantics.TypeTheoretic.semDefArt restr scope = (Semantics.TypeTheoretic.propT (Semantics.TypeTheoretic.unique restr) × Semantics.TypeTheoretic.semUniversal restr scope)

def Semantics.TypeTheoretic.defArt_entails_universal {E : Type} (P Q : Ppty E) (h : semDefArt P Q) : semUniversal P Q

The definite article entails the universal.

Equations

• Semantics.TypeTheoretic.defArt_entails_universal P Q h = h.2

def Semantics.TypeTheoretic.unique_and_universal_gives_defArt {E : Type} (P Q : Ppty E) (hu : unique P) (hf : semUniversal P Q) : semDefArt P Q

Uniqueness and universality together give the definite article.

Equations

• Semantics.TypeTheoretic.unique_and_universal_gives_defArt P Q hu hf = ({ down := hu }, hf)

§5.6 Fixed-point types (ℱ)

def Semantics.TypeTheoretic.FixedPtType {E : Type} (P : Ppty E) : Type

Fixed-point type of an individual-level property.

Equations

• Semantics.TypeTheoretic.FixedPtType P = ((x : E) × P x)

theorem Semantics.TypeTheoretic.fixedPtType_sigma {E : Type} (P : Ppty E) : FixedPtType P = ((x : E) × P x)

§5.7 Individual vs frame level nouns

def Semantics.TypeTheoretic.FrameType {E : Type} (p : Ppty E) : Type

FrameType maps a predicate to its fixed-point type.

Equations

• Semantics.TypeTheoretic.FrameType p = Semantics.TypeTheoretic.FixedPtType p

def Semantics.TypeTheoretic.pFrame {E : Type} (p : Ppty E) : FramePpty (FrameType p)

A frame-level version of an individual-level predicate.

Equations

• Semantics.TypeTheoretic.pFrame p frame = p frame.fst

theorem Semantics.TypeTheoretic.pFrame_reduces {E : Type} (p : Ppty E) (x : E) (e : p x) : pFrame p ⟨x, e⟩ = p x

def Semantics.TypeTheoretic.frameType_subtype {E : Type} (p : Ppty E) (r : FrameType p) : p r.fst

Equations

• Semantics.TypeTheoretic.frameType_subtype p r = r.snd

def Semantics.TypeTheoretic.frame_implies_fixedPt {E : Type} (p : Ppty E) (r : FrameType p) (_e : pFrame p r) : p r.fst

Equations

• Semantics.TypeTheoretic.frame_implies_fixedPt p r _e = r.snd

RestrictCommonNoun

def Semantics.TypeTheoretic.restrictPpty {E : Type} (P T : Ppty E) : Ppty E

Restrict a property to a subtype.

Equations

• Semantics.TypeTheoretic.restrictPpty P T x = (P x × T x)

def Semantics.TypeTheoretic.restrictPpty_strengthens {E : Type} (P T : Ppty E) (x : E) (h : restrictPpty P T x) : P x

Equations

• Semantics.TypeTheoretic.restrictPpty_strengthens P T x h = h.1

§5.8 Passengers and ships

structure Semantics.TypeTheoretic.TravelFrame (Loc : Type) : Type

A travel frame.

• source : Loc
• goal : Loc

@[implicit_reducible]

instance Semantics.TypeTheoretic.instDecidableEqTravelFrame {Loc✝ : Type} [DecidableEq Loc✝] : DecidableEq (TravelFrame Loc✝)

Equations

• Semantics.TypeTheoretic.instDecidableEqTravelFrame = Semantics.TypeTheoretic.instDecidableEqTravelFrame.decEq

def Semantics.TypeTheoretic.instDecidableEqTravelFrame.decEq {Loc✝ : Type} [DecidableEq Loc✝] (x✝ x✝¹ : TravelFrame Loc✝) : Decidable (x✝ = x✝¹)

Equations

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

structure Semantics.TypeTheoretic.PassengerFrame (E Loc : Type) (passenger : E → Prop) (take_journey : E → TravelFrame Loc → Prop) : Type

A passenger frame.

• x : E
• isPassenger : passenger self.x
• journey : TravelFrame Loc
• takesJourney : take_journey self.x self.journey

def Semantics.TypeTheoretic.intransVerbFrame {E Frame : Type} (getInd : Frame → E) (p : E → Type) : FramePpty Frame

IntransVerbIndToFrame.

Equations

• Semantics.TypeTheoretic.intransVerbFrame getInd p frame = p (getInd frame)

Plural predicates

def Semantics.TypeTheoretic.pluralPred {E : Type} (p : E → Type) (A : E → Prop) : Type

A plural (distributive) predicate.

Equations

• Semantics.TypeTheoretic.pluralPred p A = ((a : E) → A a → p a)

def Semantics.TypeTheoretic.pluralPred_entails_each {E : Type} (p : E → Type) (A : E → Prop) (h : pluralPred p A) (a : E) (ha : A a) : p a

Equations

• Semantics.TypeTheoretic.pluralPred_entails_each p A h a ha = h a ha

Proper parts of records (mereology)

structure Semantics.TypeTheoretic.IsProperPart (R₁ R₂ : Type) : Type

A projection from record type R₂ to R₁ witnesses that R₁ is a "part" of R₂.

• project : R₂ → R₁
• notIso : ¬Function.Bijective self.project

def Semantics.TypeTheoretic.passengerToInd {E Loc : Type} {passenger : E → Prop} {take_journey : E → TravelFrame Loc → Prop} : PassengerFrame E Loc passenger take_journey → E

Equations

• Semantics.TypeTheoretic.passengerToInd pf = pf.x

theorem Semantics.TypeTheoretic.same_person_different_journeys {E Loc : Type} {passenger : E → Prop} {take_journey : E → TravelFrame Loc → Prop} (pf₁ pf₂ : PassengerFrame E Loc passenger take_journey) (_hx : pf₁.x = pf₂.x) (hj : pf₁.journey ≠ pf₂.journey) : pf₁ ≠ pf₂

Two different passenger frames can project to the same individual.

Copula variants

def Semantics.TypeTheoretic.semBeID {E : Type} (x y : E) : Type

SemBe_ID: identity for individuals.

Equations

• Semantics.TypeTheoretic.semBeID x y = Semantics.TypeTheoretic.propT (x = y)

def Semantics.TypeTheoretic.semBeScalar {Frame : Type} (scale : Scale Frame) (frame : Frame) (n : ℕ) : Type

SemBe_scalar: scalar identity via a scale function.

Equations

• Semantics.TypeTheoretic.semBeScalar scale frame n = Semantics.TypeTheoretic.propT (scale frame = n)

inductive Semantics.TypeTheoretic.TempLoc : Type

• chicago : TempLoc
• stLouis : TempLoc

@[implicit_reducible]

instance Semantics.TypeTheoretic.instReprTempLoc : Repr TempLoc

Equations

• Semantics.TypeTheoretic.instReprTempLoc = { reprPrec := Semantics.TypeTheoretic.instReprTempLoc.repr }

def Semantics.TypeTheoretic.instReprTempLoc.repr : TempLoc → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.TypeTheoretic.instDecidableEqTempLoc : DecidableEq TempLoc

Equations

• Semantics.TypeTheoretic.instDecidableEqTempLoc x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.TypeTheoretic.tempAt : TempLoc → ℕ → Prop

Equations

• Semantics.TypeTheoretic.tempAt _loc _x = True

@[reducible, inline]

abbrev Semantics.TypeTheoretic.ConcreteTempFrame : Type

Equations

• Semantics.TypeTheoretic.ConcreteTempFrame = Semantics.TypeTheoretic.AmbTempFrame Semantics.TypeTheoretic.TempLoc Semantics.TypeTheoretic.tempAt

def Semantics.TypeTheoretic.chicago90 : ConcreteTempFrame

Equations

• Semantics.TypeTheoretic.chicago90 = { x := 90, loc := Semantics.TypeTheoretic.TempLoc.chicago, constraint := trivial }

def Semantics.TypeTheoretic.chicago95 : ConcreteTempFrame

Equations

• Semantics.TypeTheoretic.chicago95 = { x := 95, loc := Semantics.TypeTheoretic.TempLoc.chicago, constraint := trivial }

def Semantics.TypeTheoretic.tempRising : RiseEvent ConcreteTempFrame ζ_temp

Equations

• Semantics.TypeTheoretic.tempRising = { before := Semantics.TypeTheoretic.chicago90, after := Semantics.TypeTheoretic.chicago95, rises := Semantics.TypeTheoretic.tempRising._proof_1 }

theorem Semantics.TypeTheoretic.temp_is_ninety : ζ_temp chicago90 = 90

theorem Semantics.TypeTheoretic.ninety_not_a_frame : framePptyOnInd (fun (x : ConcreteTempFrame) => PUnit.{1}) 90 = Bot

"The dog is Fido" vs "The temperature is ninety"

inductive Semantics.TypeTheoretic.Dog5 : Ind4 → Type

• fido : Dog5 Ind4.sam

def Semantics.TypeTheoretic.dogIsFido : semBeID Ind4.sam Ind4.sam

Equations

• Semantics.TypeTheoretic.dogIsFido = { down := ⋯ }

def Semantics.TypeTheoretic.tempIsNinety : semBeScalar ζ_temp chicago90 90

Equations

• Semantics.TypeTheoretic.tempIsNinety = { down := Semantics.TypeTheoretic.tempIsNinety._proof_1 }

Definite article phenomena

theorem Semantics.TypeTheoretic.dogUnique : unique Dog5

def Semantics.TypeTheoretic.theDogLeft : semDefArt Dog5 Leaves4

Equations

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

Fixed-point type phenomena

def Semantics.TypeTheoretic.fidoDogFrame : FixedPtType Dog5

Equations

• Semantics.TypeTheoretic.fidoDogFrame = ⟨Semantics.TypeTheoretic.Ind4.sam, Semantics.TypeTheoretic.Dog5.fido⟩

def Semantics.TypeTheoretic.fixedPt_witness_satisfies : Dog5 fidoDogFrame.fst

Equations

• Semantics.TypeTheoretic.fixedPt_witness_satisfies = Semantics.TypeTheoretic.fidoDogFrame.snd

Passenger individuation

def Semantics.TypeTheoretic.isPassenger5 : Ind4 → Prop

Equations

• Semantics.TypeTheoretic.isPassenger5 x✝ = True

def Semantics.TypeTheoretic.takesJourney5 : Ind4 → TravelFrame TempLoc → Prop

Equations

• Semantics.TypeTheoretic.takesJourney5 x✝¹ x✝ = True

def Semantics.TypeTheoretic.journey1 : TravelFrame TempLoc

Equations

• Semantics.TypeTheoretic.journey1 = { source := Semantics.TypeTheoretic.TempLoc.chicago, goal := Semantics.TypeTheoretic.TempLoc.stLouis }

def Semantics.TypeTheoretic.journey2 : TravelFrame TempLoc

Equations

• Semantics.TypeTheoretic.journey2 = { source := Semantics.TypeTheoretic.TempLoc.stLouis, goal := Semantics.TypeTheoretic.TempLoc.chicago }

def Semantics.TypeTheoretic.samPassenger1 : PassengerFrame Ind4 TempLoc isPassenger5 takesJourney5

Equations

• Semantics.TypeTheoretic.samPassenger1 = { x := Semantics.TypeTheoretic.Ind4.sam, isPassenger := trivial, journey := Semantics.TypeTheoretic.journey1, takesJourney := trivial }

def Semantics.TypeTheoretic.samPassenger2 : PassengerFrame Ind4 TempLoc isPassenger5 takesJourney5

Equations

• Semantics.TypeTheoretic.samPassenger2 = { x := Semantics.TypeTheoretic.Ind4.sam, isPassenger := trivial, journey := Semantics.TypeTheoretic.journey2, takesJourney := trivial }

theorem Semantics.TypeTheoretic.passenger_individuation : samPassenger1.x = samPassenger2.x ∧ samPassenger1 ≠ samPassenger2

Questions as Dependent Types

[Gin12]

In TTR, a question is a function from a record type to a type — essentially a dependent function (x : R) → T(x). A polar question is a proposition (0-ary: no open parameters). A wh-question has open parameters: "Who runs?" is λ (x : Ind) => Run(x).

An answer to a question Q : R → Type is a witness ⟨r, Q r⟩ — a record r together with evidence that Q r is inhabited.

This connects to KOS: the DGB's QUD can be typed as TTRQuestion E, and Answerhood can be instantiated so that a fact resolves a question when it provides a witness.

structure Semantics.TypeTheoretic.TTRQuestion (R : Type) : Type 1

A TTR question: a dependent type over a domain.

[Gin12] Ch. 4: "A question is a function from a (possibly empty) record type to a type." Polar questions have R = Unit; wh-questions have R = the domain of quantification.

• body : R → Type

  The body of the question: maps each possible answer to its content type

structure Semantics.TypeTheoretic.TTRAnswer (R : Type) (q : TTRQuestion R) : Type

A complete answer to a TTR question: a witness.

• witness : R

  The answer value

• evidence : q.body self.witness

  Evidence that the answer satisfies the question body

def Semantics.TypeTheoretic.TTRQuestion.polar (P : Type) : TTRQuestion Unit

A polar question: no open parameters, just a proposition.

Equations

• Semantics.TypeTheoretic.TTRQuestion.polar P = { body := fun (x : Unit) => P }

def Semantics.TypeTheoretic.TTRQuestion.wh {E : Type} (P : E → Type) : TTRQuestion E

A wh-question: "Which x satisfies P?"

Equations

• Semantics.TypeTheoretic.TTRQuestion.wh P = { body := P }

def Semantics.TypeTheoretic.TTRQuestion.isResolved {R : Type} (q : TTRQuestion R) : Prop

A question is resolved when a witness exists.

Equations

• q.isResolved = ∃ (r : R), Nonempty (q.body r)

theorem Semantics.TypeTheoretic.TTRQuestion.polar_resolved_iff (P : Type) : (polar P).isResolved ↔ Nonempty P

A polar question is resolved iff the proposition is inhabited.

theorem Semantics.TypeTheoretic.TTRQuestion.wh_resolved_iff {E : Type} (P : E → Type) : (wh P).isResolved ↔ ∃ (e : E), Nonempty (P e)

A wh-question is resolved iff some entity satisfies the predicate.

def Semantics.TypeTheoretic.Parametric.toTTRQuestion (p : Parametric Type) : TTRQuestion p.Bg

Bridge: TTR parametric content (Parametric) as a question.

A Parametric T has background type Bg and foreground Bg → T. When T = Type, this IS a TTR question: each background value determines a type (the question's content at that resolution).

Equations

• p.toTTRQuestion = { body := p.fg }

Austinian Propositions for Discourse

[Gin12] [BP83]

§6.5 defines TrueAustinianProp as a situation–type pair that carries its own witness (always true by construction). This suffices for truth-conditional semantics but not for discourse: when A asserts "Bo is here", the content enters FACTS as a checkable claim that can be true or false.

[Gin12] Ch. 4 uses Austinian propositions as the content type for DGB FACTS. The key difference: the situation and type are independent — the proposition is true iff the situation satisfies the type, but this need not hold.

CheckableAustinian separates the situation from the classifying predicate, enabling:

1. Propositions that can be false (sit doesn't satisfy the type)
2. A bridge to (W → Bool) for HasContextSet integration
3. DGB FACTS typed as checkable Austinian propositions

structure Semantics.TypeTheoretic.CheckableAustinian (S : Type) : Type

A checkable Austinian proposition: situation + classifying predicate.

Unlike TrueAustinianProp (which carries its own witness), a CheckableAustinian separates the situation from the predicate, so it can be false.

[Gin12] Ch. 4: [sit = s, sit-type = T] where truth requires s : T. [BP83]: situation supports a type.

• sit : S

  The situation being classified

• sitType : S → Prop

  The classifying predicate (situation type)

def Semantics.TypeTheoretic.CheckableAustinian.isTrue {S : Type} (p : CheckableAustinian S) : Prop

A checkable Austinian proposition is true iff the situation satisfies the type.

Equations

• p.isTrue = p.sitType p.sit

def Semantics.TypeTheoretic.CheckableAustinian.isFalse {S : Type} (p : CheckableAustinian S) : Prop

A checkable Austinian proposition is false iff the situation doesn't satisfy the type.

Equations

• p.isFalse = ¬p.sitType p.sit

structure Semantics.TypeTheoretic.BCheckableAustinian (S : Type) : Type

Decidable variant for computational use.

• sit : S
• sitType : S → Bool

def Semantics.TypeTheoretic.BCheckableAustinian.isTrue {S : Type} (p : BCheckableAustinian S) : Bool

Decidable truth check.

Equations

• p.isTrue = p.sitType p.sit

def Semantics.TypeTheoretic.BCheckableAustinian.toBProp {S : Type} (p : BCheckableAustinian S) : S → Bool

Convert a decidable Austinian to S → Bool: evaluate at each world/situation.

Equations

• p.toBProp = p.sitType

theorem Semantics.TypeTheoretic.BCheckableAustinian.toBProp_at_sit {S : Type} (p : BCheckableAustinian S) (h : p.isTrue = true) : p.toBProp p.sit = true

A true Austinian proposition's toBProp holds at its situation.