Przepiórkowski (2021): Three improvements to the HPSG model theory

This file formalizes the paper's first two proposals about the models of an HPSG grammar. The first replaces exhaustive models of a whole language by rooted models of single utterances, in which every entity is a component of a distinguished root, and lets the quantifiers range over the whole universe. The second addresses Höhle's Problem, the spurious ambiguity that arises when objects that look alike may or may not be token-identical, by an identity principle from which a cycle exempts the referential indices.

For the first proposal the file proves how the new quantifiers relate to Richter's. The two agree at a root, they can disagree elsewhere, and a closed principle that never mentions the described entity holds throughout the rooted model generated by r exactly when it holds at r in Richter's sense. For the second it proves that the identity principle makes every species without attributes unique, and that the definition of the copy relation has two solutions on a cyclic index, only one of which identifies the indices of two pronouns.

Implementation notes

The paper adds a term r for the root, so that a grammar can constrain the root directly. Here a root principle is an ordinary formula that is evaluated at the root, which comes to the same thing because r followed by a path denotes at any entity what the colon followed by that path denotes at the root. The paper's definition of the copy relation applies the relation symbol to terms, although its own syntax, like Richter's, admits only variables there. The values are bound to quantified variables first. The index of the illustration has a gender and the attribute INT, without person and number.

The third proposal, a second-order extension of the description language for the coordination of unlike categories, is not formalized.

References

• [Prz21]
• [Ric24]

First-order quantification

def Przepiorkowski2021.SatisfiesFO {Srt : Type u} [PartialOrder Srt] {Sig : HPSG.RSRL.Signature Srt} {U : Type v} (I : HPSG.RSRL.Interpretation Sig U) (g : ℕ → U) (u : U) : HPSG.RSRL.Desc Sig → Prop

Satisfaction with quantifiers that range over the whole universe, as the paper defines it for rooted interpretations. The clauses for the atomic formulae and the connectives are those of Interpretation.Satisfies.

Equations

• Przepiorkowski2021.SatisfiesFO I g u (HPSG.RSRL.Desc.sortAssign t σ) = ∃ v ∈ I.termDenot g t u, I.S v ≤ σ
• Przepiorkowski2021.SatisfiesFO I g u (HPSG.RSRL.Desc.pathEq t₁ t₂) = ∃ v ∈ I.termDenot g t₁ u, v ∈ I.termDenot g t₂ u
• Przepiorkowski2021.SatisfiesFO I g u (HPSG.RSRL.Desc.rel ρ xs) = I.R ρ fun (i : Fin (Sig.arity ρ)) => g (xs i)
• Przepiorkowski2021.SatisfiesFO I g u d.neg = ¬Przepiorkowski2021.SatisfiesFO I g u d
• Przepiorkowski2021.SatisfiesFO I g u (d.and e) = (Przepiorkowski2021.SatisfiesFO I g u d ∧ Przepiorkowski2021.SatisfiesFO I g u e)
• Przepiorkowski2021.SatisfiesFO I g u (d.or e) = (Przepiorkowski2021.SatisfiesFO I g u d ∨ Przepiorkowski2021.SatisfiesFO I g u e)
• Przepiorkowski2021.SatisfiesFO I g u (d.imp e) = (Przepiorkowski2021.SatisfiesFO I g u d → Przepiorkowski2021.SatisfiesFO I g u e)
• Przepiorkowski2021.SatisfiesFO I g u (HPSG.RSRL.Desc.ex x_1 d) = ∃ (w : U), Przepiorkowski2021.SatisfiesFO I (Function.update g x_1 w) u d
• Przepiorkowski2021.SatisfiesFO I g u (HPSG.RSRL.Desc.all x_1 d) = ∀ (w : U), Przepiorkowski2021.SatisfiesFO I (Function.update g x_1 w) u d

def Przepiorkowski2021.ModelsFO {Srt : Type u} [PartialOrder Srt] {Sig : HPSG.RSRL.Signature Srt} {U : Type v} (I : HPSG.RSRL.Interpretation Sig U) (G : HPSG.RSRL.Grammar Sig) : Prop

An interpretation is a model of a grammar under first-order quantification.

Equations

• Przepiorkowski2021.ModelsFO I G = ∀ (u : U), ∀ d ∈ G, Przepiorkowski2021.SatisfiesFO I (fun (x : ℕ) => u) u d

theorem Przepiorkowski2021.satisfiesFO_iff_satisfies {Srt : Type u} [PartialOrder Srt] {Sig : HPSG.RSRL.Signature Srt} {U : Type v} {I : HPSG.RSRL.Interpretation Sig U} {u : U} {d : HPSG.RSRL.Desc Sig} (hu : I.IsRootedAt u) {g : ℕ → U} : SatisfiesFO I g u d ↔ I.Satisfies g u d

At an entity that every entity is a component of, quantification over components and quantification over the universe agree.

def Przepiorkowski2021.ColonFreeTerm {Srt : Type u} [PartialOrder Srt] {Sig : HPSG.RSRL.Signature Srt} : HPSG.RSRL.Term Sig → Prop

A term that does not start at the described entity.

Equations

• Przepiorkowski2021.ColonFreeTerm HPSG.RSRL.Term.colon = False
• Przepiorkowski2021.ColonFreeTerm (HPSG.RSRL.Term.var a) = True
• Przepiorkowski2021.ColonFreeTerm (t.feat a) = Przepiorkowski2021.ColonFreeTerm t

def Przepiorkowski2021.ColonFree {Srt : Type u} [PartialOrder Srt] {Sig : HPSG.RSRL.Signature Srt} : HPSG.RSRL.Desc Sig → Prop

A formula none of whose terms starts at the described entity.

Equations

• Przepiorkowski2021.ColonFree (HPSG.RSRL.Desc.sortAssign t σ) = Przepiorkowski2021.ColonFreeTerm t
• Przepiorkowski2021.ColonFree (HPSG.RSRL.Desc.pathEq t₁ t₂) = (Przepiorkowski2021.ColonFreeTerm t₁ ∧ Przepiorkowski2021.ColonFreeTerm t₂)
• Przepiorkowski2021.ColonFree (HPSG.RSRL.Desc.rel ρ xs) = True
• Przepiorkowski2021.ColonFree d.neg = Przepiorkowski2021.ColonFree d
• Przepiorkowski2021.ColonFree (d.and e) = (Przepiorkowski2021.ColonFree d ∧ Przepiorkowski2021.ColonFree e)
• Przepiorkowski2021.ColonFree (d.or e) = (Przepiorkowski2021.ColonFree d ∧ Przepiorkowski2021.ColonFree e)
• Przepiorkowski2021.ColonFree (d.imp e) = (Przepiorkowski2021.ColonFree d ∧ Przepiorkowski2021.ColonFree e)
• Przepiorkowski2021.ColonFree (HPSG.RSRL.Desc.ex x_1 d) = Przepiorkowski2021.ColonFree d
• Przepiorkowski2021.ColonFree (HPSG.RSRL.Desc.all x_1 d) = Przepiorkowski2021.ColonFree d

def Przepiorkowski2021.QuantifierFree {Srt : Type u} [PartialOrder Srt] {Sig : HPSG.RSRL.Signature Srt} : HPSG.RSRL.Desc Sig → Prop

A formula without quantifiers.

Equations

• Przepiorkowski2021.QuantifierFree (HPSG.RSRL.Desc.sortAssign t σ) = True
• Przepiorkowski2021.QuantifierFree (HPSG.RSRL.Desc.pathEq t₁ t₂) = True
• Przepiorkowski2021.QuantifierFree (HPSG.RSRL.Desc.rel ρ xs) = True
• Przepiorkowski2021.QuantifierFree d.neg = Przepiorkowski2021.QuantifierFree d
• Przepiorkowski2021.QuantifierFree (d.and e) = (Przepiorkowski2021.QuantifierFree d ∧ Przepiorkowski2021.QuantifierFree e)
• Przepiorkowski2021.QuantifierFree (d.or e) = (Przepiorkowski2021.QuantifierFree d ∧ Przepiorkowski2021.QuantifierFree e)
• Przepiorkowski2021.QuantifierFree (d.imp e) = (Przepiorkowski2021.QuantifierFree d ∧ Przepiorkowski2021.QuantifierFree e)
• Przepiorkowski2021.QuantifierFree (HPSG.RSRL.Desc.ex x_1 d) = False
• Przepiorkowski2021.QuantifierFree (HPSG.RSRL.Desc.all x_1 d) = False

@[instance_reducible]

instance Przepiorkowski2021.instDecidableColonFreeTerm {Srt : Type u} [PartialOrder Srt] {Sig : HPSG.RSRL.Signature Srt} : DecidablePred ColonFreeTerm

Equations

• Przepiorkowski2021.instDecidableColonFreeTerm HPSG.RSRL.Term.colon = isFalse ⋯
• Przepiorkowski2021.instDecidableColonFreeTerm (HPSG.RSRL.Term.var a) = isTrue trivial
• Przepiorkowski2021.instDecidableColonFreeTerm (t.feat a) = Przepiorkowski2021.instDecidableColonFreeTerm t

@[instance_reducible]

instance Przepiorkowski2021.instDecidableColonFree {Srt : Type u} [PartialOrder Srt] {Sig : HPSG.RSRL.Signature Srt} : DecidablePred ColonFree

Equations

• Przepiorkowski2021.instDecidableColonFree (HPSG.RSRL.Desc.sortAssign t σ) = ⋯.mpr inferInstance
• Przepiorkowski2021.instDecidableColonFree (HPSG.RSRL.Desc.pathEq t₁ t₂) = ⋯.mpr inferInstance
• Przepiorkowski2021.instDecidableColonFree (HPSG.RSRL.Desc.rel ρ xs) = ⋯.mpr inferInstance
• Przepiorkowski2021.instDecidableColonFree d.neg = Przepiorkowski2021.instDecidableColonFree d
• Przepiorkowski2021.instDecidableColonFree (HPSG.RSRL.Desc.ex x_1 d) = Przepiorkowski2021.instDecidableColonFree d
• Przepiorkowski2021.instDecidableColonFree (HPSG.RSRL.Desc.all x_1 d) = Przepiorkowski2021.instDecidableColonFree d
• Przepiorkowski2021.instDecidableColonFree (d.and e) = ⋯.mpr inferInstance
• Przepiorkowski2021.instDecidableColonFree (d.or e) = ⋯.mpr inferInstance
• Przepiorkowski2021.instDecidableColonFree (d.imp e) = ⋯.mpr inferInstance

@[instance_reducible]

instance Przepiorkowski2021.instDecidableQuantifierFree {Srt : Type u} [PartialOrder Srt] {Sig : HPSG.RSRL.Signature Srt} : DecidablePred QuantifierFree

Equations

• Przepiorkowski2021.instDecidableQuantifierFree (HPSG.RSRL.Desc.sortAssign t σ) = isTrue trivial
• Przepiorkowski2021.instDecidableQuantifierFree (HPSG.RSRL.Desc.pathEq t₁ t₂) = isTrue trivial
• Przepiorkowski2021.instDecidableQuantifierFree (HPSG.RSRL.Desc.rel ρ xs) = isTrue trivial
• Przepiorkowski2021.instDecidableQuantifierFree (HPSG.RSRL.Desc.ex x_1 d) = isFalse ⋯
• Przepiorkowski2021.instDecidableQuantifierFree (HPSG.RSRL.Desc.all x_1 d) = isFalse ⋯
• Przepiorkowski2021.instDecidableQuantifierFree d.neg = Przepiorkowski2021.instDecidableQuantifierFree d
• Przepiorkowski2021.instDecidableQuantifierFree (d.and e) = ⋯.mpr inferInstance
• Przepiorkowski2021.instDecidableQuantifierFree (d.or e) = ⋯.mpr inferInstance
• Przepiorkowski2021.instDecidableQuantifierFree (d.imp e) = ⋯.mpr inferInstance

theorem Przepiorkowski2021.satisfiesFO_iff_satisfies_of_quantifierFree {Srt : Type u} [PartialOrder Srt] {Sig : HPSG.RSRL.Signature Srt} {U : Type v} {I : HPSG.RSRL.Interpretation Sig U} {g : ℕ → U} {u : U} {d : HPSG.RSRL.Desc Sig} (hd : QuantifierFree d) : SatisfiesFO I g u d ↔ I.Satisfies g u d

Without quantifiers the two notions of satisfaction agree at every entity.

theorem Przepiorkowski2021.satisfiesFO_congr {Srt : Type u} [PartialOrder Srt] {Sig : HPSG.RSRL.Signature Srt} {U : Type v} {I : HPSG.RSRL.Interpretation Sig U} {u u' : U} {d : HPSG.RSRL.Desc Sig} (hd : ColonFree d) {g g' : ℕ → U} : (∀ x ∈ d.freeVars, g x = g' x) → (SatisfiesFO I g u d ↔ SatisfiesFO I g' u' d)

Under first-order quantification, a formula that never mentions the described entity depends neither on that entity nor on the values of variables that are not free in it.

Rooted models

theorem Przepiorkowski2021.modelsFO_generated_iff_of_colonFree {Srt : Type u} [PartialOrder Srt] {Sig : HPSG.RSRL.Signature Srt} {U : Type v} {I : HPSG.RSRL.Interpretation Sig U} {G : HPSG.RSRL.Grammar Sig} (r : U) (hG : ∀ d ∈ G, ColonFree d ∧ d.freeVars = ∅) : ModelsFO (I.generated r) G ↔ ∀ d ∈ G, I.Satisfies (fun (x : ℕ) => r) r d

Closed principles that never mention the described entity hold throughout the rooted interpretation generated by r, under first-order quantification, exactly when they hold at r under quantification over components.

theorem Przepiorkowski2021.modelsFO_generated_iff_of_quantifierFree {Srt : Type u} [PartialOrder Srt] {Sig : HPSG.RSRL.Signature Srt} {U : Type v} {I : HPSG.RSRL.Interpretation Sig U} {G : HPSG.RSRL.Grammar Sig} (r : U) (hG : ∀ d ∈ G, QuantifierFree d) : ModelsFO (I.generated r) G ↔ ∀ (v : U), I.IsComponentOf r v → ∀ d ∈ G, I.Satisfies (fun (x : ℕ) => v) v d

Principles without quantifiers hold throughout the rooted interpretation generated by r exactly when they hold of every component of r.

@[instance_reducible]

instance Przepiorkowski2021.decidableSatisfiesFO {Srt : Type u} [PartialOrder Srt] {Sig : HPSG.RSRL.Signature Srt} {U : Type v} {I : HPSG.RSRL.Interpretation Sig U} [Fintype U] [DecidableEq U] [DecidableLE Srt] [(ρ : Sig.Rel) → DecidablePred (I.R ρ)] (g : ℕ → U) (u : U) (d : HPSG.RSRL.Desc Sig) : Decidable (SatisfiesFO I g u d)

Equations

• Przepiorkowski2021.decidableSatisfiesFO g u (HPSG.RSRL.Desc.sortAssign t σ) = ⋯.mpr inferInstance
• Przepiorkowski2021.decidableSatisfiesFO g u (HPSG.RSRL.Desc.pathEq t₁ t₂) = ⋯.mpr inferInstance
• Przepiorkowski2021.decidableSatisfiesFO g u (HPSG.RSRL.Desc.rel ρ xs) = ⋯.mpr inferInstance
• Przepiorkowski2021.decidableSatisfiesFO g u d.neg = ⋯.mpr inferInstance
• Przepiorkowski2021.decidableSatisfiesFO g u (d.and e) = ⋯.mpr inferInstance
• Przepiorkowski2021.decidableSatisfiesFO g u (d.or e) = ⋯.mpr inferInstance
• Przepiorkowski2021.decidableSatisfiesFO g u (d.imp e) = ⋯.mpr inferInstance
• Przepiorkowski2021.decidableSatisfiesFO g u (HPSG.RSRL.Desc.ex x_1 d) = ⋯.mpr inferInstance
• Przepiorkowski2021.decidableSatisfiesFO g u (HPSG.RSRL.Desc.all x_1 d) = ⋯.mpr inferInstance

Binding theory in rooted models

theorem Przepiorkowski2021.modelsFO_clause_iff (σ : HPSG.RSRL.Binding.Srt) (i γ n : HPSG.RSRL.Binding.Ent) : ModelsFO ((HPSG.RSRL.Binding.clause σ i γ n).generated HPSG.RSRL.Binding.Ent.s) HPSG.RSRL.Binding.grammar ↔ ∀ d ∈ HPSG.RSRL.Binding.grammar, (HPSG.RSRL.Binding.clause σ i γ n).Satisfies (fun (x : ℕ) => HPSG.RSRL.Binding.Ent.s) HPSG.RSRL.Binding.Ent.s d

The binding principles hold throughout the utterance that the verb's sign generates exactly when they hold at that sign in Richter's sense.

Stranded structures and root principles

@[reducible, inline]

abbrev Przepiorkowski2021.oneGap : HPSG.RSRL.Interpretation HPSG.Construction.sig Sag2010.Ent

A topicalized construct of Studies/Sag2010, whose head daughter has one gap.

Equations

• Przepiorkowski2021.oneGap = Sag2010.FGClause.topicalized.construct HPSG.Construction.Srt.austinean Sag2010.Ent.nil

@[reducible, inline]

abbrev Przepiorkowski2021.twoGaps : HPSG.RSRL.Interpretation HPSG.Construction.sig Sag2010.Ent

A nonsubject wh-interrogative construct of Studies/Sag2010 whose head daughter has two gaps, so that its mother still has one.

Equations

• Przepiorkowski2021.twoGaps = Sag2010.FGClause.whInterrogative.construct HPSG.Construction.Srt.question Sag2010.Ent.g2

@[reducible]

def Przepiorkowski2021.strandedIndex : HPSG.RSRL.Interpretation HPSG.Construction.sig Unit

An index on its own, which belongs to no utterance. The paper's stranded structures are rooted in local objects, which the signature lacks; an index is likewise a component of signs that no principle mentions.

Equations

• Przepiorkowski2021.strandedIndex = { S := fun (x : Unit) => HPSG.Construction.Srt.idx, A := fun (x : HPSG.Construction.sig.Attr) (x_1 : Unit) => none, R := HPSG.Construction.noRel }

def Przepiorkowski2021.rootPrinciples : List (HPSG.RSRL.Desc HPSG.Construction.sig)

The principles that hold of the root of an utterance, which is a construct whose mother has an empty GAP list.

Equations

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

def Przepiorkowski2021.IsUtterance {U : Type u_1} (I : HPSG.RSRL.Interpretation HPSG.Construction.sig U) (r : U) : Prop

An interpretation is an utterance with root r when it is rooted at r, is a model of the grammar under first-order quantification, and satisfies the root principles at r.

Equations

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

theorem Przepiorkowski2021.isUtterance_generated_iff {U : Type u_1} {I : HPSG.RSRL.Interpretation HPSG.Construction.sig U} (r : U) : IsUtterance (I.generated r) ⟨r, ⋯⟩ ↔ (∀ (v : U), I.IsComponentOf r v → ∀ d ∈ HPSG.Construction.grammar, I.Satisfies (fun (x : ℕ) => v) v d) ∧ ∀ d ∈ rootPrinciples, I.Satisfies (fun (x : ℕ) => r) r d

The interpretation that r generates is an utterance exactly when the components of r satisfy the grammar and r satisfies the root principles, all in Richter's sense.

Höhle's Problem

inductive Przepiorkowski2021.Identity.Srt : Type

The sorts of the illustration are a phrase, referential indices, empty lists and one gender value.

• top : Srt
• phrase : Srt
• ref : Srt
• elist : Srt
• fem : Srt

@[instance_reducible]

instance Przepiorkowski2021.Identity.instDecidableEqSrt : DecidableEq Srt

Equations

• Przepiorkowski2021.Identity.instDecidableEqSrt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Przepiorkowski2021.Identity.instFintypeSrt : Fintype Srt

Equations

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

def Przepiorkowski2021.Identity.instReprSrt.repr : Srt → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Przepiorkowski2021.Identity.instReprSrt : Repr Srt

Equations

• Przepiorkowski2021.Identity.instReprSrt = { reprPrec := Przepiorkowski2021.Identity.instReprSrt.repr }

def Przepiorkowski2021.Identity.Srt.parent : Srt → Option Srt

The immediate supersort of each sort other than top.

Equations

• Przepiorkowski2021.Identity.Srt.top.parent = none
• x✝.parent = some Przepiorkowski2021.Identity.Srt.top

def Przepiorkowski2021.Identity.Srt.rank : Srt → ℕ

The depth of a sort below top.

Equations

• Przepiorkowski2021.Identity.Srt.top.rank = 0
• x✝.rank = 1

@[instance_reducible]

instance Przepiorkowski2021.Identity.instPartialOrderSrt : PartialOrder Srt

Equations

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

@[instance_reducible]

instance Przepiorkowski2021.Identity.instDecidableLESrt : DecidableLE Srt

Equations

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

inductive Przepiorkowski2021.Identity.Attr : Type

A phrase has two indices and two lists, and an index has a gender and the attribute INT.

• IDX1 : Attr
• IDX2 : Attr
• L1 : Attr
• L2 : Attr
• GEND : Attr
• INT : Attr

@[instance_reducible]

instance Przepiorkowski2021.Identity.instDecidableEqAttr : DecidableEq Attr

Equations

• Przepiorkowski2021.Identity.instDecidableEqAttr x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Przepiorkowski2021.Identity.instFintypeAttr : Fintype Attr

Equations

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

@[instance_reducible]

instance Przepiorkowski2021.Identity.instReprAttr : Repr Attr

Equations

• Przepiorkowski2021.Identity.instReprAttr = { reprPrec := Przepiorkowski2021.Identity.instReprAttr.repr }

def Przepiorkowski2021.Identity.instReprAttr.repr : Attr → ℕ → Std.Format

Equations

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

def Przepiorkowski2021.Identity.Attr.decl : Attr → List (Srt × Srt)

The sorts that introduce each attribute, with its value sort there.

Equations

• Przepiorkowski2021.Identity.Attr.IDX1.decl = [(Przepiorkowski2021.Identity.Srt.phrase, Przepiorkowski2021.Identity.Srt.ref)]
• Przepiorkowski2021.Identity.Attr.IDX2.decl = [(Przepiorkowski2021.Identity.Srt.phrase, Przepiorkowski2021.Identity.Srt.ref)]
• Przepiorkowski2021.Identity.Attr.L1.decl = [(Przepiorkowski2021.Identity.Srt.phrase, Przepiorkowski2021.Identity.Srt.elist)]
• Przepiorkowski2021.Identity.Attr.L2.decl = [(Przepiorkowski2021.Identity.Srt.phrase, Przepiorkowski2021.Identity.Srt.elist)]
• Przepiorkowski2021.Identity.Attr.GEND.decl = [(Przepiorkowski2021.Identity.Srt.ref, Przepiorkowski2021.Identity.Srt.fem)]
• Przepiorkowski2021.Identity.Attr.INT.decl = [(Przepiorkowski2021.Identity.Srt.ref, Przepiorkowski2021.Identity.Srt.ref)]

inductive Przepiorkowski2021.Identity.Rel : Type

The one relation symbol is the copy relation.

• copies : Rel

@[instance_reducible]

instance Przepiorkowski2021.Identity.instDecidableEqRel : DecidableEq Rel

Equations

• Przepiorkowski2021.Identity.instDecidableEqRel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Przepiorkowski2021.Identity.instFintypeRel : Fintype Rel

Equations

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

@[instance_reducible]

instance Przepiorkowski2021.Identity.instReprRel : Repr Rel

Equations

• Przepiorkowski2021.Identity.instReprRel = { reprPrec := Przepiorkowski2021.Identity.instReprRel.repr }

def Przepiorkowski2021.Identity.instReprRel.repr : Rel → ℕ → Std.Format

Equations

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

@[reducible]

def Przepiorkowski2021.Identity.sig : HPSG.RSRL.Signature Srt

The signature of the illustration.

Equations

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

def Przepiorkowski2021.Identity.uniqueEmptyList : HPSG.RSRL.Desc sig

The Unique Empty List Condition says that any two empty lists are the same object.

Equations

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

def Przepiorkowski2021.Identity.generalIdentity : HPSG.RSRL.Desc sig

The General Identity Principle says that copies are the same object.

Equations

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

def Przepiorkowski2021.Identity.sameSpecies : HPSG.RSRL.Desc sig

The objects at the variables 1 and 2 have the same species.

Equations

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

def Przepiorkowski2021.Identity.copiesAt (α : Attr) : HPSG.RSRL.Desc sig

If the attribute α is defined on the object at 1, its values at 1 and 2 are copies.

Equations

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

def Przepiorkowski2021.Identity.copiesDef : HPSG.RSRL.Desc sig

The definition of the copy relation. Two objects are copies exactly when they have the same species and the values of every attribute defined on them are copies.

Equations

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

def Przepiorkowski2021.Identity.intensionality : HPSG.RSRL.Desc sig

The Universal Intensionality Principle says that the INT value of an object is the object itself.

Equations

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

def Przepiorkowski2021.Identity.principles : HPSG.RSRL.Grammar sig

The identity principles of the proposal.

Equations

• Przepiorkowski2021.Identity.principles = [Przepiorkowski2021.Identity.copiesDef, Przepiorkowski2021.Identity.generalIdentity, Przepiorkowski2021.Identity.intensionality]

theorem Przepiorkowski2021.Identity.colonFree_principles (d : HPSG.RSRL.Desc sig) : d ∈ uniqueEmptyList :: principles → ColonFree d ∧ d.freeVars = ∅

The principles are closed and never mention the described entity, so they hold throughout a rooted model exactly when they hold at its root.

theorem Przepiorkowski2021.Identity.eq_of_attributeless {U : Type u_1} {I : HPSG.RSRL.Interpretation sig U} {g : ℕ → U} {r a b : U} (hdef : I.Satisfies g r copiesDef) (hgip : I.Satisfies g r generalIdentity) (ha : I.IsComponentOf r a) (hb : I.IsComponentOf r b) {σ : Srt} (hσ : σ = Srt.elist ∨ σ = Srt.fem) (hsa : I.S a = σ) (hsb : I.S b = σ) (hattr : ∀ (α : sig.Attr), I.A α a = none) : a = b

In a model of the definition of copies and of the General Identity Principle, two components that belong to the same species without attributes are the same object. The principle therefore subsumes the Unique Empty List Condition, and it would identify the indices of any two pronouns of the same gender if an index had no attribute that made it cyclic.

inductive Przepiorkowski2021.Identity.Ent : Type

The entities of an utterance with two pronouns are the phrase, two indices, two empty lists and the feminine gender.

• p : Ent
• i1 : Ent
• i2 : Ent
• e1 : Ent
• e2 : Ent
• f : Ent

@[instance_reducible]

instance Przepiorkowski2021.Identity.instDecidableEqEnt : DecidableEq Ent

Equations

• Przepiorkowski2021.Identity.instDecidableEqEnt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Przepiorkowski2021.Identity.instFintypeEnt : Fintype Ent

Equations

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

@[instance_reducible]

instance Przepiorkowski2021.Identity.instReprEnt : Repr Ent

Equations

• Przepiorkowski2021.Identity.instReprEnt = { reprPrec := Przepiorkowski2021.Identity.instReprEnt.repr }

def Przepiorkowski2021.Identity.instReprEnt.repr : Ent → ℕ → Std.Format

Equations

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

def Przepiorkowski2021.Identity.Ent.sort : Ent → Srt

The sort of each entity.

Equations

• Przepiorkowski2021.Identity.Ent.p.sort = Przepiorkowski2021.Identity.Srt.phrase
• Przepiorkowski2021.Identity.Ent.i1.sort = Przepiorkowski2021.Identity.Srt.ref
• Przepiorkowski2021.Identity.Ent.i2.sort = Przepiorkowski2021.Identity.Srt.ref
• Przepiorkowski2021.Identity.Ent.e1.sort = Przepiorkowski2021.Identity.Srt.elist
• Przepiorkowski2021.Identity.Ent.e2.sort = Przepiorkowski2021.Identity.Srt.elist
• Przepiorkowski2021.Identity.Ent.f.sort = Przepiorkowski2021.Identity.Srt.fem

@[reducible]

def Przepiorkowski2021.Identity.utterance (coindexed oneElist : Bool) (R : Ent → Ent → Prop) : HPSG.RSRL.Interpretation sig Ent

The utterance whose two pronouns share their index or not, whose two lists are the same empty list or not, and whose copy relation is R. Each index is its own INT value.

Equations

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

@[instance_reducible]

instance Przepiorkowski2021.Identity.instDecidablePredForallFinAritySrtSigEntRUtteranceOfDecidableRel (c o : Bool) (R : Ent → Ent → Prop) [DecidableRel R] (ρ : sig.Rel) : DecidablePred ((utterance c o R).R ρ)

Equations

• Przepiorkowski2021.Identity.instDecidablePredForallFinAritySrtSigEntRUtteranceOfDecidableRel c o R ρ xs = inst✝ (xs 0) (xs 1)

def Przepiorkowski2021.Identity.leastCopies (a b : Ent) : Prop

The smallest copy relation, which holds between objects of the same species without attributes.

Equations

• Przepiorkowski2021.Identity.leastCopies a b = (a.sort = b.sort ∧ (a.sort = Przepiorkowski2021.Identity.Srt.elist ∨ a.sort = Przepiorkowski2021.Identity.Srt.fem))

def Przepiorkowski2021.Identity.greatestCopies (a b : Ent) : Prop

The largest copy relation, which holds between all objects of the same species.

Equations

• Przepiorkowski2021.Identity.greatestCopies a b = (a.sort = b.sort)

@[instance_reducible]

instance Przepiorkowski2021.Identity.instDecidableRelEntLeastCopies : DecidableRel leastCopies

Equations

• Przepiorkowski2021.Identity.instDecidableRelEntLeastCopies x✝¹ x✝ = id inferInstance

@[instance_reducible]

instance Przepiorkowski2021.Identity.instDecidableRelEntGreatestCopies : DecidableRel greatestCopies

Equations

• Przepiorkowski2021.Identity.instDecidableRelEntGreatestCopies x✝¹ x✝ = id inferInstance

theorem Przepiorkowski2021.Identity.copiesDef_underdetermined : (utterance false true leastCopies).Satisfies (fun (x : ℕ) => Ent.p) Ent.p copiesDef ∧ (utterance false true greatestCopies).Satisfies (fun (x : ℕ) => Ent.p) Ent.p copiesDef ∧ ¬leastCopies Ent.i1 Ent.i2 ∧ greatestCopies Ent.i1 Ent.i2

The definition of copies does not determine the relation on cyclic structures. With the two pronouns not coindexed, both the smallest and the largest relation satisfy it, and they differ on whether the two indices are copies.

theorem Przepiorkowski2021.Identity.generalIdentity_exempts_indices : (∀ (c : Bool), (utterance c true leastCopies).Satisfies (fun (x : ℕ) => Ent.p) Ent.p generalIdentity) ∧ ¬(utterance false false leastCopies).Satisfies (fun (x : ℕ) => Ent.p) Ent.p generalIdentity ∧ ¬(utterance false true greatestCopies).Satisfies (fun (x : ℕ) => Ent.p) Ent.p generalIdentity

Under the smallest relation the General Identity Principle leaves the two indices distinct, so the coindexed and the non-coindexed reading both survive, while two empty lists are still excluded. Under the largest relation it rejects the non-coindexed reading.

theorem Przepiorkowski2021.Identity.modelsFO_utterance : (∀ (c : Bool), ModelsFO ((utterance c true leastCopies).generated Ent.p) principles) ∧ ¬ModelsFO ((utterance false false leastCopies).generated Ent.p) principles

Under the smallest copy relation, the coindexed and the non-coindexed utterance with one empty list are both rooted models of the identity principles, and the utterance with two empty lists is not.