Types of Intensional Logic (Definition 1)

The set of types is the smallest set Y such that:

• e ∈ Y (entities)
• t ∈ Y (truth values)
• If a, b ∈ Y then ⟨a, b⟩ ∈ Y (functions)
• If a ∈ Y then ⟨s, a⟩ ∈ Y (intensions)

We use the canonical Semantics.Montague.Ty which has:

• .e : entities
• .t : truth values
• .s : possible worlds
• .fn / ⇒ : function types

Intensions ⟨s, a⟩ are represented as .s ⇒ a.

def Phenomena.Quantification.Studies.Montague1973.«term𝐞» : Lean.ParserDescr

Equations

• Phenomena.Quantification.Studies.Montague1973.«term𝐞» = Lean.ParserDescr.node `Phenomena.Quantification.Studies.Montague1973.«term𝐞» 1024 (Lean.ParserDescr.symbol "𝐞")

def Phenomena.Quantification.Studies.Montague1973.«term𝐭» : Lean.ParserDescr

Equations

• Phenomena.Quantification.Studies.Montague1973.«term𝐭» = Lean.ParserDescr.node `Phenomena.Quantification.Studies.Montague1973.«term𝐭» 1024 (Lean.ParserDescr.symbol "𝐭")

def Phenomena.Quantification.Studies.Montague1973.«term𝐬» : Lean.ParserDescr

Equations

• Phenomena.Quantification.Studies.Montague1973.«term𝐬» = Lean.ParserDescr.node `Phenomena.Quantification.Studies.Montague1973.«term𝐬» 1024 (Lean.ParserDescr.symbol "𝐬")

def Phenomena.Quantification.Studies.Montague1973.«term⦃_,_⦄» : Lean.ParserDescr

Equations

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

@[reducible, inline]

abbrev Phenomena.Quantification.Studies.Montague1973.Ty.intens (a : Semantics.Montague.Ty) : Semantics.Montague.Ty

Intension type: ⟨s, a⟩

Equations

• ⦃𝐬, a⦄ = ⦃ 𝐬, a⦄

def Phenomena.Quantification.Studies.Montague1973.«term⦃𝐬,_⦄» : Lean.ParserDescr

Equations

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

@[reducible, inline]

abbrev Phenomena.Quantification.Studies.Montague1973.Ty.ptq_et : Semantics.Montague.Ty

Common derived types

Equations

• Phenomena.Quantification.Studies.Montague1973.Ty.ptq_et = ⦃𝐞, 𝐭⦄

@[reducible, inline]

abbrev Phenomena.Quantification.Studies.Montague1973.Ty.ptq_eet : Semantics.Montague.Ty

Equations

• Phenomena.Quantification.Studies.Montague1973.Ty.ptq_eet = ⦃𝐞, ⦃𝐞, 𝐭⦄⦄

@[reducible, inline]

abbrev Phenomena.Quantification.Studies.Montague1973.Ty.ptq_ett : Semantics.Montague.Ty

Equations

• Phenomena.Quantification.Studies.Montague1973.Ty.ptq_ett = ⦃⦃𝐞, 𝐭⦄, 𝐭⦄

@[reducible, inline]

abbrev Phenomena.Quantification.Studies.Montague1973.Ty.setIntens : Semantics.Montague.Ty

Equations

• Phenomena.Quantification.Studies.Montague1973.Ty.setIntens = ⦃⦃𝐬, ⦃𝐞, 𝐭⦄⦄, 𝐭⦄

inductive Phenomena.Quantification.Studies.Montague1973.Cat : Type

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

instance Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat : DecidableEq Cat

Equations

• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat = Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq

def Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq (x✝ x✝¹ : Cat) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq Phenomena.Quantification.Studies.Montague1973.Cat.t Phenomena.Quantification.Studies.Montague1973.Cat.t = isTrue ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq Phenomena.Quantification.Studies.Montague1973.Cat.t (a /' a_1) = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq Phenomena.Quantification.Studies.Montague1973.Cat.t (a \' a_1) = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq Phenomena.Quantification.Studies.Montague1973.Cat.t (a //' a_1) = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq Phenomena.Quantification.Studies.Montague1973.Cat.e Phenomena.Quantification.Studies.Montague1973.Cat.e = isTrue ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq Phenomena.Quantification.Studies.Montague1973.Cat.e (a /' a_1) = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq Phenomena.Quantification.Studies.Montague1973.Cat.e (a \' a_1) = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq Phenomena.Quantification.Studies.Montague1973.Cat.e (a //' a_1) = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq Phenomena.Quantification.Studies.Montague1973.Cat.CN Phenomena.Quantification.Studies.Montague1973.Cat.CN = isTrue ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq Phenomena.Quantification.Studies.Montague1973.Cat.CN (a /' a_1) = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq Phenomena.Quantification.Studies.Montague1973.Cat.CN (a \' a_1) = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq Phenomena.Quantification.Studies.Montague1973.Cat.CN (a //' a_1) = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq Phenomena.Quantification.Studies.Montague1973.Cat.IV Phenomena.Quantification.Studies.Montague1973.Cat.IV = isTrue ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq Phenomena.Quantification.Studies.Montague1973.Cat.IV (a /' a_1) = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq Phenomena.Quantification.Studies.Montague1973.Cat.IV (a \' a_1) = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq Phenomena.Quantification.Studies.Montague1973.Cat.IV (a //' a_1) = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq Phenomena.Quantification.Studies.Montague1973.Cat.TV Phenomena.Quantification.Studies.Montague1973.Cat.TV = isTrue ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq Phenomena.Quantification.Studies.Montague1973.Cat.TV (a /' a_1) = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq Phenomena.Quantification.Studies.Montague1973.Cat.TV (a \' a_1) = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq Phenomena.Quantification.Studies.Montague1973.Cat.TV (a //' a_1) = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq Phenomena.Quantification.Studies.Montague1973.Cat.T Phenomena.Quantification.Studies.Montague1973.Cat.T = isTrue ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq Phenomena.Quantification.Studies.Montague1973.Cat.T (a /' a_1) = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq Phenomena.Quantification.Studies.Montague1973.Cat.T (a \' a_1) = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq Phenomena.Quantification.Studies.Montague1973.Cat.T (a //' a_1) = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq (a /' a_1) Phenomena.Quantification.Studies.Montague1973.Cat.t = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq (a /' a_1) Phenomena.Quantification.Studies.Montague1973.Cat.e = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq (a /' a_1) Phenomena.Quantification.Studies.Montague1973.Cat.CN = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq (a /' a_1) Phenomena.Quantification.Studies.Montague1973.Cat.IV = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq (a /' a_1) Phenomena.Quantification.Studies.Montague1973.Cat.TV = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq (a /' a_1) Phenomena.Quantification.Studies.Montague1973.Cat.T = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq (a /' a_1) (a_2 \' a_3) = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq (a /' a_1) (a_2 //' a_3) = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq (a \' a_1) Phenomena.Quantification.Studies.Montague1973.Cat.t = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq (a \' a_1) Phenomena.Quantification.Studies.Montague1973.Cat.e = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq (a \' a_1) Phenomena.Quantification.Studies.Montague1973.Cat.CN = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq (a \' a_1) Phenomena.Quantification.Studies.Montague1973.Cat.IV = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq (a \' a_1) Phenomena.Quantification.Studies.Montague1973.Cat.TV = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq (a \' a_1) Phenomena.Quantification.Studies.Montague1973.Cat.T = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq (a \' a_1) (a_2 /' a_3) = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq (a \' a_1) (a_2 //' a_3) = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq (a //' a_1) Phenomena.Quantification.Studies.Montague1973.Cat.t = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq (a //' a_1) Phenomena.Quantification.Studies.Montague1973.Cat.e = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq (a //' a_1) Phenomena.Quantification.Studies.Montague1973.Cat.CN = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq (a //' a_1) Phenomena.Quantification.Studies.Montague1973.Cat.IV = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq (a //' a_1) Phenomena.Quantification.Studies.Montague1973.Cat.TV = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq (a //' a_1) Phenomena.Quantification.Studies.Montague1973.Cat.T = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq (a //' a_1) (a_2 /' a_3) = isFalse ⋯
• Phenomena.Quantification.Studies.Montague1973.instDecidableEqCat.decEq (a //' a_1) (a_2 \' a_3) = isFalse ⋯

instance Phenomena.Quantification.Studies.Montague1973.instReprCat : Repr Cat

Equations

• Phenomena.Quantification.Studies.Montague1973.instReprCat = { reprPrec := Phenomena.Quantification.Studies.Montague1973.instReprCat.repr }

def Phenomena.Quantification.Studies.Montague1973.instReprCat.repr : Cat → ℕ → Std.Format

Equations

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

def Phenomena.Quantification.Studies.Montague1973.«term_/'_» : Lean.TrailingParserDescr

Equations

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

def Phenomena.Quantification.Studies.Montague1973.«term_\'_» : Lean.TrailingParserDescr

Equations

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

def Phenomena.Quantification.Studies.Montague1973.«term_//'_» : Lean.TrailingParserDescr

Equations

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

def Phenomena.Quantification.Studies.Montague1973.catToTy : Cat → Semantics.Montague.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

• Phenomena.Quantification.Studies.Montague1973.catToTy Phenomena.Quantification.Studies.Montague1973.Cat.e = 𝐞
• Phenomena.Quantification.Studies.Montague1973.catToTy Phenomena.Quantification.Studies.Montague1973.Cat.t = 𝐭
• Phenomena.Quantification.Studies.Montague1973.catToTy Phenomena.Quantification.Studies.Montague1973.Cat.CN = ⦃𝐬, ⦃𝐞, 𝐭⦄⦄
• Phenomena.Quantification.Studies.Montague1973.catToTy Phenomena.Quantification.Studies.Montague1973.Cat.IV = ⦃𝐬, ⦃𝐞, 𝐭⦄⦄
• Phenomena.Quantification.Studies.Montague1973.catToTy Phenomena.Quantification.Studies.Montague1973.Cat.TV = ⦃⦃𝐬, Phenomena.Quantification.Studies.Montague1973.Ty.ptq_ett⦄, ⦃𝐬, ⦃𝐞, 𝐭⦄⦄⦄
• Phenomena.Quantification.Studies.Montague1973.catToTy Phenomena.Quantification.Studies.Montague1973.Cat.T = ⦃⦃𝐬, ⦃𝐞, 𝐭⦄⦄, 𝐭⦄
• Phenomena.Quantification.Studies.Montague1973.catToTy (a /' b) = ⦃⦃𝐬, Phenomena.Quantification.Studies.Montague1973.catToTy b⦄, Phenomena.Quantification.Studies.Montague1973.catToTy a⦄
• Phenomena.Quantification.Studies.Montague1973.catToTy (a \' b) = ⦃⦃𝐬, Phenomena.Quantification.Studies.Montague1973.catToTy b⦄, Phenomena.Quantification.Studies.Montague1973.catToTy a⦄
• Phenomena.Quantification.Studies.Montague1973.catToTy (a //' b) = ⦃⦃𝐬, Phenomena.Quantification.Studies.Montague1973.catToTy b⦄, Phenomena.Quantification.Studies.Montague1973.catToTy a⦄

theorem Phenomena.Quantification.Studies.Montague1973.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 Phenomena.Quantification.Studies.Montague1973.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

• Phenomena.Quantification.Studies.Montague1973.PTQModel = Semantics.Montague.Model

@[reducible, inline]

abbrev Phenomena.Quantification.Studies.Montague1973.PTQModel.Den (m : PTQModel) (τ : Semantics.Montague.Ty) : Type

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

Equations

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

@[reducible, inline]

abbrev Phenomena.Quantification.Studies.Montague1973.PTQModel.Intens (m : PTQModel) (a : Semantics.Montague.Ty) : Type

Intension: function from worlds to extensions

Equations

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

structure Phenomena.Quantification.Studies.Montague1973.LexEntry (m : PTQModel) : Type

Lexical Entry Structure

Each word has:

• Surface form
• Syntactic category
• Translation (semantic representation)

• form : String
• cat : Cat

inductive Phenomena.Quantification.Studies.Montague1973.SynRule : Type

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

def Phenomena.Quantification.Studies.Montague1973.instDecidableEqSynRule.decEq (x✝ x✝¹ : SynRule) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Quantification.Studies.Montague1973.instDecidableEqSynRule : DecidableEq SynRule

Equations

• Phenomena.Quantification.Studies.Montague1973.instDecidableEqSynRule = Phenomena.Quantification.Studies.Montague1973.instDecidableEqSynRule.decEq

def Phenomena.Quantification.Studies.Montague1973.instReprSynRule.repr : SynRule → ℕ → Std.Format

Equations

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

instance Phenomena.Quantification.Studies.Montague1973.instReprSynRule : Repr SynRule

Equations

• Phenomena.Quantification.Studies.Montague1973.instReprSynRule = { reprPrec := Phenomena.Quantification.Studies.Montague1973.instReprSynRule.repr }

inductive Phenomena.Quantification.Studies.Montague1973.TransRule : Type

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

def Phenomena.Quantification.Studies.Montague1973.instDecidableEqTransRule.decEq (x✝ x✝¹ : TransRule) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Quantification.Studies.Montague1973.instDecidableEqTransRule : DecidableEq TransRule

Equations

• Phenomena.Quantification.Studies.Montague1973.instDecidableEqTransRule = Phenomena.Quantification.Studies.Montague1973.instDecidableEqTransRule.decEq

def Phenomena.Quantification.Studies.Montague1973.instReprTransRule.repr : TransRule → ℕ → Std.Format

Equations

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

instance Phenomena.Quantification.Studies.Montague1973.instReprTransRule : Repr TransRule

Equations

• Phenomena.Quantification.Studies.Montague1973.instReprTransRule = { reprPrec := Phenomena.Quantification.Studies.Montague1973.instReprTransRule.repr }

inductive Phenomena.Quantification.Studies.Montague1973.ScopeReading : Type

Scope Reading

Represents different scope orderings of quantifiers.

• surface : ScopeReading
• inverse : ScopeReading

instance Phenomena.Quantification.Studies.Montague1973.instDecidableEqScopeReading : DecidableEq ScopeReading

Equations

• Phenomena.Quantification.Studies.Montague1973.instDecidableEqScopeReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Quantification.Studies.Montague1973.instReprScopeReading : Repr ScopeReading

Equations

• Phenomena.Quantification.Studies.Montague1973.instReprScopeReading = { reprPrec := Phenomena.Quantification.Studies.Montague1973.instReprScopeReading.repr }

def Phenomena.Quantification.Studies.Montague1973.instReprScopeReading.repr : ScopeReading → ℕ → Std.Format

Equations

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

inductive Phenomena.Quantification.Studies.Montague1973.ToyEntity : Type

A toy model for demonstrating scope ambiguity.

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

• m1 : ToyEntity
• m2 : ToyEntity
• w1 : ToyEntity
• w2 : ToyEntity

instance Phenomena.Quantification.Studies.Montague1973.instDecidableEqToyEntity : DecidableEq ToyEntity

Equations

• Phenomena.Quantification.Studies.Montague1973.instDecidableEqToyEntity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Quantification.Studies.Montague1973.instReprToyEntity : Repr ToyEntity

Equations

• Phenomena.Quantification.Studies.Montague1973.instReprToyEntity = { reprPrec := Phenomena.Quantification.Studies.Montague1973.instReprToyEntity.repr }

def Phenomena.Quantification.Studies.Montague1973.instReprToyEntity.repr : ToyEntity → ℕ → Std.Format

Equations

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

def Phenomena.Quantification.Studies.Montague1973.instBEqToyEntity.beq : ToyEntity → ToyEntity → Bool

Equations

• Phenomena.Quantification.Studies.Montague1973.instBEqToyEntity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Quantification.Studies.Montague1973.instBEqToyEntity : BEq ToyEntity

Equations

• Phenomena.Quantification.Studies.Montague1973.instBEqToyEntity = { beq := Phenomena.Quantification.Studies.Montague1973.instBEqToyEntity.beq }

def Phenomena.Quantification.Studies.Montague1973.toyPTQModel : PTQModel

Equations

• Phenomena.Quantification.Studies.Montague1973.toyPTQModel = { Entity := Phenomena.Quantification.Studies.Montague1973.ToyEntity, decEq := inferInstance }

def Phenomena.Quantification.Studies.Montague1973.isMan : ToyEntity → Bool

Predicate: is a man

Equations

• Phenomena.Quantification.Studies.Montague1973.isMan Phenomena.Quantification.Studies.Montague1973.ToyEntity.m1 = true
• Phenomena.Quantification.Studies.Montague1973.isMan Phenomena.Quantification.Studies.Montague1973.ToyEntity.m2 = true
• Phenomena.Quantification.Studies.Montague1973.isMan x✝ = false

def Phenomena.Quantification.Studies.Montague1973.isWoman : ToyEntity → Bool

Predicate: is a woman

Equations

• Phenomena.Quantification.Studies.Montague1973.isWoman Phenomena.Quantification.Studies.Montague1973.ToyEntity.w1 = true
• Phenomena.Quantification.Studies.Montague1973.isWoman Phenomena.Quantification.Studies.Montague1973.ToyEntity.w2 = true
• Phenomena.Quantification.Studies.Montague1973.isWoman x✝ = false

def Phenomena.Quantification.Studies.Montague1973.allEntities : List ToyEntity

All entities

Equations

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

def Phenomena.Quantification.Studies.Montague1973.loveSurface : ToyEntity → ToyEntity → Bool

Love relation for surface scope scenario.

m1 loves w1, m2 loves w2 (different women)

Equations

• Phenomena.Quantification.Studies.Montague1973.loveSurface Phenomena.Quantification.Studies.Montague1973.ToyEntity.m1 Phenomena.Quantification.Studies.Montague1973.ToyEntity.w1 = true
• Phenomena.Quantification.Studies.Montague1973.loveSurface Phenomena.Quantification.Studies.Montague1973.ToyEntity.m2 Phenomena.Quantification.Studies.Montague1973.ToyEntity.w2 = true
• Phenomena.Quantification.Studies.Montague1973.loveSurface x✝¹ x✝ = false

def Phenomena.Quantification.Studies.Montague1973.loveInverse : ToyEntity → ToyEntity → Bool

Love relation for inverse scope scenario.

m1 loves w1, m2 loves w1 (same woman)

Equations

• Phenomena.Quantification.Studies.Montague1973.loveInverse Phenomena.Quantification.Studies.Montague1973.ToyEntity.m1 Phenomena.Quantification.Studies.Montague1973.ToyEntity.w1 = true
• Phenomena.Quantification.Studies.Montague1973.loveInverse Phenomena.Quantification.Studies.Montague1973.ToyEntity.m2 Phenomena.Quantification.Studies.Montague1973.ToyEntity.w1 = true
• Phenomena.Quantification.Studies.Montague1973.loveInverse x✝¹ x✝ = false

def Phenomena.Quantification.Studies.Montague1973.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.

def Phenomena.Quantification.Studies.Montague1973.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.

theorem Phenomena.Quantification.Studies.Montague1973.surface_scope_surface_scenario : surfaceScopeTrue loveSurface = true

Surface scope is true in surface scenario.

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

theorem Phenomena.Quantification.Studies.Montague1973.inverse_scope_surface_scenario : inverseScopeTrue loveSurface = false

Inverse scope is false in surface scenario.

No single woman is loved by all men.

theorem Phenomena.Quantification.Studies.Montague1973.surface_scope_inverse_scenario : surfaceScopeTrue loveInverse = true

Both scopes are true in inverse scenario.

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

theorem Phenomena.Quantification.Studies.Montague1973.inverse_scope_inverse_scenario : inverseScopeTrue loveInverse = true

theorem Phenomena.Quantification.Studies.Montague1973.scope_readings_differ : surfaceScopeTrue loveSurface ≠ inverseScopeTrue loveSurface

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 Phenomena.Quantification.Studies.Montague1973.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 Phenomena.Quantification.Studies.Montague1973.Derivation : Type

Derivation Tree

Represents a syntactic derivation with rule applications.

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

def Phenomena.Quantification.Studies.Montague1973.instReprDerivation.repr : Derivation → ℕ → Std.Format

Equations

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

instance Phenomena.Quantification.Studies.Montague1973.instReprDerivation : Repr Derivation

Equations

• Phenomena.Quantification.Studies.Montague1973.instReprDerivation = { reprPrec := Phenomena.Quantification.Studies.Montague1973.instReprDerivation.repr }

def Phenomena.Quantification.Studies.Montague1973.Derivation.cat : Derivation → Cat

Derived category of a derivation.

Equations

• (Phenomena.Quantification.Studies.Montague1973.Derivation.lex a a_1).cat = a_1
• (Phenomena.Quantification.Studies.Montague1973.Derivation.apply Phenomena.Quantification.Studies.Montague1973.SynRule.S4 a_1 a_2).cat = Phenomena.Quantification.Studies.Montague1973.Cat.t
• (Phenomena.Quantification.Studies.Montague1973.Derivation.apply Phenomena.Quantification.Studies.Montague1973.SynRule.S5 a_1 a_2).cat = Phenomena.Quantification.Studies.Montague1973.Cat.IV
• (Phenomena.Quantification.Studies.Montague1973.Derivation.apply a a_1 a_2).cat = Phenomena.Quantification.Studies.Montague1973.Cat.t
• (Phenomena.Quantification.Studies.Montague1973.Derivation.quantIn a a_1 a_2).cat = Phenomena.Quantification.Studies.Montague1973.Cat.t