Preferential and rational consequence relations

This file defines preferential and rational consequence relations between sets of worlds. It proves that the consequence relation of a well-founded preorder on worlds is preferential, and that it is rational when the preorder is also total.

A nonmonotonic consequence relation φ |~ ψ reads "if φ, normally ψ". Kraus, Lehmann and Magidor call such a relation preferential when it satisfies reflexivity, left logical equivalence, right weakening, cut, cautious monotonicity and Or. IsPreferential takes And in place of cut: And is derivable in their system, and cut from the fields of IsPreferential (IsPreferential.cut). They show that the preferential relations are exactly those defined by a preferential model, a set of states labelled by worlds and ordered by a strict partial order that satisfies a smoothness condition, where φ |~ ψ holds when the minimal φ-states satisfy ψ. Lehmann and Magidor call a preferential relation rational when it also satisfies rational monotonicity, and show that the rational relations are exactly those defined by a ranked model, whose order is pulled back from a total order along a ranking of the states. The theorems of this file are the soundness halves of the two representation theorems, for models whose states are the worlds themselves.

Main declarations

• Nonmonotonic.IsPreferential: the rules of system P for a relation between propositions.
• Nonmonotonic.IsRational: system P together with rational monotonicity.
• Nonmonotonic.Entails: the consequence relation of a preorder on worlds, under which the most normal φ-worlds are all ψ-worlds.
• Nonmonotonic.isPreferential_entails, Nonmonotonic.isRational_entails: soundness for well-founded preorders and for well-founded total preorders.
• Nonmonotonic.IsPreferential.cut: the cut rule of the cumulative systems is derivable.
• Nonmonotonic.exists_not_isRational_entails: a three-world preorder with an incomparable world whose consequence relation violates rational monotonicity.

Implementation notes

• Propositions are sets of worlds, so left logical equivalence holds by extensionality and is not a field.
• The smoothness condition asks each definable set of states to have a minimal state below each of its members. Here every set of worlds is a proposition, and well-foundedness of the strict order gives the condition for all of them (Preorder.exists_le_mem_minimals). It holds on every finite set of worlds.
• A preorder is a term rather than an instance, as for Preorder.minimals, because ordering sources, ranking functions and epistemic states each determine their own order on the same worlds.

References

• S. Kraus, D. Lehmann and M. Magidor, Nonmonotonic Reasoning, Preferential Models and Cumulative Logics (1990)
• D. Lehmann and M. Magidor, What Does a Conditional Knowledge Base Entail? (1992)
• C. Strasser and G. A. Antonelli, Non-monotonic Logic (2024)

structure Nonmonotonic.IsPreferential {W : Type u_1} (r : Set W → Set W → Prop) : Prop

A consequence relation between propositions is preferential when it satisfies the rules of system P.

• refl (φ : Set W) : r φ φ

  Every proposition is a consequence of itself (reflexivity).

• rightWeakening {φ ψ χ : Set W} : r φ ψ → ψ ⊆ χ → r φ χ

  A consequence may be weakened (right weakening).

• and {φ ψ χ : Set W} : r φ ψ → r φ χ → r φ (ψ ∩ χ)

  Two consequences of one premise conjoin (And).

• or {φ ψ χ : Set W} : r φ χ → r ψ χ → r (φ ∪ ψ) χ

  A common consequence of two premises follows from their disjunction (Or).

• cautiousMonotonicity {φ ψ χ : Set W} : r φ ψ → r φ χ → r (φ ∩ ψ) χ

  A premise may be strengthened by one of its consequences (cautious monotonicity).

structure Nonmonotonic.IsRational {W : Type u_1} (r : Set W → Set W → Prop) extends Nonmonotonic.IsPreferential r : Prop

A preferential relation is rational when it also satisfies rational monotonicity.

• refl (φ : Set W) : r φ φ
• rightWeakening {φ ψ χ : Set W} : r φ ψ → ψ ⊆ χ → r φ χ
• and {φ ψ χ : Set W} : r φ ψ → r φ χ → r φ (ψ ∩ χ)
• or {φ ψ χ : Set W} : r φ χ → r ψ χ → r (φ ∪ ψ) χ
• cautiousMonotonicity {φ ψ χ : Set W} : r φ ψ → r φ χ → r (φ ∩ ψ) χ
• rationalMonotonicity {φ ψ χ : Set W} : r φ χ → ¬r φ ψᶜ → r (φ ∩ ψ) χ

  A premise may be strengthened by any proposition whose negation is not among its consequences (rational monotonicity).

theorem Nonmonotonic.IsPreferential.of_subset {W : Type u_1} {r : Set W → Set W → Prop} {φ ψ : Set W} (h : IsPreferential r) (hφψ : φ ⊆ ψ) : r φ ψ

A preferential relation extends entailment (supraclassicality).

theorem Nonmonotonic.IsPreferential.compl_union {W : Type u_1} {r : Set W → Set W → Prop} {φ ψ χ : Set W} (h : IsPreferential r) (hχ : r (φ ∩ ψ) χ) : r φ (ψᶜ ∪ χ)

A conjunct of the premise may be moved into the consequence as the antecedent of a material conditional.

theorem Nonmonotonic.IsPreferential.cut {W : Type u_1} {r : Set W → Set W → Prop} {φ ψ χ : Set W} (h : IsPreferential r) (hψ : r φ ψ) (hχ : r (φ ∩ ψ) χ) : r φ χ

A consequence used as an extra premise may be discharged (cut).

def Nonmonotonic.Entails {W : Type u_1} (p : Preorder W) (φ ψ : Set W) : Prop

Entails p φ ψ holds when the most normal φ-worlds are ψ-worlds, where w ≤ v in p reads "w is at least as normal as v".

Equations

• Nonmonotonic.Entails p φ ψ = (p.minimals φ ⊆ ψ)

theorem Nonmonotonic.isPreferential_entails {W : Type u_1} {p : Preorder W} (hp : WellFounded LT.lt) : IsPreferential (Entails p)

The consequence relation of a well-founded preorder is preferential. Well-foundedness is needed for cautious monotonicity alone.

theorem Nonmonotonic.isPreferential_entails_of_finite {W : Type u_1} [Finite W] (p : Preorder W) : IsPreferential (Entails p)

On finitely many worlds every preorder defines a preferential relation.

theorem Nonmonotonic.isRational_entails {W : Type u_1} {p : Preorder W} (hp : WellFounded LT.lt) (hc : Std.Total LE.le) : IsRational (Entails p)

The consequence relation of a well-founded total preorder is rational. A minimal φ-world in ψ is as normal as every minimal φ ∩ ψ-world, so these are minimal for φ.

theorem Nonmonotonic.exists_not_isRational_entails : ∃ (p : Preorder (Fin 3)), ¬IsRational (Entails p)

Totality cannot be dropped. Let 0 be more normal than 2 and 1 comparable to neither. Then normally 0 or 1 holds and it is not normal that 0 holds, yet given 1 or 2 it is not normal that 0 or 1 holds, since 2 is then minimal.