Direct finite semiorder representation

The order used here is the one introduced by Scott and Suppes (1958): x ≼ y says that every predecessor of x is a predecessor of y, and every successor of y is a successor of x. Its antisymmetrization is the paper's quotient by substitutability.

def Scott1964.MeasurementStructures.ScottWeakOrder {A : Type u} (P : A → A → Prop) (x y : A) : Prop

The Scott--Suppes weak order associated with a strict preference.

Equations

• Scott1964.MeasurementStructures.ScottWeakOrder P x y = ((∀ (z : A), P z x → P z y) ∧ ∀ (z : A), P y z → P x z)

def Scott1964.MeasurementStructures.PreferenceSubstitute {A : Type u} (P : A → A → Prop) (x y : A) : Prop

Substitute alternatives have identical strict-preference profiles.

Equations

• Scott1964.MeasurementStructures.PreferenceSubstitute P x y = ((∀ (z : A), P z x ↔ P z y) ∧ ∀ (z : A), P x z ↔ P y z)

theorem Scott1964.MeasurementStructures.scottWeakOrder_refl {A : Type u} (P : A → A → Prop) (x : A) : ScottWeakOrder P x x

theorem Scott1964.MeasurementStructures.scottWeakOrder_trans {A : Type u} (P : A → A → Prop) : IsTrans A (ScottWeakOrder P)

theorem Scott1964.MeasurementStructures.scottWeakOrder_total {A : Type u} (P : A → A → Prop) (hA : ∀ (x y z w : A), P x y → P z w → P x w ∨ P z y) (hB : ∀ (x y z w : A), P x y → P z x → P w y ∨ P z w) (x y : A) : ScottWeakOrder P x y ∨ ScottWeakOrder P y x

theorem Scott1964.MeasurementStructures.preferenceSubstitute_iff {A : Type u} (P : A → A → Prop) {x y : A} : PreferenceSubstitute P x y ↔ ScottWeakOrder P x y ∧ ScottWeakOrder P y x

theorem Scott1964.MeasurementStructures.preference_implies_scottWeakOrder {A : Type u} (P : A → A → Prop) (hirr : ∀ (x : A), ¬P x x) (hA : ∀ (x y z w : A), P x y → P z w → P x w ∨ P z y) {x y : A} (hxy : P x y) : ScottWeakOrder P x y

theorem Scott1964.MeasurementStructures.scottWeakOrder_preference_scottWeakOrder {A : Type u} (P : A → A → Prop) {x x₁ y₁ y : A} (hxx₁ : ScottWeakOrder P x x₁) (hx₁y₁ : P x₁ y₁) (hy₁y : ScottWeakOrder P y₁ y) : P x y

theorem Scott1964.MeasurementStructures.finite_staircase_representation (A : Type u) [Finite A] [LinearOrder A] (P : A → A → Prop) (hforward : ∀ {x y : A}, P x y → y < x) (hmono : ∀ {x x' y y' : A}, x ≤ x' → y' ≤ y → P x y → P x' y') : ∃ (f : A → ℝ), (∀ (x y : A), P x y ↔ f x ≥ f y + 1) ∧ ∀ {x y : A}, x < y → f x < f y

A finite relation whose lower sections are nested along a linear order has a unit-threshold representation. This is the finite recursive core of the Scott--Suppes construction.