Charnavel (2019): Locality and Logophoricity: A Theory of Exempt Anaphora

Charnavel argues that no anaphor is exempt from Condition A. An anaphor that seems to lack a local binder is bound by a silent logophoric pronoun at the edge of its spell-out domain, which refers to the logophoric center of that domain, an attitude holder or an empathy locus. Plain and exempt anaphors are then one element under one condition, and they differ in whether the binder is pronounced. Here a sentence is a tree with the indices the book prints, the binding domain of a position is its smallest spell-out domain, and a representation is licit when it meets Conditions A and C with nothing exempt.

Main statements

• condition_overt: Condition A with the silent pronouns counted is Condition A among the pronounced noun phrases with the anaphors the silent pronouns bind exempt.
• locallyBound_overt_of_licit, index_eq_of_licit: an anaphor that no silent pronoun is coindexed with, as an inanimate one, has a pronounced binder in its domain, and anaphors without pronounced binders in a domain with one silent pronoun corefer.
• grammatical_iff, not_exists_forall_iff_rep: the model gives the book's judgment on each example formalized here, and no condition on structure alone does, two of the examples having one structure and opposite judgments.
• acceptable_iff_isLogophoric, exists_unacceptable_mem_centersOf_iff: on the examples an anaphor without a pronounced binder is acceptable exactly when its antecedent is an attitude holder or an empathy locus, so the source and the pivot of Sells take in antecedents that exempt nothing and the self does not.

Implementation notes

• A noun phrase with a subject is labelled Det and its subject is its first daughter; it is a spell-out domain for every position but that subject, beside the clause S and the verb phrase V. Other noun phrases are N.
• The logophoric centers of a sentence are entered by index as the book's tests give them, the speaker being 0. The tests themselves are not modelled.
• Condition B is not checked. The book leaves it open and finds that the silent pronoun never triggers it, which a pronoun's having the domain of an anaphor would not allow (condition_pronoun_overt, locallyBound_pronoun).

TODO

• Plural and split antecedents, and with them exhaustive binding.
• The interpretation the logophoric operator imposes on its domain, read de se and from the center's own perspective.
• The long-distance anaphors of the last chapter, Icelandic sig and Mandarin ziji among them.

References

• [Cha19c]
• [CS16a]
• [Sel87]

Perspective centers

inductive Charnavel2019.Center : Type

The kinds of perspective center the book tells apart.

• nonAttitudinalSource : Center

  The source of a report who holds no attitude toward its content.

• attitudeHolder : Center

  One whose thought or speech a clause reports, the speaker included.

• empathyLocus : Center

  One whose sensory or emotional experience the speaker takes up.

• deicticCenter : Center

  A spatial point of reference, which need have no mental state.

@[instance_reducible]

instance Charnavel2019.instDecidableEqCenter : DecidableEq Center

Equations

• Charnavel2019.instDecidableEqCenter x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Charnavel2019.instFintypeCenter : Fintype Center

Equations

• Charnavel2019.instFintypeCenter = { elems := { val := ↑Charnavel2019.Center.enumList, nodup := Charnavel2019.Center.enumList_nodup }, complete := Charnavel2019.instFintypeCenter._proof_1 }

def Charnavel2019.instReprCenter.repr : Center → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Charnavel2019.instReprCenter : Repr Center

Equations

• Charnavel2019.instReprCenter = { reprPrec := Charnavel2019.instReprCenter.repr }

def Charnavel2019.Center.IsLogophoric (c : Center) : Prop

A center is logophoric when its perspective is mental and first-personal, as an attitude holder's and an empathy locus's are.

Equations

• c.IsLogophoric = (c = Charnavel2019.Center.attitudeHolder ∨ c = Charnavel2019.Center.empathyLocus)

@[instance_reducible]

instance Charnavel2019.instDecidablePredCenterIsLogophoric : DecidablePred Center.IsLogophoric

Equations

• Charnavel2019.instDecidablePredCenterIsLogophoric x✝ = { decide := decide (x✝ = Charnavel2019.Center.attitudeHolder) || decide (x✝ = Charnavel2019.Center.empathyLocus), reflects_decide := ⋯ }

def Charnavel2019.centersOf : Reference.LogophoricRole → Finset Center

The centers each role of Sells takes in, whole or in part, in the book's comparison of the two taxonomies.

Equations

• Charnavel2019.centersOf Reference.LogophoricRole.source = {Charnavel2019.Center.nonAttitudinalSource, Charnavel2019.Center.attitudeHolder}
• Charnavel2019.centersOf Reference.LogophoricRole.self = {Charnavel2019.Center.attitudeHolder, Charnavel2019.Center.empathyLocus}
• Charnavel2019.centersOf Reference.LogophoricRole.pivot = {Charnavel2019.Center.empathyLocus, Charnavel2019.Center.deicticCenter}

theorem Charnavel2019.exists_mem_centersOf_not_isLogophoric_iff {r : Reference.LogophoricRole} : (∃ c ∈ centersOf r, ¬c.IsLogophoric) ↔ r ≠ Reference.LogophoricRole.self

The source and the pivot each take in a center that is not logophoric, and the self does not.

theorem Charnavel2019.isLogophoric_iff_exists_ne {c : Center} : c.IsLogophoric ↔ ∃ (r : Reference.LogophoricRole) (r' : Reference.LogophoricRole), r ≠ r' ∧ c ∈ centersOf r ∧ c ∈ centersOf r'

Each logophoric center falls under two of the roles and each of the others under one, so neither logophoric center is a role of Sells.

Representations

inductive Charnavel2019.Item : Type

What stands at a noun phrase position, with its referential index.

• anaphor (index : ℕ) : Item
• name (index : ℕ) : Item
• pronoun (index : ℕ) : Item
• trace (index : ℕ) : Item
• logophor (index : ℕ) : Item

  The silent logophoric pronoun.

@[instance_reducible]

instance Charnavel2019.instDecidableEqItem : DecidableEq Item

Equations

• Charnavel2019.instDecidableEqItem = Charnavel2019.instDecidableEqItem.decEq

def Charnavel2019.instDecidableEqItem.decEq (x✝ x✝¹ : Item) : Decidable (x✝ = x✝¹)

Equations

• Charnavel2019.instDecidableEqItem.decEq (Charnavel2019.Item.anaphor a) (Charnavel2019.Item.anaphor b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Charnavel2019.instDecidableEqItem.decEq (Charnavel2019.Item.anaphor index) (Charnavel2019.Item.name index_1) = isFalse ⋯
• Charnavel2019.instDecidableEqItem.decEq (Charnavel2019.Item.anaphor index) (Charnavel2019.Item.pronoun index_1) = isFalse ⋯
• Charnavel2019.instDecidableEqItem.decEq (Charnavel2019.Item.anaphor index) (Charnavel2019.Item.trace index_1) = isFalse ⋯
• Charnavel2019.instDecidableEqItem.decEq (Charnavel2019.Item.anaphor index) (Charnavel2019.Item.logophor index_1) = isFalse ⋯
• Charnavel2019.instDecidableEqItem.decEq (Charnavel2019.Item.name index) (Charnavel2019.Item.anaphor index_1) = isFalse ⋯
• Charnavel2019.instDecidableEqItem.decEq (Charnavel2019.Item.name a) (Charnavel2019.Item.name b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Charnavel2019.instDecidableEqItem.decEq (Charnavel2019.Item.name index) (Charnavel2019.Item.pronoun index_1) = isFalse ⋯
• Charnavel2019.instDecidableEqItem.decEq (Charnavel2019.Item.name index) (Charnavel2019.Item.trace index_1) = isFalse ⋯
• Charnavel2019.instDecidableEqItem.decEq (Charnavel2019.Item.name index) (Charnavel2019.Item.logophor index_1) = isFalse ⋯
• Charnavel2019.instDecidableEqItem.decEq (Charnavel2019.Item.pronoun index) (Charnavel2019.Item.anaphor index_1) = isFalse ⋯
• Charnavel2019.instDecidableEqItem.decEq (Charnavel2019.Item.pronoun index) (Charnavel2019.Item.name index_1) = isFalse ⋯
• Charnavel2019.instDecidableEqItem.decEq (Charnavel2019.Item.pronoun a) (Charnavel2019.Item.pronoun b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Charnavel2019.instDecidableEqItem.decEq (Charnavel2019.Item.pronoun index) (Charnavel2019.Item.trace index_1) = isFalse ⋯
• Charnavel2019.instDecidableEqItem.decEq (Charnavel2019.Item.pronoun index) (Charnavel2019.Item.logophor index_1) = isFalse ⋯
• Charnavel2019.instDecidableEqItem.decEq (Charnavel2019.Item.trace index) (Charnavel2019.Item.anaphor index_1) = isFalse ⋯
• Charnavel2019.instDecidableEqItem.decEq (Charnavel2019.Item.trace index) (Charnavel2019.Item.name index_1) = isFalse ⋯
• Charnavel2019.instDecidableEqItem.decEq (Charnavel2019.Item.trace index) (Charnavel2019.Item.pronoun index_1) = isFalse ⋯
• Charnavel2019.instDecidableEqItem.decEq (Charnavel2019.Item.trace a) (Charnavel2019.Item.trace b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Charnavel2019.instDecidableEqItem.decEq (Charnavel2019.Item.trace index) (Charnavel2019.Item.logophor index_1) = isFalse ⋯
• Charnavel2019.instDecidableEqItem.decEq (Charnavel2019.Item.logophor index) (Charnavel2019.Item.anaphor index_1) = isFalse ⋯
• Charnavel2019.instDecidableEqItem.decEq (Charnavel2019.Item.logophor index) (Charnavel2019.Item.name index_1) = isFalse ⋯
• Charnavel2019.instDecidableEqItem.decEq (Charnavel2019.Item.logophor index) (Charnavel2019.Item.pronoun index_1) = isFalse ⋯
• Charnavel2019.instDecidableEqItem.decEq (Charnavel2019.Item.logophor index) (Charnavel2019.Item.trace index_1) = isFalse ⋯
• Charnavel2019.instDecidableEqItem.decEq (Charnavel2019.Item.logophor a) (Charnavel2019.Item.logophor b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Charnavel2019.instReprItem.repr : Item → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Charnavel2019.instReprItem : Repr Item

Equations

• Charnavel2019.instReprItem = { reprPrec := Charnavel2019.instReprItem.repr }

def Charnavel2019.Item.index : Item → ℕ

The referential index of an item.

Equations

• (Charnavel2019.Item.anaphor i).index = i
• (Charnavel2019.Item.name i).index = i
• (Charnavel2019.Item.pronoun i).index = i
• (Charnavel2019.Item.trace i).index = i
• (Charnavel2019.Item.logophor i).index = i

def Charnavel2019.Item.class? : Item → Option Binding.BindingClass

The binding class under which an item is checked. An anaphor falls under Condition A and a name under Condition C.

Equations

• (Charnavel2019.Item.anaphor index).class? = some Binding.BindingClass.reflexive
• (Charnavel2019.Item.name index).class? = some Binding.BindingClass.rExpression
• x✝.class? = none

def Charnavel2019.Item.IsSilent : Item → Prop

An item is silent when it is the logophoric pronoun.

Equations

• (Charnavel2019.Item.logophor index).IsSilent = True
• x✝.IsSilent = False

@[instance_reducible]

instance Charnavel2019.Item.instDecidablePredIsSilent : DecidablePred IsSilent

Equations

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

@[reducible, inline]

abbrev Charnavel2019.Rep : Type

A representation is a tree whose noun phrases carry items.

Equations

• Charnavel2019.Rep = PhraseStructure.Tree PhraseStructure.Cat (Option Charnavel2019.Item)

@[reducible, inline]

abbrev Charnavel2019.w (c : PhraseStructure.Cat) : Rep

A word that is no noun phrase.

Equations

• Charnavel2019.w c = PhraseStructure.Tree.terminal c none

@[reducible, inline]

abbrev Charnavel2019.dp (i : Item) : Rep

A one-word noun phrase.

Equations

• Charnavel2019.dp i = PhraseStructure.Tree.terminal PhraseStructure.Cat.N (some i)

@[reducible, inline]

abbrev Charnavel2019.poss (i : Item) : Rep

A noun phrase of a possessor, its subject, and a head noun.

Equations

• Charnavel2019.poss i = PhraseStructure.Tree.node PhraseStructure.Cat.Det [Charnavel2019.dp i, Charnavel2019.w PhraseStructure.Cat.N]

@[reducible, inline]

abbrev Charnavel2019.pp (x : Rep) : Rep

A prepositional phrase.

Equations

• Charnavel2019.pp x = PhraseStructure.Tree.node PhraseStructure.Cat.P [Charnavel2019.w PhraseStructure.Cat.P, x]

@[reducible, inline]

abbrev Charnavel2019.cp (x : Rep) : Rep

A clause under its complementizer.

Equations

• Charnavel2019.cp x = PhraseStructure.Tree.node PhraseStructure.Cat.C [Charnavel2019.w PhraseStructure.Cat.C, x]

def Charnavel2019.nominals (t : Rep) : List (Core.Order.TreePath × Item)

The noun phrases of a representation, each with its position.

Equations

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

@[reducible, inline]

abbrev Charnavel2019.Nominal (t : Rep) : Type

The type of noun phrases of a representation.

Equations

• Charnavel2019.Nominal t = { x : Core.Order.TreePath × Charnavel2019.Item // x ∈ Charnavel2019.nominals t }

@[reducible, inline]

abbrev Charnavel2019.Overt (t : Rep) : Type

The pronounced noun phrases of a representation.

Equations

• Charnavel2019.Overt t = { x : Charnavel2019.Nominal t // ¬(↑x).2.IsSilent }

def Charnavel2019.spellout (t : Rep) (b : Core.Order.TreePath) : Set Core.Order.TreePath

The spell-out domains that bound the domain of the position b are the clauses, the verb phrases, and the noun phrases with a subject, their first daughter, other than b.

Equations

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

@[instance_reducible]

instance Charnavel2019.instDecidablePredTreePathMemSetSpellout (t : Rep) (b : Core.Order.TreePath) : DecidablePred fun (x : Core.Order.TreePath) => x ∈ spellout t b

Equations

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

@[reducible, inline]

abbrev Charnavel2019.configuration (t : Rep) : Binding.Configuration (Nominal t)

The configuration on the noun phrases of t takes c-command and the smallest spell-out domain.

Equations

• Charnavel2019.configuration t = Binding.Configuration.comap (fun (x : Charnavel2019.Nominal t) => (↑x).1) (PhraseStructure.Tree.configuration t (Charnavel2019.spellout t))

@[reducible, inline]

abbrev Charnavel2019.Coindexed {t : Rep} (a b : Nominal t) : Prop

Two noun phrases are coindexed when their items bear the same index.

Equations

• Charnavel2019.Coindexed a b = ((↑a).2.index = (↑b).2.index)

def Charnavel2019.Licit (t : Rep) : Prop

A representation is licit when coindexation meets Conditions A and C on it with no anaphor exempt.

Equations

• Charnavel2019.Licit t = (Charnavel2019.configuration t).Satisfies Charnavel2019.Coindexed ∅ fun (x : Charnavel2019.Nominal t) => (↑x).2.class?

@[instance_reducible]

instance Charnavel2019.instDecidableLicit {t : Rep} : Decidable (Licit t)

Equations

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

The silent pronoun and the three conditions

Leaving the silent pronouns out of account turns each condition on the whole representation into a condition on the pronounced noun phrases. For Condition A their bindees become exempt.

@[reducible, inline]

abbrev Charnavel2019.overtConfiguration (t : Rep) : Binding.Configuration (Overt t)

The configuration on the pronounced noun phrases alone.

Equations

• Charnavel2019.overtConfiguration t = Binding.Configuration.comap Subtype.val (Charnavel2019.configuration t)

@[reducible, inline]

abbrev Charnavel2019.silentlyBound (t : Rep) : Set (Overt t)

The pronounced noun phrases that a silent pronoun binds in their domain. Of the anaphors, these are the ones that seem exempt.

Equations

• Charnavel2019.silentlyBound t = (Charnavel2019.configuration t).covertlyBound Charnavel2019.Coindexed Subtype.val

theorem Charnavel2019.mem_silentlyBound_iff {t : Rep} {b : Overt t} : b ∈ silentlyBound t ↔ ∃ x ∈ (configuration t).domain ↑b, (↑x).2.IsSilent ∧ (configuration t).Binds Coindexed x ↑b

A noun phrase is silently bound when a silent pronoun of its domain c-commands it and bears its index.

theorem Charnavel2019.condition_overt {t : Rep} {c : Binding.BindingClass} {b : Overt t} (hc : c.IsAnaphor) : (overtConfiguration t).Condition (Function.onFun Coindexed Subtype.val) (silentlyBound t) b c ↔ (configuration t).Condition Coindexed ∅ (↑b) c

Condition A with the silent pronouns counted is Condition A among the pronounced noun phrases with the silently bound anaphors exempt.

theorem Charnavel2019.condition_rExpression_overt {t : Rep} {b : Overt t} : ((overtConfiguration t).Condition (Function.onFun Coindexed Subtype.val) ∅ b Binding.BindingClass.rExpression ∧ ¬∃ (x : Nominal t), (↑x).2.IsSilent ∧ (configuration t).Binds Coindexed x ↑b) ↔ (configuration t).Condition Coindexed ∅ (↑b) Binding.BindingClass.rExpression

A name meets Condition C with the silent pronouns counted exactly when it meets it among the pronounced noun phrases and no silent pronoun binds it, so a silent pronoun that c-commands a name of its index rules the representation out.

theorem Charnavel2019.condition_pronoun_overt {t : Rep} {b : Overt t} : (overtConfiguration t).Condition (Function.onFun Coindexed Subtype.val) ∅ b Binding.BindingClass.pronoun ∧ b ∉ silentlyBound t ↔ (configuration t).Condition Coindexed ∅ (↑b) Binding.BindingClass.pronoun

Were a pronoun held to Condition B in its spell-out domain, it would have to be free of the silent pronoun there as well as of the pronounced noun phrases.

theorem Charnavel2019.locallyBound_overt_of_licit {t : Rep} {b : Overt t} (ht : Licit t) (hb : (↑↑b).2.class? = some Binding.BindingClass.reflexive) (h : ∀ (x : Nominal t), (↑x).2.IsSilent → ¬Coindexed x ↑b) : (overtConfiguration t).LocallyBound (Function.onFun Coindexed Subtype.val) b

An anaphor that no silent pronoun is coindexed with is bound by a pronounced noun phrase in its domain. Since a logophoric center has a mental state, an inanimate anaphor is such an anaphor, and so is plain.

theorem Charnavel2019.index_eq_of_licit {t : Rep} (ht : Licit t) {a b : Overt t} (ha : (↑↑a).2.class? = some Binding.BindingClass.reflexive) (hb : (↑↑b).2.class? = some Binding.BindingClass.reflexive) (hna : ¬(overtConfiguration t).LocallyBound (Function.onFun Coindexed Subtype.val) a) (hnb : ¬(overtConfiguration t).LocallyBound (Function.onFun Coindexed Subtype.val) b) (h : ∀ x ∈ (configuration t).domain ↑a, ∀ y ∈ (configuration t).domain ↑b, (↑x).2.IsSilent → (↑y).2.IsSilent → x = y) : (↑↑a).2.index = (↑↑b).2.index

Two anaphors without pronounced binders corefer when their domains hold one silent pronoun between them, there being one logophoric operator to a spell-out domain.

theorem Charnavel2019.condition_clause_of_condition {t : Rep} {c : Binding.BindingClass} {b : Nominal t} (hc : c.IsAnaphor) (h : (configuration t).Condition Coindexed ∅ b c) : (Binding.Configuration.comap (fun (x : Nominal t) => (↑x).1) (PhraseStructure.Tree.clauseConfiguration t)).Condition Coindexed ∅ b c

The spell-out domains include the clauses, so an anaphor that meets Condition A in its spell-out domain meets it in its minimal clause.

Sentences

structure Charnavel2019.Sentence : Type

A sentence is given by its representation for each value of its silent pronoun and by the logophoric centers the pronoun can refer to.

• rep : ℕ → Rep

  The representation in which the silent pronoun bears a given index.

• centers : Finset ℕ

  The indices of the logophoric centers of the pronoun's domain, which are the speaker, 0, and those the book's tests make attitude holders or empathy loci, none of them inanimate.

def Charnavel2019.Sentence.Grammatical (s : Sentence) : Prop

A sentence is grammatical when its representation is licit with the silent pronoun referring to a logophoric center.

Equations

• s.Grammatical = ∃ i ∈ s.centers, Charnavel2019.Licit (s.rep i)

@[instance_reducible]

instance Charnavel2019.instDecidableGrammatical (s : Sentence) : Decidable s.Grammatical

Equations

• Charnavel2019.instDecidableGrammatical s = { decide := decide (∃ (a : ℕ) (_ : a ∈ s.centers), (fun (i : ℕ) => Charnavel2019.Licit (s.rep i)) a), reflects_decide := ⋯ }

def Charnavel2019.innShade : Sentence

Cette auberge fait de l'ombre à son propre jardin. The trace of the subject binds the anaphor in the verb phrase. The inn is inanimate and so no center.

Equations

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

def Charnavel2019.innGarden : Sentence

Cette auberge bénéficie du fait que son propre jardin est plus spacieux. The anaphor sits in the subject of a tensed clause.

Equations

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

def Charnavel2019.marieHotel : Sentence

Marie bénéficie du fait que son propre hôtel est plus spacieux. The structure is that of the inn sentence with an animate antecedent. The book runs no test on this sentence, and Marie is entered as a center on the strength of the anaphor's being exempt.

Equations

• Charnavel2019.marieHotel = { rep := Charnavel2019.innGarden.rep, centers := {0, 1} }

def Charnavel2019.earthSpins : Sentence

La Terre tourne sur elle-même.

Equations

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

def Charnavel2019.earthPhotos : Sentence

La Terre a bénéficié du fait que des photos d'elle-même ont montré les effets de la pollution.

Equations

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

def Charnavel2019.robertProject : Sentence

Robert dit que son rival a voté pour son propre projet. Robert is the attitude holder of the embedded clause.

Equations

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

def Charnavel2019.paulHouse : Sentence

Le courage de Paul a sauvé des flammes sa propre maison. Paul is an empathy locus, and the silent pronoun at the edge of the verb phrase does not c-command him.

Equations

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

def Charnavel2019.lucieMorale : Sentence

Les commentaires des internautes sur elle-même ont atteint le moral de Lucie. The subject is a spell-out domain with its own silent pronoun, and Lucie, an empathy locus, lies outside it.

Equations

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

def Charnavel2019.lucieBlog : Sentence

Les commentaires des internautes sur elle-même sur le blog de Lucie ont atteint son moral. Lucie now lies inside the domain of the silent pronoun.

Equations

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

def Charnavel2019.lucieSister (first second : ℕ → Item) : Sentence

Les commentaires des internautes sur elle(-même) et sa (propre) soeur ont atteint le moral de Lucie, with an anaphor and a pronoun in the domain of the silent pronoun.

Equations

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

def Charnavel2019.paulNewspapers : Sentence

Irène tient de Paul qu'hier, plusieurs journaux ont parlé de lui-même. Paul is the source of the report and no attitude holder or empathy locus; Irène, 2, can be the empathy locus.

Equations

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

def Charnavel2019.virginal : Sentence

Le tableau à la gauche de l'épinette pourrait contenir une représentation d'elle-même. The virginal is a deictic center, and inanimate, so no logophoric center.

Equations

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

def Charnavel2019.teacherPlaced : Sentence

Le professeur de musique est placé à droite de sa propre élève. The addressee, 2, is the empathy locus, and the trace of the subject binds the anaphor.

Equations

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

def Charnavel2019.teacherStudent : Sentence

Il semble qu'à la droite du professeur de musique, sa propre élève joue de l'épinette. The music teacher is a deictic center outside the tensed clause of the anaphor.

Equations

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

def Charnavel2019.mothers (mine hers : ℕ → Item) : Sentence

Julie pense que ma (propre) mère et sa (propre) mère devraient se parler, with each possessor an anaphor or a pronoun. Julie and the speaker are attitude holders.

Equations

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

def Charnavel2019.solangeCyril : Sentence

Solange pense que Cyril est fier d'elle-même et de sa propre fille. The silent pronoun binds the first anaphor and the trace of Cyril the second.

Equations

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

def Charnavel2019.sentences : List (Datum × Sentence)

The examples, each with its sentence.

Equations

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

theorem Charnavel2019.map_fst_sentences : List.map Prod.fst sentences = Examples.all

Every example has a sentence.

def Charnavel2019.antecedent? (d : Datum) : Option Center

The kind of perspective center the paper's tests make the antecedent of an example.

Equations

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

theorem Charnavel2019.grammatical_iff (p : Datum × Sentence) : p ∈ sentences → (p.1.judgment = Judgment.acceptable ↔ p.2.Grammatical)

Each example is acceptable exactly when its sentence is grammatical.

theorem Charnavel2019.not_exists_forall_iff_rep : ¬∃ (P : (ℕ → Rep) → Prop), ∀ p ∈ sentences, p.1.judgment = Judgment.acceptable ↔ P p.2.rep

The inn sentence and the Marie sentence have one structure and opposite judgments, so no condition on structure alone, as an exemption by position is, separates the acceptable examples from the others.

theorem Charnavel2019.locallyBound_pronoun : (configuration ((lucieSister Item.pronoun Item.anaphor).rep 1)).LocallyBound Coindexed ⟨({ toList := [0, 3, 1, 0] }, Item.pronoun 1), locallyBound_pronoun._proof_1⟩

Where a pronoun is coindexed with the silent pronoun of its spell-out domain, the silent pronoun binds it there, and the sentence is acceptable. Condition B, which bars a pronoun bound in its domain, therefore cannot have the domain of Condition A.

theorem Charnavel2019.mem_centers_iff (p : Datum × Sentence) : p ∈ sentences → (∀ k ∈ antecedent? p.1, 1 ∈ p.2.centers ↔ k.IsLogophoric) ∧ (p.1.feature? "animacy" = some "inanimate" → 1 ∉ p.2.centers)

The centers entered for the sentences agree with the examples. The antecedent, which bears the index 1, is a center exactly when the tests make it an attitude holder or an empathy locus, and it is none when it is inanimate.

theorem Charnavel2019.licit_rep_antecedent (p : Datum × Sentence) : p ∈ sentences → (antecedent? p.1).isSome = true → Licit (p.2.rep 1)

Where the tests classify the antecedent, the representation in which the silent pronoun refers to it is licit, so only its being no logophoric center rules an example out.

theorem Charnavel2019.acceptable_iff_isLogophoric (d : Datum) : d ∈ Examples.all → ∀ k ∈ antecedent? d, d.judgment = Judgment.acceptable ↔ k.IsLogophoric

Where the tests classify the antecedent, the anaphor is acceptable exactly when the antecedent is an attitude holder or an empathy locus.

theorem Charnavel2019.exists_unacceptable_mem_centersOf_iff {r : Reference.LogophoricRole} : (∃ d ∈ Examples.all, d.judgment ≠ Judgment.acceptable ∧ ∃ k ∈ antecedent? d, k ∈ centersOf r) ↔ r ≠ Reference.LogophoricRole.self

The source and the pivot of Sells, and not the self, each take in the antecedent of an unacceptable anaphor, a source that holds no attitude and a deictic center.