Formal Objects and Propositions in Megalodon as of February 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