Bridge: Compositional Truth Conditions → Entailment Data

@cite{montague-1973}

Connects Montague compositional semantics derivations to the empirical truth-condition judgments in Phenomena.Entailment.Basic.

Each bridge theorem verifies that the compositional derivation matches the empirical judgment for a specific sentence.

theorem Phenomena.Entailment.CompositionalBridge.captures_john_sleeps : Semantics.Montague.ToyLexicon.sleeps_sem Semantics.Montague.ToyLexicon.john_sem = true ↔ johnSleepsTrue.judgedTrue = true

theorem Phenomena.Entailment.CompositionalBridge.captures_mary_sleeps : Semantics.Montague.ToyLexicon.sleeps_sem Semantics.Montague.ToyLexicon.mary_sem = false ↔ marySleepsFalse.judgedTrue = false

theorem Phenomena.Entailment.CompositionalBridge.captures_intransitive_contrast : Semantics.Montague.ToyLexicon.sleeps_sem Semantics.Montague.ToyLexicon.john_sem = johnSleepsTrue.judgedTrue ∧ Semantics.Montague.ToyLexicon.sleeps_sem Semantics.Montague.ToyLexicon.mary_sem = marySleepsFalse.judgedTrue

theorem Phenomena.Entailment.CompositionalBridge.captures_transitive_seeing : Semantics.Montague.ToyLexicon.sees_sem Semantics.Montague.ToyLexicon.mary_sem Semantics.Montague.ToyLexicon.john_sem = johnSeesMaryTrue.judgedTrue ∧ Semantics.Montague.ToyLexicon.sees_sem Semantics.Montague.ToyLexicon.john_sem Semantics.Montague.ToyLexicon.john_sem = johnSeesJohnFalse.judgedTrue