Preface
Formal Objects and Propositions in Megalodon as of February 2021
Chad E. Brown
Draft of February 11, 2021
Contents:
Preface
1
Basic Logic
2
Equality
2.1
Eq
2.2
Notation for Equality
2.3
Functional Extensionality
3
Existential Quantifiers
3.1
Ex
3.2
Notation for Existential Quantifiers
4
Further Primitives and Axioms
5
Some Basic Results
5.6
If-then-else on Sets
5.1
PropN
5.2
Further Results
5.3
Exactly 1 of 2
5.4
Exactly 1 of 3
5.5
More Basic Results
5.5
More Basic Results
5.6
If-then-else on Sets
6
Basic Set Theory
7
Natural Numbers I
8
Ordinals
9
Comparing the Sizes of Sets
10
Misc
11
Description and If-then-else
11.1
Descr_ii
11.2
Descr_iii
11.3
Descr_iio
11.4
Descr_Vo1
11.5
Descr_Vo2
11.6
If_ii
11.7
If_iii
11.8
If_Vo1
11.9
If_iio
11.10
If_Vo2
12
Recursion on Sets
12.1
EpsilonRec_i
12.2
EpsilonRec_ii
12.3
EpsilonRec_iii
12.4
EpsilonRec_iio
12.5
EpsilonRec_Vo1
12.6
EpsilonRec_Vo2
13
If-then-else, Description and Recursion again
13.1
If_Vo3
13.2
Descr_Vo3
13.3
EpsilonRec_Vo3
13.4
If_Vo4
13.5
Descr_Vo4
13.6
EpsilonRec_Vo4
14
Predicates and Relations
15
Zermelo’s Well-Ordering Theorem
15.1
Zermelo1908
16
More Logical Properties
17
Natural Numbers II
17.1
NatRec
17.2
NatArith
18
Natural Numbers III and Ordinals
19
Disjoint Unions
20
Pairs, Sums, Functions and Products
20.1
pair_setsum
20.2
Dependent Sums
20.3
Functions
20.4
Tuples as Functions on Naturals
20.5
Dependent Products
20.6
Pairs as Tuples
20.6.1
Abstracting with Two Variables
20.7
Encodings of Functions and Predicates as Sets
20.7.1
Tuples with More Than 2 Components
20.8
Notation for Sums and Products
21
Surreal Numbers I
21.1
Surreal Numbers as Predicates on Ordinals
21.2
Surreal Numbers as Sets
21.3
TaggedSets
21.4
Surreal Numbers as Sets II
21.5
TaggedSets2
21.6
Ordinals are Surreal Numbers
21.7
SurrealRecI
21.8
SurrealRecII
21.9
SurrealRec2
21.10
More Results about Surreal Numbers
22
Explicit Number Structures
22.1
explicit_Nats
22.2
Omega gives Explicit Naturals
22.3
explicit_Nats_zero
22.4
explicit_Nats_one
22.5
explicit_Nats_transfer
23
Groups
23.1
AssocComm
23.2
Group1
23.2.1
Group1Explicit
23.2.2
Group1Explicit2
Group1Explicit2RepIndep
23.2.3
Group1Explicit3RepIndep
23.3
Groups Encoded as a Set
23.4
Group2
23.5
Group3
23.6
Subgroup as a Relation on Encoded Groups
23.7
Group4
23.8
Groups of Permutations
23.9
Group2
24
Rings
24.1
explicit_Ring
24.2
explicit_Ring_with_id
24.3
explicit_Ring_with_id_RepIndep2
24.4
explicit_CRing_with_id
24.5
explicit_CRing_with_id_RepIndep2
24.6
Packing two Binary Operations and a Constant into a Set
25
Explicit Reals
25.1
explicit_Reals
26
Rings II
26.1
CRing_with_id
27
Explicit Reals II and Fields
27.1
explicit_Reals
27.1.1
explicit_Reals_Q_min_props
27.1.2
Q is Minimal as a Subfield of R
27.2
explicit_Field_transfer
27.3
explicit_Field_RepIndep2
27.4
Fields Encoded as Sets
27.5
explicit_OrderedField_transfer
27.6
Selectors for Fields
27.7
Field
27.8
Field2
27.9
Basic Results about Fields
27.10
explicit_Reals_transfer
28
Surreal Numbers II
28.1
SurrealArithmetic
28.2
Complex Surreals
28.3
Complex
28.4
Complex II
28.5
Int
28.6
Packing Two Operations, a Relation and Two Constants
28.7
explicit_OrderedField_RepIndep2
28.8
Unpacking Ordered Fields
28.9
explicit_Reals_RepIndep2
28.10
Unpacking Explicit Reals
28.11
RealsStruct