Montague (1973): The Proper Treatment of Quantification in Ordinary English

Montague's fragment of English builds its sentences by analysis trees, which record the rules used, so a sentence with two readings has two trees. An interpretation gives every word a sense, its extension at each index (a possible world at a moment). Nouns and verbs apply to individual concepts, functions from indices to individuals, so the temperature can name something whose value changes over time. Montague's meaning postulates single out the logically possible interpretations. In these, names and ordinary nouns concern only constant concepts, those with the same value at every index, and most verbs depend only on the current values of their arguments. One sentence entails another when every logically possible interpretation makes the second true wherever it makes the first true.

Main statements

• every_man_walks_iff, a_man_walks_iff, the_man_walks_iff: the simple sentences mean what their first-order paraphrases say, because ordinary nouns hold only of constant concepts.
• Interp.LogicallyPossible.extTV_starTV: an ordinary transitive verb is determined by the relation between individuals that it expresses; likewise for nouns and intransitive verbs.
• aWomanLovesEveryMan.not_entails: a woman loves every man has two readings, one for each order of the quantifiers, and they are not equivalent.
• not_entails_ninetyRises: from the temperature is ninety and the temperature rises it does not follow that ninety rises.
• a_price_rises_needs_concepts: a price rises can be true although no individual price rises.
• johnSeeksAUnicorn.exists_unicorn_of_deRe, johnSeeksAUnicorn.not_entails: on one reading John seeks a unicorn implies that there are unicorns, and on the other it does not.

Implementation notes

Montague translates each tree into intensional logic and then interprets the logic; Analysis.realize does both steps at once, as his footnote 13 allows. One index type stands for his world–moment pairs, and tense is omitted. Of his nine meaning postulates, only the five that mention no word outside the fragment are imposed.

References

• [Mon73]

Categories and the category-to-type map

inductive Montague1973.Cat : Type

The syntactic categories are e, t, and the functor categories A/B and A//B, which are distinct categories with the same type.

• e : Cat
• t : Cat
• slash : Cat → Cat → Cat
• dslash : Cat → Cat → Cat

@[instance_reducible]

instance Montague1973.instDecidableEqCat : DecidableEq Cat

Equations

• Montague1973.instDecidableEqCat = Montague1973.instDecidableEqCat.decEq

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

Equations

• One or more equations did not get rendered due to their size.
• Montague1973.instDecidableEqCat.decEq Montague1973.Cat.e Montague1973.Cat.e = isTrue ⋯
• Montague1973.instDecidableEqCat.decEq Montague1973.Cat.e Montague1973.Cat.t = isFalse Montague1973.instDecidableEqCat.decEq._proof_3
• Montague1973.instDecidableEqCat.decEq Montague1973.Cat.e (a.slash a_1) = isFalse ⋯
• Montague1973.instDecidableEqCat.decEq Montague1973.Cat.e (a.dslash a_1) = isFalse ⋯
• Montague1973.instDecidableEqCat.decEq Montague1973.Cat.t Montague1973.Cat.e = isFalse Montague1973.instDecidableEqCat.decEq._proof_6
• Montague1973.instDecidableEqCat.decEq Montague1973.Cat.t Montague1973.Cat.t = isTrue ⋯
• Montague1973.instDecidableEqCat.decEq Montague1973.Cat.t (a.slash a_1) = isFalse ⋯
• Montague1973.instDecidableEqCat.decEq Montague1973.Cat.t (a.dslash a_1) = isFalse ⋯
• Montague1973.instDecidableEqCat.decEq (a.slash a_1) Montague1973.Cat.e = isFalse ⋯
• Montague1973.instDecidableEqCat.decEq (a.slash a_1) Montague1973.Cat.t = isFalse ⋯
• Montague1973.instDecidableEqCat.decEq (a.slash a_1) (a_2.dslash a_3) = isFalse ⋯
• Montague1973.instDecidableEqCat.decEq (a.dslash a_1) Montague1973.Cat.e = isFalse ⋯
• Montague1973.instDecidableEqCat.decEq (a.dslash a_1) Montague1973.Cat.t = isFalse ⋯
• Montague1973.instDecidableEqCat.decEq (a.dslash a_1) (a_2.slash a_3) = isFalse ⋯

@[instance_reducible]

instance Montague1973.instReprCat : Repr Cat

Equations

• Montague1973.instReprCat = { reprPrec := Montague1973.instReprCat.repr }

def Montague1973.instReprCat.repr : Cat → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• 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.t prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Montague1973.Cat.t")).group prec✝

@[reducible, inline]

abbrev Montague1973.Cat.IV : Cat

IV = t/e is the category of intransitive verb phrases.

Equations

• Montague1973.Cat.IV = Montague1973.Cat.t.slash Montague1973.Cat.e

@[reducible, inline]

abbrev Montague1973.Cat.T : Cat

T = t/IV is the category of terms.

Equations

• Montague1973.Cat.T = Montague1973.Cat.t.slash Montague1973.Cat.IV

@[reducible, inline]

abbrev Montague1973.Cat.TV : Cat

TV = IV/T is the category of transitive verb phrases.

Equations

• Montague1973.Cat.TV = Montague1973.Cat.IV.slash Montague1973.Cat.T

@[reducible, inline]

abbrev Montague1973.Cat.CN : Cat

CN = t//e is the category of common noun phrases.

Equations

• Montague1973.Cat.CN = Montague1973.Cat.t.dslash Montague1973.Cat.e

@[reducible, inline]

abbrev Montague1973.Cat.ty : Cat → Montague.Ty

The category-to-type map f sends e to e, t to t, and both A/B and A//B to ⟨⟨s, f(B)⟩, f(A)⟩.

Equations

• Montague1973.Cat.e.ty = Montague.Ty.e
• Montague1973.Cat.t.ty = Montague.Ty.t
• (a.slash b).ty = (b.ty.intens ⇒ a.ty)
• (a.dslash b).ty = (b.ty.intens ⇒ a.ty)

Basic expressions and analysis trees

inductive Montague1973.ProperNoun : Type

T1(d) translates the proper nouns through the constants j, m, b, n of type e.

• john : ProperNoun
• mary : ProperNoun
• bill : ProperNoun
• ninety : ProperNoun

inductive Montague1973.Basic : Cat → Type

Basic A holds the basic expressions of category A in the domain of g that the examples use, which T1(a) translates into constants. be, necessarily and the basic terms are outside the domain of g.

• man : Basic Cat.CN
• woman : Basic Cat.CN
• unicorn : Basic Cat.CN
• price : Basic Cat.CN
• temperature : Basic Cat.CN
• walk : Basic Cat.IV
• rise : Basic Cat.IV
• love : Basic Cat.TV
• find : Basic Cat.TV
• seek : Basic Cat.TV

inductive Montague1973.Analysis : Cat → Type

Analysis A is the type of analysis trees of category A built by the rules the examples use. The leaves are the basic expressions of S1, split as T1 translates them into the domain of g, the proper nouns, the pronouns heₙ and be; the nodes are the determiners of S2, subject–predicate F₄ (S4), verb–object F₅ (S5) and quantifying-in F₁₀,ₙ (S14).

• basic {A : Cat} : Basic A → Analysis A
• name : ProperNoun → Analysis Cat.T
• he (n : ℕ) : Analysis Cat.T
• be : Analysis Cat.TV
• every : Analysis Cat.CN → Analysis Cat.T
• the : Analysis Cat.CN → Analysis Cat.T
• a : Analysis Cat.CN → Analysis Cat.T
• f4 : Analysis Cat.T → Analysis Cat.IV → Analysis Cat.t
• f5 : Analysis Cat.TV → Analysis Cat.T → Analysis Cat.IV
• f10 (n : ℕ) : Analysis Cat.T → Analysis Cat.t → Analysis Cat.t

Interpretations and the induced interpretation of English

structure Montague1973.Interp (E W : Type) : Type

An interpretation ⟨A, I, J, ≤, F⟩ of the fragment's constants has one type W of points of reference, and F gives each constant a sense, an extension at every index.

• name : ProperNoun → W → E

  F assigns each of the constants j, m, b, n an individual concept.

• const {A : Cat} : Basic A → W → Montague.Ty.Domain E W A.ty

  F assigns the constant g(α) a sense of type f(A).

def Montague1973.Analysis.realize {E W : Type} (M : Interp E W) {A : Cat} : Analysis A → Assignment (W → E) → W → Montague.Ty.Domain E W A.ty

φ.realize M g i is the extension at index i, under the assignment g of the individual-concept variables xₙ, of the translation of φ by T1, T2, T4, T5 and T14. The proper nouns translate to j*, …, that is P̂ P{^j}; heₙ to P̂ P{xₙ}; be to 𝒫̂ x̂ 𝒫{ŷ [ˇx = ˇy]}; the determiners to the quantifiers every, the and some over individual concepts; the rules of functional application to δ'(^β'); and quantifying-in to α'(x̂ₙ φ').

Equations

• One or more equations did not get rendered due to their size.
• Montague1973.Analysis.realize M (Montague1973.Analysis.basic α) x✝¹ x✝ = M.const α x✝
• Montague1973.Analysis.realize M (Montague1973.Analysis.name α) x✝¹ x✝ = fun (P : Montague.Ty.Domain E W Montague1973.Cat.IV.ty.intens) => P x✝ (M.name α)
• Montague1973.Analysis.realize M (Montague1973.Analysis.he n) x✝¹ x✝ = fun (P : Montague.Ty.Domain E W Montague1973.Cat.IV.ty.intens) => P x✝ (x✝¹ n)
• Montague1973.Analysis.realize M ζ.every x✝¹ x✝ = fun (P : Montague.Ty.Domain E W Montague1973.Cat.IV.ty.intens) => Quantifier.GQ.every (Montague1973.Analysis.realize M ζ x✝¹ x✝) (P x✝)
• Montague1973.Analysis.realize M ζ.the x✝¹ x✝ = fun (P : Montague.Ty.Domain E W Montague1973.Cat.IV.ty.intens) => Quantifier.GQ.the (Montague1973.Analysis.realize M ζ x✝¹ x✝) (P x✝)
• Montague1973.Analysis.realize M ζ.a x✝¹ x✝ = fun (P : Montague.Ty.Domain E W Montague1973.Cat.IV.ty.intens) => Quantifier.GQ.some (Montague1973.Analysis.realize M ζ x✝¹ x✝) (P x✝)
• Montague1973.Analysis.realize M (α.f4 δ) x✝¹ x✝ = Montague1973.Analysis.realize M α x✝¹ x✝ fun (j : W) => Montague1973.Analysis.realize M δ x✝¹ j
• Montague1973.Analysis.realize M (δ.f5 β) x✝¹ x✝ = Montague1973.Analysis.realize M δ x✝¹ x✝ fun (j : W) => Montague1973.Analysis.realize M β x✝¹ j

*-counterparts and extensional senses

rigidCN, extIV and extTV build a sense from a set of individuals or a relation between them, and δ* recovers the set or relation from the sense.

def Montague1973.starIV {E W : Type} (δ : Montague.Ty.Domain E W (Montague.Ty.e.intens ⇒ Montague.Ty.t)) : E → Prop

starIV δ is δ* for δ of type f(IV) = f(CN), the set û δ(^u) of individuals whose constant concept is in δ.

Equations

• Montague1973.starIV δ u = δ fun (x : W) => u

def Montague1973.starTV {E W : Type} (δ : Montague.Ty.Domain E W Cat.TV.ty) : E → E → Prop

starTV δ is δ* for δ of type f(TV), the relation v̂ û δ(^u, ^v*) with the object first, so starTV δ v u says that u bears δ to v.

Equations

• Montague1973.starTV δ v u = δ (fun (j : W) (P : Montague.Ty.Domain E W Montague1973.Cat.IV.ty.intens) => P j fun (x : W) => v) fun (x : W) => u

def Montague1973.rigidCN {E W : Type} (m : W → E → Prop) : W → Montague.Ty.Domain E W Cat.CN.ty

rigidCN m is the common-noun sense holding of the constant concepts of members of m, the form postulate (2) gives an ordinary noun.

Equations

• Montague1973.rigidCN m i x = (Reference.IsRigid x ∧ m i (x i))

def Montague1973.extIV {E W : Type} (m : W → E → Prop) : W → Montague.Ty.Domain E W Cat.IV.ty

extIV m is the intransitive-verb sense x̂ M{ˇx} of a property M of individuals, the form postulate (3) requires.

Equations

• Montague1973.extIV m i x = m i (x i)

def Montague1973.extTV {E W : Type} (S : W → E → E → Prop) : W → Montague.Ty.Domain E W Cat.TV.ty

extTV S is the transitive-verb sense 𝒫̂ x̂ 𝒫{ŷ S{ˇx, ˇy}} of a relation-in-intension S between individuals, object first, the form postulate (4) requires.

Equations

• Montague1973.extTV S i Q x = Q i fun (j : W) (y : Montague.Ty.Domain E W Montague1973.Cat.e.ty.intens) => S j (y j) (x j)

@[simp]

theorem Montague1973.starIV_rigidCN {E W : Type} (m : W → E → Prop) (i : W) : starIV (rigidCN m i) = m i

@[simp]

theorem Montague1973.starIV_extIV {E W : Type} (m : W → E → Prop) (i : W) : starIV (extIV m i) = m i

@[simp]

theorem Montague1973.starTV_extTV {E W : Type} (S : W → E → E → Prop) (i : W) : starTV (extTV S i) = S i

theorem Montague1973.realize_be {E W : Type} (M : Interp E W) (g : Assignment (W → E)) : (fun (i : W) => Analysis.realize M Analysis.be g i) = extTV fun (x : W) (v u : E) => u = v

The translation of be has the form postulate (4) requires in every interpretation, the relation being identity, so the extensionality of be need not be postulated.

Meaning postulates and logical consequence

structure Montague1973.Interp.LogicallyPossible {E W : Type} (M : Interp E W) : Prop

An interpretation is logically possible when the meaning postulates (1)–(5) hold. The proper nouns are rigid, the ordinary common nouns (all but price and temperature) hold only of constant concepts, the intransitive verbs other than rise and the transitive verbs other than seek are extensional, and seek is extensional in subject position.

• name_rigid (α : ProperNoun) : Reference.IsRigid (M.name α)

  Postulate (1) is ∨u □[u = α].

• noun_rigid (α : Basic Cat.CN) : α ≠ Basic.price → α ≠ Basic.temperature → ∀ (i : W) (x : Montague.Ty.Domain E W Cat.e.ty.intens), M.const α i x → Reference.IsRigid x

  Postulate (2) is □[δ(x) → ∨u x = ^u].

• iv_ext (α : Basic Cat.IV) : α ≠ Basic.rise → M.const α ∈ Set.range extIV

  Postulate (3) is ∨M ∧x □[δ(x) ↔ M{ˇx}].

• tv_ext (α : Basic Cat.TV) : α ≠ Basic.seek → M.const α ∈ Set.range extTV

  Postulate (4) is ∨S ∧x ∧𝒫 □[δ(x, 𝒫) ↔ 𝒫{ŷ S{ˇx, ˇy}}].

• seek_ext (Q : W → Montague.Ty.Domain E W Cat.T.ty) : (fun (i : W) => M.const Basic.seek i Q) ∈ Set.range extIV

  Postulate (5) is ∧𝒫 ∨M ∧x □[δ(x, 𝒫) ↔ M{ˇx}].

def Montague1973.Entails (Γ : Set (Analysis Cat.t)) (ψ : Analysis Cat.t) : Prop

Γ entails ψ when every logically possible interpretation makes ψ true at every index at which it makes every member of Γ true, a sentence being true at an index when its translation is true there under every assignment.

Equations

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

theorem Montague1973.Interp.LogicallyPossible.rigidCN_starIV {E W : Type} {M : Interp E W} (h : M.LogicallyPossible) {α : Basic Cat.CN} (h₁ : α ≠ Basic.price) (h₂ : α ≠ Basic.temperature) : (rigidCN fun (i : W) => starIV (M.const α i)) = M.const α

An ordinary common noun is definable from its *-counterpart on constant concepts, □[δ(x) ↔ ∨u[x = ^u] ∧ δ*(ˇx)]. The paper's □[δ(x) ↔ δ*(ˇx)] holds only for intransitive verbs, as the editors note, since an ordinary noun fails of every non-constant concept.

theorem Montague1973.Interp.LogicallyPossible.extIV_starIV {E W : Type} {M : Interp E W} (h : M.LogicallyPossible) {α : Basic Cat.IV} (hα : α ≠ Basic.rise) : (extIV fun (i : W) => starIV (M.const α i)) = M.const α

An intransitive verb other than rise is definable from its *-counterpart, □[δ(x) ↔ δ*(ˇx)].

theorem Montague1973.Interp.LogicallyPossible.extTV_starTV {E W : Type} {M : Interp E W} (h : M.LogicallyPossible) {α : Basic Cat.TV} (hα : α ≠ Basic.seek) : (extTV fun (i : W) => starTV (M.const α i)) = M.const α

A transitive verb other than seek is definable from its *-counterpart, □[δ(x, 𝒫) ↔ 𝒫{ŷ δ*(ˇx, ˇy)}].

Quantifying over constant concepts

When a quantifier's restriction holds only of constant concepts, as an ordinary noun does, quantifying over the concepts is quantifying over individuals.

theorem Montague1973.every_iff_of_rigid {E W : Type} [Nonempty W] {R S : (W → E) → Prop} (hR : ∀ (x : W → E), R x → Reference.IsRigid x) : Quantifier.GQ.every R S ↔ Quantifier.GQ.every (starIV R) (starIV S)

theorem Montague1973.some_iff_of_rigid {E W : Type} [Nonempty W] {R S : (W → E) → Prop} (hR : ∀ (x : W → E), R x → Reference.IsRigid x) : Quantifier.GQ.some R S ↔ Quantifier.GQ.some (starIV R) (starIV S)

theorem Montague1973.the_iff_of_rigid {E W : Type} [Nonempty W] {R S : (W → E) → Prop} (hR : ∀ (x : W → E), R x → Reference.IsRigid x) : Quantifier.GQ.the R S ↔ Quantifier.GQ.the (starIV R) (starIV S)

The examples of §4: extensional cases

theorem Montague1973.bill_walks_iff {E W : Type} {M : Interp E W} (h : M.LogicallyPossible) (g : Assignment (W → E)) (i : W) : Analysis.realize M ((Analysis.name ProperNoun.bill).f4 (Analysis.basic Basic.walk)) g i ↔ starIV (M.const Basic.walk i) (M.name ProperNoun.bill i)

Bill walks translates to walk'*(b).

theorem Montague1973.a_man_walks_iff {E W : Type} {M : Interp E W} (h : M.LogicallyPossible) (g : Assignment (W → E)) (i : W) : Analysis.realize M ((Analysis.basic Basic.man).a.f4 (Analysis.basic Basic.walk)) g i ↔ Quantifier.GQ.some (starIV (M.const Basic.man i)) (starIV (M.const Basic.walk i))

a man walks translates to ∨u[man'*(u) ∧ walk'*(u)].

theorem Montague1973.every_man_walks_iff {E W : Type} {M : Interp E W} (h : M.LogicallyPossible) (g : Assignment (W → E)) (i : W) : Analysis.realize M ((Analysis.basic Basic.man).every.f4 (Analysis.basic Basic.walk)) g i ↔ Quantifier.GQ.every (starIV (M.const Basic.man i)) (starIV (M.const Basic.walk i))

every man walks translates to ∧u[man'*(u) → walk'*(u)].

theorem Montague1973.the_man_walks_iff {E W : Type} {M : Interp E W} (h : M.LogicallyPossible) (g : Assignment (W → E)) (i : W) : Analysis.realize M ((Analysis.basic Basic.man).the.f4 (Analysis.basic Basic.walk)) g i ↔ Quantifier.GQ.the (starIV (M.const Basic.man i)) (starIV (M.const Basic.walk i))

the man walks translates to ∨v∧u[[man'*(u) ↔ u = v] ∧ walk'*(v)].

theorem Montague1973.john_finds_a_unicorn_iff {E W : Type} {M : Interp E W} (h : M.LogicallyPossible) (g : Assignment (W → E)) (i : W) : Analysis.realize M ((Analysis.name ProperNoun.john).f4 ((Analysis.basic Basic.find).f5 (Analysis.basic Basic.unicorn).a)) g i ↔ Quantifier.GQ.some (starIV (M.const Basic.unicorn i)) fun (x : E) => starTV (M.const Basic.find i) x (M.name ProperNoun.john i)

John finds a unicorn translates to ∨u[unicorn'*(u) ∧ find'*(j, u)].

theorem Montague1973.bill_is_mary_iff {E W : Type} {M : Interp E W} (g : Assignment (W → E)) (i : W) : Analysis.realize M ((Analysis.name ProperNoun.bill).f4 (Analysis.be.f5 (Analysis.name ProperNoun.mary))) g i ↔ M.name ProperNoun.bill i = M.name ProperNoun.mary i

Bill is Mary translates to b = m.

theorem Montague1973.bill_is_a_man_iff {E W : Type} {M : Interp E W} (h : M.LogicallyPossible) (g : Assignment (W → E)) (i : W) : Analysis.realize M ((Analysis.name ProperNoun.bill).f4 (Analysis.be.f5 (Analysis.basic Basic.man).a)) g i ↔ starIV (M.const Basic.man i) (M.name ProperNoun.bill i)

Bill is a man translates to man'*(b).

A woman loves every man: two analysis trees

def Montague1973.aWomanLovesEveryMan.direct : Analysis Cat.t

The direct analysis of a woman loves every man is F₄(a woman, F₅(love, every man)).

Equations

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

def Montague1973.aWomanLovesEveryMan.quantifiedIn : Analysis Cat.t

The quantifying-in analysis of a woman loves every man is F₁₀,₀(every man, F₄(a woman, F₅(love, he₀))).

Equations

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

theorem Montague1973.aWomanLovesEveryMan.direct_iff {E W : Type} {M : Interp E W} (h : M.LogicallyPossible) (g : Assignment (W → E)) (i : W) : Analysis.realize M direct g i ↔ Quantifier.Polyadic.surfaceScope Quantifier.GQ.some Quantifier.GQ.every (starIV (M.const Basic.woman i)) (starIV (M.const Basic.man i)) (flip (starTV (M.const Basic.love i)))

The direct analysis translates to ∨u[woman'*(u) ∧ ∧v[man'*(v) → love'*(u, v)]], on which the existential scopes over the universal.

theorem Montague1973.aWomanLovesEveryMan.quantifiedIn_iff {E W : Type} {M : Interp E W} (h : M.LogicallyPossible) (g : Assignment (W → E)) (i : W) : Analysis.realize M quantifiedIn g i ↔ Quantifier.Polyadic.inverseScope Quantifier.GQ.some Quantifier.GQ.every (starIV (M.const Basic.woman i)) (starIV (M.const Basic.man i)) (flip (starTV (M.const Basic.love i)))

The quantifying-in analysis translates to ∧v[man'*(v) → ∨u[woman'*(u) ∧ love'*(u, v)]], on which the universal scopes over the existential.

Countermodels over one index

def Montague1973.staticInterp : Interp ℕ Unit

staticInterp has a single index and four individuals, the men 0 and 1 and the women 2 and 3. Each man is loved by a woman, no woman loves both men, nothing is a unicorn, and John seeks everything.

Equations

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

theorem Montague1973.staticInterp_logicallyPossible : staticInterp.LogicallyPossible

theorem Montague1973.aWomanLovesEveryMan.not_entails : ¬Entails {quantifiedIn} direct

A woman loves every man is ambiguous, since its quantifying-in reading does not entail its direct one.

John seeks a unicorn: de dicto and de re

def Montague1973.johnSeeksAUnicorn.deDicto : Analysis Cat.t

The de dicto analysis of John seeks a unicorn is F₄(John, F₅(seek, a unicorn)).

Equations

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

def Montague1973.johnSeeksAUnicorn.deRe : Analysis Cat.t

The de re analysis of John seeks a unicorn is F₁₀,₀(a unicorn, F₄(John, F₅(seek, he₀))).

Equations

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

theorem Montague1973.johnSeeksAUnicorn.deDicto_iff {E W : Type} {M : Interp E W} (h : M.LogicallyPossible) (g : Assignment (W → E)) (i : W) : Analysis.realize M deDicto g i ↔ M.const Basic.seek i (fun (j : W) (P : Montague.Ty.Domain E W Cat.IV.ty.intens) => Quantifier.GQ.some (starIV (M.const Basic.unicorn j)) (starIV (P j))) (M.name ProperNoun.john)

The de dicto analysis translates to seek'(^j, P̂ ∨u[unicorn'*(u) ∧ P{^u}]).

theorem Montague1973.johnSeeksAUnicorn.deRe_iff {E W : Type} {M : Interp E W} (h : M.LogicallyPossible) (g : Assignment (W → E)) (i : W) : Analysis.realize M deRe g i ↔ Quantifier.GQ.some (starIV (M.const Basic.unicorn i)) fun (x : E) => starTV (M.const Basic.seek i) x (M.name ProperNoun.john i)

The de re analysis translates to ∨u[unicorn'*(u) ∧ seek'*(j, u)].

theorem Montague1973.johnSeeksAUnicorn.exists_unicorn_of_deRe {E W : Type} {M : Interp E W} (h : M.LogicallyPossible) (g : Assignment (W → E)) (i : W) (H : Analysis.realize M deRe g i) : ∃ (u : E), starIV (M.const Basic.unicorn i) u

The de re reading entails that there are unicorns.

theorem Montague1973.johnSeeksAUnicorn.deDicto_without_unicorns (g : Assignment (Unit → ℕ)) : Analysis.realize staticInterp deDicto g () ∧ ∀ (u : ℕ), ¬starIV (staticInterp.const Basic.unicorn ()) u

The de dicto reading is true in staticInterp, where there are no unicorns.

theorem Montague1973.johnSeeksAUnicorn.not_entails : ¬Entails {deDicto} deRe

John seeks a unicorn is ambiguous, since its de dicto reading does not entail its de re one.

The temperature puzzle

def Montague1973.theTemperatureIsNinety : Analysis Cat.t

the temperature is ninety is analysed as F₄(the temperature, F₅(be, ninety)).

Equations

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

def Montague1973.theTemperatureRises : Analysis Cat.t

the temperature rises is analysed as F₄(the temperature, rise).

Equations

• Montague1973.theTemperatureRises = (Montague1973.Analysis.basic Montague1973.Basic.temperature).the.f4 (Montague1973.Analysis.basic Montague1973.Basic.rise)

def Montague1973.ninetyRises : Analysis Cat.t

ninety rises is analysed as F₄(ninety, rise).

Equations

• Montague1973.ninetyRises = (Montague1973.Analysis.name Montague1973.ProperNoun.ninety).f4 (Montague1973.Analysis.basic Montague1973.Basic.rise)

theorem Montague1973.theTemperatureIsNinety_iff {E W : Type} (M : Interp E W) (g : Assignment (W → E)) (i : W) : Analysis.realize M theTemperatureIsNinety g i ↔ Quantifier.GQ.the (M.const Basic.temperature i) fun (y : Montague.Ty.Domain E W Cat.e.ty.intens) => y i = M.name ProperNoun.ninety i

the temperature is ninety translates to ∨y[∧x[temperature'(x) ↔ x = y] ∧ [ˇy] = n].

theorem Montague1973.theTemperatureRises_iff {E W : Type} (M : Interp E W) (g : Assignment (W → E)) (i : W) : Analysis.realize M theTemperatureRises g i ↔ Quantifier.GQ.the (M.const Basic.temperature i) (M.const Basic.rise i)

the temperature rises translates to ∨y[∧x[temperature'(x) ↔ x = y] ∧ rise'(y)].

theorem Montague1973.ninetyRises_iff {E W : Type} (M : Interp E W) (g : Assignment (W → E)) (i : W) : Analysis.realize M ninetyRises g i ↔ M.const Basic.rise i (M.name ProperNoun.ninety)

ninety rises translates to rise'(^n).

theorem Montague1973.a_price_rises_iff {E W : Type} (M : Interp E W) (g : Assignment (W → E)) (i : W) : Analysis.realize M ((Analysis.basic Basic.price).a.f4 (Analysis.basic Basic.rise)) g i ↔ Quantifier.GQ.some (M.const Basic.price i) (M.const Basic.rise i)

a price rises translates to ∨x[price'(x) ∧ rise'(x)], with an individual-concept variable.

def Montague1973.temperatureConcept : Fin 2 → ℕ

temperatureConcept is a temperature of 90 at the first moment and 95 at the second.

Equations

• Montague1973.temperatureConcept = ![90, 95]

def Montague1973.temperatureInterp : Interp ℕ (Fin 2)

temperatureInterp interprets the fragment over numbers and two moments. price and temperature hold of the one concept temperatureConcept, a concept rises at a moment if its value is larger at a later one, and nothing else holds of anything.

Equations

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

theorem Montague1973.temperatureInterp_logicallyPossible : temperatureInterp.LogicallyPossible

theorem Montague1973.not_entails_ninetyRises : ¬Entails {theTemperatureIsNinety, theTemperatureRises} ninetyRises

Partee's argument is invalid, since at the first moment of temperatureInterp the temperature is ninety and the temperature rises are true and ninety rises is false.

theorem Montague1973.a_price_rises_needs_concepts (g : Assignment (Fin 2 → ℕ)) : Analysis.realize temperatureInterp ((Analysis.basic Basic.price).a.f4 (Analysis.basic Basic.rise)) g 0 ∧ ¬Quantifier.GQ.some (starIV (temperatureInterp.const Basic.price 0)) (starIV (temperatureInterp.const Basic.rise 0))

a price rises is true at the first moment of temperatureInterp while its individual-variable symbolization ∨u[price'*(u) ∧ rise'*(u)] is false, so unlike a man walks it needs individual-concept variables.