Recently I have been reading Kleene's *Introduction to Metamathematics* and have found his descriptions of the various foundations for mathematics exciting.
I am excited not only to find such well written descriptions of the methods of metamathematics, but also to find another mathematician whose beliefs appear to be quite close to my own, at least in his description of metamathematics.
I do not claim to know to what extent his beliefs about non-mathematical things are in line with my own as I have found through experience that a mathematicians beliefs about mathematics, though they should logically have a strong influence on their beliefs about non mathematical things, tend to have a sporadic impact if any on their non-mathematical beliefs.

His text has been inspiring both because of its clear descriptions of formal mathematics in a way which is much more prescient than the others that I have read, and noticeably accessible in its accommodations of a wider scope of investigation into intuitionistic logic, and because of its support of my belief that there must be greater effort put into describing the mechanics of mathematics, that is the details of the actions which are themselves mathematical.
Specifically, the recognition that to the formalist the objects of mathematics are certain texts which represent a formal description of some area of mathematics without appealing to the meaning that is usually attached to the objects described by the formalism.
As much as mathematics is meant to discover things which are timelessly relevant it would seem the formalists have made a key observation which will persist, in some form, for at least the next century if not the next millennium.

Unsurprisingly, while I've been reading Kleene's IM I have been comparing its observations to Bourbaki's *Theory of Sets*.
Much of the criticism of the work of Bourbaki is focused on its Hilbertian foundations.
There are also those who dislike that Bourbaki only mildly mentions the work of Gödel, Kleene, Bernays, Cohen, Church, Schoenfield, Tarski, Brower, Gentzen, Skolem, and all the other mathematicians, logicians, and mathematical logicians who have contributed to our modern understanding of the foundations of mathematics.

The claim that Bourbaki's Theory of Sets is Hilbertain is strict in that it uses a form of Hilbert's Epsilon Calculus as its logical foundation.
Instead of using Hilbert's \(\epsilon\) notation, Bourbaki uses a distinct \(\tau\) and \(\square\) notation with linkages.
Informally, if \(R(x)\) is a relation and if there is an object which satisfies the relation \(R(x)\) when substituted for \(x\) then \(\epsilon x R(x)\) represents such an object, otherwise \(\epsilon xR(x)\) is a thing about which nothing meaningful can be said.
Again, this vague description is not meant to be anything other than an informal description.
I do not yet know enough about the development of Hilbert's epsilon calculus to make a formal comparison between its use in his program, and its use in Bourbaki's theory of sets.

Though I am not deeply familiar with Hilbert's epsilon calculus in general, I am familiar with the logic of Bourbaki, and find it interesting that the logical symbols \(\tau\) and \(\square\) are used, together with an informal notion of substitution, to define the existential and universal quantifiers.
Additionally, the modern role of the axiom of choice is reduced entirely to certain statements involving the \(\tau\) notation.
This is yet another point of contention with most modern mathematical logicians, as some believe this method "hides" the use of the axiom of choice in the formal language rather than as an additional axiom on a footing equal to the pairing axiom or power set axiom.

As far as Bourbaki is concerned, the purpose of their description of formal mathematics is to avoid circumlocutions leading up to their development of their theory of sets.
Bourbaki does not set out to show how their theory of sets sits among the differing foundations of mathematics, they simply wish to get as quickly as possible to a description of sets so that they can proceed with their treatment of the rest of modern mathematics.
Said another way, it is not the purpose of Bourbaki to formalize mathematics, but rather to present it as being describable using the basic notions of set theory.
The belief that mathematics may be almost entirely based on set theory is often given the hyperbolic name "Cantor's Paradise" so as to give credit to Cantor's independent discovery and creation of the precursors to modern set theory.

It is admitted by Bourbaki that their informal goal is to use set theory as a way of classifying and organizing modern mathematics.
Specifically, the final chapter of *Theory of Sets* is entitled *Structures* and the second section is entitle *Species of Structures*.
Though the definition of structure is given formally, it includes the formal language of set theory developed earlier in the book.
The basic idea is that a structure is an element of some set which is built from the fundamental constructions permissible in Bourbaki's set theory.
For example, within the classical theory of sets a topology \(\mathcal{T}\) on a set \(X\) is a collection of subsets of \(X\) which satisfy two relations:

- if \(\mathcal{U}\) is a subset of \(\mathcal{T}\) then \(\bigcup \mathcal{U} \in \mathcal{T}\); and
- if \(\mathcal{U}\) is a finite subset of \(\mathcal{T}\) then \(\bigcap \mathcal{U} \in \mathcal{T}\).

Thus, a topology on a set \(X\) belongs to \(P(P(X))\), the power set of the power set of \(X\).
Furthermore, the collection of all topologies on a set \(X\) is a subset of \(P(P(X))\) whose members satisfy these two topological relations.
Consequently, the set of all topologies on a set \(X\) is a unique member of \(P(P(P(X)))\), so that what it means to be a topology on \(X\) is governed in part by a specific set of axioms and membership to a set constructed from \(X\) by iterating the power set operation.

A somewhat simpler example is the structure of relations on a set, which are completely described by being a member of the cartesian product of the set under consideration.
That is, a relation on a set \(X\) is a member of \(X \times X\) and the collection of all relations on a set \(X\) is \(P(X \times X)\).
So that \(R\) is a relation on a set \(X\) if and only if \(R \in P(X \times X)\).
Here it is clearer that what it means to be a relation, or what the structure of a relation is, on a set \(X\) is characterized by the construction of the power set of the cartesian product of \(X\) with itself.

So the species of structures which are examined in mathematics are, as is assumed by Bourbaki, of this form.
Each species of structure has some set or collection of sets as its base, like \(X\) in the previous two examples, and may be specified by writing down to which set constructed from \(X\) the structure belongs as well as the basic axioms that the structure must satisfy.

Much of the detail has been removed from this informal description, and modern mathematicians have continued to develop these ideas, though it still seems that the notion of structure is meaningless outside of a formal description of mathematics.
The modern notion of structure has been taken back from the theory of sets by the model theorists (and universal algebraists) so as to not only permit varying structures of set theory, but also provide a more comprehensive framework for structures describable using a formal language which might not contain a theory of sets.
In this context, specifically the model theoretic, a structure is more commonly referred to as an interpretation.

This push towards the logical foundations of mathematics brings me back to my interest in Kleene's IM.
Though Shoenfield's *Mathematical Logic* is considered the modern introduction to mathematical logic, Kleene's IM, as well as his own *Mathematical Logic* which may be bought as a Dover book, is a much slower and digestible than Shoenfield's terse and dense book.
Both are beautiful and for those interested in modern mathematical logic the two texts, Kleene's IM and Shoenfield's ML, are required reading.
One important component of Kleene's IM which is sadly missing from Shoenfield's ML is Intuitionistic Logic.
Kleene gives a description of the three most well known approaches to the problem of finding a foundation for mathematics: the logicists of which Russell and Whitehead are the principle members, the formalists of which Hilbert is most well known, and the Intuitionists of which Brouwer is the most well known.

Though each school of thought is based on a differing set of beliefs each shares some characteristics with the others.
In particular, the use of formal languages may be identified across each school.
Though, it is interesting to note that Gödel's monumental paper *On Formally Undecidable Propositions of Principia Mathematica and Related Systems* is rooted in his recognition that the logical mechanisms employed by Russell where not formally described, and that once they were certain questions of consistency and completeness naturally arose.
Russell's description of mathematical logic was of a decidedly philosophic nature, occasionally relying on informal descriptions rather than formal syntactic rules, as he believed that his foundation of mathematics was a description not of a philosophic ideal, from Plato, but rather a tool for describing that section of philosophic logic which results in our modern study of mathematics.
His thesis, that mathematics is reducible to logic, is often misunderstood as referring to the modern use of formal texts to describe mathematics.
Rather, Russell would clearly identify formal texts as being part of mathematics, and the type of thing which must ultimately be justified from a philosophically defendable position, one which necessarily requires the acceptance of some metaphysic and logic which itself need not be a formal mathematics.

The distinction between the formal and informal components of mathematics is expertly revealed in Kleene's IM.
It is the principle reason his exposition is so familiar to modern mathematical logicians.
The study of metamathematics is the formal study of formal mathematics, which, apparently, requires the use of informal mathematics.
The use of certain fundamentally informal mathematical notions forms the center piece of Brouwer's intuitionism, wherein he believes that the only mathematical arguments which are admissible are those which are supported by a sort of informal acquaintance with certain features of the natural numbers.
One of these informal notions is that one can not realize a completed set of natural numbers.
Thus a proof of a statement "for all natural numbers \(n\) it is that \(P(n)\)" where \(P(n)\) is some statement about natural numbers, must proceed without the assumption that there is a collection of all those natural numbers \(n\) for which \(P(n)\) is true and a collection of all those natural numbers for which \(P(n)\) is false, otherwise these joint collections would entail the realization of the whole collection of natural numbers.
This excludes the use of the classical proof by contradiction which presupposes the existence of such sets.
That is, such a proof requires you to accept that \(P(n)\) is "already known to be true or false" of each natural number, something which Brouwer rejects.
Obviously these descriptions are informal, hence the value of Kleene's IM.

Kleene's metamathematics gives a framework for dealing not only with classical logics, but also those of the intuitionistic variety.
This process is exactly analogous to that employed in the discovery and description of non-Euclidean geometries.

In the future I hope to provide clear and exact descriptions of these informal reflections.
The tools for such an exposition appear to be in Kleene's IM and, if not, will likely be found in Shoenfield's ML.