Main.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

PartitionPrinciple

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_PP_of_dense line 90
Source documentation
Purely logical conversion of reverse-injection witnesses to the full Partition Principle sentence. Its quantifiers range over all HS names.
```
theorem forces_PP_of_dense
    (h : ∀ (p : P) (f X Y : S.Name),
      S.Forces ![f,X,Y] p (SetLanguage.surjection 0 1 2) →
      ∃ q, q ≤ p ∧ ∃ j : S.Name, S.Forces ![j,Y,X] q (SetLanguage.injection 0 1 2))
    (p : P) : S.Forces Fin.elim0 p SetLanguage.PP := by
…
```
Mentions: OAI.PartitionConsistency.SetLanguage.surjection, OAI.PartitionConsistency.SetLanguage.injection, OAI.PartitionConsistency.SetLanguage.PP
theorem OAI.PartitionConsistency.ConcreteSystem.reverse_injection_dense line 133
Source documentation
All-set reduction for the constructed system, including the empty-set case. The presentation and subsequent choices are made at arbitrary ranks.
```
theorem reverse_injection_dense (f X Y : S.Name) (p : P)
    (hf : S.Forces ![f,X,Y] p (SetLanguage.surjection 0 1 2)) :
    ∃ q, q ≤ p ∧ ∃ j : S.Name, S.Forces ![j,Y,X] q (SetLanguage.injection 0 1 2) := by
…
```
Mentions: OAI.PartitionConsistency.ConcreteSystem.P, OAI.PartitionConsistency.SetLanguage.surjection, OAI.PartitionConsistency.SetLanguage.injection
theorem OAI.PartitionConsistency.ConcreteSystem.forces_PP line 151
Source documentation
The Partition Principle for arbitrary internal sets and surjections.
```
theorem forces_PP (p : P) : S.Forces Fin.elim0 p SetLanguage.PP :=
…
```
Mentions: OAI.PartitionConsistency.ConcreteSystem.P, OAI.PartitionConsistency.SetLanguage.PP
theorem OAI.PartitionConsistency.ConcreteSystem.forces_target line 156
Source documentation
The actual symmetric forcing interpretation supplies every axiom of the full target theory, with no inaccessible-cardinal or model-existence premise.
```
theorem forces_target (p : P) : ∀ φ ∈ SetLanguage.targetTheory, S.Forces Fin.elim0 p φ := by
…
```
Mentions: OAI.PartitionConsistency.ConcreteSystem.P, OAI.PartitionConsistency.SetLanguage.targetTheory
theorem OAI.PartitionConsistency.ConcreteSystem.consistent_target line 167
Source documentation
Soundness of the nontrivial regular forcing interpretation rules out an ordinary finite first-order proof of contradiction from the target theory.
```
theorem consistent_target : Consistent SetLanguage.targetTheory :=
…
```
Mentions: OAI.PartitionConsistency.Consistent, OAI.PartitionConsistency.SetLanguage.targetTheory
theorem OAI.PartitionConsistency.main_consistency line 181
Source documentation
Relative consistency for pure first-order set theories, with syntactic consistency and no transitive-ground or inaccessible-cardinal hypothesis.
Distinct definitions of this name: ComparatorChallenges/PartitionConsistency.lean:318 (same statement text; different proof or body). Qualify references as OAI.PartitionConsistency.main_consistency@path.
```
theorem main_consistency :
    Consistent SetLanguage.ZF → Consistent SetLanguage.targetTheory := by
…
```
Mentions: OAI.PartitionConsistency.Consistent, OAI.PartitionConsistency.SetLanguage.ZF, OAI.PartitionConsistency.SetLanguage.targetTheory