Linglib.Phenomena.Quantification.Studies.Montague1973

One or more equations did not get rendered due to their size.
Montague1973.instReprCat.repr Montague1973.Cat.t prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Montague1973.Cat.t")).group prec✝
Montague1973.instReprCat.repr Montague1973.Cat.e prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Montague1973.Cat.e")).group prec✝
Montague1973.instReprCat.repr Montague1973.Cat.CN prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Montague1973.Cat.CN")).group prec✝
Montague1973.instReprCat.repr Montague1973.Cat.IV prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Montague1973.Cat.IV")).group prec✝
Montague1973.instReprCat.repr Montague1973.Cat.TV prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Montague1973.Cat.TV")).group prec✝
Montague1973.instReprCat.repr Montague1973.Cat.T prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Montague1973.Cat.T")).group prec✝

Instances For

source

def Montague1973.«term_/'_» :

Lean.TrailingParserDescr

Equations

Montague1973.«term_/'_» = Lean.ParserDescr.trailingNode `Montague1973.«term_/'_» 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " /' ") (Lean.ParserDescr.cat `term 0))

Instances For

source

def Montague1973.«term_\'_» :

Lean.TrailingParserDescr

Equations

Montague1973.«term_\'_» = Lean.ParserDescr.trailingNode `Montague1973.«term_\'_» 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " \\' ") (Lean.ParserDescr.cat `term 0))

Instances For

source

def Montague1973.«term_//'_» :

Lean.TrailingParserDescr

Equations

Montague1973.«term_//'_» = Lean.ParserDescr.trailingNode `Montague1973.«term_//'_» 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " //' ") (Lean.ParserDescr.cat `term 0))

Instances For

source

def Montague1973.catToTy :

Cat → Core.Logic.Intensional.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

source

theorem 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.

source

@[reducible, inline]

abbrev Montague1973.PTQModel :

Type 1

Intensional Frame

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

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

Equations

Montague1973.PTQModel = Core.Logic.Intensional.Frame

Instances For

source

@[reducible, inline]

abbrev Montague1973.PTQModel.Den (F : PTQModel) (τ : Core.Logic.Intensional.Ty) :

Type

Denotation of a type in a frame (uses canonical Denot)

Equations

F.Den τ = Core.Logic.Intensional.Frame.Denot F τ

Instances For

source

@[reducible, inline]

abbrev Montague1973.PTQModel.Intens (F : PTQModel) (a : Core.Logic.Intensional.Ty) :

Type

Intension: function from indices to extensions

Equations

F.Intens a = (F.Index → Core.Logic.Intensional.Frame.Denot F a)

Instances For

source

structure Montague1973.LexEntry (F : PTQModel) :

Type

Lexical Entry Structure

Each word has:

Surface form
Syntactic category
Translation (semantic representation)

form : String
cat : Cat

Instances For

source

inductive 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

Instances For

source

def Montague1973.instDecidableEqSynRule.decEq (x✝ x✝¹ : SynRule) :

Decidable (x✝ = x✝¹)

Equations

Instances For

source

@[implicit_reducible]

instance Montague1973.instDecidableEqSynRule :

DecidableEq SynRule

Equations

Montague1973.instDecidableEqSynRule = Montague1973.instDecidableEqSynRule.decEq

source

@[implicit_reducible]

instance Montague1973.instReprSynRule :

Repr SynRule

Equations

Montague1973.instReprSynRule = { reprPrec := Montague1973.instReprSynRule.repr }

source

def Montague1973.instReprSynRule.repr :

SynRule → ℕ → Std.Format

Equations

One or more equations did not get rendered due to their size.
Montague1973.instReprSynRule.repr Montague1973.SynRule.S1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Montague1973.SynRule.S1")).group prec✝
Montague1973.instReprSynRule.repr Montague1973.SynRule.S2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Montague1973.SynRule.S2")).group prec✝
Montague1973.instReprSynRule.repr Montague1973.SynRule.S3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Montague1973.SynRule.S3")).group prec✝
Montague1973.instReprSynRule.repr Montague1973.SynRule.S4 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Montague1973.SynRule.S4")).group prec✝
Montague1973.instReprSynRule.repr Montague1973.SynRule.S5 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Montague1973.SynRule.S5")).group prec✝