def CCG.TruthConditions.ccg_john_sleeps : DerivStep

"John sleeps" - backward application

Equations

• CCG.TruthConditions.ccg_john_sleeps = (CCG.DerivStep.lex { form := "John", cat := CCG.NP }).bapp (CCG.DerivStep.lex { form := "sleeps", cat := CCG.IV })

def CCG.TruthConditions.ccg_mary_sleeps : DerivStep

"Mary sleeps" - backward application

Equations

• CCG.TruthConditions.ccg_mary_sleeps = (CCG.DerivStep.lex { form := "Mary", cat := CCG.NP }).bapp (CCG.DerivStep.lex { form := "sleeps", cat := CCG.IV })

def CCG.TruthConditions.ccg_john_laughs : DerivStep

"John laughs" - backward application

Equations

• CCG.TruthConditions.ccg_john_laughs = (CCG.DerivStep.lex { form := "John", cat := CCG.NP }).bapp (CCG.DerivStep.lex { form := "laughs", cat := CCG.IV })

def CCG.TruthConditions.ccg_mary_laughs : DerivStep

"Mary laughs" - backward application

Equations

• CCG.TruthConditions.ccg_mary_laughs = (CCG.DerivStep.lex { form := "Mary", cat := CCG.NP }).bapp (CCG.DerivStep.lex { form := "laughs", cat := CCG.IV })

def CCG.TruthConditions.ccg_john_sees_mary : DerivStep

"John sees Mary" - forward then backward application

Equations

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

def CCG.TruthConditions.ccg_mary_sees_john : DerivStep

"Mary sees John" - forward then backward application

Equations

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

def CCG.TruthConditions.ccg_john_eats_pizza : DerivStep

"John eats pizza" - forward then backward application

Equations

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

def CCG.TruthConditions.extendedLexicon : SemLexicon Semantics.Montague.toyModel

Extended lexicon with all entities and predicates

Equations

• One or more equations did not get rendered due to their size.
• CCG.TruthConditions.extendedLexicon "John" (CCG.Cat.atom CCG.Atom.NP) = some { cat := CCG.NP, meaning := Semantics.Montague.ToyEntity.john }
• CCG.TruthConditions.extendedLexicon "Mary" (CCG.Cat.atom CCG.Atom.NP) = some { cat := CCG.NP, meaning := Semantics.Montague.ToyEntity.mary }
• CCG.TruthConditions.extendedLexicon "pizza" (CCG.Cat.atom CCG.Atom.NP) = some { cat := CCG.NP, meaning := Semantics.Montague.ToyEntity.pizza }
• CCG.TruthConditions.extendedLexicon "book" (CCG.Cat.atom CCG.Atom.NP) = some { cat := CCG.NP, meaning := Semantics.Montague.ToyEntity.book }
• CCG.TruthConditions.extendedLexicon "sleeps" ((CCG.Cat.atom CCG.Atom.S).lslash (CCG.Cat.atom CCG.Atom.NP)) = some { cat := CCG.IV, meaning := Semantics.Montague.ToyLexicon.sleeps_sem }
• CCG.TruthConditions.extendedLexicon "laughs" ((CCG.Cat.atom CCG.Atom.S).lslash (CCG.Cat.atom CCG.Atom.NP)) = some { cat := CCG.IV, meaning := Semantics.Montague.ToyLexicon.laughs_sem }
• CCG.TruthConditions.extendedLexicon word cat = none

def CCG.TruthConditions.ccgTruth (d : DerivStep) : Option Bool

Get truth value from CCG derivation

Equations

• CCG.TruthConditions.ccgTruth d = CCG.getMeaning (d.interp CCG.TruthConditions.extendedLexicon)

theorem CCG.TruthConditions.ccg_predicts_john_sleeps : ccgTruth ccg_john_sleeps = some Phenomena.Entailment.johnSleepsTrue.judgedTrue

CCG correctly predicts "John sleeps" is true

theorem CCG.TruthConditions.ccg_predicts_mary_sleeps : ccgTruth ccg_mary_sleeps = some Phenomena.Entailment.marySleepsFalse.judgedTrue

CCG correctly predicts "Mary sleeps" is false

theorem CCG.TruthConditions.ccg_predicts_john_laughs : ccgTruth ccg_john_laughs = some Phenomena.Entailment.johnLaughsTrue.judgedTrue

CCG correctly predicts "John laughs" is true

theorem CCG.TruthConditions.ccg_predicts_mary_laughs : ccgTruth ccg_mary_laughs = some Phenomena.Entailment.maryLaughsTrue.judgedTrue

CCG correctly predicts "Mary laughs" is true

theorem CCG.TruthConditions.ccg_predicts_john_sees_mary : ccgTruth ccg_john_sees_mary = some Phenomena.Entailment.johnSeesMaryTrue.judgedTrue

CCG correctly predicts "John sees Mary" is true

theorem CCG.TruthConditions.ccg_predicts_mary_sees_john : ccgTruth ccg_mary_sees_john = some Phenomena.Entailment.marySeesJohnTrue.judgedTrue

CCG correctly predicts "Mary sees John" is true

structure CCG.TruthConditions.TestCase : Type

A test case: derivation paired with expected judgment

• deriv : DerivStep
• expected : Bool

def CCG.TruthConditions.intransitiveTestCases : List TestCase

All intransitive verb test cases

Equations

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

def CCG.TruthConditions.transitiveTestCases : List TestCase

All transitive verb test cases

Equations

• CCG.TruthConditions.transitiveTestCases = [{ deriv := CCG.TruthConditions.ccg_john_sees_mary, expected := true }, { deriv := CCG.TruthConditions.ccg_mary_sees_john, expected := true }]

def CCG.TruthConditions.ccgPredictsCorrectly (tc : TestCase) : Bool

Check if CCG predicts a test case correctly

Equations

• CCG.TruthConditions.ccgPredictsCorrectly tc = (CCG.TruthConditions.ccgTruth tc.deriv == some tc.expected)

theorem CCG.TruthConditions.ccg_predicts_all_intransitive : intransitiveTestCases.all ccgPredictsCorrectly = true

CCG correctly predicts ALL intransitive test cases.

This is the key theorem: compositional semantics via CCG produces exactly the empirically observed truth values.

theorem CCG.TruthConditions.ccg_predicts_all_transitive : transitiveTestCases.all ccgPredictsCorrectly = true

CCG correctly predicts ALL transitive test cases.

theorem CCG.TruthConditions.ccg_predicts_all_cases : (intransitiveTestCases ++ transitiveTestCases).all ccgPredictsCorrectly = true

CCG correctly predicts ALL test cases.

The syntax → semantics pipeline produces correct truth conditions for the entire test suite.