OrdinalChoice.lean`

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Antichain

theorem OAI.PartitionConsistency.ForcingQuotient.maximal_antichain line 16
Source documentation
Every set of forcing conditions has a maximal incompatible subfamily. The conclusion is predensity in that set; no cardinal chain condition is used.
```
theorem maximal_antichain (D : Set P) :
    ∃ A : Set P, A ⊆ D ∧
      (∀ p ∈ A, ∀ q ∈ A, ∀ r, r ≤ p → r ≤ q → p = q) ∧
      ∀ d ∈ D, ∃ a ∈ A, ∃ r, r ≤ d ∧ r ≤ a := by
…
```
theorem OAI.PartitionConsistency.ProductForcing.localized_maximum line 64
Source documentation
The local maximum principle furnished by root probes. Unlike the ordinary maximum principle, the conclusion has a specified literal supporting diagram, chosen before the witness. The name is a mixture over a Cohen antichain.
```
theorem localized_maximum [Infinite M] [Infinite I] [Uncountable K]
    (hcard : Cardinal.mk M = μ) (hsize : Cardinal.mk M < Cardinal.mk I)
    (hmerger : HasFiniteMergers M) (e : M)
    (he : Cardinal.mk ((Set.range (fun x : M => e * x))ᶜ : Set M) = Cardinal.mk M)
    (hprobes : RootProbes e K)
    {n} (φ : Formula (n+1)) (v : Fin n → (system (M := M) (I := I) (κ := κ) hμ).Name)
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.RootProbes, OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.ProductForcing.system
def OAI.PartitionConsistency.SetLanguage.familyMember line 154
Source documentation
Auxiliary formula for a value selected from the set F(i). Its variables are the family graph, the index, and the selected value.
```
def familyMember : Formula 3 :=
…
```
Mentions: OAI.PartitionConsistency.Formula
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_nonemptyFamily line 165
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_choiceForFamily line 180
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_familyMember line 208
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.nonemptyFamily_member line 219
Source documentation
A member of the domain of a forced nonempty family has a possible choice value. Both the family's set value and the member are internal names.
```
theorem nonemptyFamily_member {n} (v : Fin n → S.Name) (p : P) (F d : Fin n)
    (hf : S.Forces v p (SetLanguage.nonemptyFamily F d)) (x : S.Name)
    (hx : S.atomic.MemF p x (v d)) :
    S.Forces ![v F,x] p SetLanguage.familyMember.ex := by
…
```
Mentions: OAI.PartitionConsistency.SetLanguage.nonemptyFamily
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.familyMember_mem line 237
Source documentation
Once the family's value at an index is specified, a selected member belongs to that value. This uses single-valuedness of the actual graph.
```
theorem familyMember_mem {n} (v : Fin n → S.Name) (p : P) (F d : Fin n)
    (hfun : S.Forces v p (SetLanguage.functionOn F d)) (x y z : S.Name)
    (hx : S.atomic.MemF p x (v d)) (ha : S.App p (v F) x y)
    (hz : S.Forces ![v F,x,z] p SetLanguage.familyMember) : S.atomic.MemF p z y := by
…
```
Mentions: OAI.PartitionConsistency.SetLanguage.functionOn, OAI.PartitionConsistency.SetLanguage.familyMember
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_ACwo_of_dense line 251
Source documentation
The ordinary first-order ACwo sentence follows from dense internal choice graphs. This is only a logical unpacking, with the ordinal and all family hypotheses unchanged.
```
theorem forces_ACwo_of_dense
    (h : ∀ (p : P) (η F : S.Name),
      S.Forces ![η] p (SetLanguage.ordinal 0) →
      S.Forces ![F,η] p (SetLanguage.nonemptyFamily 0 1) →
      ∃ q, q ≤ p ∧ ∃ c : S.Name,
        S.Forces ![c,η,F] q (SetLanguage.choiceForFamily 0 1 2)) (p : P) :
    S.Forces Fin.elim0 p SetLanguage.ACwo := by
…
```
Mentions: OAI.PartitionConsistency.SetLanguage.ordinal, OAI.PartitionConsistency.SetLanguage.nonemptyFamily, OAI.PartitionConsistency.SetLanguage.choiceForFamily, OAI.PartitionConsistency.SetLanguage.ACwo
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.indexedGraph_choiceForFamily line 301
Source documentation
Uniformly supported local choices yield an actual internal set function, not an external function substituted for the conclusion of ACwo.
```
theorem indexedGraph_choiceForFamily (X : ZFSet.{u}) (F : S.Name)
    (f : X → S.Name) (H : Subgroup Γ) (hH : H ∈ S.filter)
    (hfix : ∀ g ∈ H, ∀ i, g • f i = f i) (p : P)
    (hfun : S.Forces ![F,Name.check X] p (SetLanguage.functionOn 0 1))
    (hf : ∀ i : X, S.Forces ![F,Name.check i.val,f i] p SetLanguage.familyMember) :
    S.Forces ![S.indexedGraph X f H hH hfix,Name.check X,F] p
      (SetLanguage.choiceForFamily 0 1 2) := by
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.check, OAI.PartitionConsistency.SetLanguage.functionOn, OAI.PartitionConsistency.SetLanguage.familyMember, OAI.PartitionConsistency.SetLanguage.choiceForFamily
theorem OAI.PartitionConsistency.ProductForcing.ground_family_choice line 340
Source documentation
One previously chosen extension of the supporting diagram supports all choices from a ground-indexed family, at arbitrary name ranks. The result is an internal graph; the uniform maximum principle only constructs its name.
```
theorem ground_family_choice [Infinite M] [Infinite I] [Uncountable K]
    (hcard : Cardinal.mk M = μ) (hsize : Cardinal.mk M < Cardinal.mk I)
    (hmerger : HasFiniteMergers M) (e : M)
    (he : Cardinal.mk ((Set.range (fun x : M => e * x))ᶜ : Set M) = Cardinal.mk M)
    (hprobes : RootProbes e K) (X : ZFSet.{u})
    (F : (system (M := M) (I := I) (κ := κ) hμ).Name)
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.RootProbes, OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.ground_family_choice_dense line 385
Source documentation
An arbitrary starting condition for a ground-indexed nonempty family can be strengthened to force a choice graph. The family's support and the Cohen condition are both put in the root before using probes.
```
theorem ground_family_choice_dense [Infinite M] [Infinite I] [Uncountable K]
    (hcard : Cardinal.mk M = μ) (hsize : Cardinal.mk M < Cardinal.mk I)
    (hmerger : HasFiniteMergers M) (e : M)
    (he : Cardinal.mk ((Set.range (fun x : M => e * x))ᶜ : Set M) = Cardinal.mk M)
    (hprobes : RootProbes e K) (X : ZFSet.{u})
    (F : (system (M := M) (I := I) (κ := κ) hμ).Name) (t : Poset M I κ)
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.RootProbes, OAI.PartitionConsistency.ProductForcing.system, OAI.PartitionConsistency.ProductForcing.Poset
theorem OAI.PartitionConsistency.ProductForcing.forces_ACwo line 418
Source documentation
Choice for every internal ordinal-indexed family, without a rank cutoff. Ordinal preservation first decides the index set to a ground ordinal, after which one uniformly supported internal choice graph is constructed.
```
theorem forces_ACwo [Infinite M] [Infinite I] [Uncountable K]
    (hcard : Cardinal.mk M = μ) (hsize : Cardinal.mk M < Cardinal.mk I)
    (hmerger : HasFiniteMergers M) (e : M)
    (he : Cardinal.mk ((Set.range (fun x : M => e * x))ᶜ : Set M) = Cardinal.mk M)
    (hprobes : RootProbes e K) (p : Poset M I κ) :
    (system (M := M) (I := I) (κ := κ) hμ).Forces Fin.elim0 p SetLanguage.ACwo := by
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.RootProbes, OAI.PartitionConsistency.ProductForcing.Poset, OAI.PartitionConsistency.ProductForcing.system, OAI.PartitionConsistency.SetLanguage.ACwo
instance OAI.PartitionConsistency.ConcreteSystem.(instance at line 455) line 455
theorem OAI.PartitionConsistency.ConcreteSystem.rootProbes line 460
Source documentation
The probes used by ordinal choice are actually present in the saturated monoid. This is an instance of the executed requests with a=1.
```
theorem rootProbes : ProductForcing.RootProbes T.e K := by
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.RootProbes, OAI.PartitionConsistency.ConcreteSystem.K
theorem OAI.PartitionConsistency.ConcreteSystem.forces_ACwo line 472
Source documentation
No additional cardinal or support principle is assumed here.
```
theorem forces_ACwo (p : P) : S.Forces Fin.elim0 p SetLanguage.ACwo :=
…
```
Mentions: OAI.PartitionConsistency.ConcreteSystem.P, OAI.PartitionConsistency.SetLanguage.ACwo
theorem OAI.PartitionConsistency.ConcreteSystem.consistent_ZF_ACwo_not_AC line 478
Source documentation
Consistency of the ZF + ACwo + ¬AC subtheory. The full target with PP is proved below in consistent_target.
```
theorem consistent_ZF_ACwo_not_AC :
    Consistent (SetLanguage.ZF ∪ {SetLanguage.ACwo,SetLanguage.AC.neg}) := by
…
```
Mentions: OAI.PartitionConsistency.Consistent, OAI.PartitionConsistency.SetLanguage.ZF, OAI.PartitionConsistency.SetLanguage.ACwo