Documentation

def Semantics.Montague.PTQ.«term𝐭» :

Equations

Semantics.Montague.PTQ.«term𝐭» = Lean.ParserDescr.node `Semantics.Montague.PTQ.«term𝐭» 1024 (Lean.ParserDescr.symbol "𝐭")

Instances For

def Semantics.Montague.PTQ.«term𝐬» :

Equations

Semantics.Montague.PTQ.«term𝐬» = Lean.ParserDescr.node `Semantics.Montague.PTQ.«term𝐬» 1024 (Lean.ParserDescr.symbol "𝐬")

Instances For

def Semantics.Montague.PTQ.«term⦃_,_⦄» :

Equations

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

Instances For

@[reducible, inline]

abbrev Semantics.Montague.PTQ.Ty.intens (a : Ty) :

Intension type: ⟨s, a⟩

Equations

⦃𝐬, a⦄ = ⦃ 𝐬 , a⦄

Instances For

def Semantics.Montague.PTQ.«term⦃𝐬,_⦄» :

Equations

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

Instances For

@[reducible, inline]

abbrev Semantics.Montague.PTQ.Ty.ptq_et :

Common derived types

Equations

Semantics.Montague.PTQ.Ty.ptq_et = ⦃𝐞 , 𝐭 ⦄

Instances For

@[reducible, inline]

abbrev Semantics.Montague.PTQ.Ty.ptq_eet :

Equations

Semantics.Montague.PTQ.Ty.ptq_eet = ⦃𝐞 , ⦃𝐞 , 𝐭 ⦄⦄

Instances For

@[reducible, inline]

abbrev Semantics.Montague.PTQ.Ty.ptq_ett :

Equations

Semantics.Montague.PTQ.Ty.ptq_ett = ⦃⦃𝐞 , 𝐭 ⦄, 𝐭 ⦄

Instances For

@[reducible, inline]

abbrev Semantics.Montague.PTQ.Ty.setIntens :

Equations

Semantics.Montague.PTQ.Ty.setIntens = ⦃⦃𝐬, ⦃𝐞 , 𝐭 ⦄⦄, 𝐭 ⦄

Instances For

inductive Semantics.Montague.PTQ.Cat :

Syntactic Categories

Basic categories: t (sentences), e (entity-denoting), CN (common nouns), IV (intransitive verbs) Derived categories: A/B and A//B (slash categories)

The double slash // is for "intensional" arguments (take intensions).

t : Cat
e : Cat
CN : Cat
IV : Cat
TV : Cat
T : Cat
rslash : Cat → Cat → Cat
lslash : Cat → Cat → Cat
rslashI : Cat → Cat → Cat

Instances For

instance Semantics.Montague.PTQ.instDecidableEqCat :

DecidableEq Cat

Equations

Semantics.Montague.PTQ.instDecidableEqCat = Semantics.Montague.PTQ.instDecidableEqCat.decEq

def Semantics.Montague.PTQ.instDecidableEqCat.decEq (x✝ x✝¹ : Cat) :

Decidable (x✝ = x✝¹)

Equations

Instances For

def Semantics.Montague.PTQ.instReprCat.repr :

Cat → ℕ → Std.Format

Equations

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

Instances For

instance Semantics.Montague.PTQ.instReprCat :

Repr Cat

Equations

Semantics.Montague.PTQ.instReprCat = { reprPrec := Semantics.Montague.PTQ.instReprCat.repr }

def Semantics.Montague.PTQ.«term_/'_» :

Lean.TrailingParserDescr

Equations

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

Instances For

def Semantics.Montague.PTQ.«term_\'_» :

Lean.TrailingParserDescr

Equations

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

Instances For

def Semantics.Montague.PTQ.«term_//'_» :

Lean.TrailingParserDescr

Equations

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

Instances For

def Semantics.Montague.PTQ.catToTy :

Cat → Ty

The function f from categories to types.

This is the core of the syntax-semantics interface. Each syntactic category corresponds to a semantic type.

Key mappings:

f(e) = e
f(t) = t
f(CN) = f(IV) = ⟨s, ⟨e, t⟩⟩ (intensions of properties)
f(T) = ⟨⟨s, ⟨e, t⟩⟩, t⟩ (generalized quantifiers over property intensions)
f(A/B) = ⟨⟨s, f(B)⟩, f(A)⟩ (functions from intensions of B to A)

Equations

Instances For

theorem Semantics.Montague.PTQ.term_phrase_is_gq :

catToTy Cat.T = ⦃⦃𝐬, ⦃𝐞 , 𝐭 ⦄⦄, 𝐭 ⦄

Term phrases (T) denote generalized quantifiers.

"Every man" doesn't denote an entity; it denotes a function that takes a property (intension) and returns true iff every man has that property.

@[reducible, inline]

abbrev Semantics.Montague.PTQ.PTQModel :

Type 1

Intensional Model

A PTQ model uses the canonical Semantics.Montague.Model which includes:

Entity : domain of entities
World : possible worlds (indices)

Equations

Semantics.Montague.PTQ.PTQModel = Semantics.Montague.Model

Instances For

@[reducible, inline]

abbrev Semantics.Montague.PTQ.PTQModel.Den (m : PTQModel) (τ : Ty) :

Denotation of a type in a model (uses canonical interpTy)

Equations

m.Den τ = Semantics.Montague.Model.interpTy m τ

Instances For

@[reducible, inline]

abbrev Semantics.Montague.PTQ.PTQModel.Intens (m : PTQModel) (a : Ty) :

Intension: function from worlds to extensions

Equations

m.Intens a = (m.World → Semantics.Montague.Model.interpTy m a)

Instances For

structure Semantics.Montague.PTQ.LexEntry (m : PTQModel) :

Lexical Entry Structure

Each word has:

Surface form
Syntactic category
Translation (semantic representation)

form : String
cat : Cat

Instances For

inductive Semantics.Montague.PTQ.SynRule :

Syntactic Rule

A rule specifies:

Input categories
Output category
How to combine the strings (F function)

S1 : SynRule
S2 : SynRule
S3 : SynRule
S4 : SynRule
S5 : SynRule
S14 : ℕ → SynRule

Instances For

def Semantics.Montague.PTQ.instDecidableEqSynRule.decEq (x✝ x✝¹ : SynRule) :

Decidable (x✝ = x✝¹)

Equations

Instances For

instance Semantics.Montague.PTQ.instDecidableEqSynRule :

DecidableEq SynRule

Equations

Semantics.Montague.PTQ.instDecidableEqSynRule = Semantics.Montague.PTQ.instDecidableEqSynRule.decEq

def Semantics.Montague.PTQ.instReprSynRule.repr :

SynRule → ℕ → Std.Format

Equations

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

Instances For

instance Semantics.Montague.PTQ.instReprSynRule :

Repr SynRule

Equations

Semantics.Montague.PTQ.instReprSynRule = { reprPrec := Semantics.Montague.PTQ.instReprSynRule.repr }

inductive Semantics.Montague.PTQ.TransRule :

Translation Rule

Maps syntactic derivations to semantic representations. This is the homomorphism: h : Syntax → Semantics

T1 : TransRule
T2 : TransRule
T3 : TransRule
T4 : TransRule
T5 : TransRule
T14 : ℕ → TransRule

Instances For

def Semantics.Montague.PTQ.instDecidableEqTransRule.decEq (x✝ x✝¹ : TransRule) :

Decidable (x✝ = x✝¹)

Equations

Instances For

instance Semantics.Montague.PTQ.instDecidableEqTransRule :

DecidableEq TransRule

Equations

Semantics.Montague.PTQ.instDecidableEqTransRule = Semantics.Montague.PTQ.instDecidableEqTransRule.decEq

instance Semantics.Montague.PTQ.instReprTransRule :

Repr TransRule

Equations

Semantics.Montague.PTQ.instReprTransRule = { reprPrec := Semantics.Montague.PTQ.instReprTransRule.repr }

def Semantics.Montague.PTQ.instReprTransRule.repr :

TransRule → ℕ → Std.Format

Equations

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

Instances For

inductive Semantics.Montague.PTQ.ScopeReading :

Scope Reading

Represents different scope orderings of quantifiers.

surface : ScopeReading
inverse : ScopeReading

Instances For

instance Semantics.Montague.PTQ.instDecidableEqScopeReading :

DecidableEq ScopeReading

Equations

Semantics.Montague.PTQ.instDecidableEqScopeReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Montague.PTQ.instReprScopeReading :

Repr ScopeReading

Equations

Semantics.Montague.PTQ.instReprScopeReading = { reprPrec := Semantics.Montague.PTQ.instReprScopeReading.repr }

def Semantics.Montague.PTQ.instReprScopeReading.repr :

ScopeReading → ℕ → Std.Format

Equations

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

Instances For

inductive Semantics.Montague.PTQ.ToyEntity :

A toy model for demonstrating scope ambiguity.

Two men (m1, m2), two women (w1, w2).

Instances For

instance Semantics.Montague.PTQ.instDecidableEqToyEntity :

DecidableEq ToyEntity

Equations

Semantics.Montague.PTQ.instDecidableEqToyEntity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Montague.PTQ.instReprToyEntity.repr :

ToyEntity → ℕ → Std.Format

Equations

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

Instances For

instance Semantics.Montague.PTQ.instReprToyEntity :

Repr ToyEntity

Equations

Semantics.Montague.PTQ.instReprToyEntity = { reprPrec := Semantics.Montague.PTQ.instReprToyEntity.repr }

def Semantics.Montague.PTQ.instBEqToyEntity.beq :

ToyEntity → ToyEntity → Bool

Equations

Semantics.Montague.PTQ.instBEqToyEntity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Semantics.Montague.PTQ.instBEqToyEntity :

BEq ToyEntity

Equations

Semantics.Montague.PTQ.instBEqToyEntity = { beq := Semantics.Montague.PTQ.instBEqToyEntity.beq }

def Semantics.Montague.PTQ.toyPTQModel :

PTQModel

Equations

Semantics.Montague.PTQ.toyPTQModel = { Entity := Semantics.Montague.PTQ.ToyEntity, decEq := inferInstance }

Instances For

def Semantics.Montague.PTQ.isMan :

ToyEntity → Bool

Predicate: is a man

Equations

Instances For

def Semantics.Montague.PTQ.isWoman :

ToyEntity → Bool

Predicate: is a woman

Equations

Instances For

def Semantics.Montague.PTQ.allEntities :

List ToyEntity

All entities

Equations

Semantics.Montague.PTQ.allEntities = [Semantics.Montague.PTQ.ToyEntity.m1 , Semantics.Montague.PTQ.ToyEntity.m2 , Semantics.Montague.PTQ.ToyEntity.w1 , Semantics.Montague.PTQ.ToyEntity.w2 ]

Instances For

def Semantics.Montague.PTQ.loveSurface :

ToyEntity → ToyEntity → Bool

Love relation for surface scope scenario.

m1 loves w1, m2 loves w2 (different women)

Equations

Instances For

def Semantics.Montague.PTQ.loveInverse :

ToyEntity → ToyEntity → Bool

Love relation for inverse scope scenario.

m1 loves w1, m2 loves w1 (same woman)

Equations

Instances For

def Semantics.Montague.PTQ.surfaceScopeTrue (love : ToyEntity → ToyEntity → Bool) :

Bool

Surface scope reading: ∀x[man(x) → ∃y[woman(y) ∧ love(x,y)]]

"For every man, there exists a woman that he loves."

Equations

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

Instances For

def Semantics.Montague.PTQ.inverseScopeTrue (love : ToyEntity → ToyEntity → Bool) :

Bool

Inverse scope reading: ∃y[woman(y) ∧ ∀x[man(x) → love(x,y)]]

"There exists a woman such that every man loves her."

Equations

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

Instances For

surfaceScopeTrue loveSurface = true

theorem Semantics.Montague.PTQ.surface_scope_surface_scenario :

Surface scope is true in surface scenario.

When each man loves a different woman, surface scope is satisfied.

inverseScopeTrue loveSurface = false

theorem Semantics.Montague.PTQ.inverse_scope_surface_scenario :

Inverse scope is false in surface scenario.

No single woman is loved by all men.

surfaceScopeTrue loveInverse = true

theorem Semantics.Montague.PTQ.surface_scope_inverse_scenario :

Both scopes are true in inverse scenario.

When all men love the same woman, both readings are true.

inverseScopeTrue loveInverse = true

theorem Semantics.Montague.PTQ.inverse_scope_inverse_scenario :

surfaceScopeTrue loveSurface ≠ inverseScopeTrue loveSurface

theorem Semantics.Montague.PTQ.scope_readings_differ :

Scope ambiguity theorem.

The two readings are not equivalent - they differ in the surface scenario. This is why "Every man loves a woman" is ambiguous.

theorem Semantics.Montague.PTQ.inverse_entails_surface (love : ToyEntity → ToyEntity → Bool) :

inverseScopeTrue love = true → surfaceScopeTrue love = true

Inverse scope entails surface scope.

∃y∀x.R(x,y) → ∀x∃y.R(x,y)

If there's one woman everyone loves, then certainly each man loves some woman.

inductive Semantics.Montague.PTQ.Derivation :

Derivation Tree

Represents a syntactic derivation with rule applications.

lex : String → Cat → Derivation
apply : SynRule → Derivation → Derivation → Derivation
quantIn : ℕ → Derivation → Derivation → Derivation

Instances For

instance Semantics.Montague.PTQ.instReprDerivation :

Repr Derivation

Equations

Semantics.Montague.PTQ.instReprDerivation = { reprPrec := Semantics.Montague.PTQ.instReprDerivation.repr }

def Semantics.Montague.PTQ.instReprDerivation.repr :

Derivation → ℕ → Std.Format

Equations

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

Instances For