Library hydras.Schutte.AP

Additive principal ordinals

Pierre Casteran, LaBRI, Universite de Bordeaux

In this library, we define the exponential of basis omega, also called phi0.

In fact,

ω

^α , written phi0 alpha in Coq, is defined as the alpha-th additive principal ordinal.

Main Definitions

Additive principal ordinals

Definition AP : Ensemble Ord :=
  fun alpha ⇒
    zero < alpha ∧
    (∀ beta, beta < alpha → beta + alpha = alpha ).

Exponential of basis omega

Definition _phi0 := ord AP.

Notation phi0 := _phi0.

Notation "'omega^'" := phi0 (only parsing) : schutte_scope.

Omega-towers

Fixpoint omega_tower (i : nat) : Ord :=
  match i with
    0 ⇒ 1
  | S j ⇒ phi0 (omega_tower j)
  end.

The limit ordinal epsilon0

Definition epsilon0 := omega_limit omega_tower.

Proofs, proofs, proofs ...

About additive principals

Lemma AP_one : In AP 1.

Lemma least_AP : least_member lt AP 1.

Lemma AP_omega : In AP omega.

#[global] Hint Resolve zero_lt_omega : schutte.

Lemma AP_finite_eq_one : ∀ n: nat, AP n → n = 1.

Thus, omega is the second additive principal

Lemma omega_second_AP :
  least_member lt
               (fun alpha ⇒ 1 < alpha ∧ In AP alpha)
               omega.

Lemma AP_plus_closed (alpha beta gamma : Ord):
  In AP alpha → beta < alpha → gamma < alpha →
  beta + gamma < alpha.

Lemma AP_mult_Sn_closed (alpha beta: Ord) :
  AP alpha → beta < alpha → ∀ n, mult_Sn beta n < alpha.

Lemma AP_mult_fin_r_closed (alpha beta: Ord) :
  AP alpha → beta < alpha → ∀ n, beta × n < alpha.

Theorem AP_unbounded : Unbounded AP.

Theorem AP_closed : Closed AP.
Theorem AP_o_segment : the_ordering_segment AP = ordinal.

Properties of phi0

Theorem normal_phi0 : normal phi0 AP.

Lemma phi0_ordering : ordering_function phi0 ordinal AP.

Lemma phi0_elim : ∀ P : (Ord →Ord )->Prop,
    (∀ f: Ord →Ord,
        ordering_function f ordinal AP → P f ) →
    P phi0.

Lemma AP_phi0 (alpha : Ord) : In AP (phi0 alpha).
Lemma phi0_zero : phi0 zero = 1.
Lemma phi0_mono (alpha beta : Ord) :
  alpha < beta → phi0 alpha < phi0 beta.
Lemma phi0_mono_weak (alpha beta : Ord) :
  alpha ≤ beta → phi0 alpha ≤ phi0 beta.
Lemma phi0_mono_R (alpha beta : Ord) :
  phi0 alpha < phi0 beta → alpha < beta.
Lemma phi0_mono_R_weak (alpha beta: Ord):
    phi0 alpha ≤ phi0 beta → alpha ≤ beta.
Lemma phi0_inj (alpha beta : Ord) :
  phi0 alpha = phi0 beta → alpha = beta.
Lemma phi0_positive (alpha : Ord): zero < phi0 alpha.
Lemma plus_lt_phi0 (ksi alpha: Ord):
    ksi < phi0 alpha → ksi + phi0 alpha = phi0 alpha.
Lemma phi0_alpha_phi0_beta (alpha beta: Ord) :
  alpha < beta → phi0 alpha + phi0 beta = phi0 beta.
Lemma phi0_sup : ∀ U: Ensemble Ord,
    Inhabited U →
    Countable U →
    phi0 (|_| U) = |_| (image U phi0 ).
Lemma phi0_of_limit (alpha : Ord) :
  is_limit alpha →
  phi0 alpha = |_| (image (members alpha) phi0 ).
Lemma AP_to_phi0 (alpha : Ord) :
  AP alpha → ∃ beta , alpha = phi0 beta.
Lemma AP_plus_AP (alpha beta gamma : Ord) :
  zero < beta →
  phi0 alpha + beta = phi0 gamma →
  alpha < gamma ∧ beta = phi0 gamma.
Lemma is_limit_phi0 (alpha : Ord) :
  zero < alpha → is_limit (phi0 alpha).
Lemma omega_eqn : omega = phi0 1.
Lemma le_phi0 (alpha : Ord) : alpha ≤ phi0 alpha.

Properties of epsilon0

Lemma epsilon0_fxp : phi0 epsilon0 = epsilon0.

Lemma epsilon0_AP : AP epsilon0.

Lemma omega_tower_mono (i : nat) : omega_tower i < omega_tower (S i).

Lemma lt_phi0 (alpha : Ord):
  alpha < epsilon0 → alpha < phi0 alpha.

Theorem epsilon0_lfp : least_fixpoint lt phi0 epsilon0.
Lemma phi0_lt_epsilon0 (alpha : Ord) :
  alpha < epsilon0 → phi0 alpha < epsilon0.

Lemma phi0_lt_epsilon0_R (alpha : Ord):
  phi0 alpha < epsilon0 → alpha < epsilon0.