Set Theory and Foundations of Mathematics
1. First foundations of mathematics

1.1. Introduction to the foundations of mathematics

What is mathematics

Theories

The word «theory» may take diverse meanings between uses, from mathematical ones to those of ordinary language and other sciences. Let us first present the distinction by nature (general kind of objects); the other distinction, by intent (realism vs. formalism) is introduced below and in 1.9.

Non-mathematical theories describe roughly or qualitatively some systems or aspects of the world (fields of observation) which escape exact self-sufficient description. For example, usual descriptions of chemistry involve drastic approximations, recollecting some rough accounts of seemingly arbitrary effects and laws, whose deductions from quantum physics are often out of reach of direct calculations. The lack of clear distinction of objects and their properties induces risks of mistakes when approaching them and trying to infer some properties from others, such as to infer some global properties of a system from likely, fuzzy properties of its parts.

In between both, applied mathematical theories, such as theories of physics are also mathematical theories but the mathematical systems they describe are meant as idealized (simplified) versions of aspects of given real-world systems while neglecting other aspects; depending on its accuracy, this idealization (reduction to mathematics) also allows for correct deductions within accepted margins of error.

Foundations and developments

To express the properties of its models, each theory includes a list of statements, which are formulas meant as true when interpreted in any model. Its primitive statements are called axioms. Further statements called theorems are added by development to the content, under the condition that they are proven (deduced) from previous ones : this ensures them to be true in all models, provided that previous ones were. Theorems can then be used in further developments in the same way as axioms. A theory is consistent if its theorems will never contradict each other. Inconsistent theories cannot have any model, as the same statement cannot be true and false on the same system. The Completeness Theorem (1.9, 1.10, 4.7) will show that the range of all possible theorems precisely fits the more interesting reality of which statements stay true across the range of all models (which indeed exist for any consistent theory).
Other kinds of developments (definitions and constructions) adding other components beyond statements, will be described in 1.5, 1.D, 4.10 and 4.11.

Platonism vs Formalism

• The Platonic or realistic view, considers the mathematical realm or some particular described systems, as preexisting realities to be explored (or remembered, according to Plato). This is the approach of intuition which by imagining things, smells their order before formalizing them.
• A formalistic or logicist view focuses on language, rigor (syntactic rules) and dynamical aspects of a theory, starting from its formal foundation, and following the rules of development.

By its limited abilities, human thought cannot operate in any fully realistic way over infinite systems (or finite ones with unlimited size), but requires some kind of logic for extrapolation, roughly equivalent to formal reasonings developed from some foundations ; this work of formalization can prevent possible errors of intuition. Moreover, mathematical objects cannot form any completed totality, but only a forever temporary, expanding realm, whose precise form is an appearance relative to a choice of formalization.

The cycle of foundations

• Set theory describes the universe of «all mathematical objects», from the simplest to the most complex such as infinite systems (in a finite language). It can roughly be seen as one theory, but in details it will have an endless diversity of possible variants (indeed differing from each other).
• Model theory is the study of theories (their formalisms as systems of symbols), and systems (possible models of theories). Proof theory completes this by describing formal systems of rules of proofs. While model theory is usually meant as a general topic (admitting variants of concepts), it can be specified into precise versions, thus mathematical theories called logical frameworks, each giving a precise format of expression for a wide range of possible theories, and (if completed by proof theory) a format in which all proofs from any of these theories can in principle be expressed. There is an essentially unique main logical framework called first-order logic, by which the concepts of theory, theorem (i.e. provable statement) and consistency of each theory, find their natural mathematical definitions; but other logical frameworks are sometimes needed too.

Each one is the natural framework to formalize the other: each set theory is formalized as a theory described by model theory; the latter better comes as a development from set theory (defining theories and systems as complex objects) than directly as a theory. Both connections must be considered separately: both roles of set theory, as a basis and an object of study for model theory, must be distinguished. But these formalizations will take a long work to complete.

1.2. Variables, sets, functions and operations

This section (1.2) will intuitively introduce some first few concepts of set theory : those of set, function and operation. But it will start by introducing some qualifications of variables only meant as extrinsic qualities, namely to describe the status of a given variable relatively to some kinds of contexts (viewpoints) which are not yet themselves introduced at this stage. The reader is invited to not be stopped by this kind of unclarity which is likely to get resolved along the specific uses in later sections.

Then 1.3 will start introducing model theory, by which any theory (and thus any set theory) can be formalized. More subtleties (paradoxes..) in the whole picture of the foundations of mathematics will be explained later.

Constants

Free and bound variables

• The variable is called fixed when seen "from inside", which means it has a given value, and is thus usable as a constant.
• It is called bound when seen from the «outside» where the diversity of its possible values is considered fully known, gathered and processed as a whole.
• It is called free to describe a coexistence of both statuses (views over it): a local view seeing it as fixed, and an external view giving the context of its variations.

Ranges and sets

Cantor defined a set as a «gathering M of definite and separate objects of our intuition or our thought (which are called the "elements" of M) into a whole». He explained to Dedekind : «If the totality of elements of a multiplicity can be thought of... as "existing together", so that they can be gathered into "one thing", I call it a consistent multiplicity or a "set".» (We expressed this "multiplicity" as that of values of a variable).
He described the opposite case as an «inconsistent multiplicity» where «admitting a coexistence of all its elements leads to a contradiction». But non-contradiction cannot suffice to generally define sets: the consistency of a statement does not imply its truth (i.e. its negation may be true but unprovable); facts of non-contradiction are often themselves unprovable (incompleteness theorem); and two separately consistent coexistences might contradict each other (Irresistible force paradox / Omnipotence paradox).

Functions

• A set called the domain of f, denoted Dom f
• For each element x of Dom f, an object written f(x), called the image of x by f or value of f at x.

Operations

Like for functions, the arguments of operations are basically denoted not by symbols but by places around the operation symbol, to be filled by any expression giving them desired values. Diverse display conventions may be used (1.5). For instance, using the left and right spaces in parenthesis after the symbol f, we denote f(x,y) the value of a binary operation f on its fixed arguments named x and y (i.e. its value when its arguments are assigned the fixed values of x and y).

1.3. Form of theories: notions, objects and meta-objects

The variability of the model

Notions and objects

One-model theory

The diversity of logical frameworks

• The admissible forms of contents for theories ;
• In particular, the syntactic structures of possible statements and other expressions, which can be called their "grammar" ;
• The meaning of these contents and expressions on the models ;
• The rules of development of theories.

• Boolean algebra, also called propositional calculus (1.6);
• Algebra;
• First-order logic;
• Duality (for geometry) and the tensor formalism for linear algebra;
• Second-order logic (5.1, 5.2);
• Higher-order logic (5.2);
• Strong versions of set theory (1.A).

Examples of notions from various theories

Meta-objects

By its notion of «object», each one-model theory distinguishes the objects of T in M from the rest of its own objects in [T,M], which are the meta-objects. The above rule of use of the meta prefix would let every object be a meta-object; but we will make a vocabulary exception by only calling meta-object those which are not objects: symbols, types or other notions, Booleans, structures, expressions...

Components of theories

• A list of abstract types, names that will designate the types in each system;
• A language (vocabulary): list of structure symbols, names of the structures which will form the described system (1.4).
• A list of axioms chosen among expressible statements with this language (1.9).

Set-theoretical interpretations

Any interpretation converts each abstract type into a symbol (name) designating a set called interpreted type (serving as the range of variables of that type, whose use is otherwise left intact). This symbol is usually a fixed variable in the generic case, but can be accepted as constant symbol of set theory in special cases such as numbers systems (ℕ, ℝ...).
In generic interpretations, all objects (elements of interpreted types) are urelements, but other kinds of interpretations called standard by convention for specific theories may do otherwise. For example, standard interpretations of geometry represent points by urelements, but represent straight lines by sets of points.

When adopting set theory as our conceptual framework, this concept of "interpretation" becomes synonymous with the choice (designation) of a model.

1.4. Structures of mathematical systems

First-order structures

• its list of arguments (variable symbols figured as places around the operator symbol instead of names),
• for each argument, its abstract type, whose value as a set will be the range of this argument in any interpretation;
• its type of results: the type which will contain all results of the operation designated by this symbol, in any interpretation with given values of its arguments.

The list of types is completed by the Boolean type, interpreted as the pair of elements (the set of two elements) we shall denote 1 for «true» and 0 for «false». A variable of this type (outside the theory) is called a Boolean variable.

Structures of set theory

Let us admit 3 primitive notions : elements (all objects), sets and functions. Here are their main primitive structures.
One aspect of the role of sets is given by the binary predicate ∈ of belonging or membership : for any element x and any set E, we say that x is in E (or x belongs to E, or x is an element of E, or E contains x) and write x ∈ E, to mean that x is a possible value of the variables with range E.
Functions f play their role by two operators: the domain functor Dom, and the function evaluator, binary operator that is implicit in the notation f(x), with arguments f and x, giving the value of any function f at any element x of Dom f.

About ZFC set theory

• It cannot be self-contained as it must assume the framework of model theory to make sense.
• Its axioms, usually just admitted (as either intuitive, obvious, necessary or just historically selected for their consistency and the convenience of their consequences), would actually deserve more subtle and complex justifications, which cannot find place at a starting point of mathematics.
• Ordinary mathematics, using many objects usually not seen as sets, are only inelegantly developed from this basis. As the roles of all needed objects can anyway be indirectly played by sets, they did not require another formalization, but remained cases of discrepancy between the «theory» and the practice of mathematics. The complexity and weirdness of these needed developments do not disturb specialists just because once known possible, they can simply be taken for granted.

Formalizing types and structures as objects of one-model theory

Since one-model theory assumes a fixed model, it only needs one meta-type of "types" to play both roles of abstracts types (in the theory) and interpreted types (components of the model), respectively given by two meta-functors: one from variables to types, and one from objects to types. Indeed the more general notion of «set of objects» is not used and can be ignored.

1.5. Expressions and definable structures

Terms and formulas

Each expression comes in the context of a given list of available free variables. Any expression will give (define) a value (either an object or a Boolean) for each possible data of

• A system interpreting the given types and structure symbols;
• Fixed values of available free variables in this system.

For example, « x+x » is a term with two occurrences of the variable «x», and one of the addition symbol «+».

The diverse kinds of symbols

• Variables of each type:
  • Free variables, from the list of available ones ;
  • Bound variables, whose occurrences are contained by binders (see 1.8) ;
• Para-operator symbols:
• Structure symbols from the language (operators and predicates) ;
• One equality symbol per type (predicate with 2 arguments of the same type) abusively all written = ;
• Logical connectives (1.4, listed in 1.6) ;
• The conditional operator may be introduced for abbreviation (2.4).
• Binders (1.8):
  • Quantifiers ∀ and ∃ (1.10) are the only primitive binders of first-order logic ;
  • More binders will be introduced in set theory.

Root and sub-expressions

Expressions are built successively, in parallel between different lists of available free variables. The first and simplest ones are made of just one symbol (as root, having a value by itself) : constants and variables are the first terms; the Boolean constants 1 and 0 are the simplest formulas.
The next expressions are then successively built as made of the following data:

• A choice of root, occurrence of either a para-operator symbol (beyond constants we already mentioned) or a binder;
• If the root is a binder: a choice of variable symbol, to be bound by it;
• A list of previously built expressions, whose format (number and types of entries) is determined by the root : for a para-operator symbol, this format is given by its list of its arguments.

Display conventions

• Most binary para-operator symbols are displayed as one character between (separating) both arguments, such as in x+y
• Symbols with higher arities can be similarly displayed by several characters separating the entries, such as in the addition x+y+z of 3 numbers.
• Function-like displays, such as +(x,y) instead of x+y, are more usual for arities other than 2 ; parenthesis may be omitted when arities are known (Polish notation).
• A few symbols «appear» only implicitly by their special way of putting their arguments together : multiplication in xy, exponentiation in xⁿ.
• Parenthesis can be part of the notation of a symbol (function evaluator, tuples...).

Variable structures

• An ordinary variable symbol, usable by expressions which by a binder can let it range over some notion;
• A new constant symbol, to be added to the language, forming another theory with a richer language.

Structures defined by expressions

• An expression (terms define operators, while formulas define predicates and Booleans);
• Among its available free variables, a selection of those which will be bound by this definition in the role of arguments of the intended structure; the rest of them, which remain free, are called parameters.

In set theory, any function f is synonymous with the functor defined by the term f(x) with argument x and parameter f (but the domain of this functor is Dom f instead of a type).
The terms without argument define simple objects (nullary operators) ; the one made of a variable of a given type, seen as parameter, suffices to give all objects of its type.

Invariant structures

Indeed any structure named by a symbol in the language is directly defined by it without parameter, and thus invariant. As will be further discussed in 4.10, theories can be developed by definitions, which consists in naming another invariant structure by a new symbol added to the language. Among aspects of the preserved meaning of the theory, are the meta-notions of structure, invariant structure, and the range of theorems expressible with the previous language.

1.6. Logical connectives

Tautologies

Tautologies form the rules of Boolean algebra, an algebraic theory describing operations on the Boolean type, itself naturally interpreted as the pair of elements 0 and 1 (but also admitting more sophisticated interpretations beyond the scope of this chapter).

Negation

Conjunctions, disjunctions

(A ∨ B) ⇎ (¬A ∧ ¬B)
(A ∧ B) ⇎ (¬A ∨ ¬B)

Chains of conjunctions such as (A ∧ B ∧ C), abbreviate any formula with more parenthesis such as ((A ∧ B) ∧ C), all equivalent by associativity ; similarly for chains of disjunctions such as (A ∨ B ∨ C).

Implication

The formula A ∧ (A ⇒ B) is equivalent to A ∧ B but will be written A ∴ B, which reads «A therefore B», to indicate that it is deduced from the truths of A and A ⇒ B.

Chains of implications and equivalences

In a different kind of abbreviation, any chain of formulas linked by ⇔ and/or ⇒ will mean the chain of conjunctions of these implications or equivalences between adjacent formulas:

(A ⇒ B ⇒ C) ⇔ ((A ⇒ B) ∧ (B ⇒ C)) ⇒ (A ⇒ C)
(A ⇔ B ⇔ C) ⇔ ((A ⇔ B) ∧ (B ⇔ C)) ⇒ (A ⇔ C)
0 ⇒ A ⇒ A ⇒ 1
(¬A) ⇔ (A ⇒ 0) ⇔ (A ⇔ 0)
(A ∧ 1) ⇔ A ⇔ (A ∨ 0) ⇔ (1 ⇒ A) ⇔ (A ⇔ 1)
(A ∧ B) ⇒ A ⇒ (A ∨ B)

1.7. Classes in set theory

Standard universes and meta-sets

Definiteness classes

Set = «is a set»
Fnc = «is a function»

Extended definiteness

A ∧ (B ∧ C)
(A ∧ B) ∧ C

Classes will be defined by everywhere definite predicates, easily expressible by the above rule as follows.
Any predicate A can be extended beyond its domain of definiteness, in the form dA ∧ A (giving 0), or dA ⇒ A (giving 1).
For any class A and any unary predicate B definite in all A, the class defined by A∧B is called the subclass of A defined by B.

1.8. Binders in set theory

The syntax of binders

We shall first review both main binders of set theory : the set-builder and the function definer. Then 1.10 will present both main quantifiers. Finally 2.1 and 2.2 will give axioms to complete this formalization of the notions of sets and functions in set theory.

Set-builder

y ∈ {x∈E | A(x)} ⇔ (y ∈ E ∧ A(y))

Russell's paradox

Theorem. For any set E there is a set F such that F ∉ E. So, no set E can contains all sets.

This will oblige us to keep the distinctions between sets and classes.

The function definer

• x is the variable,
• E is its range,
• the notation "t(x)" stands for any term, here abbreviated (to describe the general case) using the functor symbol t defined by this term with argument x (and possible parameters here kept implicit).

Relations

Now unary relations (functions with Boolean values), will be represented as subsets S of their domain E, using the set-builder in the role of definer, and ∈ in the role of evaluator interpreting S as the predicate x ↦ (x ∈ S). This role of S still differs from the intended unary relation, as it ignores its domain E but is definite in the whole universe, giving 0 outside E. This lack of operator Dom does not matter, as E is usually known from the context (as an available variable).

1.9. Axioms and proofs

Statements

Realistic vs. axiomatic theories in mathematics and other sciences

An axiomatic theory is a formally given theory T = (τ, L, X) with an axioms list X, that means to define the class of its models, as that of all systems M interpreting the language L where all axioms (elements of X) are true, which will be denoted M⊨T.

This truth will usually be ensured for realistic theories of pure mathematics : arithmetic and set theory (though the realistic meaning of set theory will not always be clear depending on considered axioms). These theories will also admit non-standard models, making their realistic and axiomatic meanings effectively differ.
Outside pure mathematics, the truth of realistic theories may be dubious (questionable): non-mathematical statements over non-mathematical systems may be ambiguous (ill-defined), while the truth of theories of applied mathematics may be approximative, or speculative as the intended "real" systems may be unknown (contingent among other possible ones). There, a theory is called falsifiable if, in principle, the case of its falsity can be discovered by comparing its predictions (theorems) with observations. For example, biology is relative to a huge number of random choices silently accumulated by Nature on Earth during billions of years ; it has lots of "axioms" which are falsifiable and require a lot of empirical testing.
Non-realistic theories outside mathematics (not called "axiomatic" by lack of mathematical precision) would be works of fiction describing imaginary or possible future systems.

Provability

We say that A is provable in T, or a theorem of T, and write T ⊢ A if a proof of A in T exists. In practice, we only qualify as theorems the statements known as such, i.e. for which a proof is known. But synonyms for "theorem" are traditionally used according to their importance: a theorem is more important than a proposition; either of them may be deduced from an otherwise less important lemma, and easily implies an also less important corollary.

Logical validity

A proof of A using some axioms can also be seen as a proof of (conjunction of these axioms ⇒ A) without axiom, thus making this implication logically valid.

Refutability and consistency

⊢ (A ∧ ¬A) ⇔ 0
((T ⊢ A) ∧ (T ⊢ B)) ⇔ (T ⊢ A∧B)
((T ⊢ A) ∧ (T ⊢ ¬A)) ⇔ (T ⊢ 0).

Beyond the required quality of soundness of the proof theoretical part of a logical framework, more remarkable is its converse quality of completeness : that for any axiomatic theory it describes, any statement that is true in all models is provable. In other words, any unprovable statement is false somewhere, and any irrefutable statement is true somewhere. Thus, any consistent theory has existing models, but often a diversity of them, as any undecidable statement is true in some and false in others. Adding some chosen undecidable statements to axioms leads to different consistent theories which can «disagree» without conflict, all truly describing different existing systems. This resolves much of a priori divergence between Platonism and formalism while giving proper mathematical definiteness to the a priori intuitive concepts of "proof", "theorem" and "consistency".

1.10. Quantifiers

Bounded vs open quantifiers

Both main quantifiers

• The universal quantifier ∀ means «for all»: (∀x∈E, A(x)) is read «For all x in E, A(x)».
• The existential quantifier ∃ means «there exists»: (∃x∈E, A(x)) is read «There exists x in E such that A(x)».

(∀x∈E, A(x)) ⇔ {x∈E | A(x)} = E.

(∀x, A(x)) ⇔ A = (x ↦ 1)
(∃x, A(x)) ⇔ A ≠ (x ↦ 0)
(∃x, A(x)) ⇎ (∀x, ¬A(x))

(∀_C x, A(x)) ⇔ (∀x, C(x) ⇒ A(x))
(∃_C x, A(x)) ⇔ (∃x, C(x) ∧ A(x)) ⇔ ∃_C∧A x, 1

Inclusion between classes

(∀_B x, C(x)) ⇒ (∀_A x, C(x))
(∃_A x, C(x)) ⇒ (∃_B x, C(x))
(∃_C x, A(x)) ⇒ (∃_C x, B(x))
(∀_C x, A(x)) ⇒ (∀_C x, B(x))

Rules of proofs for quantifiers on a unary predicate

Existential Introduction. If we have terms t, t′,… and a proof of (A(t) ∨ A(t′) ∨ …), then ∃x, A(x).

Existential Elimination. If ∃x, A(x), then we can introduce a new free variable z with the hypothesis A(z) (the consequences will be true without restricting the generality).

While ∃ appeared as the designation of an object, ∀ appears as a deduction rule: ∀_C x, A(x) means that its negation ∃_C x, ¬A(x) leads to a contradiction.

Universal Elimination. If ∀_C x, A(x) and t is a term satisfying C(t), then A(t).

Some logically valid formulas

((∀_C x, A(x)) ∧ (∀_C x, A(x) ⇒ B(x))) ⇒ (∀_C x, B(x))
((∃_C x, A(x)) ∧ (∀_C x, A(x) ⇒ B(x))) ⇒ (∃_C x, B(x))
((∀_C x, A(x)) ∧ (∃_C x, B(x))) ⇒ (∃_C x, A(x) ∧ B(x))
(∀_C x, A(x)∨B(x)) ⇒ ((∀_C x, A(x)) ∨ (∃_C x, B(x)))
(∀_A x, ∀_B y, R(x,y)) ⇔ (∀_B y, ∀_A x, R(x,y))
(∃_A x, ∃_B y, R(x,y)) ⇔ (∃_B y, ∃_A x, R(x,y))
(∃_A x, ∀_B y, R(x,y)) ⇒ (∀_B y, ∃_A x, R(x,y))
∀x, (∀y, R(x,y)) ⇒ R(x,x) ⇒ (∃y, R(x,y))

• (∀_C x,y, ) means (∀_C x, ∀_C y, ) and so on for more variables with the same range.
• (∃_C x,y, ) means (∃_C x, ∃_C y, ) (same remark).
• (∀_C x≠y, ) means (∀_C x,y, x≠y ⇒ )
• (∃_C x≠y, ) means (∃_C x,y, x≠y ∧ )
• (∃_C x, A(x) ∴ B(x)) means (∃_C x, A(x)) ∧ (∀_C x, A(x) ⇒ B(x)), while it implies but is not always equivalent to (∃_C x, A(x) ∧ B(x)).

(L ⊢ ∃x, 1) ⇔ (a constant symbol exists in L)

Completeness of first-order logic

First-order logic was found complete as expressed by the completeness theorem, which was originally Gödel's thesis : from a suitably formalized concept of «proof», the resulting class of (potential) theorems A of any first-order theory T was found to be the "perfect" one, coinciding with the class of universally true statements (true in all models M):

∀A, (T ⊢ A) ⇔ (∀M, (M⊨T)⇒(M⊨A))

This quality of first-order logic confirms its central importance in the foundations of mathematics, after its ability to express all mathematics : any logical framework can anyway be developed from set theory (and more directly, any theory from any framework can be somehow interpreted in set theory), itself expressible as a first-order theory.

This construction is non-algorithmic : it is made of an infinity of steps, where each step may involve an infinite knowledge (of whether the given predicate on given arguments, seen as a candidate additional axiom, preserves consistency with previously accepted ones). Actually, most foundational theories such as set theories, do not have any algorithmically definable model.

1.11. Second-order universal quantifiers

As we shall do for the axioms of equality (below) and for set theory (in 2.1 and 2.2), a theory may be first expressed in second-order logic for intuitive reasons, before formally interpreting this as a convenient meta level tool to abbreviate a first-order formalization, as follows.

Second-order Universal Introduction. If T'⊢F then T entails the second-order statement (∀s, F(s)).

Second-order Universal Elimination. Once a second-order statement (∀s, F(s)) is accepted in a theory T, it is manifested in first-order logic as a schema of statements, that is an infinite list of statements of the form (∀parameters, F(s)) for each possible replacement of s by a defining expression with parameters.

Incompleteness of second-order logic

A theory is called complete if it essentially determines its model. The exact definition is that all models are isomorphic to each other (3.3); but let us understand now that it both determines all properties of its model (values of first-order statements) and excludes non-standard models.
Arithmetic (the theory describing the system ℕ of natural numbers with four symbols 0, 1, +, ⋅ ) can be formalized as a complete theory in second-order logic (axioms listed in 4.3 and 4.4). The only component of this formalization beyond first-order logic is the axiom of induction, using a ∀ ranging over "all unary predicates" (including undefinable ones). However the incompleteness theorem (1.C) will refute the possibility for any algorithm to give the correct values of all first-order statements of arithmetic.

Axioms of equality

1. ∀x, x = x (reflexivity)
2. ∀A,∀x,y, (x = y ∧ A(y)) ⇒ A(x).

∀a,b, (∀x,y, R(a, b, x,y)) ⇒ R(a, b, a,b)

Diverse definitions of A give diverse statements (assuming reflexivity):

Remark. (1.∧7.) ⇒ 3., then 3. ⇒ (4. ⇔ 7) so that (1.∧7.) ⇔ (1.∧3.∧4.).
We shall abbreviate (x = y ∧ y = z) as x = y = z.

Defining new binders

(∀x, x = x) ∴ t = t ∴ ∃x, (x = t ∴ ...).

∀x, f(x) = t(x).

∀A, (Bx, A(x)) = F(A)

where = becomes ⇔ if values are Boolean. By second-order universal elimination, this comes down to a schema of definitions in first-order logic : for each defining expression for A, the expression (Bx, A(x)) is defined like a structure symbol, by the expression defining F(A), obtained by replacing A by its defining expression inside the expression F. So its available free variables are the parameters of F plus those of A.

Philosophical aspects of the foundations of mathematics

• First, 1.A to 1.C will explain this "time" as affecting model theory ;
• then, its role in set theory (clarifying the distinction of sets among classes) will be explored in 1.D, 2.A, 2.B, 2.C ;
• finally, a more detailed description in terms of ordinal analysis is given in a separate article, assuming familiarity with ordinals.

1.A. Time in model theory

The time order between interpretations of expressions

The interpretations of a finite list of expressions may be gathered by a single other expression, taking them as sub-expressions. This big expression is interpreted after them all, but still belongs to the same theory.
Now for a single expression to handle an infinite set of expressions (such as the range of all expressions of T, or just all terms or all statements), these expressions must be treated as objects (values of a variable). If T is a foundational theory, it can define (or construct) a system looking like this, so that, in any standard model of T (in a sense we shall specify later), this definition will designate an exact copy of this set of expressions.

The infinite time between models

• A Theory theory TT (and similarly a one-theory theory 1TT) itself made of successive groups of components which roughly follow the layers of the theory T it describes :
  • A description of "abstract types" and "symbols" ;
  • The described notions of "expressions" and "statements" ;
  • 1TT may be seen as the extension of TT by unary predicate symbols τ, L, X which respectively select the classes of components of T (its types, symbols and axioms) from the given ranges of "all available ones"; or only X if "types" and "symbols" in TT only meant those of the considered theory.
  • Proof theory extends 1TT by the notion of "proof", and thus also those of "theorem" and "contradiction". This may also be simply constructed from TT's notion of "proof" for logically valid statements, since a proof of a theorem amounts to a proof of logical validity of its implication from some axioms.
• A Systems Theory describing M by interpreting there the types and structure symbols of T given from 1TT (if the types list and the language of T are finite and explicitly given then the role of its one-system theory may be played by T itself; otherwise it involves the meta-notions of "types" and "structures").
• The description of the interpretations (attribution of values) of all expressions of T in M, for any values of their free variables; thus also, interpretations of all statements. This is needed to express M⊨T (the truth of all axioms of T in M) if the axioms list is infinite.

The metaphor of the usual time

Like historians, each mathematical theory can only «at any given time» describe a system of past mathematical objects. Its interpretation in this system, «happens» forming a mathematical present outside this realm (beyond this past). Then, describing this act of interpretation, means expanding the scope of our descriptions : the model [T,M] of 1MT, encompassing the interpretations of all expressions of T in the present system M of past objects, is the next realm of the past, coming once the infinite totality of current interpretations (in M) of expressions of T becomes past.

The strength hierarchy of theories

Many strengths will be represented by versions of set theory, thus letting us call "universes" these successive models. So, any set theory being meant as describing some universe of «all mathematical objects», this merely is at any time the current «everything», made of our past, while this description itself forms something else beyond this «everything».

Strengthening axioms of set theory

• Infinity (4.4) : there exists an infinite set, or equivalently a set ℕ of all natural numbers;
• The Specification schema amounts to generalizing the use of the set builder to unary predicates A defined using open quantifiers. But this amounts to recognizing the universe and other classes as kinds of sets (though not objects of any single kind) and hides the possible dependence of the result on the universe (range of all objects), which will often be conceived as variable (2.A). These oddities are usually limited by rejecting the set builder notation as inappropriate, leaving this as an axiom schema
  (∀A)∀_SetE, ∃_SetF, ∀x, x ∈ F ⇔ (x∈E ∧ A(x))
• Out of the scope of this introduction, the Collection schema implies the Replacement schema, which implies the Specification schema, with possible converses depending on other axioms.
• Powerset (2.7)

The main foundational theories

• Let us call Finite Objects theories (FOT) these 3 theories which are of the same strength:
  • First-order arithmetic (Z₁), reducing induction to an axiom schema by second-order universal elimination.
  • Finite Set Theory (FST), with Specification schema and negation of Infinity
  • Theory theory (TT).
• Several subsystems of second-order arithmetic, equivalent to versions of set theory featuring successively more elaborate results of ordinary mathematics (analysis...); Model theory (MT), which can interpret all expressions in all countable systems (= made of ℕ with any structures given as sets), is among the weakest of these.
• Second-order arithmetic (Z₂), formalizable as set theory with Infinity and Specification (does Replacement make it stronger ?), or (almost equivalently but in a different formalism) Infinity and the powerset of only ℕ;
• Mc Lane set theory, with Infinity and Powerset, is the comfortable one for most needs;
• Zermelo set theory is slightly stronger, with Infinity, Powerset and Specification.
• Zermelo-Fraenkel set theory (ZF) is much stronger, with Infinity, Powerset and Replacement; it implies Collection.

1.B. Truth undefinability

Standard objects and quotes

Non-standard models can be understood as extensions of the standard one: they still contain all standard objects, i.e. copies of objects of the standard model, defined as values of their mathematical quotes; but differ by having more objects beyond these, called non-standard objects (not quotable). Non-standard numbers will also be called pseudo-finite : they are seen by the theory as «finite» but with the schema of properties of being «absolutely indescribably large» : larger than any standard number, thus actually infinite.
In expressions of statements or classes of foundational theories, it usually makes no difference to allow finite-valued parameters (= whose type belongs to a FOT part of the theory) insofar as they are more precisely meant to only take standard values, and can thus be replaced by their quotes.

Truth Undefinability theorems

Let S be the meta-class of statements of T, and S the class defined in 1TT and thus in T to play the role of S in any model M of T. For any statement F∈S, its quote ⌜F⌝ designates in M the element of S playing the role of that statement : 1TT⊢ (⌜F⌝∈S).

Let S₁ be the meta-class of formulas of T with only one free variable (with range S but this detail may be ignored), meant to define invariant unary predicates over S. Now none of these can match the truth of statements in the same model:

Truth Undefinability Theorem (weak version). For any model M of T, the meta-class {A∈S | M⊨A} of statements true in M, differs from any invariant class, in M, of objects "statements":

∀C∈S₁, ∀M⊨T, ∃A∈S, M⊨ (A ⇎ C(⌜A⌝))

The tradition focuses on proving the strong version (details in Part 5) : the proof using the liar paradox provides an explicit A, defined as ¬C(⌜A⌝) where the quote ⌜A⌝ is obtained by an explicit (finitistic) but complex self-reference technique. So it gives the "pure" information of a "known unknown" : the necessary failure of C to interpret an explicit A "simply" made of ¬C over a complex ground term.

The hierarchy of formulas

For FST, the essential condition for a class to be a set is finiteness. Similarly in arithmetic, quantifiers can be bounded using the order : (∃x<k, ) and (∀x<k, ) respectively abbreviate (∃x, x<k ∧ ) and (∀x, x<k ⇒ ) and the same for ≤.
The values of bounded statements of FOTs, are independent of the model as their interpretation only involves standard objects. Any standard object of a FOT has all the same bounded properties (= expressed by bounded formulas with no other free variable) in any model.

Refined versions

• the strong version just lets A be ¬C with argument replaced by an explicit ground term (without binder but quite complex);
• the Berry paradox shows the existence of some A among statements which are TT-provably equivalent to big connectives over instances of C applied to diverse such terms (but simpler).

∃B∈S, C(⌜B⌝) ⇎ C(⌜C(⌜B⌝)⌝)

Truth predicates

1. ∀A∈X, C(A) i.e. it contains all axioms of T
2. ∀A∈S, C(A)∨C(¬A)
3. C is consistent.

2. ∀A∈S, C(A) ⇎ C(¬A)
3. C contains all logical consequences of any conjunction of its own elements.

1. Take all statements in an arbitrary order;
2. Add each to axioms if consistent with previously accepted axioms.

Properties of models

Yet the Completeness theorem, while simply expressed in set theories with Infinity, also appears in TT as a schema of theorems, which for any definition of a consistent theory, conceives a model as a class of objects with TT-defined structures. Our simple construction (4.6) ensures the truth of axioms and ignores other statements. By following it, all statements become interpreted as special cases of TT-statements (with parameters τ, L, X composing T, to be replaced by their definitions). The truth predicate so obtained on that class may not be TT-invariant, but is anyway MT-invariant provided that T was (as MT can define truth over the class of TT-statements).

But applying the Completeness theorem to a given truth predicate (which can be TT-defined), proves in TT the existence of a model whose properties conform to it, though its interpreted notions are not sets. This presents in 2 steps how to construct a model with TT-invariant properties, while the same goal is also achieved by the single but harder construction of the traditional proof (by Henkin) of the completeness theorem.

1.C. Introduction to incompleteness

Existential classes

• Any such ∃x, A(x) is equivalent to the halting of an algorithm that enumerates all x, interprets A on each, and stops when it finds A true there;
• The halting condition of any algorithm is an existential statement ∃t, A(t) where A(t) says it halts at time t (details are of course much more complex).

Provability predicates

• The truth of an existential statement (∃x, A(x)) implies its FOT-provability (by existential introduction over the quote of x), so both are equivalent;
• Any effective concept of theorem (class of provable statements s) of any theory in any framework, must be an existential class (∃p, V(p,s)) for some V(p,s) meaning that p is a valid proof of s.

1. Give a first-order theory with an existential class of axioms (usual ones, including all theories from our list, even have bounded definitions);
2. Apply there the concept of proof of first-order logic.

FOT (+ symbols τ, L, X with axioms) ⊢ ∀s, (∃p, V(p,s)) ⇔ (∃p, V'(p,s))

Conversely, if C is an existential class of "theorems" among first-order statements of a theory, and contains the first-order logical consequences of any conjunction of its elements (intuitively, the proving framework contains the power of first-order logic), then C is the class of T-provable statements by first-order logic, for some algorithmically defined first-order theory T : at least trivially, the theory which takes C as its class of axioms.

A theory T stronger than FOT will be qualified as FOT-sound if, on the class of FOT-statements, T-provability implies truth (in the standard model of FOT).

The diversity of non-standard models

Even with identical first-order properties (a condition we can adopt by taking as "axioms" all true statements from a given model, while this is not TT-invariant for standard models of theories containing TT), models can differ by meta-level properties : this will be seen for arithmetic in 4.7, and for any theory with an infinite model by the Löwenheim-Skolem theorem.
But truth undefinability implies that some constructed models also differ from the standard one by first-order properties, because of their invariance. This still goes for "almost complete" foundational theories (e.g. approaching a complete second-order theory by second-order universal elimination).

First incompleteness theorem

First incompleteness theorem. Any algorithmically defined and consistent theory stronger than FOT is incomplete.

A ⇒ (A is FOT-provable) ⇒ C(⌜A⌝)

• If T is complete (C(B)∨C(¬B)) then it proves its own inconsistency, i.e. C(⌜C(⌜0⌝)⌝).
• If T is FOT-sound, then C coincides with truth on all existential statements, thus on all C(A). So there exist T-undecidable C(A). Such C(A) is false but T-irrefutable, i.e. A is T-unprovable but this unprovability is itself T-unprovable.

Second incompleteness theorem

¬C(⌜0⌝) ⇒ ∀A∈S, ¬C(⌜¬C⌝:A)

Also equivalently, T cannot prove the existence of any truth predicate over a notion it describes as the set of its own statements. This is somehow explained, though not directly implied, by weak truth undefinability, which prevents using the current model as an example, since the truth over all standard statements there cannot be T-defined as any invariant predicate (not even speculatively i.e. only working in some models).

Proving times

• No limit to the expectable size of the smallest proof(s) (or example x such that B(x) for some bounded B) can be systematically expressed (predicted) just depending on the size of the theorem (or the size of B, beyond the smallest ones) : such proofs may be too big to be stored in our galaxy, or even indescribably big. (An example of statement expected to require a very big proof is given as object of Gödel's speed-up theorem).
• Undecidable (thus false) existential statements (∃x, A(x)) only have non-standard examples of x such that A(x); but these look very similar to the true case, as non-standard objects are precisely those appearing "indescribably big" in the non-standard model containing them (just extending the range of meant "describable sizes" to all standard ones).

In a kind of paradox, while the completeness theorem is proven by constructing (using actual infinity) a counter example (model) from the fact of absence of proof, there is no "inverse construction" which from the fact about infinities that no system can exist with given properties, would produce any finite witness that is its proof (which must nevertheless exist).
Instead, analyzing this construction can reveal that the size (complexity) of a proof roughly reflects the number of well-chosen elements that must be described in an attempted construction of a counter-example, to discover the necessary failure of such a construction ; the chosen formalization of proof theory can only affect the size of proofs in more moderate (describable) proportions.

1.D. Set theory as a unified framework

Structure definers in diverse theories

1. All such S belong to E
2. V can occur in the expression A and use x anyhow in its arguments. So V(x, x) is allowed, which is expected as 1. ensures the definiteness of any V(S, S).

In the construction (1.5) of a type K of structures defined by a formula A, a binder with range K abbreviates a successive use of binders on all the parameters of A. Here A and the interpreting model come first, then the range K of structures with its evaluator V are created outside them : A has no sub-term with type K, thus does not use V.

In set theory, the ranges of binders are the sets. Thus, beyond its simplifying advantage of removing types, set theory will get more power by its strengthening axioms which amount to accept more classes as sets.

• Keeping 1. and rejecting 2. will be shown consistent by Skolem's Paradox (4.7) but would be quite unnatural.
• Even weirder is NF ("New Foundations", so called as it was new when first published in 1937), combining 1. with a lighter version of 2. restricting the syntax of A to forbid occurrences of (x∈x) or any way to define it.
• The most extreme is lambda calculus, that keeps both points but tolerates the resulting contradiction by ignoring Boolean logic with its concept of "contradiction". This "theory" does not describe any object but only its own terms, seen as computable functions. As a computation system, its contradictions are computations which keep running never giving any result.

The unified framework of theories

Given a theory T so described, let T₀ be the external theory, also inserted in set theory, which looks like a copy of T as any component k of T₀ is the copy of an object serving as a component of T. In a suitable formalism, T₀ can be defined from T as made of the k such that Universe⊨ ⌜k⌝∈T, i.e. the value of the quoting term ⌜k⌝ interpreted in the universe belongs to T.
But there is no general inverse definition, of T from a T₀ with infinitely many components, as an object cannot be defined from a given infinity of meta-objects. Any infinite list of components of T₀ needs to fit some definition, to get the idealized image T of T₀ by interpreting that definition in the universe. (The defining formula must be bounded for T₀ to match the above definition from this T).

• Any T with an infinity of components also has non-standard ones; but T₀ only copies its standard components. Then a model of T₀ may fail to be a model of T by not fitting some non-standard axioms of T.
• T may be inconsistent while T₀ is consistent, due to a non-standard contradiction (may it use non-standard axioms or only standard ones). Such a T has no model in this universe, letting models of T₀ either only exist outside it, or also in it with the above described failure to be a model of T.

Set theory as its own unified framework

Zeno's Paradox

• the «closed» view, sees a reachable end;
  
• the «open» view ignores this end, but only sees the movement towards it, never reaching it.

As each generic theory can use binders over types, it sees types as wholes (sets) and «reaches the end» of its model seen as «closed». But any framework encompassing it (one-model theory or set theory) escapes this whole. Now set theory has multiple models, from a universe to a meta-universe (containing more sets : meta-sets, and new functions between them) and so on (a meta-meta-universe...). To reflect the endless possibilities of escaping any given universe, requires an «open» theory integrating each universe as a part (past) of a later universe, forming an endless sequence of growing realities, with no view of any definite totality. The role of this open theory is played by set theory itself, with the way its expressions only bind variables on sets.