Documentation

Linglib.Phenomena.ScalarImplicatures.Studies.Horn1972

Horn Scales #

@cite{horn-1972}

Connects the string-based HornScaleDatumPair records in Phenomena/ScalarImplicatures/Basic.lean to the typed Horn scale algebra in Theories/Semantics/Alternatives/HornScale.lean (Quantifiers.entails, Connectives.entails, Modals.entails, strongerAlternatives).

Structure #

For each string-level scale datum (someAllDatum, orAndDatum, possibleNecessaryDatum), we prove:

  1. Entailment agreement: the typed entails function matches the string-level stronger/weaker ordering.

  2. Alternative agreement: strongerAlternatives on the typed scale produces the expected set.

  3. Scale membership: the datum's strongerTerm is indeed stronger in the typed scale.

source
theorem Phenomena.ScalarImplicatures.Studies.Horn1972.all_entails_some :
Alternatives.Quantifiers.entails Alternatives.Quantifiers.QuantExpr.all Alternatives.Quantifiers.QuantExpr.some_ = true

"all" entails "some" in the typed algebra.

source
theorem Phenomena.ScalarImplicatures.Studies.Horn1972.most_entails_some :
Alternatives.Quantifiers.entails Alternatives.Quantifiers.QuantExpr.most Alternatives.Quantifiers.QuantExpr.some_ = true

"most" entails "some" in the typed algebra.

source
theorem Phenomena.ScalarImplicatures.Studies.Horn1972.someAll_ordering_match :
someAllDatum.strongerTerm = "all" ∧ Alternatives.Quantifiers.entails Alternatives.Quantifiers.QuantExpr.all Alternatives.Quantifiers.QuantExpr.some_ = true

someAllDatum's strongerTerm is "all", and all entails some.

source
theorem Phenomena.ScalarImplicatures.Studies.Horn1972.some_stronger_alts :
Alternatives.strongerAlternatives Alternatives.Quantifiers.quantScale Alternatives.Quantifiers.QuantExpr.some_ = [Alternatives.Quantifiers.QuantExpr.most, Alternatives.Quantifiers.QuantExpr.all]

"some" has stronger alternatives [most, all] in the typed scale.

source
theorem Phenomena.ScalarImplicatures.Studies.Horn1972.and_entails_or :
Alternatives.Connectives.entails Alternatives.Connectives.ConnExpr.and_ Alternatives.Connectives.ConnExpr.or_ = true

"and" entails "or" in the typed algebra.

source
theorem Phenomena.ScalarImplicatures.Studies.Horn1972.orAnd_ordering_match :
orAndDatum.strongerTerm = "and" ∧ Alternatives.Connectives.entails Alternatives.Connectives.ConnExpr.and_ Alternatives.Connectives.ConnExpr.or_ = true

orAndDatum's strongerTerm is "and", and and entails or.

source
theorem Phenomena.ScalarImplicatures.Studies.Horn1972.or_stronger_alts :
Alternatives.strongerAlternatives Alternatives.Connectives.connScale Alternatives.Connectives.ConnExpr.or_ = [Alternatives.Connectives.ConnExpr.and_]

"or" has stronger alternatives [and] in the typed scale.

source
theorem Phenomena.ScalarImplicatures.Studies.Horn1972.necessary_entails_possible :
Alternatives.Modals.entails Alternatives.Modals.ModalExpr.necessary Alternatives.Modals.ModalExpr.possible = true

"necessary" entails "possible" in the typed algebra.

source
theorem Phenomena.ScalarImplicatures.Studies.Horn1972.possibleNecessary_ordering_match :
possibleNecessaryDatum.strongerTerm = "necessary" ∧ Alternatives.Modals.entails Alternatives.Modals.ModalExpr.necessary Alternatives.Modals.ModalExpr.possible = true

possibleNecessaryDatum's strongerTerm is "necessary", and necessary entails possible.

source
theorem Phenomena.ScalarImplicatures.Studies.Horn1972.possible_stronger_alts :
Alternatives.strongerAlternatives Alternatives.Modals.modalScale Alternatives.Modals.ModalExpr.possible = [Alternatives.Modals.ModalExpr.necessary]

"possible" has stronger alternatives [necessary] in the typed scale.

source
theorem Phenomena.ScalarImplicatures.Studies.Horn1972.all_scales_agree :
(someAllDatum.strongerTerm = "all" ∧ Alternatives.Quantifiers.entails Alternatives.Quantifiers.QuantExpr.all Alternatives.Quantifiers.QuantExpr.some_ = true) ∧ (orAndDatum.strongerTerm = "and" ∧ Alternatives.Connectives.entails Alternatives.Connectives.ConnExpr.and_ Alternatives.Connectives.ConnExpr.or_ = true) ∧ possibleNecessaryDatum.strongerTerm = "necessary" ∧ Alternatives.Modals.entails Alternatives.Modals.ModalExpr.necessary Alternatives.Modals.ModalExpr.possible = true

All three string-level datum pairs agree with the typed algebra: each datum's strongerTerm is the stronger element in its typed scale.

source
theorem Phenomena.ScalarImplicatures.Studies.Horn1972.entailment_reflexive :
Alternatives.Quantifiers.entails Alternatives.Quantifiers.QuantExpr.some_ Alternatives.Quantifiers.QuantExpr.some_ = true ∧ Alternatives.Connectives.entails Alternatives.Connectives.ConnExpr.or_ Alternatives.Connectives.ConnExpr.or_ = true ∧ Alternatives.Modals.entails Alternatives.Modals.ModalExpr.possible Alternatives.Modals.ModalExpr.possible = true

Entailment is reflexive on all three scales.