Per-position signature profiles for two-place operators

Linguistic operators carry one entailment signature per argument position — every is anti-additive in its restrictor and monotone in its scope, no is anti-additive in both ([PW06] §5.8–5.9, [vB84]). Sig₂ records a signature pair, Sig₂.SoundFor says each component is sound for the corresponding section, and EntailmentSig.SoundFor.comp₂ composes an outer context into both positions at once — the shape of locality computations like K&L's not ∘ every-scope. The "DE on a constant parameter" idiom (adversatives, conditional antecedents) is the special case of reading one section of a Sig₂.SoundFor.

The GQ bridges connect the profile to the existing per-position machinery in Quantification: the four DoubleMono cells realize mono/anti profiles, and Left/RightAntiAdditive are sectionwise IsAntiAdditive at the Prop instance. every_sem and no_sem get certified profiles as worked instances.

Main declarations

• Sig₂, Sig₂.SoundFor: per-position signature profile and its soundness;
• EntailmentSig.SoundFor.comp₂: outer composition acts componentwise;
• DoubleMono.toSig₂ and the four cell theorems sig₂_soundFor_upUp … sig₂_soundFor_downDown;
• leftAntiAdditive_iff_isAntiAdditive, rightAntiAdditive_iff_isAntiAdditive;
• every_sem_soundFor, no_sem_soundFor: certified determiner profiles.

structure NaturalLogic.Sig₂ : Type

A per-position signature profile for a two-place operator. For determiners the positions are restrictor and scope; under the restrictor analysis of conditionals, antecedent and consequent.

• restrictor : EntailmentSig
• scope : EntailmentSig

@[implicit_reducible]

instance NaturalLogic.instDecidableEqSig₂ : DecidableEq Sig₂

Equations

• NaturalLogic.instDecidableEqSig₂ = NaturalLogic.instDecidableEqSig₂.decEq

def NaturalLogic.instDecidableEqSig₂.decEq (x✝ x✝¹ : Sig₂) : Decidable (x✝ = x✝¹)

Equations

• NaturalLogic.instDecidableEqSig₂.decEq { restrictor := a, scope := a_1 } { restrictor := b, scope := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance NaturalLogic.instReprSig₂ : Repr Sig₂

Equations

• NaturalLogic.instReprSig₂ = { reprPrec := NaturalLogic.instReprSig₂.repr }

def NaturalLogic.instReprSig₂.repr : Sig₂ → ℕ → Std.Format

Equations

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

def NaturalLogic.Sig₂.SoundFor {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] [Lattice γ] [BoundedOrder γ] (σ : Sig₂) (f : α → β → γ) : Prop

A profile is sound for a two-place operator when each component signature is sound for the corresponding section (the other argument held constant — K&L's "DE on a constant parameter" pattern, made positional).

Equations

• σ.SoundFor f = ((∀ (y : β), σ.restrictor.SoundFor fun (x : α) => f x y) ∧ ∀ (x : α), σ.scope.SoundFor (f x))

theorem NaturalLogic.EntailmentSig.SoundFor.comp₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] [Lattice γ] [BoundedOrder γ] [Lattice δ] [BoundedOrder δ] {ψ : EntailmentSig} {g : γ → δ} {σ : Sig₂} {f : α → β → γ} (hg : ψ.SoundFor g) (hf : σ.SoundFor f) : { restrictor := ψ * σ.restrictor, scope := ψ * σ.scope }.SoundFor fun (x : α) (y : β) => g (f x y)

Composing a sound outer context into a sound two-place operator composes the profile componentwise — the two-place form of EntailmentSig.SoundFor.comp.

Bridges to the GQ machinery

def Quantification.DoubleMono.toSig₂ : DoubleMono → NaturalLogic.Sig₂

The signature profile of each [vB84] double-monotonicity class, at mono/anti granularity.

Equations

• Quantification.DoubleMono.upUp.toSig₂ = { restrictor := NaturalLogic.EntailmentSig.mono, scope := NaturalLogic.EntailmentSig.mono }
• Quantification.DoubleMono.downUp.toSig₂ = { restrictor := NaturalLogic.EntailmentSig.anti, scope := NaturalLogic.EntailmentSig.mono }
• Quantification.DoubleMono.upDown.toSig₂ = { restrictor := NaturalLogic.EntailmentSig.mono, scope := NaturalLogic.EntailmentSig.anti }
• Quantification.DoubleMono.downDown.toSig₂ = { restrictor := NaturalLogic.EntailmentSig.anti, scope := NaturalLogic.EntailmentSig.anti }

theorem NaturalLogic.sig₂_soundFor_upUp {α : Type u_1} {q : Quantification.GQ α} (hr : Quantification.RestrictorUpwardMono q) (hs : Quantification.ScopeUpwardMono q) : { restrictor := EntailmentSig.mono, scope := EntailmentSig.mono }.SoundFor q

↑MON↑ (e.g. some): both positions monotone.

theorem NaturalLogic.sig₂_soundFor_downUp {α : Type u_1} {q : Quantification.GQ α} (hr : Quantification.RestrictorDownwardMono q) (hs : Quantification.ScopeUpwardMono q) : { restrictor := EntailmentSig.anti, scope := EntailmentSig.mono }.SoundFor q

↓MON↑ (e.g. every): restrictor antitone, scope monotone.

theorem NaturalLogic.sig₂_soundFor_upDown {α : Type u_1} {q : Quantification.GQ α} (hr : Quantification.RestrictorUpwardMono q) (hs : Quantification.ScopeDownwardMono q) : { restrictor := EntailmentSig.mono, scope := EntailmentSig.anti }.SoundFor q

↑MON↓ (e.g. not all): restrictor monotone, scope antitone.

theorem NaturalLogic.sig₂_soundFor_downDown {α : Type u_1} {q : Quantification.GQ α} (hr : Quantification.RestrictorDownwardMono q) (hs : Quantification.ScopeDownwardMono q) : { restrictor := EntailmentSig.anti, scope := EntailmentSig.anti }.SoundFor q

↓MON↓ (e.g. no): both positions antitone.

theorem NaturalLogic.leftAntiAdditive_iff_isAntiAdditive {α : Type u_1} (q : Quantification.GQ α) : Quantification.LeftAntiAdditive q ↔ ∀ (S : α → Prop), Entailment.IsAntiAdditive fun (R : α → Prop) => q R S

LeftAntiAdditive ([PW06] §5.9) is sectionwise anti-additivity in the restrictor, at the Prop instance.

theorem NaturalLogic.rightAntiAdditive_iff_isAntiAdditive {α : Type u_1} (q : Quantification.GQ α) : Quantification.RightAntiAdditive q ↔ ∀ (R : α → Prop), Entailment.IsAntiAdditive (q R)

RightAntiAdditive is sectionwise anti-additivity in the scope.

Certified determiner profiles

theorem NaturalLogic.every_sem_soundFor {α : Type u_1} : { restrictor := EntailmentSig.anti, scope := EntailmentSig.mono }.SoundFor Quantification.every_sem

Every realizes ↓MON↑ as a certified profile, the restrictor side derived from left anti-additivity (every_laa).

theorem NaturalLogic.no_sem_soundFor {α : Type u_1} : { restrictor := EntailmentSig.anti, scope := EntailmentSig.anti }.SoundFor Quantification.no_sem

No realizes ↓MON↓, both positions via anti-additivity (no_laa, no_raa).

Worked composition: not every

theorem NaturalLogic.not_soundFor_antiAddMult : EntailmentSig.antiAddMult.SoundFor Not

Propositional negation realizes the anti-morphism row at the Prop instance.