Percus (2000): Constraints on Some Other Variables in Syntax

This file formalizes the situation-pronoun syntax of [Per00]. Every predicate carries a situation pronoun, every clause introduces an indexed λ binding situations, and two generalizations restrict which λ a pronoun may take: Generalization X (34), that the situation pronoun a verb selects for is coindexed with the nearest λ above it, and Generalization Y (39), that the situation pronoun an adverbial quantifier selects for is likewise locally bound, whereas the pronoun inside a determiner phrase may be bound from higher up (LF.GenX, QLF.GenY). For Mary thinks that my brother is Canadian (26a) this admits the indexing (27), my brother transparent and is Canadian opaque, and excludes the indexing (33), my brother opaque and is Canadian transparent. The paper's two scenarios are two models: where Mary takes Allon, the speaker's brother, not to be the brother but to be Canadian, the sentence is judged true, and only the licensed transparent-phrase indexing makes it so (scenario_allon); where Mary takes Pierre, a Canadian, to be the brother and so to be American, the sentence is judged false, and the one indexing that would make it true is the excluded one (scenario_pierre). For Mary thinks that my brother always won the game (35a), binding the quantifier's pronoun to the matrix λ, the indexing (37), would make the sentence true when Mary is unaware of the games Pierre won, where it is judged false, and binding it to the embedded λ, the indexing (38), makes it true when Mary is deluded about games Pierre lost, where it is judged true (scenario_unaware, scenario_deluded).

Implementation notes

Situation assignments specialize the assignments of Logic/Assignment to indices of world and time, the λ-binding of situation pronouns being the predicate abstraction of [HK98]; the models have two worlds, with a trivial time coordinate for (26a) and the rounds of the game for (35a). The coindexing of both embedded pronouns with the matrix λ is ruled out independently of the generalizations (fn. 18), and the motivation of Generalization X from counterfactuals (40) is not formalized.

References

• [Per00]
• [HK98]

@[reducible, inline]

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

An assignment of situations to variable indices.

Equations

• Percus2000.SituationAssignment W T = Assignment (Reference.Index W T)

def Percus2000.believeSit {W : Type u_1} {T : Type u_2} {E : Type u_3} (dox : E → Reference.Index W T → List (Reference.Index W T)) (agent : E) (n : ℕ) (complement : SituationAssignment W T → Prop) (g : SituationAssignment W T) (s : Reference.Index W T) : Prop

Belief with situation binding: the complement holds at every doxastic alternative of the agent, the binder n reset to that alternative.

Equations

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

@[instance_reducible]

instance Percus2000.instDecidableBelieveSitOfDecidablePredSituationAssignment {W : Type u_1} {T : Type u_2} {E : Type u_3} (dox : E → Reference.Index W T → List (Reference.Index W T)) (agent : E) (n : ℕ) (complement : SituationAssignment W T → Prop) [DecidablePred complement] (g : SituationAssignment W T) (s : Reference.Index W T) : 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} {T : Type u_2} (domain : Reference.Index W T → List (Reference.Index W T)) (restrictor : Reference.Index W T) (n : ℕ) (scope : SituationAssignment W T → Prop) (g : SituationAssignment W T) : Prop

An adverb of quantification over the situations its restrictor supplies, the binder n reset to each.

Equations

• Percus2000.alwaysAt domain restrictor n scope g = ∀ s' ∈ domain restrictor, scope (Function.update g n s')

@[instance_reducible]

instance Percus2000.instDecidableAlwaysAtOfDecidablePredSituationAssignment {W : Type u_1} {T : Type u_2} (domain : Reference.Index W T → List (Reference.Index W T)) (restrictor : Reference.Index W T) (n : ℕ) (scope : SituationAssignment W T → Prop) [DecidablePred scope] (g : SituationAssignment W T) : Decidable (alwaysAt domain restrictor n scope g)

Equations

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

Generalizations X (34) and Y (39)

structure Percus2000.LF : Type

An indexing of the embedded clause of an attitude sentence, the positions S and T of (26b): the matrix λ carries index 1 and the embedded λ index 2, and the indexing records the λ the embedded verb's situation pronoun and the embedded determiner phrase's pronoun take.

• verb : ℕ
• noun : ℕ

@[instance_reducible]

instance Percus2000.instDecidableEqLF : DecidableEq LF

Equations

• Percus2000.instDecidableEqLF = Percus2000.instDecidableEqLF.decEq

def Percus2000.instDecidableEqLF.decEq (x✝ x✝¹ : LF) : Decidable (x✝ = x✝¹)

Equations

• Percus2000.instDecidableEqLF.decEq { verb := a, noun := a_1 } { verb := b, noun := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Percus2000.LF.GenX (lf : LF) : Prop

Generalization X (34): the verb's situation pronoun is coindexed with the nearest λ; the determiner phrase's pronoun is unconstrained.

Equations

• lf.GenX = (lf.verb = 2)

@[instance_reducible]

instance Percus2000.instDecidablePredLFGenX : DecidablePred LF.GenX

Equations

• Percus2000.instDecidablePredLFGenX lf = { decide := lf.verb.beq 2, reflects_decide := ⋯ }

def Percus2000.transparentDP : LF

The indexing (27), S = s₂ and T = s₁: the determiner phrase transparent and the predicate opaque.

Equations

• Percus2000.transparentDP = { verb := 2, noun := 1 }

def Percus2000.transparentPredicate : LF

The indexing (33), S = s₁ and T = s₂: the predicate transparent and the determiner phrase opaque.

Equations

• Percus2000.transparentPredicate = { verb := 1, noun := 2 }

def Percus2000.allOpaque : LF

Both pronouns bound by the embedded λ: everything opaque.

Equations

• Percus2000.allOpaque = { verb := 2, noun := 2 }

theorem Percus2000.genX_indexings : allOpaque.GenX ∧ transparentDP.GenX ∧ ¬transparentPredicate.GenX

Generalization X licenses the all-opaque and the transparent-phrase indexings and excludes the transparent-predicate indexing.

structure Percus2000.QLF : Type

An indexing for an adverb of quantification in an attitude complement, the position S of (35b): the λ its situation pronoun takes.

• quant : ℕ

def Percus2000.instDecidableEqQLF.decEq (x✝ x✝¹ : QLF) : Decidable (x✝ = x✝¹)

Equations

• Percus2000.instDecidableEqQLF.decEq { quant := a } { quant := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Percus2000.instDecidableEqQLF : DecidableEq QLF

Equations

• Percus2000.instDecidableEqQLF = Percus2000.instDecidableEqQLF.decEq

def Percus2000.QLF.GenY (q : QLF) : Prop

Generalization Y (39): the adverb's situation pronoun is coindexed with the nearest λ.

Equations

• q.GenY = (q.quant = 2)

@[instance_reducible]

instance Percus2000.instDecidablePredQLFGenY : DecidablePred QLF.GenY

Equations

• Percus2000.instDecidablePredQLFGenY q = { decide := q.quant.beq 2, reflects_decide := ⋯ }

The models

inductive Percus2000.W : Type

The actual world and Mary's belief world.

• actual : W
• belief : W

@[instance_reducible]

instance Percus2000.instDecidableEqW : DecidableEq W

Equations

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

inductive Percus2000.Person : Type

• mary : Person
• allon : Person
• pierre : Person

@[instance_reducible]

instance Percus2000.instDecidableEqPerson : DecidableEq Person

Equations

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

def Percus2000.brother : W → Person

The speaker's brother in a world: Allon in fact, Pierre in Mary's belief world, where she takes Pierre to be the brother and Allon not to be.

Equations

• Percus2000.brother Percus2000.W.actual = Percus2000.Person.allon
• Percus2000.brother Percus2000.W.belief = Percus2000.Person.pierre

@[reducible, inline]

abbrev Percus2000.Sit : Type

Situations with a trivial time coordinate.

Equations

• Percus2000.Sit = Reference.Index Percus2000.W Unit

def Percus2000.sActual : Sit

Equations

• Percus2000.sActual = (Percus2000.W.actual, ())

def Percus2000.sBelief : Sit

Equations

• Percus2000.sBelief = (Percus2000.W.belief, ())

inductive Percus2000.Scenario : Type

The paper's two scenarios for (26a): Mary takes Allon not to be the brother but to be Canadian, and the sentence is judged true; Mary takes Pierre, a Canadian, to be the brother and, knowing the speaker is American, to be American, and the sentence is judged false.

• allon : Scenario
• pierre : Scenario

@[instance_reducible]

instance Percus2000.instDecidableEqScenario : DecidableEq Scenario

Equations

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

def Percus2000.IsCanadian : Scenario → Person → Sit → Prop

Who is Canadian in which world under each scenario.

Equations

• Percus2000.IsCanadian Percus2000.Scenario.allon Percus2000.Person.allon (Percus2000.W.belief, snd) = True
• Percus2000.IsCanadian Percus2000.Scenario.pierre Percus2000.Person.pierre (Percus2000.W.actual, snd) = True
• Percus2000.IsCanadian x✝² x✝¹ x✝ = False

@[instance_reducible]

instance Percus2000.instDecidableIsCanadian (sc : Scenario) (p : Person) (s : Sit) : Decidable (IsCanadian sc p s)

Equations

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

def Percus2000.doxMary : Sit → List Sit

Mary's doxastic alternatives: the belief world.

Equations

• Percus2000.doxMary x✝ = [Percus2000.sBelief]

def Percus2000.g₀ : SituationAssignment W Unit

Equations

• Percus2000.g₀ x✝ = Percus2000.sActual

def Percus2000.canadianReading (sc : Scenario) (lf : LF) : Prop

The reading of (26a) under an indexing, (28b) and (34b): at every belief alternative of Mary's, the brother in the world the determiner phrase's pronoun denotes is Canadian at the situation the verb's pronoun denotes.

Equations

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

@[instance_reducible]

instance Percus2000.instDecidableCanadianReading (sc : Scenario) (lf : LF) : Decidable (canadianReading sc lf)

Equations

• Percus2000.instDecidableCanadianReading sc lf = id (id inferInstance)

theorem Percus2000.scenario_allon : canadianReading Scenario.allon transparentDP ∧ ¬canadianReading Scenario.allon allOpaque

The first scenario: the sentence is judged true, and the licensed transparent-phrase indexing (27) is what makes it true, the all-opaque indexing making it false.

theorem Percus2000.scenario_pierre : canadianReading Scenario.pierre transparentPredicate ∧ ¬transparentPredicate.GenX ∧ ¬canadianReading Scenario.pierre transparentDP ∧ ¬canadianReading Scenario.pierre allOpaque

The second scenario: the sentence is judged false, and the one indexing that would make it true is the transparent-predicate indexing (33), which Generalization X excludes.

Generalization Y

inductive Percus2000.Round : Type

Three rounds of the game.

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

@[instance_reducible]

instance Percus2000.instDecidableEqRound : DecidableEq Round

Equations

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

@[reducible, inline]

abbrev Percus2000.RSit : Type

Situations with a round as their time coordinate.

Equations

• Percus2000.RSit = Reference.Index Percus2000.W Percus2000.Round

inductive Percus2000.GameScenario : Type

The paper's two scenarios for (35a): Mary, unaware of the games, wrongly takes Pierre to be the brother, and Pierre won every game, the sentence being judged false; Mary is deluded that Pierre, whom she takes to be the brother, won every game he in fact lost, the sentence being judged true.

• unaware : GameScenario
• deluded : GameScenario

@[instance_reducible]

instance Percus2000.instDecidableEqGameScenario : DecidableEq GameScenario

Equations

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

def Percus2000.Won : GameScenario → Person → RSit → Prop

Who won which round in which world under each scenario.

Equations

• Percus2000.Won Percus2000.GameScenario.unaware Percus2000.Person.pierre (Percus2000.W.actual, snd) = True
• Percus2000.Won Percus2000.GameScenario.deluded Percus2000.Person.pierre (Percus2000.W.belief, snd) = True
• Percus2000.Won x✝² x✝¹ x✝ = False

@[instance_reducible]

instance Percus2000.instDecidableWon (sc : GameScenario) (p : Person) (s : RSit) : Decidable (Won sc p s)

Equations

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

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

The rounds of a situation's world.

Equations

• Percus2000.rounds s = [(Reference.Index.world s, Percus2000.Round.r1), (Reference.Index.world s, Percus2000.Round.r2), (Reference.Index.world s, Percus2000.Round.r3)]

def Percus2000.doxMaryR : RSit → List RSit

Mary's doxastic alternatives, round by round.

Equations

• Percus2000.doxMaryR s = [(Percus2000.W.belief, Reference.Index.time s)]

def Percus2000.g₃ : SituationAssignment W Round

Equations

• Percus2000.g₃ x✝ = (Percus2000.W.actual, Percus2000.Round.r1)

def Percus2000.alwaysReading (sc : GameScenario) (q : QLF) : Prop

The reading of (35a) under an indexing, (37b) and (38b): the determiner phrase's pronoun is bound by the embedded λ, and the adverb ranges over the rounds of the world its pronoun denotes.

Equations

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

@[instance_reducible]

instance Percus2000.instDecidableAlwaysReading (sc : GameScenario) (q : QLF) : Decidable (alwaysReading sc q)

Equations

• Percus2000.instDecidableAlwaysReading sc q = id (id (id inferInstance))

theorem Percus2000.scenario_unaware : alwaysReading GameScenario.unaware { quant := 1 } ∧ ¬{ quant := 1 }.GenY ∧ ¬alwaysReading GameScenario.unaware { quant := 2 }

The indexing (37), the adverb's pronoun bound by the matrix λ, would make the sentence true where it is judged false; Generalization Y excludes it.

theorem Percus2000.scenario_deluded : alwaysReading GameScenario.deluded { quant := 2 } ∧ { quant := 2 }.GenY ∧ ¬alwaysReading GameScenario.deluded { quant := 1 }

The indexing (38), the adverb's pronoun bound by the embedded λ, makes the sentence true where it is judged true, and the matrix binding would not.