Homogeneity

A homogeneous predication, in Križ's sense, is trivalent: true when the predicate holds throughout its specification points, false when it fails throughout, and undefined in between, at the worlds of its extension gap Trivalent.gapExt. Instantiations differ in the specification points: the parts of a plurality (Homogeneity.readings), closest antecedent worlds (Conditional.selectionalCounterfactual), overlapping pluralities (Kriz2016.generalisedTruthValue), best modal worlds (Studies/AghaJeretic2022). Homogeneity removers such as all, necessarily and completely denote the Beaver–Krahmer assertion operator applied pointwise, fun w ↦ ofProp (p w = 1), which collapses the gap into the negative extension (Trivalent.isBivalent_ofProp_eq_one). A family of propositions is Homogeneous at a world when its members are all true there or all false there, which is where the supervaluation over them is defined; presuppositional exhaustification presupposes this of its includable alternatives.

Main declarations

• Homogeneous: the members of a family of propositions agree at a world.
• homogeneous_coe_iff: on a finite family, agreement is definedness of the supervaluation.

References

• [Kri16]
• [Kri15b]
• [DPBS24]

def Homogeneity.Homogeneous {W : Type u_1} (S : Set (Set W)) (w : W) : Prop

The propositions of S are homogeneous at w when they are all true there or all false there.

Equations

• Homogeneity.Homogeneous S w = ((∀ α ∈ S, w ∈ α) ∨ ∀ α ∈ S, w ∉ α)

@[simp]

theorem Homogeneity.homogeneous_empty {W : Type u_1} {w : W} : Homogeneous ∅ w

@[simp]

theorem Homogeneity.homogeneous_pair {W : Type u_1} {w : W} {p q : Set W} : Homogeneous {p, q} w ↔ (w ∈ p ↔ w ∈ q)

theorem Homogeneity.homogeneous_coe_iff {W : Type u_1} {w : W} (s : Finset (Set W)) [DecidablePred fun (α : Set W) => w ∈ α] : Homogeneous (↑s) w ↔ (SignType.supervaluation s fun (x : Set W) => w ∈ x) ≠ 0

On a finite family, homogeneity at w is definedness at w of the supervaluation of truth over the family.

theorem Homogeneity.Homogeneous.mem_iff {W : Type u_1} {S : Set (Set W)} {φ : Set W} {w : W} (h : Homogeneous S w) (hl : ⋂₀ S ⊆ φ) (hu : φ ⊆ ⋃₀ S) : w ∈ φ ↔ ∀ α ∈ S, w ∈ α

Under homogeneity, a proposition between the meet and the join of S is true where every member of S is.

theorem Homogeneity.Homogeneous.notMem_iff {W : Type u_1} {S : Set (Set W)} {φ : Set W} {w : W} (h : Homogeneous S w) (hl : ⋂₀ S ⊆ φ) (hu : φ ⊆ ⋃₀ S) : w ∉ φ ↔ ∀ α ∈ S, w ∉ α

Under homogeneity, a proposition between the meet and the join of S is false where every member of S is.