Horn (1972): On the Semantic Properties of Logical Operators in English

This file formalizes [Hor72]'s account of scalar predicates and of the lexicalization of negated operators. A scale is a strict chain of propositions, each entailing the weaker ones (IsScale); asserting a member asserts its lower bound and conversationally implicates the negation of the stronger members, so that some implicates not all, a cardinal n asserts at least n and implicates at most n, and or implicates not and. The implicature can be asserted, contradicted or suspended, and suspension (warm, if not hot) is possible only by a stronger member (suspends_iff_lt); of the stronger members, the further up the scale the negated one lies, the safer the inference (safer_of_le), and the negation of the strongest is forced. The relation between some and not all is implicature rather than entailment: the two conjoin without redundancy and some is consistent with all.

Chapter 4 derives the missing O corner of Aristotle's square. An operator is compatible with a lower negation when Q φ and Q ¬φ can hold together (Compatible); on the quantifier scale this holds below the midpoint (some, half) and fails above it (most, all), and for monotone quantifiers the compatibility of Q excludes that of its contradictory (not_compatible_compl). The lexicalization hypotheses (4.59) and (4.62) let an outer negation ~Q lexicalize iff Q is compatible and an inner negation Q~ iff it is not, so none arises both as ~some and as all~ while ~all = some~ has no route (o_corner_unlexicalizable); the connectives pattern alike, with nor but no nand.

Implementation notes

• Quantifiers are conditions on the number of satisfiers out of a domain of size n, the operational procedure of (4.55); many and few, which depend on an expected size, are left out. Cardinals use the numeral substrate's lower-bound readings, and the connectives a four-world model of two disjuncts (ConnWorld).
• The modal and deontic scales, the polarity facts of Chapter 3 and the presupposition theory of Section 1.1 are not formalized.

References

• [Hor72]

Scalar predicates

def Horn1972.IsScale {W : Type u_1} {n : ℕ} (P : Fin (n + 1) → Set W) : Prop

A scale of propositions ordered from weakest to strongest: each strictly entails the weaker ones.

Equations

• Horn1972.IsScale P = StrictAnti P

theorem Horn1972.IsScale.subset {W : Type u_1} {n : ℕ} {P : Fin (n + 1) → Set W} (h : IsScale P) {i j : Fin (n + 1)} (hij : i ≤ j) : P j ⊆ P i

The stronger member entails the weaker.

def Horn1972.assertBound {W : Type u_1} {n : ℕ} (P : Fin (n + 1) → Set W) (i j : Fin (n + 1)) : Set W

Asserting the upper-bound implicature of P i against P j, only P i, the first of the constructions of (1.73).

Equations

• Horn1972.assertBound P i j = P i \ P j

theorem Horn1972.assertBound_subset {W : Type u_1} {n : ℕ} {P : Fin (n + 1) → Set W} (i j : Fin (n + 1)) : assertBound P i j ⊆ P i

theorem Horn1972.assertBound_disjoint {W : Type u_1} {n : ℕ} {P : Fin (n + 1) → Set W} (i j : Fin (n + 1)) : Disjoint (assertBound P i j) (P j)

theorem Horn1972.suspends_iff_lt {W : Type u_1} {n : ℕ} {P : Fin (n + 1) → Set W} (h : IsScale P) (i j : Fin (n + 1)) : P j ⊂ P i ↔ i < j

Suspension, P i, if not P j, admits a member without asserting it and is possible only by a stronger one: hot, if not warm is out.

theorem Horn1972.safer_of_le {W : Type u_1} {n : ℕ} {P : Fin (n + 1) → Set W} (h : IsScale P) (i : Fin (n + 1)) {j k : Fin (n + 1)} (hjk : j ≤ k) : assertBound P i j ⊆ assertBound P i k

(2.69iii): among the stronger members, negating one further up the scale is the safer inference, since it excludes less.

theorem Horn1972.compl_subset_compl_last {W : Type u_1} {n : ℕ} {P : Fin (n + 1) → Set W} (h : IsScale P) (j : Fin (n + 1)) : (P j)ᶜ ⊆ (P (Fin.last n))ᶜ

(2.69ii): the negation of the strongest member follows from the negation of any member, so it is the inference the listener must draw.

def Horn1972.Redundant {W : Type u_1} (p q : Set W) : Prop

The redundancy test (2.21): P and Q is redundant when P ∧ ¬Q is contradictory, which is when P entails Q.

Equations

• Horn1972.Redundant p q = (p ∩ qᶜ = ∅)

theorem Horn1972.redundant_iff_subset {W : Type u_1} (p q : Set W) : Redundant p q ↔ p ⊆ q

Cardinal numbers (Section 1.21)

theorem Horn1972.atLeast_succ_ssubset (m : ℕ) : Degree.Comparison.ge.interval (m + 1) ⊂ Degree.Comparison.ge.interval m

The cardinals form a scale: at least m + 1 strictly entails at least m.

theorem Horn1972.compl_atLeast_eq_fewerThan (m : ℕ) : (Degree.Comparison.ge.interval m)ᶜ = Degree.Comparison.lt.interval m

(1.59b): negating a cardinal contradicts its lower bound, fewer than m.

theorem Horn1972.bare_eq_atLeast_inter_atMost (m : ℕ) : Degree.Comparison.eq.interval m = Degree.Comparison.ge.interval m ∩ Degree.Comparison.le.interval m

The exact reading is the asserted lower bound together with the implicated upper bound.

theorem Horn1972.atLeast_consistent_with_more (m : ℕ) : (Degree.Comparison.ge.interval m ∩ Degree.Comparison.gt.interval m).Nonempty

(1.60a): I have three children, in fact more is consistent, so the upper bound is no entailment.

theorem Horn1972.only_inconsistent_with_fewer (m : ℕ) : Disjoint (Degree.Comparison.ge.interval m ∩ Degree.Comparison.le.interval m) (Degree.Comparison.lt.interval m)

(1.60b): I have only three children, in fact fewer is contradictory, since only asserts the upper bound.

The quantificational scale (Section 2.1)

def Horn1972.someQ (n : ℕ) : Set (Fin (n + 1))

The quantifiers as conditions on the number of satisfiers among n individuals.

Equations

• Horn1972.someQ n = {c : Fin (n + 1) | 1 ≤ ↑c}

def Horn1972.halfQ (n : ℕ) : Set (Fin (n + 1))

Equations

• Horn1972.halfQ n = {c : Fin (n + 1) | n ≤ 2 * ↑c}

def Horn1972.mostQ (n : ℕ) : Set (Fin (n + 1))

Equations

• Horn1972.mostQ n = {c : Fin (n + 1) | n < 2 * ↑c}

def Horn1972.allQ (n : ℕ) : Set (Fin (n + 1))

Equations

• Horn1972.allQ n = {c : Fin (n + 1) | ↑c = n}

def Horn1972.noneQ (n : ℕ) : Set (Fin (n + 1))

Equations

• Horn1972.noneQ n = {c : Fin (n + 1) | ↑c = 0}

def Horn1972.notAllQ (n : ℕ) : Set (Fin (n + 1))

Equations

• Horn1972.notAllQ n = {c : Fin (n + 1) | ↑c ≠ n}

theorem Horn1972.allQ_ssubset_mostQ {n : ℕ} (hn : 3 ≤ n) : allQ n ⊂ mostQ n

The positive scale (2.4a) on its proportional members: on a domain of at least three individuals all strictly entails most, which strictly entails some.

theorem Horn1972.mostQ_ssubset_someQ {n : ℕ} (hn : 2 ≤ n) : mostQ n ⊂ someQ n

theorem Horn1972.allQ_subset_someQ {n : ℕ} (hn : 1 ≤ n) : allQ n ⊆ someQ n

All entails some on a nonempty domain, the subalternation of the square.

theorem Horn1972.someQ_not_subset_notAllQ {n : ℕ} (hn : 1 ≤ n) : ¬someQ n ⊆ notAllQ n

Some does not entail not all: the count of everyone witnesses some and all.

theorem Horn1972.some_notAll_not_redundant {n : ℕ} (hn : 1 ≤ n) : ¬Redundant (someQ n) (notAllQ n)

(2.24b): some but not all is not redundant, so not all is an implicature of some rather than an entailment.

theorem Horn1972.someQ_inter_allQ_nonempty {n : ℕ} (hn : 1 ≤ n) : (someQ n ∩ allQ n).Nonempty

(2.24a): somebody left, in fact everyone did is consistent.

Aristotle's square and the compatibility with a lower negation (Chapter 4)

def Horn1972.innerNeg {n : ℕ} (Q : Set (Fin (n + 1))) : Set (Fin (n + 1))

Q applied to the complement predicate: the count of satisfiers becomes n - c.

Equations

• Horn1972.innerNeg Q = {c : Fin (n + 1) | c.rev ∈ Q}

theorem Horn1972.compl_someQ {n : ℕ} : (someQ n)ᶜ = noneQ n

The E corner: none is ~some and all~ alike.

theorem Horn1972.innerNeg_allQ {n : ℕ} : innerNeg (allQ n) = noneQ n

theorem Horn1972.compl_allQ {n : ℕ} : (allQ n)ᶜ = notAllQ n

The O corner: not all is ~all and some~ alike.

theorem Horn1972.innerNeg_someQ {n : ℕ} : innerNeg (someQ n) = notAllQ n

theorem Horn1972.allQ_disjoint_noneQ {n : ℕ} (hn : 1 ≤ n) : Disjoint (allQ n) (noneQ n)

The contraries A and E exclude each other on a nonempty domain, and the subcontraries I and O exhaust it.

theorem Horn1972.someQ_union_notAllQ {n : ℕ} (hn : 1 ≤ n) : someQ n ∪ notAllQ n = Set.univ

def Horn1972.Compatible {n : ℕ} (Q : Set (Fin (n + 1))) : Prop

(4.55): Q φ and Q ¬φ are compatible when some count puts both a predicate and its complement into Q.

Equations

• Horn1972.Compatible Q = ∃ c ∈ Q, c.rev ∈ Q

theorem Horn1972.someQ_compatible {n : ℕ} (hn : 2 ≤ n) : Compatible (someQ n)

Some lies below the midpoint: some of the eggs broke and some didn't is consistent.

theorem Horn1972.halfQ_compatible (k : ℕ) : Compatible (halfQ (2 * k))

Half sits at the midpoint and is compatible on an even domain.

theorem Horn1972.mostQ_not_compatible {n : ℕ} : ¬Compatible (mostQ n)

Most lies above the midpoint: most of the eggs broke and most didn't is contradictory.

theorem Horn1972.allQ_not_compatible {n : ℕ} (hn : 1 ≤ n) : ¬Compatible (allQ n)

def Horn1972.IsUpward {n : ℕ} (Q : Set (Fin (n + 1))) : Prop

A quantifier that is monotone in the count.

Equations

• Horn1972.IsUpward Q = ∀ (c d : Fin (n + 1)), c ≤ d → c ∈ Q → d ∈ Q

theorem Horn1972.not_compatible_compl {n : ℕ} {Q : Set (Fin (n + 1))} (hQ : IsUpward Q) (h : Compatible Q) : ¬Compatible Qᶜ

(4.58'): a monotone quantifier compatible with a lower negation has a contradictory that is not, so few and none sit above the midpoint of the negative scale.

def Horn1972.OuterNegationLexicalizes {n : ℕ} (Q : Set (Fin (n + 1))) : Prop

(4.59ii) and (4.62ii): an outer negation ~Q lexicalizes iff Q is compatible with a lower negation.

Equations

• Horn1972.OuterNegationLexicalizes Q = Horn1972.Compatible Q

def Horn1972.InnerNegationLexicalizes {n : ℕ} (Q : Set (Fin (n + 1))) : Prop

(4.59iii) and (4.62i): an inner negation Q~ lexicalizes iff Q is not compatible.

Equations

• Horn1972.InnerNegationLexicalizes Q = ¬Horn1972.Compatible Q

theorem Horn1972.e_corner_lexicalizable {n : ℕ} (hn : 2 ≤ n) : OuterNegationLexicalizes (someQ n) ∧ InnerNegationLexicalizes (allQ n)

The E corner has both routes: none as ~some and as all~.

theorem Horn1972.o_corner_unlexicalizable {n : ℕ} (hn : 2 ≤ n) : ¬OuterNegationLexicalizes (allQ n) ∧ ¬InnerNegationLexicalizes (someQ n)

The O corner has neither: ~all is blocked because all is incompatible with a lower negation and some~ because some is compatible, so no language lexicalizes nall.

The connectives (Sections 2.13 and 4.23)

inductive Horn1972.ConnWorld : Type

The worlds of two disjuncts: which of them hold.

• neither : ConnWorld
• onlyA : ConnWorld
• onlyB : ConnWorld
• both : ConnWorld

@[instance_reducible]

instance Horn1972.instDecidableEqConnWorld : DecidableEq ConnWorld

Equations

• Horn1972.instDecidableEqConnWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Horn1972.instReprConnWorld : Repr ConnWorld

Equations

• Horn1972.instReprConnWorld = { reprPrec := Horn1972.instReprConnWorld.repr }

def Horn1972.instReprConnWorld.repr : ConnWorld → ℕ → Std.Format

Equations

• Horn1972.instReprConnWorld.repr Horn1972.ConnWorld.neither prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Horn1972.ConnWorld.neither")).group prec✝
• Horn1972.instReprConnWorld.repr Horn1972.ConnWorld.onlyA prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Horn1972.ConnWorld.onlyA")).group prec✝
• Horn1972.instReprConnWorld.repr Horn1972.ConnWorld.onlyB prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Horn1972.ConnWorld.onlyB")).group prec✝
• Horn1972.instReprConnWorld.repr Horn1972.ConnWorld.both prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Horn1972.ConnWorld.both")).group prec✝

def Horn1972.orConn : ConnWorld → Prop

A or B, inclusive.

Equations

• Horn1972.orConn Horn1972.ConnWorld.neither = False
• Horn1972.orConn x✝ = True

def Horn1972.andConn : ConnWorld → Prop

A and B.

Equations

• Horn1972.andConn Horn1972.ConnWorld.both = True
• Horn1972.andConn x✝ = False

def Horn1972.ConnWorld.swap : ConnWorld → ConnWorld

Negating both disjuncts.

Equations

• Horn1972.ConnWorld.neither.swap = Horn1972.ConnWorld.both
• Horn1972.ConnWorld.onlyA.swap = Horn1972.ConnWorld.onlyB
• Horn1972.ConnWorld.onlyB.swap = Horn1972.ConnWorld.onlyA
• Horn1972.ConnWorld.both.swap = Horn1972.ConnWorld.neither

def Horn1972.CompatibleConn (C : ConnWorld → Prop) : Prop

Compatibility with a lower negation for a connective.

Equations

• Horn1972.CompatibleConn C = ∃ (w : Horn1972.ConnWorld), C w ∧ C w.swap

theorem Horn1972.orConn_compatible : CompatibleConn orConn

Or is compatible with a lower negation, like some.

theorem Horn1972.andConn_not_compatible : ¬CompatibleConn andConn

And is not, like all: so nor lexicalizes both ~or and and~, and there is no nand.

theorem Horn1972.orConn_not_subset_compl_andConn : ¬∀ (w : ConnWorld), orConn w → ¬andConn w

(2.46)–(2.48): and entails or, and or implicates rather than entails not and, the implicature being cancelled by or both.