Homogeneity: the conditional instantiation

Conditionals as the modal instantiation of the homogeneity substrate ([Kri16] §6.4): "if P, Q" quantifies over closest P-worlds as the bare plural quantifies over atoms, conditional excluded middle is the homogeneity gap, and necessarily is the gap remover, as all is for plurals (Homogeneity.Plural). bareConditional computes the same three-valued truth value as selectionalCounterfactual in Semantics.Conditionals.Counterfactual (see selectional_as_supervaluation); the two differ only in input representation.

Main definitions

• bareConditional: "if P, Q" over closest P-worlds, as a Prop3.
• strictConditional: "if P, necessarily Q", its gap removal.

References

• M. Križ, Homogeneity, Non-Maximality, and All
• R. Stalnaker, A Defense of Conditional Excluded Middle
• K. von Fintel, The Presupposition of Subjunctive Conditionals

def Semantics.Homogeneity.bareConditional {W : Type u_1} (closestPWorlds : W → Finset W) (Q : W → Prop) [DecidablePred Q] : Trivalent.Prop3 W

The bare conditional "if P, Q": true if Q holds at all closest P-worlds, false if at none, gapped otherwise (conditional excluded middle); vacuously true when there are no closest P-worlds.

Equations

• One or more equations did not get rendered due to their size.

def Semantics.Homogeneity.strictConditional {W : Type u_1} (closestPWorlds : W → Finset W) (Q : W → Prop) [DecidablePred Q] : Trivalent.Prop3 W

The strict conditional "if P, necessarily Q": gap removal on the bare conditional, as all is gap removal on the bare plural.

Equations

• Semantics.Homogeneity.strictConditional closestPWorlds Q = (Semantics.Homogeneity.bareConditional closestPWorlds Q).metaAssert

theorem Semantics.Homogeneity.isBivalent_strictConditional {W : Type u_1} (closestPWorlds : W → Finset W) (Q : W → Prop) [DecidablePred Q] : (strictConditional closestPWorlds Q).isBivalent

Strict conditionals are bivalent.

theorem Semantics.Homogeneity.posExt_strictConditional {W : Type u_1} (closestPWorlds : W → Finset W) (Q : W → Prop) [DecidablePred Q] : (strictConditional closestPWorlds Q).posExt = (bareConditional closestPWorlds Q).posExt

The bare and strict conditionals are true in the same worlds.

theorem Semantics.Homogeneity.necessarily_prevents_nonmax {W : Type u_1} (closestPWorlds : W → Finset W) (Q : W → Prop) [DecidablePred Q] (q : QUD W) (w : W) (h : usable q (strictConditional closestPWorlds Q) w) (hne : (closestPWorlds w).Nonempty) (w' : W) : w' ∈ closestPWorlds w → Q w'

necessarily prevents non-maximal use: a usable strict conditional makes Q hold at every closest P-world.