structure Phenomena.Entailment.TruthJudgment : Type

A truth condition judgment: given a described situation, is the sentence true?

• sentence : String

  The sentence being evaluated

• situation : String

  Description of the model/situation

• judgedTrue : Bool

  Do speakers judge this as true in the situation?

• pattern : String

  Description of the pattern being tested

instance Phenomena.Entailment.instReprTruthJudgment : Repr TruthJudgment

Equations

• Phenomena.Entailment.instReprTruthJudgment = { reprPrec := Phenomena.Entailment.instReprTruthJudgment.repr }

def Phenomena.Entailment.instReprTruthJudgment.repr : TruthJudgment → Nat → Std.Format

Equations

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

def Phenomena.Entailment.johnSleepsTrue : TruthJudgment

"John sleeps" is true when John is asleep

Equations

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

def Phenomena.Entailment.marySleepsFalse : TruthJudgment

"Mary sleeps" is false when Mary is awake

Equations

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

def Phenomena.Entailment.johnLaughsTrue : TruthJudgment

"John laughs" is true when John can laugh

Equations

• Phenomena.Entailment.johnLaughsTrue = { sentence := "John laughs", situation := "John and Mary can both laugh", judgedTrue := true, pattern := "intransitive predication" }

def Phenomena.Entailment.maryLaughsTrue : TruthJudgment

"Mary laughs" is true when Mary can laugh

Equations

• Phenomena.Entailment.maryLaughsTrue = { sentence := "Mary laughs", situation := "John and Mary can both laugh", judgedTrue := true, pattern := "intransitive predication" }

def Phenomena.Entailment.johnSeesMaryTrue : TruthJudgment

"John sees Mary" is true when John sees Mary

Equations

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

def Phenomena.Entailment.marySeesJohnTrue : TruthJudgment

"Mary sees John" is true when Mary sees John

Equations

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

def Phenomena.Entailment.johnSeesJohnFalse : TruthJudgment

"John sees John" is false when John doesn't see himself

Equations

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

def Phenomena.Entailment.johnEatsPizzaTrue : TruthJudgment

"John eats pizza" is true

Equations

• Phenomena.Entailment.johnEatsPizzaTrue = { sentence := "John eats pizza", situation := "John and Mary both eat pizza", judgedTrue := true, pattern := "transitive predication" }

def Phenomena.Entailment.maryEatsPizzaTrue : TruthJudgment

"Mary eats pizza" is true

Equations

• Phenomena.Entailment.maryEatsPizzaTrue = { sentence := "Mary eats pizza", situation := "John and Mary both eat pizza", judgedTrue := true, pattern := "transitive predication" }

def Phenomena.Entailment.johnEatsMaryFalse : TruthJudgment

"John eats Mary" is false (Mary is not food)

Equations

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

def Phenomena.Entailment.johnReadsBookTrue : TruthJudgment

"John reads book" is true

Equations

• Phenomena.Entailment.johnReadsBookTrue = { sentence := "John reads book", situation := "John reads the book", judgedTrue := true, pattern := "transitive predication" }

def Phenomena.Entailment.intransitiveJudgments : List TruthJudgment

Intransitive verb truth judgments

Equations

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

def Phenomena.Entailment.transitiveJudgments : List TruthJudgment

Transitive verb truth judgments

Equations

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

def Phenomena.Entailment.allTruthJudgments : List TruthJudgment

All truth condition judgments

Equations

• Phenomena.Entailment.allTruthJudgments = Phenomena.Entailment.intransitiveJudgments ++ Phenomena.Entailment.transitiveJudgments

structure Phenomena.Entailment.EntailmentJudgment : Type

An entailment judgment: does sentence A entail sentence B?

• premise : String

  The premise sentence

• conclusion : String

  The conclusion sentence

• judgedValid : Bool

  Do speakers judge this as valid?

• pattern : String

  Description of the pattern

instance Phenomena.Entailment.instReprEntailmentJudgment : Repr EntailmentJudgment

Equations

• Phenomena.Entailment.instReprEntailmentJudgment = { reprPrec := Phenomena.Entailment.instReprEntailmentJudgment.repr }

def Phenomena.Entailment.instReprEntailmentJudgment.repr : EntailmentJudgment → Nat → Std.Format

Equations

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

def Phenomena.Entailment.allEntailsSome : EntailmentJudgment

"All" entails "some" (on same restrictor and scope).

Equations

• Phenomena.Entailment.allEntailsSome = { premise := "All students passed", conclusion := "Some students passed", judgedValid := true, pattern := "all → some (downward on Horn scale)" }

def Phenomena.Entailment.someNotEntailsAll : EntailmentJudgment

"Some" does NOT entail "all".

Equations

• Phenomena.Entailment.someNotEntailsAll = { premise := "Some students passed", conclusion := "All students passed", judgedValid := false, pattern := "some ↛ all (upward on Horn scale invalid)" }

def Phenomena.Entailment.mostEntailsSome : EntailmentJudgment

"Most" entails "some".

Equations

• Phenomena.Entailment.mostEntailsSome = { premise := "Most students passed", conclusion := "Some students passed", judgedValid := true, pattern := "most → some" }

def Phenomena.Entailment.allEntailsMost : EntailmentJudgment

"All" entails "most" (in typical contexts).

Equations

• Phenomena.Entailment.allEntailsMost = { premise := "All students passed", conclusion := "Most students passed", judgedValid := true, pattern := "all → most" }

def Phenomena.Entailment.noEntailsNotAll : EntailmentJudgment

"No" entails "not all".

Equations

• Phenomena.Entailment.noEntailsNotAll = { premise := "No students passed", conclusion := "Not all students passed", judgedValid := true, pattern := "no → not all" }

def Phenomena.Entailment.conjunctionElimination : EntailmentJudgment

Conjunction entails each conjunct.

Equations

• Phenomena.Entailment.conjunctionElimination = { premise := "John and Mary left", conclusion := "John left", judgedValid := true, pattern := "A ∧ B → A" }

def Phenomena.Entailment.disjunctionIntroduction : EntailmentJudgment

Disjunct entails disjunction.

Equations

• Phenomena.Entailment.disjunctionIntroduction = { premise := "John left", conclusion := "John or Mary left", judgedValid := true, pattern := "A → A ∨ B" }

def Phenomena.Entailment.conjEntailsDisj : EntailmentJudgment

Conjunction entails disjunction.

Equations

• Phenomena.Entailment.conjEntailsDisj = { premise := "John and Mary left", conclusion := "John or Mary left", judgedValid := true, pattern := "A ∧ B → A ∨ B" }

def Phenomena.Entailment.disjNotEntailsConj : EntailmentJudgment

Disjunction does NOT entail conjunction.

Equations

• Phenomena.Entailment.disjNotEntailsConj = { premise := "John or Mary left", conclusion := "John and Mary left", judgedValid := false, pattern := "A ∨ B ↛ A ∧ B" }

def Phenomena.Entailment.quantifierEntailments : List EntailmentJudgment

All quantifier entailment judgments

Equations

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

def Phenomena.Entailment.connectiveEntailments : List EntailmentJudgment

All connective entailment judgments

Equations

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

def Phenomena.Entailment.allEntailments : List EntailmentJudgment

All entailment judgments

Equations

• Phenomena.Entailment.allEntailments = Phenomena.Entailment.quantifierEntailments ++ Phenomena.Entailment.connectiveEntailments

theorem Phenomena.Entailment.predication_discriminates : johnSleepsTrue.judgedTrue = true ∧ marySleepsFalse.judgedTrue = false

Predication distinguishes individuals in/out of extension

theorem Phenomena.Entailment.relations_discriminate : johnSeesMaryTrue.judgedTrue = true ∧ johnSeesJohnFalse.judgedTrue = false

Transitive relations distinguish ordered pairs

theorem Phenomena.Entailment.hornScaleReflected : allEntailsSome.judgedValid = true ∧ allEntailsMost.judgedValid = true ∧ mostEntailsSome.judgedValid = true ∧ someNotEntailsAll.judgedValid = false

The scale all > most > some is reflected in entailments

theorem Phenomena.Entailment.conjStrongerThanDisj : conjEntailsDisj.judgedValid = true ∧ disjNotEntailsConj.judgedValid = false

Conjunction is stronger than disjunction