Reciprocal predicates

A reading of the Xs R each other is the relativization of a quantifier over binary relations, a condition on the relation R restricted to the antecedent set X that is invariant under isomorphism. Dalrymple, Kanazawa, Kim, Mchombo and Peters, following Westerståhl, take three such quantifiers of type ⟨2⟩, Lindström quantifiers over the language of graphs. On two or more elements, ful relates any two distinct elements, lin joins them by a chain, and tot relates each element to another, and ful ≤ lin ≤ tot. Taking the relation as it is or with its direction ignored, as Relation.SymmGen R, gives their six schemes (Reciprocal.Recip), ordered by entailment as the product of the two parameters. Weak Reciprocity and Partitioned Strong Reciprocity lie outside the parameterization; with them the file covers the six readings that Beck orders by entailment.

Main definitions

• Reciprocal.ful, Reciprocal.lin, Reciprocal.tot: the three quantifiers of type ⟨2⟩.
• Reciprocal.StrongReciprocity R X, Reciprocal.IntermediateReciprocity R X, Reciprocal.OneWayWeakReciprocity R X: their relativizations to X.
• Reciprocal.InclusiveAlternativeOrdering R X: One-way Weak Reciprocity at Relation.SymmGen R.
• Reciprocal.Recip q R X: the scheme at a setting q : Coverage × Direction of the two parameters.
• Reciprocal.WeakReciprocity R X, Reciprocal.PartitionedStrongReciprocity R X: every member of X is R-related to another member and another to it; X has a Finpartition into strongly reciprocal cells.

Main results

• Reciprocal.ful_le_lin, Reciprocal.lin_le_tot, Reciprocal.recip_antitone: a stronger setting of the parameters entails a weaker one.
• Reciprocal.strongReciprocity_iff, Reciprocal.intermediateReciprocity_iff, Reciprocal.oneWayWeakReciprocity_iff: the relativizations stated over the members of X.
• Reciprocal.IntermediateReciprocity.weak, Reciprocal.PartitionedStrongReciprocity.weak: Weak Reciprocity follows from the intermediate and the partitioned schemes.
• Reciprocal.weakReciprocity_iff_liftRel: Weak Reciprocity is the cumulation Set.LiftRel of R with non-identity conjoined in.

References

• D. T. Langendoen, The logic of reciprocity (1978)
• R. Fiengo and H. Lasnik, The logical structure of reciprocal sentences in English (1973)
• Z. Kański, Logical symmetry and natural language reciprocals (1987)
• M. Dalrymple, M. Kanazawa, Y. Kim, S. A. Mchombo and S. Peters, Reciprocal expressions and the concept of reciprocity (1998)
• S. Beck, Reciprocals are definites (2001)
• W. Sternefeld, Reciprocity and cumulative predication (1998)
• S. Peters and D. Westerståhl, Quantifiers in Language and Logic (2006)

Three quantifiers of type ⟨2⟩

def Reciprocal.ful : FirstOrder.Language.graph.LindstromQuantifier

FUL holds when there are two or more elements and any two distinct elements are related.

Equations

• Reciprocal.ful = FirstOrder.Language.LindstromQuantifier.ofGraphProperty (fun {M : Type ?u.1} (r : M → M → Prop) => Nontrivial M ∧ Pairwise r) @Reciprocal.ful._proof_1

def Reciprocal.lin : FirstOrder.Language.graph.LindstromQuantifier

LIN holds when there are two or more elements and any two distinct elements are joined by a chain.

Equations

• Reciprocal.lin = FirstOrder.Language.LindstromQuantifier.ofGraphProperty (fun {M : Type ?u.1} (r : M → M → Prop) => Nontrivial M ∧ Pairwise (Relation.TransGen r)) @Reciprocal.lin._proof_2

def Reciprocal.tot : FirstOrder.Language.graph.LindstromQuantifier

TOT holds when there are two or more elements and each is related to another.

Equations

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

theorem Reciprocal.ful_le_lin : ful ≤ lin

theorem Reciprocal.lin_le_tot : lin ≤ tot

Relativizations

def Reciprocal.StrongReciprocity {α : Type u_1} (R : α → α → Prop) (X : Finset α) : Prop

Strong Reciprocity ([Lan78]) is ful relativized to X, so X has two or more members and any two distinct members are R-related.

Equations

• Reciprocal.StrongReciprocity R X = (FirstOrder.Language.inducedGraph R ↑X ∈ Reciprocal.ful.holds)

def Reciprocal.IntermediateReciprocity {α : Type u_1} (R : α → α → Prop) (X : Finset α) : Prop

Intermediate Reciprocity ([Lan78]) is lin relativized to X, so X has two or more members and any two distinct members are joined by a chain of R-steps through X.

Equations

• Reciprocal.IntermediateReciprocity R X = (FirstOrder.Language.inducedGraph R ↑X ∈ Reciprocal.lin.holds)

def Reciprocal.OneWayWeakReciprocity {α : Type u_1} (R : α → α → Prop) (X : Finset α) : Prop

One-way Weak Reciprocity ([DKK+98]) is tot relativized to X, so X has two or more members and each is R-related to another.

Equations

• Reciprocal.OneWayWeakReciprocity R X = (FirstOrder.Language.inducedGraph R ↑X ∈ Reciprocal.tot.holds)

def Reciprocal.InclusiveAlternativeOrdering {α : Type u_1} (R : α → α → Prop) (X : Finset α) : Prop

Inclusive Alternative Ordering ([Kan87]) is One-way Weak Reciprocity with the direction of R ignored, so each member of X is R-related to another in one direction or the other.

Equations

• Reciprocal.InclusiveAlternativeOrdering R X = Reciprocal.OneWayWeakReciprocity (Relation.SymmGen R) X

theorem Reciprocal.strongReciprocity_iff {α : Type u_1} {R : α → α → Prop} {X : Finset α} : StrongReciprocity R X ↔ X.Nontrivial ∧ (↑X).Pairwise R

theorem Reciprocal.intermediateReciprocity_iff {α : Type u_1} {R : α → α → Prop} {X : Finset α} : IntermediateReciprocity R X ↔ X.Nontrivial ∧ (↑X).Pairwise (Relation.TransGen fun (x y : α) => x ∈ X ∧ y ∈ X ∧ R x y)

theorem Reciprocal.oneWayWeakReciprocity_iff {α : Type u_1} {R : α → α → Prop} {X : Finset α} : OneWayWeakReciprocity R X ↔ X.Nontrivial ∧ ∀ x ∈ X, ∃ y ∈ X, x ≠ y ∧ R x y

theorem Reciprocal.strongReciprocity_pair {α : Type u_1} {R : α → α → Prop} [DecidableEq α] {a b : α} : StrongReciprocity R {a, b} ↔ a ≠ b ∧ R a b ∧ R b a

On two members, Strong Reciprocity relates each to the other.

@[instance_reducible]

instance Reciprocal.instDecidableStrongReciprocity {α : Type u_1} [DecidableEq α] (R : α → α → Prop) [DecidableRel R] (X : Finset α) : Decidable (StrongReciprocity R X)

Equations

• Reciprocal.instDecidableStrongReciprocity R X = decidable_of_iff (X.Nontrivial ∧ (↑X).Pairwise R) ⋯

@[instance_reducible]

instance Reciprocal.instDecidableOneWayWeakReciprocity {α : Type u_1} [DecidableEq α] (R : α → α → Prop) [DecidableRel R] (X : Finset α) : Decidable (OneWayWeakReciprocity R X)

Equations

• Reciprocal.instDecidableOneWayWeakReciprocity R X = decidable_of_iff (X.Nontrivial ∧ ∀ x ∈ X, ∃ y ∈ X, x ≠ y ∧ R x y) ⋯

@[instance_reducible]

instance Reciprocal.instDecidableInclusiveAlternativeOrdering {α : Type u_1} [DecidableEq α] (R : α → α → Prop) [DecidableRel R] (X : Finset α) : Decidable (InclusiveAlternativeOrdering R X)

Equations

• Reciprocal.instDecidableInclusiveAlternativeOrdering R X = { decide := decide (X.Nontrivial ∧ ∀ x ∈ X, ∃ y ∈ X, x ≠ y ∧ Relation.SymmGen R x y), reflects_decide := ⋯ }

theorem Reciprocal.StrongReciprocity.mono {α : Type u_1} {R S : α → α → Prop} {X : Finset α} (h : StrongReciprocity R X) (hRS : R ≤ S) : StrongReciprocity S X

theorem Reciprocal.IntermediateReciprocity.mono {α : Type u_1} {R S : α → α → Prop} {X : Finset α} (h : IntermediateReciprocity R X) (hRS : R ≤ S) : IntermediateReciprocity S X

theorem Reciprocal.OneWayWeakReciprocity.mono {α : Type u_1} {R S : α → α → Prop} {X : Finset α} (h : OneWayWeakReciprocity R X) (hRS : R ≤ S) : OneWayWeakReciprocity S X

theorem Reciprocal.StrongReciprocity.intermediate {α : Type u_1} {R : α → α → Prop} {X : Finset α} (h : StrongReciprocity R X) : IntermediateReciprocity R X

theorem Reciprocal.IntermediateReciprocity.oneWayWeak {α : Type u_1} {R : α → α → Prop} {X : Finset α} (h : IntermediateReciprocity R X) : OneWayWeakReciprocity R X

theorem Reciprocal.OneWayWeakReciprocity.inclusiveAlternativeOrdering {α : Type u_1} {R : α → α → Prop} {X : Finset α} (h : OneWayWeakReciprocity R X) : InclusiveAlternativeOrdering R X

The two parameters

Dalrymple and colleagues obtain their six schemes from two parameters: which of the three quantifiers the relation must satisfy on the antecedent set, and whether the relation is the scope relation or that relation with its direction ignored. Each parameter is ordered by strength, and the schemes are antitone in the product order.

inductive Reciprocal.Coverage : Type

How the reciprocal's relation must cover the antecedent set, ordered by strength.

• tot : Coverage

  Every member is related to another member, tot.

• lin : Coverage

  Every two distinct members are joined by a chain, lin.

• ful : Coverage

  Every two distinct members are related directly, ful.

@[instance_reducible]

instance Reciprocal.instDecidableEqCoverage : DecidableEq Coverage

Equations

• Reciprocal.instDecidableEqCoverage x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Reciprocal.instReprCoverage : Repr Coverage

Equations

• Reciprocal.instReprCoverage = { reprPrec := Reciprocal.instReprCoverage.repr }

def Reciprocal.instReprCoverage.repr : Coverage → ℕ → Std.Format

Equations

• Reciprocal.instReprCoverage.repr Reciprocal.Coverage.tot prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Reciprocal.Coverage.tot")).group prec✝
• Reciprocal.instReprCoverage.repr Reciprocal.Coverage.lin prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Reciprocal.Coverage.lin")).group prec✝
• Reciprocal.instReprCoverage.repr Reciprocal.Coverage.ful prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Reciprocal.Coverage.ful")).group prec✝

@[instance_reducible]

instance Reciprocal.instFintypeCoverage : Fintype Coverage

Equations

• Reciprocal.instFintypeCoverage = { elems := { val := ↑Reciprocal.Coverage.enumList, nodup := Reciprocal.Coverage.enumList_nodup }, complete := Reciprocal.instFintypeCoverage._proof_1 }

def Reciprocal.Coverage.rank : Coverage → ℕ

The strength of a coverage requirement.

Equations

• Reciprocal.Coverage.tot.rank = 0
• Reciprocal.Coverage.lin.rank = 1
• Reciprocal.Coverage.ful.rank = 2

@[instance_reducible]

instance Reciprocal.instLinearOrderCoverage : LinearOrder Coverage

Equations

• Reciprocal.instLinearOrderCoverage = LinearOrder.lift' Reciprocal.Coverage.rank Reciprocal.instLinearOrderCoverage._proof_1

def Reciprocal.Coverage.quantifier : Coverage → FirstOrder.Language.graph.LindstromQuantifier

The quantifier of type ⟨2⟩ a coverage requirement names.

Equations

• Reciprocal.Coverage.tot.quantifier = Reciprocal.tot
• Reciprocal.Coverage.lin.quantifier = Reciprocal.lin
• Reciprocal.Coverage.ful.quantifier = Reciprocal.ful

theorem Reciprocal.Coverage.quantifier_antitone : Antitone quantifier

theorem Reciprocal.Coverage.mem_quantifier_mono {α : Type u_1} {R S : α → α → Prop} {X : Finset α} (c : Coverage) (hRS : R ≤ S) (h : FirstOrder.Language.inducedGraph R ↑X ∈ c.quantifier.holds) : FirstOrder.Language.inducedGraph S ↑X ∈ c.quantifier.holds

inductive Reciprocal.Direction : Type

Whether the reciprocal relates the members by the scope relation itself or by that relation with its direction ignored, ordered by strength.

• alternative : Direction

  The relation with its direction ignored, Relation.SymmGen R.

• plain : Direction

  The scope relation itself.

@[instance_reducible]

instance Reciprocal.instDecidableEqDirection : DecidableEq Direction

Equations

• Reciprocal.instDecidableEqDirection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Reciprocal.instReprDirection.repr : Direction → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Reciprocal.instReprDirection : Repr Direction

Equations

• Reciprocal.instReprDirection = { reprPrec := Reciprocal.instReprDirection.repr }

@[instance_reducible]

instance Reciprocal.instFintypeDirection : Fintype Direction

Equations

• Reciprocal.instFintypeDirection = { elems := { val := ↑Reciprocal.Direction.enumList, nodup := Reciprocal.Direction.enumList_nodup }, complete := Reciprocal.instFintypeDirection._proof_1 }

def Reciprocal.Direction.rank : Direction → ℕ

The strength of a direction setting.

Equations

• Reciprocal.Direction.alternative.rank = 0
• Reciprocal.Direction.plain.rank = 1

@[instance_reducible]

instance Reciprocal.instLinearOrderDirection : LinearOrder Direction

Equations

• Reciprocal.instLinearOrderDirection = LinearOrder.lift' Reciprocal.Direction.rank Reciprocal.instLinearOrderDirection._proof_1

def Reciprocal.Direction.rel {α : Type u_1} : Direction → (α → α → Prop) → α → α → Prop

The relation a direction setting takes from the scope relation R.

Equations

• Reciprocal.Direction.alternative.rel x✝ = Relation.SymmGen x✝
• Reciprocal.Direction.plain.rel x✝ = x✝

theorem Reciprocal.Direction.rel_anti {α : Type u_1} {R : α → α → Prop} {d d' : Direction} (h : d ≤ d') : d'.rel R ≤ d.rel R

def Reciprocal.Recip {α : Type u_1} (q : Coverage × Direction) (R : α → α → Prop) (X : Finset α) : Prop

The reciprocal quantifier of [DKK+98] at a setting of the two parameters, the relativization to X of the setting's quantifier at the setting's relation. The setting (.ful, .plain) gives Strong Reciprocity and (.tot, .alternative) Inclusive Alternative Ordering.

Equations

• Reciprocal.Recip q R X = (FirstOrder.Language.inducedGraph (q.2.rel R) ↑X ∈ q.1.quantifier.holds)

theorem Reciprocal.recip_antitone {α : Type u_1} {R : α → α → Prop} {X : Finset α} : Antitone fun (q : Coverage × Direction) => Recip q R X

The entailment diagram of [DKK+98]. A stronger setting of the two parameters entails a weaker one.

Weak Reciprocity

def Reciprocal.WeakReciprocity {α : Type u_1} (R : α → α → Prop) (X : Finset α) : Prop

Weak Reciprocity ([Lan78]) holds when every member of X is R-related to another member, and another member is R-related to it.

Equations

• Reciprocal.WeakReciprocity R X = ((∀ x ∈ X, ∃ y ∈ X, R x y ∧ x ≠ y) ∧ ∀ y ∈ X, ∃ x ∈ X, R x y ∧ x ≠ y)

@[instance_reducible]

instance Reciprocal.instDecidableWeakReciprocityOfDecidableEqOfDecidableRel {α : Type u_1} [DecidableEq α] (R : α → α → Prop) [DecidableRel R] (X : Finset α) : Decidable (WeakReciprocity R X)

Equations

• Reciprocal.instDecidableWeakReciprocityOfDecidableEqOfDecidableRel R X = { decide := decide (∀ x ∈ X, ∃ y ∈ X, R x y ∧ x ≠ y) && decide (∀ y ∈ X, ∃ x ∈ X, R x y ∧ x ≠ y), reflects_decide := ⋯ }

theorem Reciprocal.weakReciprocity_iff_liftRel {α : Type u_1} (R : α → α → Prop) (X : Finset α) : WeakReciprocity R X ↔ Set.LiftRel (fun (a b : α) => R a b ∧ a ≠ b) ↑X ↑X

Weak Reciprocity is ** of the relation with non-identity conjoined into it, in the coverage form Set.LiftRel, the bivalent common ground of [Bec01] and [Ste98].

theorem Reciprocal.WeakReciprocity.oneWayWeak {α : Type u_1} {R : α → α → Prop} {X : Finset α} (h : WeakReciprocity R X) (hX : X.Nonempty) : OneWayWeakReciprocity R X

theorem Reciprocal.IntermediateReciprocity.weak {α : Type u_1} {R : α → α → Prop} {X : Finset α} (h : IntermediateReciprocity R X) : WeakReciprocity R X

Partitioned Strong Reciprocity

def Reciprocal.PartitionedStrongReciprocity {α : Type u_1} [DecidableEq α] (R : α → α → Prop) (X : Finset α) : Prop

Partitioned Strong Reciprocity ([FL73]) holds when X splits into disjoint cells within each of which Strong Reciprocity holds.

Equations

• Reciprocal.PartitionedStrongReciprocity R X = ∃ (P : Finpartition X), ∀ c ∈ P.parts, Reciprocal.StrongReciprocity R c

theorem Reciprocal.StrongReciprocity.partitionedStrong {α : Type u_1} {R : α → α → Prop} {X : Finset α} [DecidableEq α] (h : StrongReciprocity R X) : PartitionedStrongReciprocity R X

theorem Reciprocal.PartitionedStrongReciprocity.weak {α : Type u_1} {R : α → α → Prop} {X : Finset α} [DecidableEq α] (h : PartitionedStrongReciprocity R X) : WeakReciprocity R X