Scott's intransitive-indifference problem

The definitions reproduce conditions (1_P)--(3_P) in §2. The elementary direction of Theorem 2.1 is recorded here; the converse is supplied by the finite linear-inequality engine.

def Scott1964.MeasurementStructures.RealizablePreference {A : Type u} (P : A → A → Prop) : Prop

A strict preference relation is represented with discrimination threshold 1.

Equations

• Scott1964.MeasurementStructures.RealizablePreference P = ∃ (f : A → ℝ), ∀ (x y : A), P x y ↔ f x ≥ f y + 1

def Scott1964.MeasurementStructures.PrefIrrefl {A : Type u} (P : A → A → Prop) : Prop

Scott 1964, condition (1_P).

Equations

• Scott1964.MeasurementStructures.PrefIrrefl P = ∀ (x : A), ¬P x x

def Scott1964.MeasurementStructures.PrefQuadA {A : Type u} (P : A → A → Prop) : Prop

Scott 1964, condition (2_P).

Equations

• Scott1964.MeasurementStructures.PrefQuadA P = ∀ (x y z w : A), P x y → P z w → P x w ∨ P z y

def Scott1964.MeasurementStructures.PrefQuadB {A : Type u} (P : A → A → Prop) : Prop

Scott 1964, condition (3_P).

Equations

• Scott1964.MeasurementStructures.PrefQuadB P = ∀ (x y z w : A), P x y → P z x → P w y ∨ P z w

def Scott1964.MeasurementStructures.RealizablePreferenceWithGap {A : Type u} (P : A → A → Prop) : Prop

Realization with a strict margin above the conventional unit threshold.

Equations

• Scott1964.MeasurementStructures.RealizablePreferenceWithGap P = ∃ (f : A → ℝ), ∃ ε > 0, ∀ (x y : A), P x y ↔ f x ≥ f y + 1 + ε

def Scott1964.MeasurementStructures.StrictlyRealizablePreference {A : Type u} (P : A → A → Prop) : Prop

Scott's stronger conclusion following Theorem 2.1: the same unit threshold may be taken strict on every preferred pair.

Equations

• Scott1964.MeasurementStructures.StrictlyRealizablePreference P = ∃ (f : A → ℝ), ∀ (x y : A), P x y ↔ f x > f y + 1

theorem Scott1964.MeasurementStructures.RealizablePreference.irrefl {A : Type u} {P : A → A → Prop} (hP : RealizablePreference P) : PrefIrrefl P

theorem Scott1964.MeasurementStructures.RealizablePreference.quadA {A : Type u} {P : A → A → Prop} (hP : RealizablePreference P) : PrefQuadA P

theorem Scott1964.MeasurementStructures.RealizablePreference.quadB {A : Type u} {P : A → A → Prop} (hP : RealizablePreference P) : PrefQuadB P

theorem Scott1964.MeasurementStructures.RealizablePreference.necessary {A : Type u} {P : A → A → Prop} (hP : RealizablePreference P) : PrefIrrefl P ∧ PrefQuadA P ∧ PrefQuadB P

theorem Scott1964.MeasurementStructures.theorem_2_1 {A : Type u} [Finite A] (P : A → A → Prop) : RealizablePreference P ↔ PrefIrrefl P ∧ PrefQuadA P ∧ PrefQuadB P

Scott 1964, Theorem 2.1 (intransitive indifference).

The nonemptiness assumption in the source is unnecessary here. The converse uses the direct finite Scott--Suppes construction: quotient by substitutability, order the quotient by the weak order ScottWeakOrder, and represent its nested lower sections by a recursively constructed sequence.

theorem Scott1964.MeasurementStructures.realizablePreference_threshold_iff {A : Type u} (P : A → A → Prop) {c : ℝ} (hc : 0 < c) : (∃ (f : A → ℝ), ∀ (x y : A), P x y ↔ f x ≥ f y + c) ↔ RealizablePreference P

Any positive discrimination threshold can be changed to 1 by a change of units, as noted immediately before §1.

theorem Scott1964.MeasurementStructures.RealizablePreference.withGap {A : Type u} {P : A → A → Prop} (hP : RealizablePreference P) : RealizablePreferenceWithGap P

Rescaling any unit-threshold realization produces an arbitrary positive margin above the unit threshold.

theorem Scott1964.MeasurementStructures.realizablePreferenceWithGap_iff {A : Type u} (P : A → A → Prop) : RealizablePreferenceWithGap P ↔ RealizablePreference P

theorem Scott1964.MeasurementStructures.RealizablePreference.strict_of_finite {A : Type u} [Finite A] [Nonempty A] {P : A → A → Prop} (hP : RealizablePreference P) : StrictlyRealizablePreference P

On a finite set the boundary can be avoided altogether, as Scott notes after Theorem 2.1: preferred pairs lie strictly beyond the same unit threshold.