Documentation

Linglib.Phenomena.Reference.Studies.Percus2000

@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.VarAssignment from D = Time (Partee's temporal variables) to D = Situation W Time (Percus's situation variables).

Empirical Chain #

Fragments/English/Predicates/Verbal.lean
  "believe": opaqueContext = true, attitudeBuilder =.doxastic.nonVeridical
  "think": opaqueContext = true, attitudeBuilder =.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 Phenomena.Reference.Studies.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

Phenomena.Reference.Studies.Percus2000.SituationAssignment W Time = Core.VarAssignment.VarAssignment (Situation W Time)

Instances For

@[reducible, inline]

abbrev Phenomena.Reference.Studies.Percus2000.interpSitVar {W : Type u_1} {Time : Type u_2} (n : ℕ) (g : SituationAssignment W Time) :

Situation W Time

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

Equations

Phenomena.Reference.Studies.Percus2000.interpSitVar n g = Core.VarAssignment.lookupVar n g

Instances For

@[reducible, inline]

abbrev Phenomena.Reference.Studies.Percus2000.updateSitVar {W : Type u_1} {Time : Type u_2} (g : SituationAssignment W Time) (n : ℕ) (s : Situation W Time) :

SituationAssignment W Time

Modified situation assignment g[n -> s].

Equations

Phenomena.Reference.Studies.Percus2000.updateSitVar g n s = Core.VarAssignment.updateVar g n s

Instances For

@[reducible, inline]

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

SituationAssignment W Time → Situation W Time → α

Situation lambda abstraction: bind a situation variable.

Equations

Phenomena.Reference.Studies.Percus2000.sitLambdaAbs n body = Core.VarAssignment.varLambdaAbs n body

Instances For

structure Phenomena.Reference.Studies.Percus2000.PredicateBinding :

sitVarIndex : ℕ
closestBinderIndex : ℕ

Instances For

def Phenomena.Reference.Studies.Percus2000.PredicateBinding.genXCompliant (b : PredicateBinding) :

Equations

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

Instances For

def Phenomena.Reference.Studies.Percus2000.genXWellFormed (bindings : List PredicateBinding) :

Equations

Phenomena.Reference.Studies.Percus2000.genXWellFormed bindings = bindings.all Phenomena.Reference.Studies.Percus2000.PredicateBinding.genXCompliant

Instances For

def Phenomena.Reference.Studies.Percus2000.genYWellFormed (quantifierBindings : List PredicateBinding) :

Generalization Y: adverbial quantifiers must use nearest binder.

Equations

Phenomena.Reference.Studies.Percus2000.genYWellFormed quantifierBindings = quantifierBindings.all Phenomena.Reference.Studies.Percus2000.PredicateBinding.genXCompliant

Instances For

def Phenomena.Reference.Studies.Percus2000.genXYWellFormed (predicateBindings quantifierBindings : List PredicateBinding) :

Equations

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

Instances For

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

Equations

Phenomena.Reference.Studies.Percus2000.GenXAsTowerDepth ap = (ap.depth = Core.Context.DepthSpec.local)

Instances For

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

Equations

Phenomena.Reference.Studies.Percus2000.RestrictorUnconstrained _ap = True

Instances For

def Phenomena.Reference.Studies.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)) :

Equations

Phenomena.Reference.Studies.Percus2000.genXTowerWellFormed predicatePatterns _restrictorPatterns = ∀ p ∈ predicatePatterns, Phenomena.Reference.Studies.Percus2000.GenXAsTowerDepth p.snd

Instances For

theorem Phenomena.Reference.Studies.Percus2000.genX_bridge_compliant (b : PredicateBinding) :

b.genXCompliant = true ↔ b.sitVarIndex = b.closestBinderIndex

@[reducible, inline]

abbrev Phenomena.Reference.Studies.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

Phenomena.Reference.Studies.Percus2000.DoxSit W Time E = (E → Situation W Time → List (Situation W Time))

Instances For

def Phenomena.Reference.Studies.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 → Bool) (g : SituationAssignment W Time) (s : Situation W Time) :

Equations

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

Instances For

def Phenomena.Reference.Studies.Percus2000.alwaysAt {W : Type u_1} {Time : Type u_2} (domain : Situation W Time → List (Situation W Time)) (ssh : Situation W Time) (n : ℕ) (scope : SituationAssignment W Time → Bool) (g : SituationAssignment W Time) :

Equations

Phenomena.Reference.Studies.Percus2000.alwaysAt domain ssh n scope g = (domain ssh).all fun (s' : Situation W Time) => scope (Phenomena.Reference.Studies.Percus2000.updateSitVar g n s')

Instances For

theorem Phenomena.Reference.Studies.Percus2000.sitVar_receives_binder_value {W : Type u_1} {Time : Type u_2} (g : SituationAssignment W Time) (n : ℕ) (s : Situation W Time) :

interpSitVar n (updateSitVar g n s) = s

theorem Phenomena.Reference.Studies.Percus2000.sitVar_other_unaffected {W : Type u_1} {Time : Type u_2} (g : SituationAssignment W Time) (n i : ℕ) (s : Situation W Time) (h : i ≠ n) :

interpSitVar i (updateSitVar g n s) = interpSitVar i g

def Phenomena.Reference.Studies.Percus2000.toTemporalAssignment {W : Type u_1} {Time : Type u_2} (g : SituationAssignment W Time) :

Core.Tense.TemporalAssignment Time

Equations

Phenomena.Reference.Studies.Percus2000.toTemporalAssignment g n = (g n).time

Instances For

theorem Phenomena.Reference.Studies.Percus2000.temporal_projection_commutes {W : Type u_1} {Time : Type u_2} (g : SituationAssignment W Time) (n : ℕ) :

Core.Tense.interpTense n (toTemporalAssignment g) = (interpSitVar n g).time

def Phenomena.Reference.Studies.Percus2000.introducesSitBinder (v : Fragments.English.Predicates.Verbal.VerbEntry) :

Equations

Phenomena.Reference.Studies.Percus2000.introducesSitBinder v = v.opaqueContext

Instances For

def Phenomena.Reference.Studies.Percus2000.isDoxasticUniversal (v : Fragments.English.Predicates.Verbal.VerbEntry) :

Equations

Phenomena.Reference.Studies.Percus2000.isDoxasticUniversal v = match v.attitudeBuilder with | some (Core.Verbs.AttitudeBuilder.doxastic veridicality) => true | x => false

Instances For

theorem Phenomena.Reference.Studies.Percus2000.believe_introduces_sit_binder :

introducesSitBinder Fragments.English.Predicates.Verbal.believe = true

theorem Phenomena.Reference.Studies.Percus2000.think_introduces_sit_binder :

introducesSitBinder Fragments.English.Predicates.Verbal.think = true

theorem Phenomena.Reference.Studies.Percus2000.believe_is_doxastic :

isDoxasticUniversal Fragments.English.Predicates.Verbal.believe = true

theorem Phenomena.Reference.Studies.Percus2000.think_is_doxastic :

isDoxasticUniversal Fragments.English.Predicates.Verbal.think = true

theorem Phenomena.Reference.Studies.Percus2000.believe_is_nonveridical :

Fragments.English.Predicates.Verbal.believe.attitudeBuilder = some (Core.Verbs.AttitudeBuilder.doxastic Semantics.Attitudes.Doxastic.Veridicality.nonVeridical)

theorem Phenomena.Reference.Studies.Percus2000.always_is_universal :

Fragments.English.FunctionWords.always.force = Fragments.English.FunctionWords.AdvQuantForce.universal

theorem Phenomena.Reference.Studies.Percus2000.mary_is_proper :

Fragments.English.Nouns.mary.proper = true

theorem Phenomena.Reference.Studies.Percus2000.john_is_proper :

Fragments.English.Nouns.john.proper = true

theorem Phenomena.Reference.Studies.Percus2000.bill_is_proper :

Fragments.English.Nouns.bill.proper = true

theorem Phenomena.Reference.Studies.Percus2000.brother_is_common :

Fragments.English.Nouns.brother.proper = false

theorem Phenomena.Reference.Studies.Percus2000.spy_is_common :

Fragments.English.Nouns.spy.proper = false

inductive Phenomena.Reference.Studies.Percus2000.W :

actual : W
belief : W

Instances For

instance Phenomena.Reference.Studies.Percus2000.instDecidableEqW :

Equations

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

instance Phenomena.Reference.Studies.Percus2000.instBEqW :

Equations

Phenomena.Reference.Studies.Percus2000.instBEqW = { beq := Phenomena.Reference.Studies.Percus2000.instBEqW.beq }

def Phenomena.Reference.Studies.Percus2000.instBEqW.beq :

W → W → Bool

Equations

Phenomena.Reference.Studies.Percus2000.instBEqW.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Reference.Studies.Percus2000.instReprW :

Equations

Phenomena.Reference.Studies.Percus2000.instReprW = { reprPrec := Phenomena.Reference.Studies.Percus2000.instReprW.repr }

def Phenomena.Reference.Studies.Percus2000.instReprW.repr :

W → ℕ → Std.Format

Equations

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

Instances For

inductive Phenomena.Reference.Studies.Percus2000.Person :

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

Instances For

instance Phenomena.Reference.Studies.Percus2000.instDecidableEqPerson :

DecidableEq Person

Equations

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

def Phenomena.Reference.Studies.Percus2000.instBEqPerson.beq :

Person → Person → Bool

Equations

Phenomena.Reference.Studies.Percus2000.instBEqPerson.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Reference.Studies.Percus2000.instBEqPerson :

Equations

Phenomena.Reference.Studies.Percus2000.instBEqPerson = { beq := Phenomena.Reference.Studies.Percus2000.instBEqPerson.beq }

def Phenomena.Reference.Studies.Percus2000.instReprPerson.repr :

Person → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Reference.Studies.Percus2000.instReprPerson :

Equations

Phenomena.Reference.Studies.Percus2000.instReprPerson = { reprPrec := Phenomena.Reference.Studies.Percus2000.instReprPerson.repr }

@[reducible, inline]

abbrev Phenomena.Reference.Studies.Percus2000.Sit :

Equations

Phenomena.Reference.Studies.Percus2000.Sit = Situation Phenomena.Reference.Studies.Percus2000.W Unit

Instances For

def Phenomena.Reference.Studies.Percus2000.sit (w : W) :

Equations

Phenomena.Reference.Studies.Percus2000.sit w = { world := w, time := () }

Instances For

def Phenomena.Reference.Studies.Percus2000.sActual :

Equations

Phenomena.Reference.Studies.Percus2000.sActual = Phenomena.Reference.Studies.Percus2000.sit Phenomena.Reference.Studies.Percus2000.W.actual

Instances For

def Phenomena.Reference.Studies.Percus2000.sBelief :

Equations

Phenomena.Reference.Studies.Percus2000.sBelief = Phenomena.Reference.Studies.Percus2000.sit Phenomena.Reference.Studies.Percus2000.W.belief

Instances For

def Phenomena.Reference.Studies.Percus2000.entityOf (n : Fragments.English.Nouns.NounEntry) :

Equations

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

Instances For

theorem Phenomena.Reference.Studies.Percus2000.entityOf_mary :

entityOf Fragments.English.Nouns.mary = Person.mary

theorem Phenomena.Reference.Studies.Percus2000.entityOf_john :

entityOf Fragments.English.Nouns.john = Person.john

theorem Phenomena.Reference.Studies.Percus2000.entityOf_bill :

entityOf Fragments.English.Nouns.bill = Person.bill

def Phenomena.Reference.Studies.Percus2000.isCanadian :

Person → Sit → Bool

Equations

Phenomena.Reference.Studies.Percus2000.isCanadian Phenomena.Reference.Studies.Percus2000.Person.john { world := Phenomena.Reference.Studies.Percus2000.W.actual, time := time } = true
Phenomena.Reference.Studies.Percus2000.isCanadian Phenomena.Reference.Studies.Percus2000.Person.john { world := Phenomena.Reference.Studies.Percus2000.W.belief, time := time } = false
Phenomena.Reference.Studies.Percus2000.isCanadian x✝¹ x✝ = false

Instances For

def Phenomena.Reference.Studies.Percus2000.isBrotherOf :

Person → Sit → Bool

Equations

Phenomena.Reference.Studies.Percus2000.isBrotherOf Phenomena.Reference.Studies.Percus2000.Person.bill { world := Phenomena.Reference.Studies.Percus2000.W.actual, time := time } = true
Phenomena.Reference.Studies.Percus2000.isBrotherOf Phenomena.Reference.Studies.Percus2000.Person.charlie { world := Phenomena.Reference.Studies.Percus2000.W.belief, time := time } = true
Phenomena.Reference.Studies.Percus2000.isBrotherOf x✝¹ x✝ = false

Instances For

def Phenomena.Reference.Studies.Percus2000.isSpyAt :

Person → Sit → Bool

Equations

Phenomena.Reference.Studies.Percus2000.isSpyAt Phenomena.Reference.Studies.Percus2000.Person.bill { world := Phenomena.Reference.Studies.Percus2000.W.belief, time := time } = true
Phenomena.Reference.Studies.Percus2000.isSpyAt x✝¹ x✝ = false

Instances For

theorem Phenomena.Reference.Studies.Percus2000.brother_form :

Fragments.English.Nouns.brother.formSg = "brother"

theorem Phenomena.Reference.Studies.Percus2000.spy_form :

Fragments.English.Nouns.spy.formSg = "spy"

def Phenomena.Reference.Studies.Percus2000.doxMary :

Sit → List Sit

Equations

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

Instances For

def Phenomena.Reference.Studies.Percus2000.reading1_deDicto :

Equations

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

Instances For

def Phenomena.Reference.Studies.Percus2000.reading2_deRe :

Equations

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

Instances For

theorem Phenomena.Reference.Studies.Percus2000.deDicto_is_false :

reading1_deDicto = false

theorem Phenomena.Reference.Studies.Percus2000.deRe_is_true :

reading2_deRe = true

theorem Phenomena.Reference.Studies.Percus2000.readings_differ :

reading1_deDicto ≠ reading2_deRe

def Phenomena.Reference.Studies.Percus2000.reading1_bindings :

List PredicateBinding

Equations

Phenomena.Reference.Studies.Percus2000.reading1_bindings = [{ sitVarIndex := 2, closestBinderIndex := 2 }]

Instances For

def Phenomena.Reference.Studies.Percus2000.reading2_bindings :

List PredicateBinding

Equations

Phenomena.Reference.Studies.Percus2000.reading2_bindings = [{ sitVarIndex := 1, closestBinderIndex := 2 }]

Instances For

theorem Phenomena.Reference.Studies.Percus2000.reading1_genX_ok :

genXWellFormed reading1_bindings = true

theorem Phenomena.Reference.Studies.Percus2000.reading2_genX_violation :

genXWellFormed reading2_bindings = false

def Phenomena.Reference.Studies.Percus2000.empiricalJudgment_ex1 :

Equations

Phenomena.Reference.Studies.Percus2000.empiricalJudgment_ex1 = false

Instances For

theorem Phenomena.Reference.Studies.Percus2000.genX_predicts_correct_reading :

reading1_deDicto = empiricalJudgment_ex1

theorem Phenomena.Reference.Studies.Percus2000.genX_blocks_incorrect_reading :

reading2_deRe ≠ empiricalJudgment_ex1

def Phenomena.Reference.Studies.Percus2000.readingA_allDeDicto :

Equations

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

Instances For

def Phenomena.Reference.Studies.Percus2000.readingB_npDeRe :

Equations

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

Instances For

def Phenomena.Reference.Studies.Percus2000.readingC_predDeRe :

Equations

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

Instances For

theorem Phenomena.Reference.Studies.Percus2000.readingA_is_false :

readingA_allDeDicto = false

theorem Phenomena.Reference.Studies.Percus2000.readingB_is_true :

readingB_npDeRe = true

theorem Phenomena.Reference.Studies.Percus2000.readingC_is_false :

readingC_predDeRe = false

def Phenomena.Reference.Studies.Percus2000.readingA_bindings :

List PredicateBinding

Equations

Phenomena.Reference.Studies.Percus2000.readingA_bindings = [{ sitVarIndex := 2, closestBinderIndex := 2 }]

Instances For

def Phenomena.Reference.Studies.Percus2000.readingB_bindings :

List PredicateBinding

Equations

Phenomena.Reference.Studies.Percus2000.readingB_bindings = [{ sitVarIndex := 2, closestBinderIndex := 2 }]

Instances For

def Phenomena.Reference.Studies.Percus2000.readingC_bindings :

List PredicateBinding

Equations

Phenomena.Reference.Studies.Percus2000.readingC_bindings = [{ sitVarIndex := 1, closestBinderIndex := 2 }]

Instances For

theorem Phenomena.Reference.Studies.Percus2000.readingA_genX_ok :

genXWellFormed readingA_bindings = true

theorem Phenomena.Reference.Studies.Percus2000.readingB_genX_ok :

genXWellFormed readingB_bindings = true

theorem Phenomena.Reference.Studies.Percus2000.readingC_genX_violation :

genXWellFormed readingC_bindings = false

inductive Phenomena.Reference.Studies.Percus2000.Round :

r1 : Round
r2 : Round
r3 : Round

Instances For

instance Phenomena.Reference.Studies.Percus2000.instDecidableEqRound :

DecidableEq Round

Equations

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

instance Phenomena.Reference.Studies.Percus2000.instBEqRound :

Equations

Phenomena.Reference.Studies.Percus2000.instBEqRound = { beq := Phenomena.Reference.Studies.Percus2000.instBEqRound.beq }

def Phenomena.Reference.Studies.Percus2000.instBEqRound.beq :

Round → Round → Bool

Equations

Phenomena.Reference.Studies.Percus2000.instBEqRound.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

def Phenomena.Reference.Studies.Percus2000.instReprRound.repr :

Round → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Reference.Studies.Percus2000.instReprRound :

Equations

Phenomena.Reference.Studies.Percus2000.instReprRound = { reprPrec := Phenomena.Reference.Studies.Percus2000.instReprRound.repr }

@[reducible, inline]

abbrev Phenomena.Reference.Studies.Percus2000.RSit :

Equations

Phenomena.Reference.Studies.Percus2000.RSit = Situation Phenomena.Reference.Studies.Percus2000.W Phenomena.Reference.Studies.Percus2000.Round

Instances For

def Phenomena.Reference.Studies.Percus2000.wonGame :

Person → RSit → Bool

Equations

One or more equations did not get rendered due to their size.
Phenomena.Reference.Studies.Percus2000.wonGame Phenomena.Reference.Studies.Percus2000.Person.bill { world := Phenomena.Reference.Studies.Percus2000.W.belief, time := time } = true
Phenomena.Reference.Studies.Percus2000.wonGame x✝¹ x✝ = false

Instances For

def Phenomena.Reference.Studies.Percus2000.gameRounds (s : RSit) :

Equations

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

Instances For

def Phenomena.Reference.Studies.Percus2000.doxMaryR :

RSit → List RSit

Equations

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

Instances For

def Phenomena.Reference.Studies.Percus2000.genY_compliant :

Equations

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

Instances For

def Phenomena.Reference.Studies.Percus2000.genY_violation :

Equations

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

Instances For

theorem Phenomena.Reference.Studies.Percus2000.genY_compliant_is_true :

genY_compliant = true

theorem Phenomena.Reference.Studies.Percus2000.genY_violation_is_false :

genY_violation = false

theorem Phenomena.Reference.Studies.Percus2000.genY_readings_differ :

genY_compliant ≠ genY_violation

def Phenomena.Reference.Studies.Percus2000.empiricalJudgment_ex3 :

Equations

Phenomena.Reference.Studies.Percus2000.empiricalJudgment_ex3 = true

Instances For

theorem Phenomena.Reference.Studies.Percus2000.genY_predicts_correct_reading :

genY_compliant = empiricalJudgment_ex3

theorem Phenomena.Reference.Studies.Percus2000.genY_blocks_incorrect_reading :

genY_violation ≠ empiricalJudgment_ex3

def Phenomena.Reference.Studies.Percus2000.ex3_predBindings :

List PredicateBinding

Equations

Phenomena.Reference.Studies.Percus2000.ex3_predBindings = [{ sitVarIndex := 3, closestBinderIndex := 3 }]

Instances For

def Phenomena.Reference.Studies.Percus2000.ex3_quantBindings_compliant :

List PredicateBinding

Equations

Phenomena.Reference.Studies.Percus2000.ex3_quantBindings_compliant = [{ sitVarIndex := 2, closestBinderIndex := 2 }]

Instances For

def Phenomena.Reference.Studies.Percus2000.ex3_quantBindings_violation :

List PredicateBinding

Equations

Phenomena.Reference.Studies.Percus2000.ex3_quantBindings_violation = [{ sitVarIndex := 1, closestBinderIndex := 2 }]

Instances For

theorem Phenomena.Reference.Studies.Percus2000.ex3_genX_ok_for_both :

genXWellFormed ex3_predBindings = true

theorem Phenomena.Reference.Studies.Percus2000.ex3_genY_compliant_ok :

genYWellFormed ex3_quantBindings_compliant = true

theorem Phenomena.Reference.Studies.Percus2000.ex3_genY_violation_caught :

genYWellFormed ex3_quantBindings_violation = false

theorem Phenomena.Reference.Studies.Percus2000.ex3_genXY_compliant :

genXYWellFormed ex3_predBindings ex3_quantBindings_compliant = true

theorem Phenomena.Reference.Studies.Percus2000.ex3_genXY_violation :

genXYWellFormed ex3_predBindings ex3_quantBindings_violation = false