KOS over Austinian Propositions

@cite{ginzburg-2012} @cite{cooper-2023}

The TTR-typed instantiation of KOS substrate. LocProp ⊐ TTRSign is already structural in KOS/Defs.lean (via LocProp.toTTRSign and the SubtypeOf instance) — this file is not a "bridge" but a worked instantiation pattern: how do we exercise the KOS conversational rules when facts are TTR Austinian propositions and questions are TTR question-bodies?

Contents

• §1. TTRQuestionB — a Bool-valued TTR question (decidable variant of the Type 1 TTRQuestion), needed because DGB requires QContent : Type.
• §2. Austinian-fact DGB/TIS aliases (AustinianDGB, AustinianTIS).
• §3. The austinianSupport instance — a BCheckableAustinian resolves a TTRQuestionB when the situation that makes the fact true also satisfies the question body (Ch. 4).
• §4. A worked Austinian inquiry-cycle example over a tiny Weather situation type.

The Cooper-2023 ↔ Ginzburg-2012 genealogical bridge (tisToInfoState) lives in the sibling KOS/CooperInfoState.lean.

structure Dialogue.KOS.Austinian.TTRQuestionB (R : Type) : Type

A Bool-valued TTR question: stays in Type 0 for DGB compatibility.

TTRQuestion R (from TypeTheoretic/Discourse.lean) has body : R → Type, placing it in Type 1. Since DGB requires QContent : Type, we provide a decidable variant where the question body is Bool-valued.

The correspondence: TTRQuestionB R is to TTRQuestion R as Prop' W is to W → Prop — the decidable/computable variant of the same concept.

• body : R → Bool

  The decidable question body

• name : String

  Name for display

def Dialogue.KOS.Austinian.TTRQuestionB.polar (p : Bool) (name : String := "") : TTRQuestionB Unit

A polar Bool-question: is P true?

Equations

• Dialogue.KOS.Austinian.TTRQuestionB.polar p name = { body := fun (x : Unit) => p, name := name }

def Dialogue.KOS.Austinian.TTRQuestionB.wh {R : Type} (body : R → Bool) (name : String := "") : TTRQuestionB R

A wh-question: which x satisfies P?

Equations

• Dialogue.KOS.Austinian.TTRQuestionB.wh body name = { body := body, name := name }

def Dialogue.KOS.Austinian.TTRQuestionB.isResolved {R : Type} (q : TTRQuestionB R) (domain : List R) : Bool

A Bool-question is resolved when some element satisfies the body.

Equations

• q.isResolved domain = domain.any q.body

@[reducible, inline]

abbrev Dialogue.KOS.Austinian.AustinianDGB (S R Cont : Type) : Type

A DGB whose facts are checkable Austinian propositions and whose QUD entries are Bool-valued TTR questions. The Cont parameter governs the LocProp content type for pending and qud (use Unit if Pending is unused; use BCheckableAustinian S for full TTR-typed CRification).

@cite{ginzburg-2012} Ch. 4: FACTS is a set of Austinian propositions [sit = s, sit-type = T]. QUD is a poset of questions.

Equations

• Dialogue.KOS.Austinian.AustinianDGB S R Cont = Dialogue.KOS.DGB String (Semantics.TypeTheoretic.BCheckableAustinian S) (Dialogue.KOS.Austinian.TTRQuestionB R) Cont

@[reducible, inline]

abbrev Dialogue.KOS.Austinian.AustinianTIS (S R Cont : Type) : Type

A TIS with Austinian content types.

Equations

• Dialogue.KOS.Austinian.AustinianTIS S R Cont = Dialogue.KOS.TIS String (Semantics.TypeTheoretic.BCheckableAustinian S) (Dialogue.KOS.Austinian.TTRQuestionB R) Cont

@[implicit_reducible]

instance Dialogue.KOS.Austinian.austinianSupport (S : Type) : Core.Question.DecidableSupport (Semantics.TypeTheoretic.BCheckableAustinian S) (TTRQuestionB S)

A BCheckableAustinian S resolves a TTRQuestionB S when the Austinian proposition is true at a situation that satisfies the question body.

@cite{ginzburg-2012} Ch. 4: "q is resolved relative to a DGB dgb iff the FACTS in dgb contextually entail an answer to q."

For a fact ⟨s, T⟩ and question Q: the fact resolves Q when T(s) is true AND Q.body(s) is true — the situation that makes the fact true also answers the question.

Equations

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

inductive Dialogue.KOS.Austinian.Weather : Type

A simple situation type for the example.

• sunny : Weather
• rainy : Weather
• cloudy : Weather

def Dialogue.KOS.Austinian.instReprWeather.repr : Weather → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Dialogue.KOS.Austinian.instReprWeather : Repr Weather

Equations

• Dialogue.KOS.Austinian.instReprWeather = { reprPrec := Dialogue.KOS.Austinian.instReprWeather.repr }

@[implicit_reducible]

instance Dialogue.KOS.Austinian.instDecidableEqWeather : DecidableEq Weather

Equations

• Dialogue.KOS.Austinian.instDecidableEqWeather x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Dialogue.KOS.Austinian.itIsRaining : Semantics.TypeTheoretic.BCheckableAustinian Weather

"It is raining" as an Austinian proposition: situation = rainy, type = isRainy.

Equations

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

theorem Dialogue.KOS.Austinian.itIsRaining_true : itIsRaining.isTrue = true

The Austinian proposition "it is raining" is true (rainy satisfies isRainy).

def Dialogue.KOS.Austinian.isItRaining : TTRQuestionB Weather

"Is it raining?" as a Bool-valued TTR question.

Equations

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

theorem Dialogue.KOS.Austinian.raining_resolves : Core.Question.Support.supports itIsRaining isItRaining

The fact "it is raining" resolves the question "is it raining?": the situation (rainy) makes both the fact true and the question body true.

def Dialogue.KOS.Austinian.itIsSunny : Semantics.TypeTheoretic.BCheckableAustinian Weather

"It is sunny" — an Austinian proposition that does NOT resolve "is it raining?".

Equations

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

theorem Dialogue.KOS.Austinian.sunny_does_not_resolve_raining : ¬Core.Question.Support.supports itIsSunny isItRaining

A true fact about a different situation does not resolve the raining question.

def Dialogue.KOS.Austinian.adgb₀ : AustinianDGB Weather Weather Unit

An empty Austinian DGB. We use Unit for the LocProp content type since this worked example exercises only QUD and FACTS, not the Pending/CRification pipeline.

Equations

• Dialogue.KOS.Austinian.adgb₀ = Dialogue.KOS.DGB.initial

def Dialogue.KOS.Austinian.atis₁ : AustinianTIS Weather Weather Unit

After asking "Is it raining?", QUD has the question (wrapped in InfoStruc).

Equations

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

theorem Dialogue.KOS.Austinian.atis_ask_qud : atis₁.dgb.qud = [InfoStruc.fromQuestion isItRaining]

def Dialogue.KOS.Austinian.atis₂ : AustinianTIS Weather Weather Unit

After asserting "it is raining", the fact resolves the question and QUD empties.

Equations

• Dialogue.KOS.Austinian.atis₂ = Dialogue.KOS.TIS.assertRule Dialogue.KOS.Austinian.atis₁ Dialogue.KOS.Austinian.itIsRaining

theorem Dialogue.KOS.Austinian.atis_assert_resolves : atis₂.dgb.qud = []

theorem Dialogue.KOS.Austinian.atis_has_fact : itIsRaining ∈ atis₂.dgb.facts

The fact is in FACTS after assertion.