The family of sentences

The family of sentences of a trigger is the sentence unembedded and under each of the entailment-cancelling operators, negation, a polar question, the antecedent of a conditional and an epistemic possibility modal, in the terms of Chierchia and McConnell-Ginet and of Tonhauser, Beaver, Roberts and Simons; a content projects when the embedded members still carry it. A member of the family is named by the position of its sentence (FamilyVariant). Each member evaluates its sentence along a relation, the identity except under the modal (FamilyVariant.rel), and these relations are reflexive when the modal's is, so that a requirement on the local context of the sentence is a requirement on the context of the member. Example rows record a sentence's environment, whether the content projected, and the person of the matrix subject, and the readers here type those features.

References

• [CMCG90]
• [TBRS13]

inductive Presupposition.FamilyVariant : Type

A member of the family of sentences, by the position of its sentence: unembedded or under an entailment-cancelling operator.

• unembedded : FamilyVariant
• negation : FamilyVariant
• question : FamilyVariant
• conditionalAntecedent : FamilyVariant
• epistemicModal : FamilyVariant

@[instance_reducible]

instance Presupposition.instDecidableEqFamilyVariant : DecidableEq FamilyVariant

Equations

• Presupposition.instDecidableEqFamilyVariant x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Presupposition.instReprFamilyVariant : Repr FamilyVariant

Equations

• Presupposition.instReprFamilyVariant = { reprPrec := Presupposition.instReprFamilyVariant.repr }

def Presupposition.instReprFamilyVariant.repr : FamilyVariant → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Presupposition.instFintypeFamilyVariant : Fintype FamilyVariant

Equations

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

def Presupposition.FamilyVariant.rel {W : Type u_1} (M : SetRel W W) : FamilyVariant → SetRel W W

The relation along which a member of the family evaluates its sentence, where M is the accessibility of the possibility modal. The other members evaluate the sentence at the member's own world.

Equations

• Presupposition.FamilyVariant.rel M Presupposition.FamilyVariant.epistemicModal = M
• Presupposition.FamilyVariant.rel M x✝ = SetRel.id

instance Presupposition.FamilyVariant.instIsReflRel {W : Type u_1} (M : SetRel W W) [M.IsRefl] (e : FamilyVariant) : (rel M e).IsRefl

@[simp]

theorem Presupposition.FamilyVariant.rel_id {W : Type u_1} (e : FamilyVariant) : rel SetRel.id e = SetRel.id

Where the modal's accessibility is the identity, every member evaluates its sentence at its own world.

def Presupposition.FamilyVariant.table : List (String × FamilyVariant)

The members of the family as example rows record them, by the environment of the sentence.

Equations

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

def Datum.environment? (e : Datum) : Option Presupposition.FamilyVariant

The member of the family a row's sentence is, by its recorded environment.

Equations

• e.environment? = e.parse? "environment" Presupposition.FamilyVariant.table

def Datum.projective? (e : Datum) : Option Bool

Whether the row's content projected, as the row records it.

Equations

• e.projective? = e.parse? "projective" [("yes", true), ("no", false)]

def Datum.person? (e : Datum) : Option UD.Person

The person of the row's matrix subject.

Equations

• e.person? = e.parse? "person" [("1", UD.Person.first), ("2", UD.Person.second), ("3", UD.Person.third)]