Conditional operators

This file defines conditional operators on propositions, taken as sets of worlds. Most theories of the conditional derive it from a domain of antecedent-worlds: if p, q is true when q holds throughout the domain that p picks out from the evaluation point. The theories differ in the domain, which is the accessible antecedent-worlds for the strict conditional and the closest antecedent-worlds for the variably strict conditional under the Limit Assumption.

Main definitions

• ofDomain: the conditional quantifying over a domain of antecedent-worlds.
• materialImp, strictImp: the material and strict conditionals.
• variablyStrictImp: Lewis's variably strict conditional over a family of preorders.
• IsCentered: strong centering of a family of preorders.
• closestImp: the conditional of the minimal antecedent-worlds.
• orderingImp: the conditional over the best accessible antecedent-worlds under a preorder.
• might: the might counterfactual of a would conditional.

Main results

• ofDomain_eq_core: the conditional over a domain is necessity along the relation of its domain.
• closestImp_eq_variablyStrictImp: on a total ordering the two variably strict conditionals coincide wherever the Limit Assumption holds.
• mem_variablyStrictImp_compl_singleton: without closest antecedent-worlds, if p, it would not be v holds for every world v.
• isPreferential_closestImp, isRational_closestImp: the conditional at a world satisfies system P on a well-founded preorder, and rational monotonicity on a total one.

References

• D. Lewis, Counterfactuals (1973)
• D. Lewis, Adverbs of Quantification (1975)
• R. C. Stalnaker, A Theory of Conditionals (1968)
• R. C. Stalnaker, Indicative conditionals (1975)
• R. C. Stalnaker, A Defense of Conditional Excluded Middle (1981)
• A. Kratzer, The Notional Category of Modality (1981)
• 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)
• A. Kratzer, Conditionals (1986)
• C. Condoravdi, Temporal Interpretation of Modals: Modals for the Present and for the Past (2002)
• K. von Fintel, NPI Licensing, Strawson Entailment, and Context Dependency (1999)
• B. Grusdt, D. Lassiter and M. Franke, Probabilistic Modeling of Rational Communication with Conditionals (2022)
• T. Mizuno, Strategies for Anderson Conditionals: Their Implications for the Typology of O-Marking and X-Marking (2024)

Material conditional

def Conditional.materialImp {W : Type u_2} (p q : Set W) : Set W

The material conditional, true wherever the antecedent fails or the consequent holds. Classical semantics keeps this meaning and derives its apparent exceptions pragmatically ([GLF22]).

Equations

• Conditional.materialImp p q = {w : W | w ∈ p → w ∈ q}

@[simp]

theorem Conditional.mem_materialImp {W : Type u_2} {p q : Set W} {w : W} : w ∈ materialImp p q ↔ w ∈ p → w ∈ q

theorem Conditional.contraposition {W : Type u_2} {p q : Set W} : materialImp p q ⊆ materialImp qᶜ pᶜ

Contraposition is valid for the material conditional, though not for the indicative conditional of [Sta75].

Conditionals over a domain

A theory of the conditional picks out, for an evaluation point i and an antecedent p, a domain of p-worlds, and if p, q is true at i iff q holds throughout it (ofDomain): the accessible p-worlds for the strict conditional, the closest ones for [Lew73b] under the Limit Assumption (closestImp), the selected one for [Sta68] (selectionConditional), the best worlds of the modal base restricted by the antecedent for the restrictor analysis ([Lew75], [Kra86]). Principles about a single antecedent are properties of its domain: consequent monotonicity and agglomeration always hold, Conditional Excluded Middle and distribution over a disjunctive consequent when the domain has at most one world, and modus ponens when an antecedent-world lies in its own domain. Principles relating antecedents, such as antecedent strengthening or reasoning by cases, depend on how the domain varies with the antecedent.

def Conditional.ofDomain {I : Type u_1} {W : Type u_2} (D : I → Set W → Set W) (p q : Set W) : Set I

The conditional quantifying over the domain D i p, true at i when q holds at every world of D i p.

Equations

• Conditional.ofDomain D p q = {i : I | D i p ⊆ q}

@[simp]

theorem Conditional.mem_ofDomain {I : Type u_1} {W : Type u_2} {p q : Set W} {i : I} {D : I → Set W → Set W} : i ∈ ofDomain D p q ↔ D i p ⊆ q

theorem Conditional.ofDomain_eq_core {I : Type u_1} {W : Type u_2} {p q : Set W} {D : I → Set W → Set W} : ofDomain D p q = (SetRel.ofSuccessors fun (x : I) => D x p).core q

The conditional over a domain is necessity along the relation sending i to the worlds of its domain, SetRel.core of SetRel.ofSuccessors.

theorem Conditional.ofDomain_mono_right {I : Type u_1} {W : Type u_2} {p q q' : Set W} {D : I → Set W → Set W} (hq : q ⊆ q') : ofDomain D p q ⊆ ofDomain D p q'

theorem Conditional.ofDomain_inter {I : Type u_1} {W : Type u_2} {p q : Set W} {D : I → Set W → Set W} {r : Set W} : ofDomain D p (q ∩ r) = ofDomain D p q ∩ ofDomain D p r

A conditional holds of a conjunctive consequent iff it holds of both conjuncts.

theorem Conditional.ofDomain_eq_univ {I : Type u_1} {W : Type u_2} {p q : Set W} {D : I → Set W → Set W} (h : ∀ (i : I), D i p ⊆ q) : ofDomain D p q = Set.univ

theorem Conditional.ofDomain_anti_left {I : Type u_1} {W : Type u_2} {p p' q : Set W} {D : I → Set W → Set W} (hD : ∀ (i : I), D i p' ⊆ D i p) : ofDomain D p q ⊆ ofDomain D p' q

Antecedent strengthening holds when the domain of the stronger antecedent lies within the domain of the weaker.

theorem Conditional.mem_ofDomain_union {I : Type u_1} {W : Type u_2} {p p' q : Set W} {i : I} {D : I → Set W → Set W} (hD : D i (p ∪ p') ⊆ D i p ∪ D i p') (hp : i ∈ ofDomain D p q) (hp' : i ∈ ofDomain D p' q) : i ∈ ofDomain D (p ∪ p') q

A conditional holding of two antecedents holds of their disjunction when the domain of the disjunction lies within theirs.

theorem Conditional.mem_ofDomain_or {I : Type u_1} {W : Type u_2} {p q : Set W} {i : I} {D : I → Set W → Set W} {r : Set W} (h : (D i p).Subsingleton) (hq : i ∈ ofDomain D p (q ∪ r)) : i ∈ ofDomain D p q ∨ i ∈ ofDomain D p r

A conditional over a domain with at most one world distributes over a disjunctive consequent.

theorem Conditional.mem_ofDomain_or_compl {I : Type u_1} {W : Type u_2} {p q : Set W} {i : I} {D : I → Set W → Set W} (h : (D i p).Subsingleton) : i ∈ ofDomain D p q ∨ i ∈ ofDomain D p qᶜ

A conditional over a domain with at most one world satisfies Conditional Excluded Middle.

theorem Conditional.not_mem_ofDomain_and_compl {I : Type u_1} {W : Type u_2} {p q : Set W} {i : I} {D : I → Set W → Set W} {v v' : W} (hv : v ∈ D i p) (hv' : v' ∈ D i p) (hq : v ∈ q) (hq' : v' ∉ q) : i ∉ ofDomain D p q ∧ i ∉ ofDomain D p qᶜ

Two worlds of the domain that disagree on the consequent refute both if p, q and if p, not q.

theorem Conditional.forall_mem_ofDomain_or_compl_iff {I : Type u_1} {W : Type u_2} {p : Set W} {i : I} {D : I → Set W → Set W} : (∀ (r : Set W), i ∈ ofDomain D p r ∨ i ∈ ofDomain D p rᶜ) ↔ (D i p).Subsingleton

Conditional Excluded Middle for every consequent characterizes the domains with at most one world, the Alt₁ correspondence along the relation of the domain.

theorem Conditional.ofDomain_subset_materialImp {W : Type u_2} {p q : Set W} {D : W → Set W → Set W} (hD : ∀ w ∈ p, w ∈ D w p) : ofDomain D p q ⊆ materialImp p q

Modus ponens holds when every antecedent-world lies in its own domain.

theorem Conditional.materialImp_eq_ofDomain {W : Type u_2} {p q : Set W} : materialImp p q = ofDomain (fun (w : W) (p : Set W) => {w} ∩ p) p q

The material conditional quantifies over the evaluation world when it is an antecedent-world.

Strict conditional

def Conditional.strictImp {I : Type u_1} {W : Type u_2} (access : I → Set W) (p q : Set W) : Set I

The strict conditional over an accessibility map, true at i when the consequent holds at every accessible antecedent-world. The evaluation points may differ from the worlds quantified over, as for a historical modal base evaluated at world-time indices ([Con02]).

Equations

• Conditional.strictImp access p q = Conditional.ofDomain (fun (i : I) (p : Set W) => access i ∩ p) p q

@[simp]

theorem Conditional.mem_strictImp {I : Type u_1} {W : Type u_2} {access : I → Set W} {p q : Set W} {i : I} : i ∈ strictImp access p q ↔ access i ∩ p ⊆ q

theorem Conditional.mem_strictImp_forall {I : Type u_1} {W : Type u_2} {access : I → Set W} {p q : Set W} {i : I} : i ∈ strictImp access p q ↔ ∀ w ∈ access i, w ∈ p → w ∈ q

The quantifier reading of the strict conditional.

theorem Conditional.strictImp_mono_right {I : Type u_1} {W : Type u_2} {access : I → Set W} {p q q' : Set W} (hq : q ⊆ q') : strictImp access p q ⊆ strictImp access p q'

The strict conditional is monotone in its consequent.

theorem Conditional.strictImp_anti_left {I : Type u_1} {W : Type u_2} {access : I → Set W} {p p' q : Set W} (hp : p' ⊆ p) : strictImp access p q ⊆ strictImp access p' q

The strict conditional is antitone in its antecedent, the antecedent strengthening that the variably strict conditional of [Lew73b] rejects.

theorem Conditional.strictImp_union_left {I : Type u_1} {W : Type u_2} {access : I → Set W} {p p' q : Set W} : strictImp access (p ∪ p') q = strictImp access p q ∩ strictImp access p' q

The strict conditional with a disjunctive antecedent is the conjunction of the conditionals of the disjuncts, the anti-additivity of the antecedent position.

theorem Conditional.mem_strictImp_of_subset {I : Type u_1} {W : Type u_2} {access : I → Set W} {p q : Set W} {i : I} (h : access i ⊆ q) : i ∈ strictImp access p q

A strict conditional whose consequent holds throughout the accessible worlds is true for every antecedent ([Sta75], [vF99a], [Miz24]).

theorem Conditional.not_subset_of_mem_strictImp {I : Type u_1} {W : Type u_2} {access : I → Set W} {p q : Set W} {i : I} (hm : i ∈ strictImp access p q) (hq : ¬access i ⊆ q) : ¬access i ⊆ p

A true strict conditional whose consequent does not hold throughout the accessible worlds has an antecedent that excludes some accessible world ([Miz24]).

theorem Conditional.strict_implies_material {W : Type u_2} {p q : Set W} {w : W} {R : W → Set W} (h_refl : w ∈ R w) (h : w ∈ strictImp R p q) : w ∈ materialImp p q

With reflexive access, the strict conditional entails the material conditional at the evaluation world.

Variably strict conditionals

[Lew73b] §2.3 states the counterfactual over a comparative similarity system, a total preorder of the worlds for each center: if p, q is true at w iff there is no antecedent-world, or some antecedent-world v is such that the consequent holds at every antecedent-world at least as close to w as v (variablyStrictImp). Under the Limit Assumption, that closest antecedent-worlds exist whenever antecedent-worlds do, §1.4 simplifies the clause to the consequent holding at every closest antecedent-world (closestImp); the two coincide on total orderings wherever the Limit Assumption holds (closestImp_eq_variablyStrictImp), in particular for finite antecedents.

The operators take any family ord : W → Preorder W of preorders indexed by the evaluation world, the closest antecedent-worlds being the minimal ones (Preorder.minimals). Lewis reads the family as comparative similarity and requires it to be total and strongly centered (IsCentered); closestImp is also meaningful on preorders that are not total. might is §1.5's might counterfactual, the dual of a would conditional.

def Conditional.might {W : Type u_2} (op : Set W → Set W → Set W) (p q : Set W) : Set W

The might counterfactual of a would conditional op, not (if p, would not q) ([Lew73b] §1.5).

Equations

• Conditional.might op p q = (op p qᶜ)ᶜ

@[simp]

theorem Conditional.mem_might {W : Type u_2} {p q : Set W} {w : W} {op : Set W → Set W → Set W} : w ∈ might op p q ↔ w ∉ op p qᶜ

@[instance_reducible]

instance Conditional.instDecidableMemSetMightOfCompl {W : Type u_2} {p q : Set W} {w : W} {op : Set W → Set W → Set W} [Decidable (w ∈ op p qᶜ)] : Decidable (w ∈ might op p q)

Equations

• Conditional.instDecidableMemSetMightOfCompl = { decide := !decide (w ∈ op p qᶜ), reflects_decide := ⋯ }

def Conditional.IsCentered {W : Type u_2} (ord : W → Preorder W) : Prop

A family of preorders is strongly centered when every world is strictly below every other world in its own preorder, [Lew73b]'s requirement that each world be closer to itself than any other world is.

Equations

• Conditional.IsCentered ord = ∀ (w w' : W), w ≠ w' → w < w'

theorem Conditional.IsCentered.le {W : Type u_2} {ord : W → Preorder W} (hc : IsCentered ord) (w w' : W) : w ≤ w'

Under strong centering every world is at least as close to itself as any world is.

theorem Conditional.IsCentered.not_le {W : Type u_2} {ord : W → Preorder W} (hc : IsCentered ord) {w w' : W} (h : w ≠ w') : ¬w' ≤ w

Under strong centering no other world is as close to a world as the world itself.

theorem Conditional.IsCentered.minimals_eq_singleton {W : Type u_2} {p : Set W} {w : W} {ord : W → Preorder W} (hc : IsCentered ord) (hw : w ∈ p) : (ord w).minimals p = {w}

Under strong centering a world is its own unique closest world in any set containing it.

def Conditional.variablyStrictImp {W : Type u_2} (ord : W → Preorder W) (p q : Set W) : Set W

The variably strict conditional of [Lew73b] §2.3 for a universal system, one in which every world is accessible. It is vacuously true without antecedent-worlds, and otherwise true when the consequent holds at every antecedent-world at least as close as some antecedent-world, that is, when the consequent is a good possibility over the antecedent-worlds.

Equations

• Conditional.variablyStrictImp ord p q = {w : W | p = ∅ ∨ OrderingSemantics.IsGoodPossibility (ord w) p q}

@[simp]

theorem Conditional.mem_variablyStrictImp {W : Type u_2} {p q : Set W} {w : W} {ord : W → Preorder W} : w ∈ variablyStrictImp ord p q ↔ p = ∅ ∨ ∃ v ∈ p, ∀ u ∈ p, u ≤ v → u ∈ q

def Conditional.closestImp {W : Type u_2} (ord : W → Preorder W) (p q : Set W) : Set W

The conditional of the closest antecedent-worlds, true when the consequent holds at every closest antecedent-world. It is [Lew73b]'s simplification of the variably strict conditional under the Limit Assumption (§1.4).

Equations

• Conditional.closestImp ord p q = Conditional.ofDomain (fun (w : W) => (ord w).minimals) p q

@[simp]

theorem Conditional.mem_closestImp {W : Type u_2} {p q : Set W} {w : W} {ord : W → Preorder W} : w ∈ closestImp ord p q ↔ (ord w).minimals p ⊆ q

theorem Conditional.mem_closestImp_iff_forall_filter {W : Type u_2} {p q : Set W} {w : W} {ord : W → Preorder W} [Fintype W] [DecidablePred fun (x : W) => x ∈ p] : w ∈ closestImp ord p q ↔ ∀ v ∈ {x : W | x ∈ p}, (∀ u ∈ {x : W | x ∈ p}, u ≤ v → v ≤ u) → v ∈ q

Membership in closestImp over a finite type, decided by filtering the antecedent-worlds once rather than quantifying over every world.

@[instance_reducible]

instance Conditional.instDecidableMemSetClosestImpOfFintypeOfDecidableRelLeOfDecidablePred {W : Type u_2} {p q : Set W} {w : W} {ord : W → Preorder W} [Fintype W] [DecidableRel LE.le] [DecidablePred fun (x : W) => x ∈ p] [DecidablePred fun (x : W) => x ∈ q] : Decidable (w ∈ closestImp ord p q)

Equations

• Conditional.instDecidableMemSetClosestImpOfFintypeOfDecidableRelLeOfDecidablePred = decidable_of_iff (∀ v ∈ {x : W | x ∈ p}, (∀ u ∈ {x : W | x ∈ p}, u ≤ v → v ≤ u) → v ∈ q) ⋯

theorem Conditional.variablyStrictImp_subset_closestImp {W : Type u_2} {p q : Set W} {ord : W → Preorder W} (htot : ∀ (w : W), Std.Total LE.le) : variablyStrictImp ord p q ⊆ closestImp ord p q

On a total ordering the variably strict conditional entails the conditional of the closest antecedent-worlds.

theorem Conditional.closestImp_eq_variablyStrictImp {W : Type u_2} {p q : Set W} {ord : W → Preorder W} (htot : ∀ (w : W), Std.Total LE.le) (hlim : ∀ (w : W), p.Nonempty → ((ord w).minimals p).Nonempty) : closestImp ord p q = variablyStrictImp ord p q

On a total ordering satisfying the Limit Assumption for p, the two conditionals coincide ([Lew73b] §1.4).

theorem Conditional.closestImp_eq_variablyStrictImp_of_finite {W : Type u_2} {p q : Set W} {ord : W → Preorder W} (htot : ∀ (w : W), Std.Total LE.le) (hp : p.Finite) : closestImp ord p q = variablyStrictImp ord p q

On a total ordering the two conditionals coincide for a finite antecedent, which satisfies the Limit Assumption.

theorem Conditional.mem_closestImp_of_closest_eq_empty {W : Type u_2} {p q : Set W} {w : W} {ord : W → Preorder W} (h : (ord w).minimals p = ∅) : w ∈ closestImp ord p q

Without closest antecedent-worlds the conditional of the closest worlds is vacuously true.

theorem Conditional.mem_variablyStrictImp_compl_singleton {W : Type u_2} {p : Set W} {w : W} {ord : W → Preorder W} (h : (ord w).minimals p = ∅) (v : W) : w ∈ variablyStrictImp ord p {v}ᶜ

Where an antecedent has no closest worlds, as for [Lew73b]'s line more than an inch long, if p, it would not be v is true for every world v, since every antecedent-world has a strictly closer one.

theorem Conditional.notMem_might_variablyStrictImp_singleton {W : Type u_2} {p : Set W} {w : W} {ord : W → Preorder W} (h : (ord w).minimals p = ∅) (v : W) : w ∉ might (variablyStrictImp ord) p {v}

So no world is one that p might have been, [Sta81]'s objection to [Lew73b] without the Limit Assumption.

theorem Conditional.closestImp_subset_materialImp {W : Type u_2} {p q : Set W} {ord : W → Preorder W} (hc : IsCentered ord) : closestImp ord p q ⊆ materialImp p q

Under strong centering the conditional of the closest worlds entails the material conditional.

theorem Conditional.variablyStrictImp_subset_materialImp {W : Type u_2} {p q : Set W} {ord : W → Preorder W} (hc : IsCentered ord) : variablyStrictImp ord p q ⊆ materialImp p q

theorem Conditional.closestImp_eq_univ_of_subset {W : Type u_2} {p q : Set W} {ord : W → Preorder W} (h : p ⊆ q) : closestImp ord p q = Set.univ

theorem Conditional.mem_closestImp_union {W : Type u_2} {p q : Set W} {w : W} {ord : W → Preorder W} {r : Set W} (hp : w ∈ closestImp ord p r) (hq : w ∈ closestImp ord q r) : w ∈ closestImp ord (p ∪ q) r

A conditional holding of each of two antecedents holds of their disjunction.

theorem Conditional.mem_closestImp_or_of_mem_union {W : Type u_2} {p q : Set W} {w : W} {ord : W → Preorder W} {r : Set W} (htot : ∀ (w : W), Std.Total LE.le) (h : w ∈ closestImp ord (p ∪ q) r) : w ∈ closestImp ord p r ∨ w ∈ closestImp ord q r

On a total ordering, a conditional with a disjunctive antecedent entails the conditional of one of the disjuncts.

theorem Conditional.mem_might_closestImp_iff_of_closest_eq_singleton {W : Type u_2} {p q : Set W} {w : W} {ord : W → Preorder W} {v : W} (h : (ord w).minimals p = {v}) : w ∈ might (closestImp ord) p q ↔ w ∈ closestImp ord p q

With a unique closest antecedent-world, Lewis's might coincides with would.

theorem Conditional.mem_might_closestImp_iff_of_cem {W : Type u_2} {p q : Set W} {w : W} {ord : W → Preorder W} (h_nonempty : ((ord w).minimals p).Nonempty) (h_cem : w ∈ closestImp ord p q ∨ w ∈ closestImp ord p qᶜ) : w ∈ might (closestImp ord) p q ↔ w ∈ closestImp ord p q

When the antecedent has closest worlds and Conditional Excluded Middle holds, Lewis's might coincides with would, [Lew73b]'s objection to a semantics validating it as [Sta81] reports it.

Conditionals over an accessibility relation and an ordering

A modal base and an ordering source ([Kra81b]) give each evaluation point a set of accessible worlds and a preorder ranking them, and on the restrictor analysis ([Lew75], [Kra86]) if p, q is true when q holds at the best accessible p-worlds (orderingImp). The strict conditional is the case of the preorder relating every two worlds, under which every accessible antecedent-world is best (strictImp_eq_orderingImp), and the conditional of the closest worlds the case in which every world is accessible (closestImp_eq_orderingImp).

def Conditional.orderingImp {I : Type u_1} {W : Type u_2} (access : I → Set W) (ord : I → Preorder W) (p q : Set W) : Set I

The conditional over the best accessible antecedent-worlds, the minimal worlds of access i ∩ p under the preorder ord i.

Equations

• Conditional.orderingImp access ord p q = Conditional.ofDomain (fun (i : I) (p : Set W) => (ord i).minimals (access i ∩ p)) p q

@[simp]

theorem Conditional.mem_orderingImp {I : Type u_1} {W : Type u_2} {access : I → Set W} {p q : Set W} {i : I} {ord : I → Preorder W} : i ∈ orderingImp access ord p q ↔ (ord i).minimals (access i ∩ p) ⊆ q

theorem Conditional.strictImp_eq_orderingImp {I : Type u_1} {W : Type u_2} {access : I → Set W} {p q : Set W} : strictImp access p q = orderingImp access (fun (x : I) => ⊤) p q

The strict conditional is the conditional over the preorder relating every two worlds.

theorem Conditional.closestImp_eq_orderingImp {W : Type u_2} {p q : Set W} {ord : W → Preorder W} : closestImp ord p q = orderingImp (fun (x : W) => Set.univ) ord p q

The conditional of the closest worlds is the conditional in which every world is accessible.

The logic of the conditional at a world

At a world w the conditional of the closest worlds is the consequence relation that the preorder ord w defines on propositions (Nonmonotonic.Entails), true when the most normal antecedent-worlds are consequent-worlds (mem_closestImp_iff_entails). When that preorder is well-founded, which gives the Limit Assumption, the conditional therefore satisfies the rules of system P ([KLM90]), and when it is also total, as [Lew73b] requires, rational monotonicity ([LM92]). On a preorder that is not total, such as an ordering source can induce, rational monotonicity can fail (exists_not_isRational_closestImp).

theorem Conditional.mem_closestImp_iff_entails {W : Type u_2} {p q : Set W} {w : W} {ord : W → Preorder W} : w ∈ closestImp ord p q ↔ Nonmonotonic.Entails (ord w) p q

theorem Conditional.isPreferential_closestImp {W : Type u_2} {w : W} {ord : W → Preorder W} (hwf : WellFounded LT.lt) : Nonmonotonic.IsPreferential fun (p q : Set W) => w ∈ closestImp ord p q

On a well-founded preorder the conditional at a world is preferential.

theorem Conditional.isRational_closestImp {W : Type u_2} {w : W} {ord : W → Preorder W} (hwf : WellFounded LT.lt) (htot : Std.Total LE.le) : Nonmonotonic.IsRational fun (p q : Set W) => w ∈ closestImp ord p q

On a well-founded total preorder the conditional at a world is rational.

theorem Conditional.exists_not_isRational_closestImp : ∃ (ord : Fin 3 → Preorder (Fin 3)), ¬Nonmonotonic.IsRational fun (p q : Set (Fin 3)) => 0 ∈ closestImp ord p q

On a preorder that is not total the conditional need not satisfy rational monotonicity.