@cite{percus-2000}: Constraints on Situation Variables in Syntax @cite{percus-2000}

@cite{heim-kratzer-1998} @cite{kratzer-1998} @cite{partee-1973}

Formalizes Percus's theory of situation pronouns in LF and derives concrete de re / de dicto predictions from Fragment lexical entries.

Every predicate takes a situation argument, every clause introduces a lambda-s binder, and Generalization X constrains which binder can bind which variable.

Generalization X

The situation pronoun that a predicate is associated with must be bound by the minimal c-commanding situation binder.

Situation Assignment Infrastructure

Situation assignments specialize Core.Assignment from D = Time (Partee's temporal variables) to D = WorldTimeIndex W Time (Percus's situation variables).

Empirical Chain

Fragments/English/Predicates/Verbal.lean
  "believe": opaqueContext = true, attitude =.doxastic.nonVeridical
  "think": opaqueContext = true, attitude =.doxastic.nonVeridical
    ↓ (opaqueContext = true → introduces situation binder λs)
(this file: theory + empirical predictions)
  believeSit: ∀s' ∈ Dox(s). complement(g[n ↦ s'])
  genXWellFormed / genYWellFormed: filter readings
    ↓ (concrete model + predicate denotations)
  reading computations → truth values → match empirical judgments

@[reducible, inline]

abbrev Percus2000.SituationAssignment (W : Type u_1) (Time : Type u_2) : Type (max u_2 u_1)

Situation assignment function: maps variable indices to situations.

Equations

• Percus2000.SituationAssignment W Time = Core.Assignment (Core.WorldTimeIndex W Time)

@[reducible, inline]

abbrev Percus2000.interpSitVar {W : Type u_1} {Time : Type u_2} (n : ℕ) (g : SituationAssignment W Time) : Core.WorldTimeIndex W Time

Situation variable denotation: s_n^g = g(n).

Equations

• Percus2000.interpSitVar n g = g n

@[reducible, inline]

abbrev Percus2000.updateSitVar {W : Type u_1} {Time : Type u_2} (g : SituationAssignment W Time) (n : ℕ) (s : Core.WorldTimeIndex W Time) : SituationAssignment W Time

Modified situation assignment g[n -> s].

Equations

• Percus2000.updateSitVar g n s = Core.Assignment.update g n s

@[reducible, inline]

abbrev Percus2000.sitLambdaAbs {W : Type u_1} {Time : Type u_2} {α : Type u_3} (n : ℕ) (body : SituationAssignment W Time → α) : SituationAssignment W Time → Core.WorldTimeIndex W Time → α

Situation lambda abstraction: bind a situation variable.

Equations

• Percus2000.sitLambdaAbs n body g s = body (Core.Assignment.update g n s)

structure Percus2000.PredicateBinding : Type

• sitVarIndex : ℕ
• closestBinderIndex : ℕ

def Percus2000.PredicateBinding.genXCompliant (b : PredicateBinding) : Bool

Equations

• b.genXCompliant = (b.sitVarIndex == b.closestBinderIndex)

def Percus2000.genXWellFormed (bindings : List PredicateBinding) : Bool

Equations

• Percus2000.genXWellFormed bindings = bindings.all Percus2000.PredicateBinding.genXCompliant

def Percus2000.genYWellFormed (quantifierBindings : List PredicateBinding) : Bool

Generalization Y: adverbial quantifiers must use nearest binder.

Equations

• Percus2000.genYWellFormed quantifierBindings = quantifierBindings.all Percus2000.PredicateBinding.genXCompliant

def Percus2000.genXYWellFormed (predicateBindings quantifierBindings : List PredicateBinding) : Bool

Equations

• Percus2000.genXYWellFormed predicateBindings quantifierBindings = (Percus2000.genXWellFormed predicateBindings && Percus2000.genYWellFormed quantifierBindings)

def Percus2000.GenXAsTowerDepth {C : Type u_1} {R : Type u_2} (ap : Core.Context.AccessPattern C R) : Prop

Equations

• Percus2000.GenXAsTowerDepth ap = (ap.depth = Core.Context.DepthSpec.local)

def Percus2000.RestrictorUnconstrained {C : Type u_1} {R : Type u_2} (_ap : Core.Context.AccessPattern C R) : Prop

Equations

• Percus2000.RestrictorUnconstrained _ap = True

def Percus2000.genXTowerWellFormed {C : Type u_1} (predicatePatterns : List ((R : Type u_2) × Core.Context.AccessPattern C R)) (_restrictorPatterns : List ((R : Type u_3) × Core.Context.AccessPattern C R)) : Prop

Equations

• Percus2000.genXTowerWellFormed predicatePatterns _restrictorPatterns = ∀ p ∈ predicatePatterns, Percus2000.GenXAsTowerDepth p.snd

theorem Percus2000.genX_bridge_compliant (b : PredicateBinding) : b.genXCompliant = true ↔ b.sitVarIndex = b.closestBinderIndex

@[reducible, inline]

abbrev Percus2000.DoxSit (W : Type u_1) (Time : Type u_2) (E : Type u_3) : Type (max (max (max u_3 u_2) u_1) u_2 u_1)

Equations

• Percus2000.DoxSit W Time E = (E → Core.WorldTimeIndex W Time → List (Core.WorldTimeIndex W Time))

def Percus2000.believeSit {W : Type u_1} {Time : Type u_2} {E : Type u_3} (dox : DoxSit W Time E) (agent : E) (n : ℕ) (complement : SituationAssignment W Time → Prop) (g : SituationAssignment W Time) (s : Core.WorldTimeIndex W Time) : Prop

Equations

• Percus2000.believeSit dox agent n complement g s = ∀ s' ∈ dox agent s, complement (Percus2000.updateSitVar g n s')

@[implicit_reducible]

instance Percus2000.instDecidableBelieveSitOfDecidablePredSituationAssignment {W : Type u_1} {Time : Type u_2} {E : Type u_3} (dox : DoxSit W Time E) (agent : E) (n : ℕ) (complement : SituationAssignment W Time → Prop) [DecidablePred complement] (g : SituationAssignment W Time) (s : Core.WorldTimeIndex W Time) : Decidable (believeSit dox agent n complement g s)

Equations

• Percus2000.instDecidableBelieveSitOfDecidablePredSituationAssignment dox agent n complement g s = id inferInstance

def Percus2000.alwaysAt {W : Type u_1} {Time : Type u_2} (domain : Core.WorldTimeIndex W Time → List (Core.WorldTimeIndex W Time)) (ssh : Core.WorldTimeIndex W Time) (n : ℕ) (scope : SituationAssignment W Time → Prop) (g : SituationAssignment W Time) : Prop

Equations

• Percus2000.alwaysAt domain ssh n scope g = ∀ s' ∈ domain ssh, scope (Percus2000.updateSitVar g n s')

@[implicit_reducible]

instance Percus2000.instDecidableAlwaysAtOfDecidablePredSituationAssignment {W : Type u_1} {Time : Type u_2} (domain : Core.WorldTimeIndex W Time → List (Core.WorldTimeIndex W Time)) (ssh : Core.WorldTimeIndex W Time) (n : ℕ) (scope : SituationAssignment W Time → Prop) [DecidablePred scope] (g : SituationAssignment W Time) : Decidable (alwaysAt domain ssh n scope g)

Equations

• Percus2000.instDecidableAlwaysAtOfDecidablePredSituationAssignment domain ssh n scope g = id inferInstance

theorem Percus2000.sitVar_receives_binder_value {W : Type u_1} {Time : Type u_2} (g : SituationAssignment W Time) (n : ℕ) (s : Core.WorldTimeIndex W Time) : interpSitVar n (updateSitVar g n s) = s

theorem Percus2000.sitVar_other_unaffected {W : Type u_1} {Time : Type u_2} (g : SituationAssignment W Time) (n i : ℕ) (s : Core.WorldTimeIndex W Time) (h : i ≠ n) : interpSitVar i (updateSitVar g n s) = interpSitVar i g

def Percus2000.toTemporalAssignment {W : Type u_1} {Time : Type u_2} (g : SituationAssignment W Time) : Core.Time.Tense.TemporalAssignment Time

Equations

• Percus2000.toTemporalAssignment g n = (g n).time

theorem Percus2000.temporal_projection_commutes {W : Type u_1} {Time : Type u_2} (g : SituationAssignment W Time) (n : ℕ) : Core.Time.Tense.interpTense n (toTemporalAssignment g) = (interpSitVar n g).time

def Percus2000.introducesSitBinder (v : Fragments.English.Predicates.Verbal.VerbEntry) : Bool

Equations

• Percus2000.introducesSitBinder v = v.opaqueContext

def Percus2000.isDoxasticUniversal (v : Fragments.English.Predicates.Verbal.VerbEntry) : Bool

Equations

• Percus2000.isDoxasticUniversal v = match v.attitude with | some (Features.Attitude.doxastic veridicality) => true | x => false

theorem Percus2000.believe_introduces_sit_binder : introducesSitBinder Fragments.English.Predicates.Verbal.believe = true

theorem Percus2000.think_introduces_sit_binder : introducesSitBinder Fragments.English.Predicates.Verbal.think = true

theorem Percus2000.believe_is_doxastic : isDoxasticUniversal Fragments.English.Predicates.Verbal.believe = true

theorem Percus2000.think_is_doxastic : isDoxasticUniversal Fragments.English.Predicates.Verbal.think = true

theorem Percus2000.believe_is_nonveridical : Fragments.English.Predicates.Verbal.believe.attitude = some (Features.Attitude.doxastic Features.Veridicality.nonVeridical)

theorem Percus2000.always_is_universal : Fragments.English.FunctionWords.always.force = Fragments.English.FunctionWords.AdvQuantForce.universal

theorem Percus2000.mary_is_proper : Fragments.English.Nouns.mary.proper = true

theorem Percus2000.john_is_proper : Fragments.English.Nouns.john.proper = true

theorem Percus2000.bill_is_proper : Fragments.English.Nouns.bill.proper = true

theorem Percus2000.brother_is_common : Fragments.English.Nouns.brother.proper = false

theorem Percus2000.spy_is_common : Fragments.English.Nouns.spy.proper = false

inductive Percus2000.W : Type

• actual : W
• belief : W

@[implicit_reducible]

instance Percus2000.instDecidableEqW : DecidableEq W

Equations

• Percus2000.instDecidableEqW x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Percus2000.instReprW.repr : W → ℕ → Std.Format

Equations

• Percus2000.instReprW.repr Percus2000.W.actual prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Percus2000.W.actual")).group prec✝
• Percus2000.instReprW.repr Percus2000.W.belief prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Percus2000.W.belief")).group prec✝

@[implicit_reducible]

instance Percus2000.instReprW : Repr W

Equations

• Percus2000.instReprW = { reprPrec := Percus2000.instReprW.repr }

inductive Percus2000.Person : Type

• mary : Person
• john : Person
• bill : Person
• charlie : Person

@[implicit_reducible]

instance Percus2000.instDecidableEqPerson : DecidableEq Person

Equations

• Percus2000.instDecidableEqPerson x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Percus2000.instReprPerson.repr : Person → ℕ → Std.Format

Equations

• Percus2000.instReprPerson.repr Percus2000.Person.mary prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Percus2000.Person.mary")).group prec✝
• Percus2000.instReprPerson.repr Percus2000.Person.john prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Percus2000.Person.john")).group prec✝
• Percus2000.instReprPerson.repr Percus2000.Person.bill prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Percus2000.Person.bill")).group prec✝
• Percus2000.instReprPerson.repr Percus2000.Person.charlie prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Percus2000.Person.charlie")).group prec✝

@[implicit_reducible]

instance Percus2000.instReprPerson : Repr Person

Equations

• Percus2000.instReprPerson = { reprPrec := Percus2000.instReprPerson.repr }

@[reducible, inline]

abbrev Percus2000.Sit : Type

Equations

• Percus2000.Sit = Core.WorldTimeIndex Percus2000.W Unit

def Percus2000.sit (w : W) : Sit

Equations

• Percus2000.sit w = { world := w, time := () }

def Percus2000.sActual : Sit

Equations

• Percus2000.sActual = Percus2000.sit Percus2000.W.actual

def Percus2000.sBelief : Sit

Equations

• Percus2000.sBelief = Percus2000.sit Percus2000.W.belief

def Percus2000.entityOf (n : Fragments.English.Nouns.NounEntry) : Person

Equations

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

theorem Percus2000.entityOf_mary : entityOf Fragments.English.Nouns.mary = Person.mary

theorem Percus2000.entityOf_john : entityOf Fragments.English.Nouns.john = Person.john

theorem Percus2000.entityOf_bill : entityOf Fragments.English.Nouns.bill = Person.bill

def Percus2000.isCanadian (p : Person) (s : Sit) : Prop

Equations

• Percus2000.isCanadian Percus2000.Person.john s = True
• Percus2000.isCanadian p✝ s = False

@[implicit_reducible]

instance Percus2000.instDecidableIsCanadian (p : Person) (s : Sit) : Decidable (isCanadian p s)

Equations

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

def Percus2000.isBrotherOf (p : Person) (s : Sit) : Prop

Equations

• Percus2000.isBrotherOf Percus2000.Person.bill s = True
• Percus2000.isBrotherOf Percus2000.Person.charlie s = True
• Percus2000.isBrotherOf p✝ s = False

@[implicit_reducible]

instance Percus2000.instDecidableIsBrotherOf (p : Person) (s : Sit) : Decidable (isBrotherOf p s)

Equations

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

def Percus2000.isSpyAt (p : Person) (s : Sit) : Prop

Equations

• Percus2000.isSpyAt Percus2000.Person.bill s = True
• Percus2000.isSpyAt p✝ s = False

@[implicit_reducible]

instance Percus2000.instDecidableIsSpyAt (p : Person) (s : Sit) : Decidable (isSpyAt p s)

Equations

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

theorem Percus2000.brother_form : Fragments.English.Nouns.brother.formSg = "brother"

theorem Percus2000.spy_form : Fragments.English.Nouns.spy.formSg = "spy"

def Percus2000.doxMary : Sit → List Sit

Equations

• Percus2000.doxMary { world := Percus2000.W.actual, time := time } = [Percus2000.sBelief]
• Percus2000.doxMary { world := Percus2000.W.belief, time := time } = [Percus2000.sBelief]

def Percus2000.reading1_deDicto : Prop

Equations

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

@[implicit_reducible]

instance Percus2000.instDecidableReading1_deDicto : Decidable reading1_deDicto

Equations

• Percus2000.instDecidableReading1_deDicto = id (id inferInstance)

def Percus2000.reading2_deRe : Prop

Equations

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

@[implicit_reducible]

instance Percus2000.instDecidableReading2_deRe : Decidable reading2_deRe

Equations

• Percus2000.instDecidableReading2_deRe = id (id inferInstance)

theorem Percus2000.deDicto_is_false : ¬reading1_deDicto

theorem Percus2000.deRe_is_true : reading2_deRe

theorem Percus2000.readings_differ : ¬(reading1_deDicto ↔ reading2_deRe)

def Percus2000.reading1_bindings : List PredicateBinding

Equations

• Percus2000.reading1_bindings = [{ sitVarIndex := 2, closestBinderIndex := 2 }]

def Percus2000.reading2_bindings : List PredicateBinding

Equations

• Percus2000.reading2_bindings = [{ sitVarIndex := 1, closestBinderIndex := 2 }]

theorem Percus2000.reading1_genX_ok : genXWellFormed reading1_bindings = true

theorem Percus2000.reading2_genX_violation : genXWellFormed reading2_bindings = false

def Percus2000.empiricalJudgment_ex1 : Prop

Equations

• Percus2000.empiricalJudgment_ex1 = False

theorem Percus2000.genX_predicts_correct_reading : reading1_deDicto ↔ empiricalJudgment_ex1

theorem Percus2000.genX_blocks_incorrect_reading : ¬(reading2_deRe ↔ empiricalJudgment_ex1)

def Percus2000.readingA_allDeDicto : Prop

Equations

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

@[implicit_reducible]

instance Percus2000.instDecidableReadingA_allDeDicto : Decidable readingA_allDeDicto

Equations

• Percus2000.instDecidableReadingA_allDeDicto = id (id inferInstance)

def Percus2000.readingB_npDeRe : Prop

Equations

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

@[implicit_reducible]

instance Percus2000.instDecidableReadingB_npDeRe : Decidable readingB_npDeRe

Equations

• Percus2000.instDecidableReadingB_npDeRe = id (id inferInstance)

def Percus2000.readingC_predDeRe : Prop

Equations

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

@[implicit_reducible]

instance Percus2000.instDecidableReadingC_predDeRe : Decidable readingC_predDeRe

Equations

• Percus2000.instDecidableReadingC_predDeRe = id (id inferInstance)

theorem Percus2000.readingA_is_false : ¬readingA_allDeDicto

theorem Percus2000.readingB_is_true : readingB_npDeRe

theorem Percus2000.readingC_is_false : ¬readingC_predDeRe

def Percus2000.readingA_bindings : List PredicateBinding

Equations

• Percus2000.readingA_bindings = [{ sitVarIndex := 2, closestBinderIndex := 2 }]

def Percus2000.readingB_bindings : List PredicateBinding

Equations

• Percus2000.readingB_bindings = [{ sitVarIndex := 2, closestBinderIndex := 2 }]

def Percus2000.readingC_bindings : List PredicateBinding

Equations

• Percus2000.readingC_bindings = [{ sitVarIndex := 1, closestBinderIndex := 2 }]

theorem Percus2000.readingA_genX_ok : genXWellFormed readingA_bindings = true

theorem Percus2000.readingB_genX_ok : genXWellFormed readingB_bindings = true

theorem Percus2000.readingC_genX_violation : genXWellFormed readingC_bindings = false

inductive Percus2000.Round : Type

• r1 : Round
• r2 : Round
• r3 : Round

@[implicit_reducible]

instance Percus2000.instDecidableEqRound : DecidableEq Round

Equations

• Percus2000.instDecidableEqRound x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Percus2000.instReprRound.repr : Round → ℕ → Std.Format

Equations

• Percus2000.instReprRound.repr Percus2000.Round.r1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Percus2000.Round.r1")).group prec✝
• Percus2000.instReprRound.repr Percus2000.Round.r2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Percus2000.Round.r2")).group prec✝
• Percus2000.instReprRound.repr Percus2000.Round.r3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Percus2000.Round.r3")).group prec✝

@[implicit_reducible]

instance Percus2000.instReprRound : Repr Round

Equations

• Percus2000.instReprRound = { reprPrec := Percus2000.instReprRound.repr }

@[reducible, inline]

abbrev Percus2000.RSit : Type

Equations

• Percus2000.RSit = Core.WorldTimeIndex Percus2000.W Percus2000.Round

def Percus2000.wonGame (p : Person) (s : RSit) : Prop

Equations

• Percus2000.wonGame Percus2000.Person.bill s = True
• Percus2000.wonGame Percus2000.Person.bill s = True
• Percus2000.wonGame Percus2000.Person.bill s = False
• Percus2000.wonGame Percus2000.Person.bill s = True
• Percus2000.wonGame p✝ s = False

@[implicit_reducible]

instance Percus2000.instDecidableWonGame (p : Person) (s : RSit) : Decidable (wonGame p s)

Equations

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

def Percus2000.gameRounds (s : RSit) : List RSit

Equations

• Percus2000.gameRounds s = [Percus2000.rSit✝ s.world Percus2000.Round.r1, Percus2000.rSit✝ s.world Percus2000.Round.r2, Percus2000.rSit✝ s.world Percus2000.Round.r3]

def Percus2000.doxMaryR : RSit → List RSit

Equations

• Percus2000.doxMaryR { world := Percus2000.W.actual, time := r } = [{ world := Percus2000.W.belief, time := r }]
• Percus2000.doxMaryR { world := Percus2000.W.belief, time := r } = [{ world := Percus2000.W.belief, time := r }]

def Percus2000.genY_compliant : Prop

Equations

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

@[implicit_reducible]

instance Percus2000.instDecidableGenY_compliant : Decidable genY_compliant

Equations

• Percus2000.instDecidableGenY_compliant = id (id (id inferInstance))

def Percus2000.genY_violation : Prop

Equations

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

@[implicit_reducible]

instance Percus2000.instDecidableGenY_violation : Decidable genY_violation

Equations

• Percus2000.instDecidableGenY_violation = id (id (id inferInstance))

theorem Percus2000.genY_compliant_is_true : genY_compliant

theorem Percus2000.genY_violation_is_false : ¬genY_violation

theorem Percus2000.genY_readings_differ : ¬(genY_compliant ↔ genY_violation)

def Percus2000.empiricalJudgment_ex3 : Prop

Equations

• Percus2000.empiricalJudgment_ex3 = True

theorem Percus2000.genY_predicts_correct_reading : genY_compliant ↔ empiricalJudgment_ex3

theorem Percus2000.genY_blocks_incorrect_reading : ¬(genY_violation ↔ empiricalJudgment_ex3)

def Percus2000.ex3_predBindings : List PredicateBinding

Equations

• Percus2000.ex3_predBindings = [{ sitVarIndex := 3, closestBinderIndex := 3 }]

def Percus2000.ex3_quantBindings_compliant : List PredicateBinding

Equations

• Percus2000.ex3_quantBindings_compliant = [{ sitVarIndex := 2, closestBinderIndex := 2 }]

def Percus2000.ex3_quantBindings_violation : List PredicateBinding

Equations

• Percus2000.ex3_quantBindings_violation = [{ sitVarIndex := 1, closestBinderIndex := 2 }]

theorem Percus2000.ex3_genX_ok_for_both : genXWellFormed ex3_predBindings = true

theorem Percus2000.ex3_genY_compliant_ok : genYWellFormed ex3_quantBindings_compliant = true

theorem Percus2000.ex3_genY_violation_caught : genYWellFormed ex3_quantBindings_violation = false

theorem Percus2000.ex3_genXY_compliant : genXYWellFormed ex3_predBindings ex3_quantBindings_compliant = true

theorem Percus2000.ex3_genXY_violation : genXYWellFormed ex3_predBindings ex3_quantBindings_violation = false