inductive Interfaces.SyntaxSemantics.LeftPeriphery.WHFeature : Type

The ±WH feature on C, determining declarative vs interrogative clause type. alphaWH is underspecified — used for Hindi-Urdu simplex polar questions where clause-typing is not forced at CP (@cite{dayal-2025}: §4.4).

• plusWH : WHFeature
• minusWH : WHFeature
• alphaWH : WHFeature

@[implicit_reducible]

instance Interfaces.SyntaxSemantics.LeftPeriphery.instDecidableEqWHFeature : DecidableEq WHFeature

Equations

• Interfaces.SyntaxSemantics.LeftPeriphery.instDecidableEqWHFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Interfaces.SyntaxSemantics.LeftPeriphery.instReprWHFeature : Repr WHFeature

Equations

• Interfaces.SyntaxSemantics.LeftPeriphery.instReprWHFeature = { reprPrec := Interfaces.SyntaxSemantics.LeftPeriphery.instReprWHFeature.repr }

def Interfaces.SyntaxSemantics.LeftPeriphery.instReprWHFeature.repr : WHFeature → ℕ → Std.Format

Equations

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

inductive Interfaces.SyntaxSemantics.LeftPeriphery.SelectionClass : Type

Dayal's classification of embedding predicates by what left-peripheral structure they select. Refines the rogative/responsive split.

• uninterrogative: C_-WH only (believe, think)
• rogativeCP: C_+WH but not PerspP (investigate, depend on)
• rogativePerspP: CP + PerspP (wonder, the question is)
• rogativeSAP: Full structure (ask)
• responsive: C_±WH (know, remember)

• uninterrogative : SelectionClass
• rogativeCP : SelectionClass
• rogativePerspP : SelectionClass
• rogativeSAP : SelectionClass
• responsive : SelectionClass

@[implicit_reducible]

instance Interfaces.SyntaxSemantics.LeftPeriphery.instDecidableEqSelectionClass : DecidableEq SelectionClass

Equations

• Interfaces.SyntaxSemantics.LeftPeriphery.instDecidableEqSelectionClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Interfaces.SyntaxSemantics.LeftPeriphery.instReprSelectionClass.repr : SelectionClass → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Interfaces.SyntaxSemantics.LeftPeriphery.instReprSelectionClass : Repr SelectionClass

Equations

• Interfaces.SyntaxSemantics.LeftPeriphery.instReprSelectionClass = { reprPrec := Interfaces.SyntaxSemantics.LeftPeriphery.instReprSelectionClass.repr }

def Interfaces.SyntaxSemantics.LeftPeriphery.entailsKnowledge (cls : SelectionClass) : Bool

Whether the predicate's at-issue content entails the subject knows Ans(Q). This is the key semantic property that drives PerspP (in)compatibility.

• Responsive predicates (know, remember) entail knowledge at eval time
• Rogative predicates (wonder, ask) do NOT entail knowledge
• Under negation, the knowledge entailment is REMOVED

Equations

• Interfaces.SyntaxSemantics.LeftPeriphery.entailsKnowledge Interfaces.SyntaxSemantics.LeftPeriphery.SelectionClass.responsive = true
• Interfaces.SyntaxSemantics.LeftPeriphery.entailsKnowledge cls = false

def Interfaces.SyntaxSemantics.LeftPeriphery.effectiveKnowledge (cls : SelectionClass) (negated questioned : Bool) : Bool

Whether the knowledge entailment survives in the given syntactic context. Negation and questioning both remove a predicate's knowledge entailment:

• "I don't know Q" does NOT entail knowing Ans(Q)
• "Does she know Q?" does NOT entail knowing Ans(Q)

Equations

• Interfaces.SyntaxSemantics.LeftPeriphery.effectiveKnowledge cls negated questioned = (Interfaces.SyntaxSemantics.LeftPeriphery.entailsKnowledge cls && !negated && !questioned)

def Interfaces.SyntaxSemantics.LeftPeriphery.perspPConsistent (cls : SelectionClass) (negated questioned : Bool) : Bool

PerspectiveP presupposes possible ignorance: ◇¬know(x, Ans(Q)). This is inconsistent with knowing Ans(Q). Consistency holds iff effective knowledge is false.

Note: Consistency is necessary but not sufficient for quasi-subordination. The full account also requires "potentially active" (de se interest), which is why forget doesn't freely quasi-subordinate (@cite{dayal-2025}: §3.3).

Equations

• Interfaces.SyntaxSemantics.LeftPeriphery.perspPConsistent cls negated questioned = !Interfaces.SyntaxSemantics.LeftPeriphery.effectiveKnowledge cls negated questioned

def Interfaces.SyntaxSemantics.LeftPeriphery.allowsQuasiSub (cls : SelectionClass) (negated questioned : Bool) : Bool

Whether a predicate allows quasi-subordination. DERIVED from two independent conditions:

1. The predicate must select PerspP (structural requirement)
2. OR: PerspP is consistent with the predicate's semantics AND the predicate embeds interrogatives (responsive predicates under negation/question)

Equations

• One or more equations did not get rendered due to their size.
• Interfaces.SyntaxSemantics.LeftPeriphery.allowsQuasiSub Interfaces.SyntaxSemantics.LeftPeriphery.SelectionClass.uninterrogative negated questioned = false
• Interfaces.SyntaxSemantics.LeftPeriphery.allowsQuasiSub Interfaces.SyntaxSemantics.LeftPeriphery.SelectionClass.rogativeCP negated questioned = false
• Interfaces.SyntaxSemantics.LeftPeriphery.allowsQuasiSub Interfaces.SyntaxSemantics.LeftPeriphery.SelectionClass.rogativePerspP negated questioned = true
• Interfaces.SyntaxSemantics.LeftPeriphery.allowsQuasiSub Interfaces.SyntaxSemantics.LeftPeriphery.SelectionClass.rogativeSAP negated questioned = true

inductive Interfaces.SyntaxSemantics.LeftPeriphery.EmbedType : Type

The structurally distinct ways an interrogative clause can be embedded.

• subordination : EmbedType
• quasiSubordination : EmbedType
• quotation : EmbedType

@[implicit_reducible]

instance Interfaces.SyntaxSemantics.LeftPeriphery.instDecidableEqEmbedType : DecidableEq EmbedType

Equations

• Interfaces.SyntaxSemantics.LeftPeriphery.instDecidableEqEmbedType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Interfaces.SyntaxSemantics.LeftPeriphery.instReprEmbedType.repr : EmbedType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Interfaces.SyntaxSemantics.LeftPeriphery.instReprEmbedType : Repr EmbedType

Equations

• Interfaces.SyntaxSemantics.LeftPeriphery.instReprEmbedType = { reprPrec := Interfaces.SyntaxSemantics.LeftPeriphery.instReprEmbedType.repr }

def Interfaces.SyntaxSemantics.LeftPeriphery.allowsEmbedding (cls : SelectionClass) (et : EmbedType) (negated questioned : Bool) : Bool

Full embedding prediction.

Equations

• One or more equations did not get rendered due to their size.
• Interfaces.SyntaxSemantics.LeftPeriphery.allowsEmbedding Interfaces.SyntaxSemantics.LeftPeriphery.SelectionClass.uninterrogative et negated questioned = false
• Interfaces.SyntaxSemantics.LeftPeriphery.allowsEmbedding cls Interfaces.SyntaxSemantics.LeftPeriphery.EmbedType.subordination negated questioned = true
• Interfaces.SyntaxSemantics.LeftPeriphery.allowsEmbedding cls Interfaces.SyntaxSemantics.LeftPeriphery.EmbedType.quotation negated questioned = false

theorem Interfaces.SyntaxSemantics.LeftPeriphery.responsive_entails_knowledge : entailsKnowledge SelectionClass.responsive = true

Responsive predicates entail knowledge.

theorem Interfaces.SyntaxSemantics.LeftPeriphery.rogative_no_knowledge : entailsKnowledge SelectionClass.rogativePerspP = false ∧ entailsKnowledge SelectionClass.rogativeSAP = false ∧ entailsKnowledge SelectionClass.rogativeCP = false

Rogative predicates do NOT entail knowledge.

theorem Interfaces.SyntaxSemantics.LeftPeriphery.negation_removes_knowledge : effectiveKnowledge SelectionClass.responsive true false = false

Knowledge entailment is removed by negation.

theorem Interfaces.SyntaxSemantics.LeftPeriphery.question_removes_knowledge : effectiveKnowledge SelectionClass.responsive false true = false

Knowledge entailment is removed by questioning.

theorem Interfaces.SyntaxSemantics.LeftPeriphery.knowledge_blocks_perspP : perspPConsistent SelectionClass.responsive false false = false

PerspP is inconsistent with effective knowledge. This is the core semantic derivation: know(x, Ans(Q)) ∧ ◇¬know(x, Ans(Q)) is a contradiction, so PerspP is blocked.

theorem Interfaces.SyntaxSemantics.LeftPeriphery.no_knowledge_allows_perspP : perspPConsistent SelectionClass.rogativePerspP false false = true ∧ perspPConsistent SelectionClass.rogativeSAP false false = true

Without effective knowledge, PerspP is consistent. Rogatives never entail knowledge → always consistent.

theorem Interfaces.SyntaxSemantics.LeftPeriphery.responsive_rejects_quasi : allowsQuasiSub SelectionClass.responsive false false = false

Responsive predicates reject quasi-subordination in unadorned form. DERIVED: know entails knowledge → contradicts possible ignorance.

theorem Interfaces.SyntaxSemantics.LeftPeriphery.responsive_shifts_under_negation : allowsQuasiSub SelectionClass.responsive true false = true

Under negation, responsives allow quasi-subordination. DERIVED: negation removes knowledge entailment → PerspP consistent. "*I remember [was Henry a communist↑]" vs "I don't remember [was Henry a communist↑]".

theorem Interfaces.SyntaxSemantics.LeftPeriphery.responsive_shifts_under_question : allowsQuasiSub SelectionClass.responsive false true = true

Under questioning, responsives allow quasi-subordination. DERIVED: questioning removes knowledge entailment → PerspP consistent. "Does Sue remember [was Henry a communist↑]"

def Interfaces.SyntaxSemantics.LeftPeriphery.classifyVerb : String → SelectionClass

Classify each verb by string to a selection class.

Equations

• Interfaces.SyntaxSemantics.LeftPeriphery.classifyVerb "investigate" = Interfaces.SyntaxSemantics.LeftPeriphery.SelectionClass.rogativeCP
• Interfaces.SyntaxSemantics.LeftPeriphery.classifyVerb "depend on" = Interfaces.SyntaxSemantics.LeftPeriphery.SelectionClass.rogativeCP
• Interfaces.SyntaxSemantics.LeftPeriphery.classifyVerb "wonder" = Interfaces.SyntaxSemantics.LeftPeriphery.SelectionClass.rogativePerspP
• Interfaces.SyntaxSemantics.LeftPeriphery.classifyVerb "ask" = Interfaces.SyntaxSemantics.LeftPeriphery.SelectionClass.rogativeSAP
• Interfaces.SyntaxSemantics.LeftPeriphery.classifyVerb "know" = Interfaces.SyntaxSemantics.LeftPeriphery.SelectionClass.responsive
• Interfaces.SyntaxSemantics.LeftPeriphery.classifyVerb "believe" = Interfaces.SyntaxSemantics.LeftPeriphery.SelectionClass.uninterrogative
• Interfaces.SyntaxSemantics.LeftPeriphery.classifyVerb x✝ = Interfaces.SyntaxSemantics.LeftPeriphery.SelectionClass.uninterrogative

def Interfaces.SyntaxSemantics.LeftPeriphery.classifyCrossLingVerb : String → SelectionClass

Classify Hindi-Urdu verbs from the cross-linguistic shiftiness data.

Equations

• Interfaces.SyntaxSemantics.LeftPeriphery.classifyCrossLingVerb "ja:n-na: ca:h-na: (want to know)" = Interfaces.SyntaxSemantics.LeftPeriphery.SelectionClass.rogativePerspP
• Interfaces.SyntaxSemantics.LeftPeriphery.classifyCrossLingVerb "ja:n-na: (know)" = Interfaces.SyntaxSemantics.LeftPeriphery.SelectionClass.responsive
• Interfaces.SyntaxSemantics.LeftPeriphery.classifyCrossLingVerb x✝ = Interfaces.SyntaxSemantics.LeftPeriphery.SelectionClass.responsive

H1. Derive SelectionClass from VerbEntry

Instead of classifying verbs by string matching (classifyVerb "know" =>.responsive), we derive the selection class from the primitive fields already encoded in each VerbEntry: factivePresup, speechActVerb, opaqueContext, complementType, attitude, takesQuestionBase.

def Interfaces.SyntaxSemantics.LeftPeriphery.deriveSelectionClass (v : Fragments.English.Predicates.Verbal.VerbEntry) : SelectionClass

Derive the left-peripheral selection class from a VerbEntry's structural properties. This replaces ad-hoc string-based classification with a principled derivation from the verb's primitive semantic fields.

The logic:

• Factives are responsive (knowledge-entailing)
• Non-veridical doxastic attitudes are uninterrogative
• Speech-act verbs that take questions are rogativeSAP (speech-act layer)
• Opaque-context verbs that take questions are rogativePerspP (perspective layer)
• Other question-taking verbs are rogativeCP (CP layer only)
• Everything else is uninterrogative

Equations

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

theorem Interfaces.SyntaxSemantics.LeftPeriphery.derived_class_matches_manual : deriveSelectionClass Fragments.English.Predicates.Verbal.know = classifyVerb "know" ∧ deriveSelectionClass Fragments.English.Predicates.Verbal.wonder = classifyVerb "wonder" ∧ deriveSelectionClass Fragments.English.Predicates.Verbal.ask = classifyVerb "ask" ∧ deriveSelectionClass Fragments.English.Predicates.Verbal.investigate = classifyVerb "investigate" ∧ deriveSelectionClass Fragments.English.Predicates.Verbal.believe = classifyVerb "believe"

The structurally derived classification matches the manually-assigned string-based classification for all verbs in the embedding data.

H2. Compositional PerspP via possible ignorance

PerspP introduces a not-at-issue presupposition: the perspectival center possibly doesn't know the answer to the question. We formalize this using diaAt (existential modal, ◇) from Doxastic.lean and QUD.ans from Core/Question/Partition/Cells.lean.

def Interfaces.SyntaxSemantics.LeftPeriphery.possibleIgnorance {W : Type u_1} {E : Type u_2} (R : Semantics.Attitudes.Doxastic.AccessRel W E) (center : E) (Q : Semantics.Questions.GSQuestion W) (w : W) (worlds : List W) : Prop

Whether x possibly doesn't know Ans(Q) at world w: ◇¬know(x, Ans(Q)) = ∃w' ∈ R(x,w). ¬(Ans(Q,w) holds at w')

This is PerspP's not-at-issue presupposition (@cite{dayal-2025}: §2.3). Uses diaAt from Doxastic.lean and QUD.ans from Core/Question/Partition/Cells.lean.

Equations

• Interfaces.SyntaxSemantics.LeftPeriphery.possibleIgnorance R center Q w worlds = Semantics.Attitudes.Doxastic.diaAt R center w worlds fun (w' : W) => QUD.ans Q w w' = false

structure Interfaces.SyntaxSemantics.LeftPeriphery.PerspPResult (W : Type u_1) : Type u_1

PerspP as a presuppositional question denotation. At-issue: the question Q itself. Not-at-issue presupposition: ◇¬know(center, Ans(Q)).

• question : Core.Question W

  The at-issue question content (unchanged by PerspP)

• presupSatisfied : Prop

  Whether the possible-ignorance presupposition is satisfied

def Interfaces.SyntaxSemantics.LeftPeriphery.applyPerspP {W : Type u_1} {E : Type u_2} (R : Semantics.Attitudes.Doxastic.AccessRel W E) (center : E) (Q : Semantics.Questions.GSQuestion W) (w : W) (worlds : List W) (hamblinQ : Core.Question W) : PerspPResult W

Apply PerspP to a question: checks possible-ignorance presupposition.

Equations

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

H3. Veridical predicates block PerspP

The key compositional derivation: a veridical doxastic predicate that holds at Q entails □(Ans(Q)), which contradicts ◇¬(Ans(Q)). Therefore PerspP's possible-ignorance presupposition is inconsistent with responsive predicates in bare (non-negated, non-questioned) contexts.

theorem Interfaces.SyntaxSemantics.LeftPeriphery.box_excludes_dia_neg {W : Type u_1} {E : Type u_2} (R : Semantics.Attitudes.Doxastic.AccessRel W E) (agent : E) (w : W) (worlds : List W) (p : W → Prop) (hBox : Semantics.Attitudes.Doxastic.boxAt R agent w worlds p) : ¬Semantics.Attitudes.Doxastic.diaAt R agent w worlds fun (w' : W) => ¬p w'

box and dia are duals: □p → ¬◇¬p. If p holds at all accessible worlds, there is no accessible world where ¬p.

theorem Interfaces.SyntaxSemantics.LeftPeriphery.veridical_question_entails_box_ans {W : Type u_1} {E : Type u_2} (V : Semantics.Attitudes.Doxastic.DoxasticPredicate W E) (_hV : V.veridicality = Features.Veridicality.veridical) (agent : E) (Q : Semantics.Questions.GSQuestion W) (w : W) (worlds : List W) (hHolds : Semantics.Attitudes.Doxastic.boxAt V.access agent w worlds fun (w' : W) => QUD.ans Q w w' = true) : ¬Semantics.Attitudes.Doxastic.diaAt V.access agent w worlds fun (w' : W) => QUD.ans Q w w' = false

A veridical doxastic predicate entails the subject believes Ans(Q). "x knows Q" at w means there exists a true answer p that x box-believes. In particular, x box-believes Ans(Q,w) (the complete answer at w).

TODO: Full proof requires showing that holdsAtQuestion with the G&S-derived Hamblin denotation implies boxAt for Ans(Q,w). The key step is: holdsAtQuestion finds some true p that x box-believes; since the question is a partition, that p determines the same cell as Ans(Q,w).

theorem Interfaces.SyntaxSemantics.LeftPeriphery.veridical_blocks_perspP {W : Type u_1} {E : Type u_2} (V : Semantics.Attitudes.Doxastic.DoxasticPredicate W E) (hV : V.veridicality = Features.Veridicality.veridical) (agent : E) (Q : Semantics.Questions.GSQuestion W) (w : W) (worlds : List W) (hBox : Semantics.Attitudes.Doxastic.boxAt V.access agent w worlds fun (w' : W) => QUD.ans Q w w' = true) : ¬possibleIgnorance V.access agent Q w worlds

Therefore PerspP's possible-ignorance presupposition is inconsistent with a veridical predicate that box-knows Ans(Q).

This is the compositional explanation for why responsive predicates (know, remember) reject quasi-subordination: their knowledge entailment □(Ans(Q)) contradicts PerspP's ◇¬(Ans(Q)).

H4. Bridge theorems

Connect the compositional semantics (veridicality, box/dia) to the Boolean predicates (entailsKnowledge, perspPConsistent). This shows the Boolean predicates are correct because they track the compositional story.

def Interfaces.SyntaxSemantics.LeftPeriphery.verbEntryIsVeridical (v : Fragments.English.Predicates.Verbal.VerbEntry) : Bool

Factive verbs correspond to veridical doxastic predicates. This is the structural link: factivePresup determines veridicality.

Equations

• Interfaces.SyntaxSemantics.LeftPeriphery.verbEntryIsVeridical v = v.factivePresup

theorem Interfaces.SyntaxSemantics.LeftPeriphery.responsive_iff_veridical_question_taker (v : Fragments.English.Predicates.Verbal.VerbEntry) (hQ : (v.complementType == Semantics.Lexical.ComplementType.question || decide (v.takesQuestionBase = true)) = true) (hClass : deriveSelectionClass v = SelectionClass.responsive) : verbEntryIsVeridical v = true

The derived selection class assigns.responsive exactly to verbs whose factivePresup is true and which can embed questions. This connects the structural derivation to the semantic one.

theorem Interfaces.SyntaxSemantics.LeftPeriphery.boolean_tracks_compositional (cls : SelectionClass) : entailsKnowledge cls = true ↔ cls = SelectionClass.responsive

The Boolean entailsKnowledge agrees with the compositional story: responsive predicates entail knowledge (veridicality + box), and non-responsive predicates do not.

Forward direction: responsive → veridical → box-knows Ans(Q) → PerspP blocked. This is exactly what veridical_blocks_perspP proves at the compositional level. The Boolean perspPConsistent tracks this faithfully.

I1. Field-based derivation

This derivation keys off the surface-level lexical fields directly: factivePresup, takesQuestionBase, complementType, speechActVerb, opaqueContext.

Each branch depends on a different field, so changing one field in the fragment breaks exactly one per-verb theorem below.

def Interfaces.SyntaxSemantics.LeftPeriphery.fieldSelectionClass (v : Fragments.English.Predicates.Verbal.VerbEntry) : SelectionClass

Derive selection class from VerbEntry fields.

Class	Condition
uninterrogative	!takesQuestionBase && complementType !=.question
responsive	factivePresup && takesQuestionBase
rogativeSAP	complementType ==.question && speechActVerb
rogativePerspP	complementType ==.question && opaqueContext
rogativeCP	complementType ==.question (fallthrough)

Equations

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

I2. Per-verb verification theorems

Each proved by native_decide. Changing one VerbEntry field breaks exactly one theorem — this is the dense dependency web.

theorem Interfaces.SyntaxSemantics.LeftPeriphery.know_is_responsive : fieldSelectionClass Fragments.English.Predicates.Verbal.know = SelectionClass.responsive

theorem Interfaces.SyntaxSemantics.LeftPeriphery.believe_is_uninterrogative : fieldSelectionClass Fragments.English.Predicates.Verbal.believe = SelectionClass.uninterrogative

theorem Interfaces.SyntaxSemantics.LeftPeriphery.wonder_is_rogativePerspP : fieldSelectionClass Fragments.English.Predicates.Verbal.wonder = SelectionClass.rogativePerspP

theorem Interfaces.SyntaxSemantics.LeftPeriphery.ask_is_rogativeSAP : fieldSelectionClass Fragments.English.Predicates.Verbal.ask = SelectionClass.rogativeSAP

theorem Interfaces.SyntaxSemantics.LeftPeriphery.investigate_is_rogativeCP : fieldSelectionClass Fragments.English.Predicates.Verbal.investigate = SelectionClass.rogativeCP

theorem Interfaces.SyntaxSemantics.LeftPeriphery.depend_on_is_rogativeCP : fieldSelectionClass Fragments.English.Predicates.Verbal.depend_on = SelectionClass.rogativeCP

theorem Interfaces.SyntaxSemantics.LeftPeriphery.remember_rog_is_responsive : fieldSelectionClass Fragments.English.Predicates.Verbal.remember_rog = SelectionClass.responsive

theorem Interfaces.SyntaxSemantics.LeftPeriphery.forget_rog_is_responsive : fieldSelectionClass Fragments.English.Predicates.Verbal.forget_rog = SelectionClass.responsive

theorem Interfaces.SyntaxSemantics.LeftPeriphery.discover_is_responsive : fieldSelectionClass Fragments.English.Predicates.Verbal.discover = SelectionClass.responsive

I3. Cross-layer agreement

The three classification methods — string-based classifyVerb, semantic deriveSelectionClass, and field-based VerbEntry.selectionClass — all agree.

theorem Interfaces.SyntaxSemantics.LeftPeriphery.classifyVerb_agrees_with_selectionClass : classifyVerb "know" = fieldSelectionClass Fragments.English.Predicates.Verbal.know ∧ classifyVerb "wonder" = fieldSelectionClass Fragments.English.Predicates.Verbal.wonder ∧ classifyVerb "ask" = fieldSelectionClass Fragments.English.Predicates.Verbal.ask ∧ classifyVerb "investigate" = fieldSelectionClass Fragments.English.Predicates.Verbal.investigate ∧ classifyVerb "depend on" = fieldSelectionClass Fragments.English.Predicates.Verbal.depend_on ∧ classifyVerb "believe" = fieldSelectionClass Fragments.English.Predicates.Verbal.believe

String-based classification matches field-based derivation.

theorem Interfaces.SyntaxSemantics.LeftPeriphery.deriveSelectionClass_agrees_with_selectionClass : deriveSelectionClass Fragments.English.Predicates.Verbal.know = fieldSelectionClass Fragments.English.Predicates.Verbal.know ∧ deriveSelectionClass Fragments.English.Predicates.Verbal.wonder = fieldSelectionClass Fragments.English.Predicates.Verbal.wonder ∧ deriveSelectionClass Fragments.English.Predicates.Verbal.ask = fieldSelectionClass Fragments.English.Predicates.Verbal.ask ∧ deriveSelectionClass Fragments.English.Predicates.Verbal.investigate = fieldSelectionClass Fragments.English.Predicates.Verbal.investigate ∧ deriveSelectionClass Fragments.English.Predicates.Verbal.believe = fieldSelectionClass Fragments.English.Predicates.Verbal.believe

Semantic derivation matches field-based derivation.

J1. EpistemicModel abstraction

PerspP's presupposition is about possible ignorance: the perspectival center might not know the answer. We abstract over the knowledge notion so the derivation works with any epistemic semantics (doxastic, veridical, etc.).

structure Interfaces.SyntaxSemantics.LeftPeriphery.EpistemicModel (W : Type u_1) : Type u_1

An abstract epistemic model: tells us whether the agent knows a proposition.

• knows : (W → Bool) → Bool

def Interfaces.SyntaxSemantics.LeftPeriphery.perspPPresupComp {W : Type u_1} (ep : EpistemicModel W) (q : Semantics.Questions.GSQuestion W) (w : W) : Bool

PerspP presupposition (compositional version): the agent does NOT know the complete answer to Q at w. Uses QUD.ans from Cells.lean.

Equations

• Interfaces.SyntaxSemantics.LeftPeriphery.perspPPresupComp ep q w = !ep.knows (QUD.ans q w)

J2. Canonical epistemic models

def Interfaces.SyntaxSemantics.LeftPeriphery.veridicalModel {W : Type u_1} (w : W) : EpistemicModel W

Veridical model: knows p iff p is true at w (T axiom). This is the model for responsive predicates (know, remember) in bare (non-negated, non-questioned) contexts.

Equations

• Interfaces.SyntaxSemantics.LeftPeriphery.veridicalModel w = { knows := fun (p : W → Bool) => p w }

def Interfaces.SyntaxSemantics.LeftPeriphery.ignorantModel {W : Type u_1} : EpistemicModel W

Ignorant model: knows nothing. This is the model for rogative predicates (wonder, ask).

Equations

• Interfaces.SyntaxSemantics.LeftPeriphery.ignorantModel = { knows := fun (x : W → Bool) => false }

J3. Grounding theorems

These prove the Boolean layer (perspPConsistent) is faithful to the compositional semantics.

theorem Interfaces.SyntaxSemantics.LeftPeriphery.responsive_contradicts_perspP_comp {W : Type u_1} (q : Semantics.Questions.GSQuestion W) (w : W) : perspPPresupComp (veridicalModel w) q w = false

A veridical knower's PerspP presupposition is false: they know Ans(Q,w), so possible ignorance fails. Uses QUD.ans_true_at_index from Cells.lean.

theorem Interfaces.SyntaxSemantics.LeftPeriphery.rogative_allows_perspP_comp {W : Type u_1} (q : Semantics.Questions.GSQuestion W) (w : W) : perspPPresupComp ignorantModel q w = true

An ignorant agent's PerspP presupposition is true: they don't know anything.

theorem Interfaces.SyntaxSemantics.LeftPeriphery.perspP_boolean_grounded : perspPConsistent SelectionClass.responsive false false = false ∧ ∀ (W : Type) (q : Semantics.Questions.GSQuestion W) (w : W), perspPPresupComp (veridicalModel w) q w = false

The Boolean perspPConsistent.responsive false false = false is consistent with the compositional derivation: both say responsive blocks PerspP.

The Boolean layer says: responsive + not negated + not questioned → inconsistent. The compositional layer says: veridical model → ¬(possible ignorance).

J4. Bridge to DoxasticPredicate

A DoxasticPredicate from Doxastic.lean induces an EpistemicModel at a given world, agent, and domain. This connects the modal-logic semantics to the abstract epistemic layer used by PerspP.

def Interfaces.SyntaxSemantics.LeftPeriphery.doxasticToEpistemicModel {W : Type u_1} {E : Type u_2} (V : Semantics.Attitudes.Doxastic.DoxasticPredicate W E) [(a : E) → (w w' : W) → Decidable (V.access a w w')] (agent : E) (w : W) (worlds : List W) : EpistemicModel W

A DoxasticPredicate induces an EpistemicModel at a world.

Equations

• Interfaces.SyntaxSemantics.LeftPeriphery.doxasticToEpistemicModel V agent w worlds = { knows := fun (p : W → Bool) => decide (V.holdsAt agent (fun (w' : W) => p w' = true) w worlds) }

theorem Interfaces.SyntaxSemantics.LeftPeriphery.veridical_model_blocks_perspP {W : Type u_1} {E : Type u_2} (V : Semantics.Attitudes.Doxastic.DoxasticPredicate W E) [(a : E) → (w w' : W) → Decidable (V.access a w w')] (_hV : V.veridicality = Features.Veridicality.veridical) (agent : E) (Q : Semantics.Questions.GSQuestion W) (w : W) (worlds : List W) (hHolds : V.holdsAt agent (fun (w' : W) => QUD.ans Q w w' = true) w worlds) : perspPPresupComp (doxasticToEpistemicModel V agent w worlds) Q w = false

A veridical predicate that box-knows Ans(Q) blocks PerspP through the epistemic model bridge.

TODO: Full proof requires showing holdsAt for veridical predicates at the answer proposition entails the answer is true at the eval world (which follows from veridical_entails_complement + boxAt).

Connection to @cite{dayal-1996}'s answerhood theory

The Ans(Q) referenced throughout this module — in PerspP's ◇¬know(x, Ans(Q)) and SAP's obligation to assert Ans(Q) — corresponds to @cite{dayal-1996}'s strongest true answer when the question's Exhaustivity Presupposition (EP) is satisfied. See Theories/Semantics/Questions/Exhaustivity.lean for the topical Prop/Set operators (dayalAns, IsExhaustivelyResolvable, relExh).

When EP fails (e.g., ability-can questions under first-order scope), there is no unique strongest answer, and the question licenses mention-some readings; in such cases Ans(Q) is not well-defined in Dayal's sense, though @cite{xiang-2022}'s Relativized Exhaustivity may still hold.