ForcingQuotient.lean`

39 declarations, 0 contain sorry, 0 declared as axioms

External generic filters and the name-quotient truth lemma. These results do not supply the internal symmetric system or its ZF axioms. They work on a set of name codes with specified atomic forcing relations.

def OAI.PartitionConsistency.ForcingQuotient.Dense line 14
Source documentation
Stronger conditions are smaller.
```
def Dense {P : Type*} [Preorder P] (D : Set P) : Prop :=
…
```
abbrev OAI.PartitionConsistency.ForcingQuotient.GenericFilter line 18
Source documentation
A forcing filter is an order ideal for the opposite order.
```
abbrev GenericFilter (P : Type*) [Preorder P] := Order.Ideal (OrderDual P)
```
theorem OAI.PartitionConsistency.ForcingQuotient.exists_generic_through line 22
Source documentation
Countably many dense sets can be met through any given condition. This is Mathlib's Rasiowa–Sikorski lemma with the forcing order convention.
```
theorem exists_generic_through {P I : Type*} [Preorder P] [Countable I]
    (D : I → Set P) (dense : ∀ i, Dense (D i)) (p : P) :
    ∃ G : GenericFilter P, p ∈ G ∧ ∀ i, ∃ q, q ∈ G ∧ q ∈ D i := by
…
```
Mentions: OAI.PartitionConsistency.ForcingQuotient.Dense, OAI.PartitionConsistency.ForcingQuotient.GenericFilter
def OAI.PartitionConsistency.ForcingQuotient.Compatible line 38
Source documentation
Conditions have a common strengthening.
```
def Compatible (p q : P) : Prop := ∃ r, r ≤ p ∧ r ≤ q
```
theorem OAI.PartitionConsistency.ForcingQuotient.dense_local_or_incompatible line 43
Source documentation
A below-p dense set, padded by conditions incompatible with p, is dense in the whole poset. This is how existential local witnesses are obtained from an external generic filter.
```
theorem dense_local_or_incompatible (p : P) (D : Set P)
    (hD : ∀ q, q ≤ p → ∃ r, r ≤ q ∧ r ∈ D) :
    Dense {q | q ∈ D ∨ ¬ Compatible q p} := by
…
```
Mentions: OAI.PartitionConsistency.ForcingQuotient.Dense, OAI.PartitionConsistency.ForcingQuotient.Compatible
theorem OAI.PartitionConsistency.ForcingQuotient.compatible_of_mem line 53
structure OAI.PartitionConsistency.ForcingQuotient.AtomicData line 61
Source documentation
Atomic forcing laws on a set of name codes. These are only the equality, substitution and monotonicity laws; this structure contains no ZF axioms, Choice or Partition Principle assertions.
```
structure AtomicData (P N : Type*) [Preorder P] where
…
```
def OAI.PartitionConsistency.ForcingQuotient.AtomicData.EqG line 76
Source documentation
Equality of codes after adjoining the generic filter.
```
def EqG (a b : N) : Prop := ∃ p, p ∈ G ∧ A.EqF p a b
```
def OAI.PartitionConsistency.ForcingQuotient.AtomicData.MemG line 79
Source documentation
Membership before descent to equivalence classes.
```
def MemG (a b : N) : Prop := ∃ p, p ∈ G ∧ A.MemF p a b
```
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.eqG_refl line 81
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.eqG_symm line 85
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.eqG_trans line 89
def OAI.PartitionConsistency.ForcingQuotient.AtomicData.nameSetoid line 97
Source documentation
The setoid of internal name codes; no recursion on membership is used.
```
def nameSetoid : Setoid N where
…
```
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.memG_transport line 101
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.memG_congr line 112
abbrev OAI.PartitionConsistency.ForcingQuotient.AtomicData.Extension line 118
Source documentation
The domain of the extension is a quotient of a set of internal name codes.
```
abbrev Extension := Quotient (A.nameSetoid G)
```
def OAI.PartitionConsistency.ForcingQuotient.AtomicData.nameClass line 120
def OAI.PartitionConsistency.ForcingQuotient.AtomicData.Membership line 123
Source documentation
Membership on the quotient is independent of both representatives.
```
def Membership (x y : A.Extension G) : Prop :=
…
```
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.nameClass_eq_iff line 127
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.membership_nameClass line 130
inductive OAI.PartitionConsistency.ForcingQuotient.BasicFormula line 137
Source documentation
A basis of classical first-order syntax, with last-variable binders. All formulas in the target language translate to this basis.
```
inductive BasicFormula : ℕ → Type where
…
```
def OAI.PartitionConsistency.ForcingQuotient.BasicFormula.Realize line 148

def OAI.PartitionConsistency.ForcingQuotient.AtomicData.Force line 163

Source documentation

Formula-by-formula forcing: existential forcing is local density, NOT a maximum principle or selection of a single global witness name.

def Force (A : AtomicData P N) {n} (v : Fin n → N) (p : P) : BasicFormula n → Prop
  | .bot => False
  | .mem x y => A.MemF p (v x) (v y)
  | .equal x y => A.EqF p (v x) (v y)
  | .conj φ ψ => A.Force v p φ ∧ A.Force v p ψ
  | .neg φ => ∀ q, q ≤ p → ¬ A.Force v q φ
  | .ex φ => ∀ q, q ≤ p → ∃ r, r ≤ q ∧ ∃ x : N, A.Force (Fin.snoc v x) r φ

Mentions: OAI.PartitionConsistency.ForcingQuotient.AtomicData, OAI.PartitionConsistency.ForcingQuotient.BasicFormula

theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.force_mono line 171
def OAI.PartitionConsistency.ForcingQuotient.AtomicData.decisions line 182
Source documentation
Conditions deciding the fixed standard formula at a fixed tuple of names.
```
def decisions {n} (φ : BasicFormula n) (v : Fin n → N) : Set P :=
…
```
Mentions: OAI.PartitionConsistency.ForcingQuotient.BasicFormula
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.decisions_dense line 185
def OAI.PartitionConsistency.ForcingQuotient.AtomicData.witnesses line 197
Source documentation
Local existential witnesses, together with conditions which force that there are no witnesses. A generic must meet this uniformly dense set.
```
def witnesses {n} (φ : BasicFormula (n + 1)) (v : Fin n → N) : Set P :=
…
```
Mentions: OAI.PartitionConsistency.ForcingQuotient.BasicFormula
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.witnesses_dense line 200
abbrev OAI.PartitionConsistency.ForcingQuotient.AtomicData.Request line 214
Source documentation
All the dense sets needed for the external induction on standard formulas. Because each formula has finitely many free variables, the requests are countable whenever the set of name codes is countable.
```
abbrev Request (N : Type*) :=
…
```
def OAI.PartitionConsistency.ForcingQuotient.AtomicData.requestSet line 217
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.requestSet_dense line 221
def OAI.PartitionConsistency.ForcingQuotient.AtomicData.IsGeneric line 229
Source documentation
A filter meets the decision and local-witness dense sets for each fixed standard formula and tuple. This property is constructed below; it is not a truth lemma or an assumption that any set-theoretic axiom is forced.
```
def IsGeneric (G : GenericFilter P) : Prop :=
…
```
Mentions: OAI.PartitionConsistency.ForcingQuotient.GenericFilter
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.exists_generic line 237
Source documentation
Choose a filter through a prescribed condition, meeting any specified countable family of dense sets as well as every standard formula request.
```
theorem exists_generic [Countable N] {I : Type*} [Countable I]
    (D : I → Set P) (hD : ∀ i, Dense (D i)) (p : P) :
    ∃ G : GenericFilter P, p ∈ G ∧ (∀ i, ∃ q, q ∈ G ∧ q ∈ D i) ∧ A.IsGeneric G := by
…
```
Mentions: OAI.PartitionConsistency.ForcingQuotient.Dense, OAI.PartitionConsistency.ForcingQuotient.GenericFilter
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.truth line 256
Source documentation
Truth in the quotient of names. The proof is an external induction on the finite formula, never on the membership relation or rank of a name code. Existential witnesses are obtained locally, without a maximum principle.
```
theorem truth (G : GenericFilter P) (hG : A.IsGeneric G)
    {n} (φ : BasicFormula n) (v : Fin n → N) :
    BasicFormula.Realize (A.Membership G) (A.nameClass G ∘ v) φ ↔
      ∃ p, p ∈ G ∧ A.Force v p φ := by
…
```
Mentions: OAI.PartitionConsistency.ForcingQuotient.GenericFilter, OAI.PartitionConsistency.ForcingQuotient.BasicFormula, OAI.PartitionConsistency.ForcingQuotient.BasicFormula.Realize

def OAI.PartitionConsistency.Formula.toBasic line 315

Source documentation

Translation to the finite Boolean/existential basis used in the quotient truth proof. This changes no set-theoretic predicate or quantifier domain.

def toBasic {n} : Formula n → BasicFormula n
  | .bot => .bot
  | .mem x y => .mem x y
  | .equal x y => .equal x y
  | .imp φ ψ => .neg (.conj (toBasic φ) (.neg (toBasic ψ)))
  | .conj φ ψ => .conj (toBasic φ) (toBasic ψ)
  | .disj φ ψ => .neg (.conj (.neg (toBasic φ)) (.neg (toBasic ψ)))
  | .all φ => .neg (.ex (.neg (toBasic φ)))
  | .ex φ => .ex (toBasic φ)

/-- Classical truth is invariant under the translation to the basis. -/

Mentions: OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.Formula.neg

theorem OAI.PartitionConsistency.Formula.realize_toBasic line 326
Source documentation
Classical truth is invariant under the translation to the basis.
```
theorem realize_toBasic {M : Type*} (E : M → M → Prop) {n}
    (φ : Formula n) (v : Fin n → M) :
    BasicFormula.Realize E v φ.toBasic ↔ Realize E v φ := by
…
```
Mentions: OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.Formula.Realize
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.formula_truth line 351
Source documentation
The quotient truth lemma for the entire syntax used in the target statement, including implication, disjunction and universal quantification.
```
theorem formula_truth (G : GenericFilter P) (hG : A.IsGeneric G)
    {n} (φ : Formula n) (v : Fin n → N) :
    Formula.Realize (A.Membership G) (A.nameClass G ∘ v) φ ↔
      ∃ p, p ∈ G ∧ A.Force v p φ.toBasic := by
…
```
Mentions: OAI.PartitionConsistency.ForcingQuotient.GenericFilter, OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.Formula.Realize
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.models_iff line 361
Source documentation
The induced quotient satisfies exactly the sentences forced somewhere in the generic filter. This is a general logical equivalence, not a construction forcing the particular target theory.
```
theorem models_iff (G : GenericFilter P) (hG : A.IsGeneric G) (T : Theory) :
    Models (A.Membership G) T ↔
      ∀ φ ∈ T, ∃ p, p ∈ G ∧ A.Force Fin.elim0 p φ.toBasic := by
…
```
Mentions: OAI.PartitionConsistency.ForcingQuotient.GenericFilter, OAI.PartitionConsistency.Theory, OAI.PartitionConsistency.Models
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.consistent_of_forcing line 377
Source documentation
General forcing-to-consistency soundness for countable names. This theorem is uniform in the theory T; it does not assert that the target theory is forced. Producing its atomic data and proving all of the forced-axiom premises for the paper's symmetric system remain separate, uncompleted obligations.
```
theorem consistent_of_forcing [Countable N] [Nonempty N] (p₀ : P) {T : Theory}
    (h : ∀ φ ∈ T, A.Force Fin.elim0 p₀ φ.toBasic) : Consistent T := by
…
```
Mentions: OAI.PartitionConsistency.Theory, OAI.PartitionConsistency.Consistent