SetLanguage.lean`

34 declarations, 0 contain sorry, 0 declared as axioms

All abbreviations in this namespace expand to formulas of the pure language of equality and membership. Functions are sets of Kuratowski pairs inside the structure. In particular, no quantification over external Lean functions is used in PP, Choice, or ordinal-indexed Choice.

def OAI.PartitionConsistency.SetLanguage.subset line 16
Source documentation
a ⊆ b.
Also declared: ComparatorChallenges/PartitionConsistency.lean:118 (same declaration text).
```
def subset {n} (a b : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.empty line 20
Source documentation
a = ∅.
Also declared: ComparatorChallenges/PartitionConsistency.lean:122 (same declaration text).
```
def empty {n} (a : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.nonempty line 24
Source documentation
a ≠ ∅, stated as existence of a member.
Also declared: ComparatorChallenges/PartitionConsistency.lean:126 (same declaration text).
```
def nonempty {n} (a : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.unorderedPair line 28
Source documentation
p = {x,y}.
Also declared: ComparatorChallenges/PartitionConsistency.lean:130 (same declaration text).
```
def unorderedPair {n} (p x y : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.successor line 33
Source documentation
b = a ∪ {a}.
Also declared: ComparatorChallenges/PartitionConsistency.lean:135 (same declaration text).
```
def successor {n} (b a : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.orderedPair line 38
Source documentation
Kuratowski ordered pair: p = {{x},{x,y}}.
Also declared: ComparatorChallenges/PartitionConsistency.lean:140 (same declaration text).
```
def orderedPair {n} (p x y : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.edge line 44
Source documentation
The internal graph relation ⟨x,y⟩ ∈ f.
Also declared: ComparatorChallenges/PartitionConsistency.lean:146 (same declaration text).
```
def edge {n} (f x y : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.functionOn line 51
Source documentation
f is a set graph of a function whose domain is exactly d. The first conjunct excludes non-pairs and graph entries outside the domain; the second conjunct asserts totality and single-valuedness.
Also declared: ComparatorChallenges/PartitionConsistency.lean:153 (same declaration text).
```
def functionOn {n} (f d : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.mapsTo line 59
Source documentation
Internal set function f : d → r.
Also declared: ComparatorChallenges/PartitionConsistency.lean:161 (same declaration text).
```
def mapsTo {n} (f d r : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.surjection line 65
Source documentation
Internal set surjection f : d ↠ r.
Also declared: ComparatorChallenges/PartitionConsistency.lean:167 (same declaration text).
```
def surjection {n} (f d r : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.injection line 71
Source documentation
Internal set injection f : d ↪ r.
Also declared: ComparatorChallenges/PartitionConsistency.lean:173 (same declaration text).
```
def injection {n} (f d r : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.transitiveSet line 79
Source documentation
Transitivity of a set (not transitivity of the external structure).
Also declared: ComparatorChallenges/PartitionConsistency.lean:181 (same declaration text).
```
def transitiveSet {n} (a : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.membershipLinear line 84
Source documentation
Membership is an internal strict linear order on a.
Also declared: ComparatorChallenges/PartitionConsistency.lean:186 (same declaration text).
```
def membershipLinear {n} (a : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.membershipWellFounded line 94
Source documentation
Every nonempty internal subset of a has a membership-minimal element. This does NOT assert external well-foundedness of the relation.
Also declared: ComparatorChallenges/PartitionConsistency.lean:196 (same declaration text).
```
def membershipWellFounded {n} (a : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.ordinal line 100
Source documentation
A von Neumann ordinal: a transitive set internally wellordered by membership.
Also declared: ComparatorChallenges/PartitionConsistency.lean:202 (same declaration text).
```
def ordinal {n} (a : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.choiceOn line 104
Source documentation
A choice function on the set A of nonempty sets.
Also declared: ComparatorChallenges/PartitionConsistency.lean:206 (same declaration text).
```
def choiceOn {n} (c A : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.nonemptyFamily line 110
Source documentation
A graph F coding a family of nonempty sets indexed by ordinal η.
Also declared: ComparatorChallenges/PartitionConsistency.lean:212 (same declaration text).
```
def nonemptyFamily {n} (F η : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.choiceForFamily line 116
Source documentation
c(ξ) ∈ F(ξ) for every ξ ∈ η, with c an internal function.
Also declared: ComparatorChallenges/PartitionConsistency.lean:218 (same declaration text).
```
def choiceForFamily {n} (c η F : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.PP line 124
Source documentation
The Partition Principle. The reverse injection is not required to be a section of the original surjection. Both X and Y range over all sets.
Also declared: ComparatorChallenges/PartitionConsistency.lean:226 (same declaration text).
```
def PP : Sentence :=
…
```
Mentions: OAI.PartitionConsistency.Sentence
def OAI.PartitionConsistency.SetLanguage.AC line 128
Source documentation
Ordinary Choice for every set of nonempty sets.
Also declared: ComparatorChallenges/PartitionConsistency.lean:230 (same declaration text).
```
def AC : Sentence :=
…
```
Mentions: OAI.PartitionConsistency.Sentence
def OAI.PartitionConsistency.SetLanguage.ACwo line 133
Source documentation
Choice for every ordinal-indexed family of nonempty sets, including ordinals which may fail to be well founded from outside a model.
Also declared: ComparatorChallenges/PartitionConsistency.lean:235 (same declaration text).
```
def ACwo : Sentence :=
…
```
Mentions: OAI.PartitionConsistency.Sentence
def OAI.PartitionConsistency.SetLanguage.extensionality line 139
Also declared: ComparatorChallenges/PartitionConsistency.lean:241 (same declaration text).
def OAI.PartitionConsistency.SetLanguage.emptySet line 142
Also declared: ComparatorChallenges/PartitionConsistency.lean:244 (same declaration text).
def OAI.PartitionConsistency.SetLanguage.pairing line 144
Also declared: ComparatorChallenges/PartitionConsistency.lean:246 (same declaration text).
def OAI.PartitionConsistency.SetLanguage.union line 146
Also declared: ComparatorChallenges/PartitionConsistency.lean:248 (same declaration text).
def OAI.PartitionConsistency.SetLanguage.powerSet line 149
Also declared: ComparatorChallenges/PartitionConsistency.lean:251 (same declaration text).
def OAI.PartitionConsistency.SetLanguage.infinity line 151
Also declared: ComparatorChallenges/PartitionConsistency.lean:253 (same declaration text).
def OAI.PartitionConsistency.SetLanguage.foundation line 155
Also declared: ComparatorChallenges/PartitionConsistency.lean:257 (same declaration text).
def OAI.PartitionConsistency.SetLanguage.separation line 162
Source documentation
The instance of Separation for an entirely arbitrary formula p(params,x). All parameters are universally closed. Neither the quantifier complexity of p nor the number of parameters is bounded.
Also declared: ComparatorChallenges/PartitionConsistency.lean:264 (same declaration text).
```
def separation {n} (p : Formula (n + 1)) : Sentence :=
…
```
Mentions: OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.Sentence
def OAI.PartitionConsistency.SetLanguage.relation line 171
Source documentation
Substitution into a binary formula with n additional parameters.
Also declared: ComparatorChallenges/PartitionConsistency.lean:273 (same declaration text).
```
def relation {n m} (p : Formula (n + 2)) (params : Fin n → Fin m) (x y : Fin m) :
    Formula m :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.replacement line 178
Source documentation
The instance of Replacement for an entirely arbitrary formula p(params,x,y): if it is single-valued and total on A, its image is a set. As with Separation, the parameters are all universally closed.
Also declared: ComparatorChallenges/PartitionConsistency.lean:280 (same declaration text).
```
def replacement {n} (p : Formula (n + 2)) : Sentence :=
…
```
Mentions: OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.Sentence
inductive OAI.PartitionConsistency.SetLanguage.IsZFAxiom line 195
Source documentation
Exactly the axioms and all schema instances of pure first-order ZF.
Also declared: ComparatorChallenges/PartitionConsistency.lean:297 (same declaration text).
```
inductive IsZFAxiom : Sentence → Prop where
…
```
Mentions: OAI.PartitionConsistency.Sentence
def OAI.PartitionConsistency.SetLanguage.ZF line 207
Source documentation
Zermelo–Fraenkel set theory, without Choice.
Also declared: ComparatorChallenges/PartitionConsistency.lean:309 (same declaration text).
```
def ZF : Theory := {p | IsZFAxiom p}
```
Mentions: OAI.PartitionConsistency.Theory, OAI.PartitionConsistency.SetLanguage.IsZFAxiom
def OAI.PartitionConsistency.SetLanguage.targetTheory line 210
Source documentation
The exact theory in target thm:main-consistency.
Also declared: ComparatorChallenges/PartitionConsistency.lean:312 (same declaration text).
```
def targetTheory : Theory := ZF ∪ {PP, ACwo, AC.neg}
…
```
Mentions: OAI.PartitionConsistency.Theory, OAI.PartitionConsistency.SetLanguage.ZF, OAI.PartitionConsistency.SetLanguage.PP, OAI.PartitionConsistency.SetLanguage.ACwo