inductive Phenomena.Questions.Embedding.EmbedType : Type

The structurally distinct ways an interrogative clause can be embedded.

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

@[implicit_reducible]

instance Phenomena.Questions.Embedding.instDecidableEqEmbedType : DecidableEq EmbedType

Equations

• Phenomena.Questions.Embedding.instDecidableEqEmbedType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Questions.Embedding.instReprEmbedType.repr : EmbedType → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Questions.Embedding.instReprEmbedType : Repr EmbedType

Equations

• Phenomena.Questions.Embedding.instReprEmbedType = { reprPrec := Phenomena.Questions.Embedding.instReprEmbedType.repr }

structure Phenomena.Questions.Embedding.EmbeddingDatum : Type

Embedding judgment for a predicate.

• verb : String
• subordination : Bool

  "V whether/who..."

• quasiSubordination : Bool

  "V [did S leave↑]" (embedded inversion + matrix intonation)

• quotation : Bool

  'V, "Did S leave?"'

• embedsDeclarative : Bool

  Does it also embed declarative complements?

def Phenomena.Questions.Embedding.instReprEmbeddingDatum.repr : EmbeddingDatum → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Questions.Embedding.instReprEmbeddingDatum : Repr EmbeddingDatum

Equations

• Phenomena.Questions.Embedding.instReprEmbeddingDatum = { reprPrec := Phenomena.Questions.Embedding.instReprEmbeddingDatum.repr }

def Phenomena.Questions.Embedding.investigate_d : EmbeddingDatum

Equations

• Phenomena.Questions.Embedding.investigate_d = { verb := "investigate", subordination := true, quasiSubordination := false, quotation := false, embedsDeclarative := false }

def Phenomena.Questions.Embedding.depend_on_d : EmbeddingDatum

Equations

• Phenomena.Questions.Embedding.depend_on_d = { verb := "depend on", subordination := true, quasiSubordination := false, quotation := false, embedsDeclarative := false }

def Phenomena.Questions.Embedding.wonder_d : EmbeddingDatum

Equations

• Phenomena.Questions.Embedding.wonder_d = { verb := "wonder", subordination := true, quasiSubordination := true, quotation := false, embedsDeclarative := false }

def Phenomena.Questions.Embedding.ask_d : EmbeddingDatum

Equations

• Phenomena.Questions.Embedding.ask_d = { verb := "ask", subordination := true, quasiSubordination := true, quotation := true, embedsDeclarative := false }

def Phenomena.Questions.Embedding.know_d : EmbeddingDatum

Equations

• Phenomena.Questions.Embedding.know_d = { verb := "know", subordination := true, quasiSubordination := false, quotation := false, embedsDeclarative := true }

def Phenomena.Questions.Embedding.care_d : EmbeddingDatum

Predicate of Relevance: responsive but resists question-to-proposition reduction (@cite{elliott-etal-2017}). The reduction-resistance is a separate property — see Elliott2017.

Equations

• Phenomena.Questions.Embedding.care_d = { verb := "care", subordination := true, quasiSubordination := false, quotation := false, embedsDeclarative := true }

def Phenomena.Questions.Embedding.matter_d : EmbeddingDatum

Predicate of Relevance (@cite{elliott-etal-2017}).

Equations

• Phenomena.Questions.Embedding.matter_d = { verb := "matter", subordination := true, quasiSubordination := false, quotation := false, embedsDeclarative := true }

def Phenomena.Questions.Embedding.believe_d : EmbeddingDatum

Equations

• Phenomena.Questions.Embedding.believe_d = { verb := "believe", subordination := false, quasiSubordination := false, quotation := false, embedsDeclarative := true }

def Phenomena.Questions.Embedding.allEmbeddingData : List EmbeddingDatum

Equations

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

theorem Phenomena.Questions.Embedding.quasi_sub_implies_sub (d : EmbeddingDatum) : d ∈ allEmbeddingData → d.quasiSubordination = true → d.subordination = true

Quasi-subordination implies subordination (@cite{dayal-2025}: (20)).

theorem Phenomena.Questions.Embedding.quotation_implies_quasi_sub (d : EmbeddingDatum) : d ∈ allEmbeddingData → d.quotation = true → d.quasiSubordination = true

Quotation implies quasi-subordination (@cite{dayal-2025}: (20)).

structure Phenomena.Questions.Embedding.ShiftinessDatum : Type

Context-dependent quasi-subordination judgment.

• verb : String
• sentence : String
• negated : Bool
• questioned : Bool
• quasiSubOk : Bool

def Phenomena.Questions.Embedding.instReprShiftinessDatum.repr : ShiftinessDatum → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Questions.Embedding.instReprShiftinessDatum : Repr ShiftinessDatum

Equations

• Phenomena.Questions.Embedding.instReprShiftinessDatum = { reprPrec := Phenomena.Questions.Embedding.instReprShiftinessDatum.repr }

def Phenomena.Questions.Embedding.remember_bare : ShiftinessDatum

Equations

• Phenomena.Questions.Embedding.remember_bare = { verb := "remember", sentence := "*I remember [was Henry a communist↑]", negated := false, questioned := false, quasiSubOk := false }

def Phenomena.Questions.Embedding.remember_negated : ShiftinessDatum

Equations

• Phenomena.Questions.Embedding.remember_negated = { verb := "remember", sentence := "I don't remember [was Henry a communist↑]", negated := true, questioned := false, quasiSubOk := true }

def Phenomena.Questions.Embedding.remember_questioned : ShiftinessDatum

Equations

• Phenomena.Questions.Embedding.remember_questioned = { verb := "remember", sentence := "Does Sue remember [was Henry a communist↑]", negated := false, questioned := true, quasiSubOk := true }

def Phenomena.Questions.Embedding.forget_quasi_sub : ShiftinessDatum

Equations

• Phenomena.Questions.Embedding.forget_quasi_sub = { verb := "forget", sentence := "I have forgotten [did Ann get A's↑]", negated := false, questioned := false, quasiSubOk := true }

def Phenomena.Questions.Embedding.allShiftinessData : List ShiftinessDatum

Equations

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