Documentation

Linglib.Studies.Horn1972

Horn Scales #

[Hor72]

Entailment orderings on the three classic Horn scales — ⟨some, most, all⟩, ⟨or, and⟩, ⟨possible, necessary⟩ — verified in the typed Horn scale algebra of Semantics/Alternatives/HornScale.lean (Quantifiers.entails, Connectives.entails, Modals.entails, strongerAlternatives).

source
theorem 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 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 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 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 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 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 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 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.