Usually these are called "transfinite numbers". According to https://en.wikipedia.org/wiki/Transfinite_number, the term "transfinite" was coined by Cantor, who distinguished between "absolutely infinite" and merely transfinite, and sometimes reserved the term 'infinite' for 'absolutely infinite'. But nowadays most people call the transfinite numbers infinite, so we have two words that mean the same thing (transfinite and infinite).

There's the cardinals or 'cardinal numbers'. These are probably what you are thinking of when you think of a 'number'. Intuitively, a cardinal number is telling you how many of something there is. Two sets are defined to have the same cardinality if and only if there is a bijection between them (this property is called 'equinumerosity'). Now the cardinal numbers are the equivalence classes w/r/t equinumerosity. So each finite integer is a cardinal number. The absolute value notation (two vertical bars surrounding something) is often used to mean "the cardinality of"; e.g.

X | can be read "the cardinality of X", but this is ambiguous with absolute value; sometimes "card(X)" is used instead. |

The infinite cardinal corresponding to the cardinality of the natural numbers (that is, the size of the set of all natural numbers) is called aleph-naught or aleph-null, where 'aleph' is the name of a special symbol (see https://en.wikipedia.org/wiki/Aleph_number#Aleph-naught for a picture).

There are other distinct sets with the same cardinality as the natural numbers. For example, the integers, and the rationals (see below). The term 'countable set' is defined to be any set with the same cardinality as some subset of the natural numbers (some authors use 'countable' to mean only the countably infinite sets, that is, to exclude finite sets). This makes sense because if a set S is countable, that means that there is a bijection between S and some subset of the naturals, which means that there is a surjective function from the naturals to S, which means that you can 'count' starting with 1, 2, 3, .., and at each step you can produce an element of S, and eventually you will reach any given element of S. In other words, you can order the elements of S in such a way so that you can count them, and if you had infinite time to count up to the aleph-naught, then you would hit all of the elements of S. Another way of saying this is that any countable set can be indexed by the natural numbers.

Because the notion of bijection is used to define cardinality, there are some unintuitive results. The cardinality of the positive integers is the same as the cardinality of the naturals, even though the integers have 0 and the naturals don't. You can see this by constructing a bijection; 1->0, 2->1, 3->2, .... Notice that all the naturals appear on the left, and all the integers appear on the right. The cardinality of all of the integers is also the same; 1->0, 2->1, 3->-1, 4->2, 5->-2, etc.

Similarly, the cardinality of the odd natural numbers is the same as the cardinality of all of the natural numbers. You can see this by constructing a bijection; 1<->3, 2<->5, 3<->7, ...; you can count through the naturals on the left and hit all of the odds, or you can count through the odds on the right and hit all of the naturals.

Similarly, the cardinality of all pairs of naturals is the same as the cardinality of all of the naturals. In fact, for any natural number k, the cardinality of the set of all k-tuples of naturals is the same as the cardinality of all of the naturals. The bijection is to represent, for example, the sequence [1,8,2,2,4] as 1^1 * 8^3 + 2^5 + 2^7 + 4^11. That is, we create the number whose factorization encodes the sequence by setting the multiplicity of each prime factor to an item in the sequence (the https://en.wikipedia.org/wiki/Fundamental_theorem_of_arithmetic tells us that each natural number has a unique factorization into prime factors). This bijection is sometimes called https://en.wikipedia.org/wiki/G%C3%B6del_numbering_for_sequences .

Because rationals are equivalence classes over pairs of natural numbers, we can encode the rationals as pairs and then observe that they are countable. Since the natural numbers can be embedded within the rationals, there must be infinitely many rationals, therefore their cardinality is the same as the naturals.

See https://en.wikipedia.org/wiki/Hilbert%27s_paradox_of_the_Grand_Hotel

If math made any sense then there would be only one kind of cardinal infinity, but it doesn't. A set that is not countable is called uncountable (and an uncountable set is always infinite). Cantor proved that there exist cardinal numbers bigger than aleph-naught; the theorem is called the 'diagonal theorem' and the technique he invented and used is called 'diagonalization'.

Cantor's diagonal proof in particular shows that the cardinality of the real numbers is strictly greater than the cardinality of the natural numbers; that is, it shows that there does not exist any bijection between the natural numbers and the reals. In other words, there is no way to order the reals so that you can count them one-by-one in order and hit all of them; there is no way to index all of the reals by natural numbers.

(One version of) the proof goes like this. Proof by contradiction: assume that the conclusion is false, that is, that you can index all of the reals by natural numbers. That means that you have an (infinitely long) table with two columns; in each row, the left column has a natural number, and the right column has a real number. Going down the left columns, the natural number appear in order, 1, 2, 3, ... . Going down the right column, let's define a notation for the reals that appear; call them r_1, r_2, r_3, ... . Now, we will construct a real number R that does not appear anywhere in the right-hand column. We will construct R via specifying each digit in its decimal expansion. To the left of the decimal point, R is zero. To the right of the decimal point, each digit of R depends on a different row.

We set the first digit to the right of the decimal point of R to be equal to (the first digit to the right of the decimal point of the decimal expansion of r_1) + 1, except that if (the first digit to the right of the decimal point of the decimal expansion of r_1) is 9, then we wrap back to 0.

We set the second digit to the right of the decimal point of R to be equal to (the second digit to the right of the decimal point of the decimal expansion of r_2) + 1, except that if (the first digit to the right of the decimal point of the decimal expansion of r_1) is 9, then we wrap back to 0.

And so on.

(by the way, the next step of the proof as i describe it here is actually wrong; there's a problem because of things like .99999... repeating equals 1. i won't go into the fix, but see here if you care: https://en.wikipedia.org/wiki/Cantor%27s_diagonal_argument#Real_numbers )

Now, it remains to be shown that R is not equal to r_i for any i. It's not, because if it were, then the decimal expansion of R would be identical to r_i in every digit. But, by construction, it differs at digit i after the decimal point. The figure at the top of https://en.wikipedia.org/wiki/Cantor's_diagonal_argument helps:

Diagonalization is in general good for showing that some set of things is not all-encompassing, and it is also used to show that the halting problem is uncomputable, and therefore that there exists mathematically definable functions for which there exists no algorithm to compute them. The general idea of diagonalization is to show that the type of object which is not contained in some domain can be broken into at least as many parts as there elements in the domain which does not contain it, and then for any putative bijection between elements of the domain and uncontainable objects, to construct an object which is not in the bijection by making it different from each of its peers in at least one part.

todo most reals are irrational. most reals are undefinable. most reals are uncomputable.

Another cardinality-related use of diagonalization shows that power sets can be used to increase cardinality. More generally, one can start with any set S and take the 'power set' P(S) of that set, that is, the set of all subsets of that set. A diagonalization argument called "Cantor's theorem" can be used to prove that the cardinality of the power set of any set is strictly greater than the cardinality of the original set.

The proof goes like this. Proof by contradiction: assume that there is a bijection between S and P(S). This implies there is a surjective function f from S to P(S). We will show that no function f from S to P(S) can be surjective. It suffices to construct, for any function f from S to P(S), an element p of P(S) which is not in the image of f.

Recall that elements of P(S) are subsets of S. Therefore, p is a subset of S, and for any element x in S, f(x) is a subset of S. Take p to be the following subset of S: the set of every element x in S such that x is not in f(x).

It remains to be shown that p is not in the image of f, that is, there is no element y in S such that f(y) = p. For any element y in S, either y is in f(y), or it's not. If y is in f(y), then by the definition of p, y is not in p. In this case, because y is in f(y) and y is not in p, p must not be equal to f(y). On the other hand, if y is not in f(y), then by the definition of p, y is in p. In this case, because y is not in f(y) and y is in p, p must not be equal to f(y). So in either case, for any y, p is not f(y).

Beth-naught (see https://en.wikipedia.org/wiki/Beth_number for a picture of the Beth symbol), is defined as equal to Aleph-naught. Beth-one is equal to the powerset of Beth-naught. Beth-two is equal to the powerset of Beth-one. And so on. By Cantor's theorem, the Beth numbers form a strictly increasing sequence.

Another name for Beth-one is "the cardinality of the continuum".

Beth-one is also the cardinality of the set of all continuous functions from reals to reals. But the set of all functions, not necessarily continuous, from reals to reals is of cardinality Beth-two.

The aleph numbers are used to represent the cardinals. Like the Beth numbers, they are written alpha-i, where i is some ordinal.

not sure about this part: Aleph-one is be defined as the next larger well-ordered cardinal after aleph-naught. Aleph-two is defined as the next larger well-ordered cardinal after aleph-one. Etc.

An alternate characterization of aleph-one is the cardinality of the set of all countable ordinal numbers (see below). From the ZF axioms (without AC), it can be shown that this implies that there are no cardinals which are simultaneously larger than aleph-naught but smaller than aleph-one.

Just as cardinals are the equivalence classes w/r/t the equinumerous relation, ordinals are the equivalence classes w/r/t the order isomorphic relation.

The order isomorphic relation is strictly stronger than the equinumerous relation. Two sets are defined to be order isomorphic if there is a bijection f between them such that x <= y iff f(x) <= f(y).

todo the basic order types at the beginning of https://en.wikipedia.org/wiki/Ordinality

The order type of the natural numbers is w, written as lowercase omega (and pronounced omega).

see https://en.wikipedia.org/wiki/Ordinality

maybe see https://sites.google.com/site/largenumbers/home/a-1/infinite_numbers , but i have found at least one error in that page (the power set of aleph null is indeed the cardinality of the real numbers; the question he is probably thinking of, the continuum hypotheses, is whether or not there are any other cardinals which are greater than aleph null but less than the powerset of aleph null, or in other words, is aleph one is equal to the powerset of aleph null)

""indefinitely far" is exactly what ordinals are good at: basically every time one says "and so on" when enumerating ordinals, it defines a larger ordinal" -- [1]

Links:

links:

- http://stanford.edu/~jbooher/expos/ordinals_promys.pdf
- https://people.maths.ox.ac.uk/knight/lectures/ordinals.pdf
- http://euclid.colorado.edu/~monkd/m6730/gradsets04.pdf
- http://planetmath.org/ordinalarithmetic
- http://math.stackexchange.com/questions/627291/easy-visualizations-of-small-countable-ordinals
- http://ncatlab.org/nlab/show/ordinal+number

In naive set theory (see https://en.wikipedia.org/wiki/Na%C3%AFve_set_theory ), the set of all sets is a set, and you can construct sets by starting with the set of all sets and then imposing a filter condition to create a subset.

Consider the set of all sets which are not members of themselves. Is this set a member of itself?

If it is, then it shouldn't be, by it's definition as the set of all sets which are NOT members of themselves.

But if it isn't, then it should be.

See https://en.wikipedia.org/wiki/Russell_paradox .

There is no largest cardinal number.

And therefore, you can't have a set S of all cardinal numbers. For if you did, then, following https://en.wikipedia.org/wiki/Cantor%27s_paradox#Statements_and_proofs , let T be the union of the elements of S. Then every element of S is a subset of T, and hence is of cardinality less than or equal to the cardinality of T. Cantor's diagonalization theorem then implies that every element of S is of cardinality strictly less than the cardinality of 2T.

See https://en.wikipedia.org/wiki/Cantor%27s_paradox .

Let S be the set of all ordinals. S is an ordinal itself. Therefore we can construct its successor S + 1, and S < S + 1. But since S is the set of all ordinals, (S + 1) is an ordinal, so (S + 1) must be in S. But then we have S + 1 < S. S + 1 < S and S < S + 1 cannot both be true, so we have a contradiction.

(note: this only works as written if ordinals are defined the von Neumann way. Otherwise, see https://en.wikipedia.org/wiki/Burali-Forti_paradox#Stated_more_generally for a more general statement)

Generally by something similar to stratification, e.g. stratifying the conceptual universe into levels of reference and disallowing the construction of things that refer to other objects on their same level.

In traditional ZFC set theory (see below), we construct axioms for sets that do not allow you to construct a set of all sets. However, we still say that there is a 'class' of all sets. Every set is also a class, but not every class is a set. A class that is not also a set is called a 'proper class'. The class of all sets is a proper class. You can do the same sorts of things with classes that you can do with sets, for example, there is a predicate 'memberOf' that tells you whether some object is a member of a class.

In my opinion this isn't a very intuitive way to handle things, but i haven't ever had time to try to come up with anything else.

It seems to me that people tell you that the notion of 'set' is both (a) a formalization of the notion of grouping or collecting or aggregating things together, and (b) a formalization of the notion of a type of thing.

For an example of (a), if you own five chickens, you might consider the set of your five chickens. For an example of (b), you might consider the set of all humans.

I don't think either of these is correct. If 'set' were a formalization of (b), then you would be able to construct the set of all sets. If 'set' were a formalization of (a), then we would expect that anytime we find an object that behaves like a grouping, it should be a set. But proper classes behave like groupings. So if 'set' were a formalization of (a), then every class would also be a set.

Therefore, i think that the concept of 'set' as defined in ZFC axiomatic set theory is neither a formalization of (a) nor of (b). Sets are a particular subtype of the notion of a type of thing; and sets are a particular grouping of some things; and they are a formalization of the notion of grouping where the domain is restricted to certain things; but they are not a formalization of the very notion of a type of thing, nor are they a formalization of the very notion of groupings of things.

The current standard foundational axioms are ZFC set theory (ZFC stands for Zermelo–Fraenkel? plus the axiom of Choice)

Today it's generally accepted, but there was and still is some controversy over the axiom of choice. Often you see results that use the axiom of choice note that it was used.

Troublingly, it is not known if ZFC is consistent.

Sometimes abbreviated AC.

AC is independent of ZF, that is, of Zermelo–Fraenkel? set theory.

If the axiom of choice is assumed, then:

- the class of cardinal numbers is totally ordered
- the next larger well-ordered cardinal is equal to the next larger cardinal

If the axiom of choice is not true, then there may be:

- cardinals larger than aleph-zero but incomparable with aleph-one

Arguments for:

- todo

Arguments against:

- it is incompatible with https://en.wikipedia.org/wiki/Axiom_of_determinacy

A weaker version of the axiom of choice is the https://en.wikipedia.org/wiki/Axiom_of_countable_choice , which is also independent of ZF. The axiom of countable choice is sufficient to imply that Aleph-naught is smaller than any other cardinal.

If the axiom of countable choice is NOT assumed, then it is possible that Dedekind-infinite sets (sets for which a proper subset of the set may be put into bijection with the whole set) may not be equivalent to infinite sets as defined as "a set that cannot be put in bijection with any finite ordinal". The axiom of equivalence of Dedekind-infinite sets with infinite sets is strictly weaker than the axiom of countable choice. See https://en.wikipedia.org/wiki/Dedekind-infinite_set .

Is aleph-one equal to beth-one? That is, are there any well-ordered cardinalities in between the cardinality of the naturals and the cardinality of the reals?

Godel and Cohen established that this is independent of the ZFC axioms.

Arguments for:

- todo

Arguments against:

A weaker version of the continuum hypothesis is https://en.wikipedia.org/wiki/Martin%27s_axiom .

A stronger version of the continuum hypothesis is the generalized continuum hypothesis (GCH), which states that for all i, Aleph-i is equal to Beth-i. The generalized continuum hypothesis is independent of ZFC, but it does imply AC. GCH is true in the constructive universe. "GCH implies that every cardinality n is smaller than some Aleph number, and thus can be ordered". See https://en.wikipedia.org/wiki/Continuum_hypothesis#The_generalized_continuum_hypothesis .

https://en.wikipedia.org/wiki/Constructible_universe

https://en.wikipedia.org/wiki/Von_Neumann_universe

https://en.wikipedia.org/wiki/Grothendieck_universe

Many alternative mathematical foundations are motivated by a philosophical conviction that classical mathematics allows one to talk about impossible objects, and/or that it makes unwarranted assumptions. An alternative foundation often restricts the expressiveness of the language or the power of logic to prevent this. For example, in constructivist mathematics, you can't talk about objects that you can't construct and/or you can't form non-constructive proofs. In intuitionistic logic you can't use the law of the excluded middle (that is, you can't conclude that not(not(x)) -> x) (i think this turns out to be related to constructivism). In computable mathematics you only talk about computable sets.

(todo: compare/contrast intuitionist vs constructivist; are they the same thing or different or subsets of one another? i'm not sure)

Reverse mathematics is the enterprise of starting with some non-standard approach to the foundations of mathematics, and seeing which theorems of classical mathematics still hold in your non-standard approach. More generally, reverse mathematics seeks to characterize, for various interesting theorems, which axioms and constructions are minimally sufficient for proving that theorem. See also http://en.wikipedia.org/wiki/Reverse_mathematics , http://plato.stanford.edu/entries/hilbert-program/#1.3 , http://www.math.psu.edu/simpson/talks/banff0812/talk.pdf

If this seems silly to you, consider how much time and effort in classical mathematics is devoted to understanding things like the relationship between various kinds of infinity and how these relationships change based on the presence or absence of axioms which no one can agree on whether they are false or true, and which can be proven to be unnecessary for any use except for talking about infinite things.

Mathematics has a problem, or at least an annoying issue. Imagine that one day, people started thinking about the natural numbers; simple enough to imagine, and to visualize. Now add the rationals; still simple enough to imagine, and to visualize. And then one day they start thinking about 2-D. And then we start thinking about distances between points in 2-D. This is all very fundamental stuff that has a clear and certain connection to reality, wouldn't you agree?

What is the distance between the points (1,1) and (0,0)? This is the same as the length of the third side of the triangle defined by vertices (0,0), (0,1), (1,1). By the Pythagorean theorem, since this is a right triangle, and the length of the other sides are each 1, we have x * x = 2, where x is the distance between (0,0) and (1,1).

So the distance between (0,0) and (1,1) is provably irrational (see http://en.wikipedia.org/wiki/Square_root_of_2#Proofs_of_irrationality ).

So, okay, we want our concept of the number line to include any possible distance, right? So we'd better add sqrt(2) in there, and all of the other square roots. And if we calculate distance in 3-D, we'll find that we have to add in cube roots too, and so on up to n-th roots (and of course we want it to be closed under all basic arithmeticial operations). So now our number line consists of the simple algebraic numbers (not sure if that is a frequently used term, I saw one or two people on Google calling it that), that is, all numbers that can be obtained from the integers using a finite number of integer additions, subtractions, multiplications, divisions, and taking nth roots (where n is a positive integer).

Well gee, let's take a closer look at that thing we wrote above, "x * x = 2". Y'know, you can visualize this by graphing a function "f(x) = x*x", and seeing when it hits 2. Actually, you could also just displace it, and graph the function "f(x) = x*x - 2", and see when it hits zero. In fact you could make up lots of functions, using just the arithmetical operations of addition, subtraction, multiplication, and exponentiation, and see when they hit zero. If we restrict the second argument of the exponent to integers, then these functions are polynomials, and the places where they hit zero are their roots.

If we consider all of the roots of all of the polynomials (but only for those polynomials that "have roots", that is, when if we draw the function we see it intersect the horizontal axis somewhere), some of them are not "simple algebraic numbers" as defined above. This is proven by Galois theory. It seems sensible to want all of the roots of all of the polynomials which have roots in our number line, because the root of some function in our graph can be clearly visualized and so seems to have a clear and certain connection to reality. Now we have the "real algebraic numbers" (note: this is not yet the algebraic closure over the rationals, because we do not yet have any complex numbers).

Note: Wikipedia tells me that "The set of real algebraic numbers is linearly ordered, countable, densely ordered, and without first or last element, so is order-isomorphic to the set of rational numbers.". So the real algebraic numbers are still pretty comprehensible.

Great, now let's consider circles. What's the circumference of a circle of radius 1? 2*pi. It can be proved that this is not an algebraic number (see http://en.wikipedia.org/wiki/Lindemann–Weierstrass_theorem#Transcendence_of_e_an ). We call real numbers that are not algebraic numbers "real transcendentals". So we have at least one transcendental that has a clear and certain connection to reality.

OK, these numbers are getting pretty annoying to write down. We have all these numbers that are at some precise spot on the number line, but that we can only talk about it terms of some weird definition. Can't we represent pi in terms of numbers and operations that came before it? Well, no, we can't, that's the whole point. But wait.. we can approximate it. The Gregory–Leibniz? series (see http://en.wikipedia.org/wiki/Leibniz_formula_for_%CF%80 ) approximates pi by adding and subtracting rationals. If you could somehow do this forever, you'd reach pi. In fact, if you desire an approximation to pi which is no farther away from pi than any given distance that you choose, you can find one in finite time. Maybe we can just think in terms of the rational numbers, and in order to talk about pi, we can invent a new concept, "limit", and we can just say that pi is the "limit" of this process of approximating it.

Even if we did that, it would still be annoying to write all these numbers down, so put that thought on hold for a minute. If we draw numbers on the number line, we can easily see that this one is to the right of that other one and to the left of this third one, and that it is farther away from the that one and closer to this one, etc. Wouldn't it be nice to have a notation that is more like that picture, and less like "here's a number that is the root of 'x^2 - 2'; here's a number which is '0.5*the circumference of a circle of radius 1'"?

So we invent decimal notation. Great, pi = 3.1415... Now i can easily see and remember that sqrt(2) < pi < 4, and i can easily keep track of how far apart they are. This seems pretty concrete, right? Seems to be connected to reality? Of course, you can't actually write out pi this way. But you can get closer and closer... and if you could go on like that forever, you'd reach pi. So, great, for all practical purposes the decimals can represent everything. In fact, let's just redefine everything in terms of decimals and limits.

It turns out that if you add limits to a number line to produce a new number line (called the "completion"), then you get the real numbers whether you start with the rationals or the decimals (see http://en.wikipedia.org/wiki/Construction_of_the_real_numbers ). So, it seems pretty sensible to have our number line be the reals. (note: the etymology of the name 'real' appears to be as a label used by Descartes in the 17th century to distinguish 'real' solutions to polynomials from 'imaginary' ones [2])

The theory of the reals is closely related to http://en.wikipedia.org/wiki/Second-order_arithmetic and http://en.wikipedia.org/wiki/Mathematical_analysis (the word "analysis" is applied to other 'realish' things too such as http://en.wikipedia.org/wiki/Analytic_function ).

Right? That's connnected to reality, right?

Well, maybe not. Once you have the reals you get all sorts of non-intuitive results. You have uncountable cardinality; an infinity of an infinity. In fact, because the cardinality of finite strings over a finite alphabet is countable, and because any actual written description of a real number is of this form, this means that most real numbers cannot even be described. Consideration of basic properties of cardinality, given that uncountable cardinality exists, leads to controversies such as the axiom of choice and the continuum hypothesis. The reals lead to all sorts of counterintuitive results (todo, give some examples). Today, the most popular set theory devised to deal with them (ZFC) hasn't been proved consistent and past versions had to be revised a few times due to all sorts of paradoxical inconsistencies, giving rise to the fear that if it looked good but turned out to be wrong before, and if we can't prove it's consistent now, then maybe it's still wrong.

"God made the integers, all the rest is the work of man" -- Kronecker

Maybe things are just complicated. Or, maybe we made a mistake when we decided to think about infinite objects as if they were real, and we should just throw out all that. Maybe since something infinite is impossible, it's no wonder that we get all sorts of paradoxes when we analyze them. This viewpoint is finitism.

But dang it, it's easier to write things using decimal notation, and easier to prove things using limits, and it's easier to THINK about trancendentals as limits of decimal expansions. Maybe, really, all there are are finite things, but infinities and limits and such can be a convenient notational shorthand for verbose statements about finite things. Maybe infinities are just notational plumbing for thoughts about finite things, and it'll be complicated to work out this plumbing, but once we do, it'll be done and we can go back to studying finite things, and we'll have a guarantee that we can use the language of infinity, while being confident that philosophical controversies about the nature of infinity won't change mathematical results about finite things (see http://en.wikipedia.org/wiki/Conservative_extension ).

So that's where we were sometime in the early 1900s. To skip ahead and tell you where we are now, this programme was first incarnated as "Hilbert's programme", which was shown to be unachievable; but some people are still working on a number of distinct, distant variants of it; as one might suspect, even understanding what those variants are and what the differences between them are, is very complicated; however, if one of them eventually succeeds and takes over in the distant future, maybe it'll make mathematics simpler for future mathematicians by not having to constantly deal with all these paradoxes caused by infinities.

If one takes the Platonic view that these strange objects actually exist in some sense, then propositions relating to them are either true or not. This assumption then allows the use of mathematical tools such as the law of the excluded middle, non-constructive proofs, quantification over them, etc. However, if one is uncertain of their existence, then one might want to be more careful, and consider that some propositions relating to these supposed entities might just be incoherent/invalid, rather than valid propositions which are either true or false.

random paper on Feferman's philosophy: http://math.stanford.edu/~feferman/papers/Logic_Math_ConceptStructuralism.pdf http://math.stanford.edu/~feferman/papers/CategoricityOpenEnded.pdf

In the classical approach, difficult-to-understand concepts end up leaking into "ordinary" math and forcing every serious student of mathematics to come to grips with them. In some sense, this means that in order to do mathematics the conventional way, you have to spend a lot of time understanding theorems about "impossible" things. You also might end up studying questions whose relevance to the real world is in doubt (eg Does mathematics need new axioms? by Feferman claims that one impetus for the exploration of new axioms that assert the existence of various infinite cardinals is resolution of the Continuum Hypothesis, which Feferman feels "is an inherently vague problem"; see also [3]). Unlike much of 'ordinary' math, there is disagreement among experts as to which assumptions regarding the "impossible" things are valid (eg the existence of various large cardinals; eg the continuum hypothesis). (note however that historically there were similar disagreements in ordinary math, eg i think the existence of negative numbers, complex numbers used to be controversial).

You can see how one might conclude that these concepts might be merely artifacts of our way of talking about math, and that given this doubt, it would be better to restructure mathematical discourse so that you don't have to think about them very much unless you want to. In other words, I am proposing the without taking a position on the correctness of alternative mathematical foundations, one might want them for the practical reason of simplifying the learning of mathematics (since mathematics is too large to be learned by any one person in one lifetime, and hence professional mathematicians are always learning, simplying the learning of mathematics should be useful not only to undergraduates but also professional mathematicians).

On the other hand, if the object is only to save the mathematician from having to waste time dealing with technical artifacts in the course of ordinary mathematics, then this is often frustrated in that the actual mechanics of various alternative mathematics often turn out to be more complicated than classical mathematics. E.g. often there is a non-constructive proof which is shorter than any known constructive proof of the same proposition. This is to be expected, because alternative foundations are often the same as classical foundations, but with some restrictions on reasoning. If one's motivation for alternative mathematical foundations, however, is a firm belief that classical foundations are unjustified, then the 'easier' proof from classical mathematics is just wrong, so there is no choice but to take the more difficult alternative route. On the other hand, perhaps some of the seeming complexity in the alternative foundations is due to the temporary/present-day need to be able to express them in terms of mainstream foundations; eg some stuff in non-standard analysis is stated with ultrafilters, the weirdness of which kind of defeats the purpose; but maybe that's only to connect it with mainstream foundations (i'm not sure).

But continuing down the path of alternative foundations as a pedagogical tool, this statement from Wikipedia is relevant; "More formally, Hilbert believed that it is possible to show that any theorem about finite mathematical objects that can be obtained using ideal infinite objects can be also obtained without them. Therefore allowing infinite mathematical objects would not cause a problem regarding finite objects. This led to Hilbert's program of proving consistency of set theory using finitistic means as this would imply that adding ideal mathematical objects is conservative over the finitistic part. Hilbert's views are also associated with formalist philosophy of mathematics. Hilbert's goal of proving the consistency of set theory or even arithmetic through finitistic means turned out to be an impossible task due to Kurt Gödel's incompleteness theorems. However, by Harvey Friedman's grand conjecture most mathematical results should be provable using finitistic means." More information on Friedman's "grand conjecture" can be found at http://en.wikipedia.org/wiki/Grand_conjecture#Friedman.27s_grand_conjecture . (note that Friedman also engages in trying to find interesting mathematical proofs that cannot be made by finitistic means; afaict he thinks he's found some but Feferman thinks they are not believable unless you are already accepting the existence of various cardinals whose existence he doubts).

From here on in, we'll just use the phrase "crazy things" to refer to those objects and styles of proof that a restricted alternative foundation wants to rule out.

In other words, Hilbert hoped to find a subset of mathematics which talked about only non-crazy things and which could be verified without talking about crazy things and which was sufficient to do all ordinary mathematics. Godel proved that this wasn't possible; that any reasonable candidate for doing ordinary mathematics cannot be formally verified without talking about crazy things.

Even if ALL important mathematics cannot be done without talking about crazy things, there is still the hope that MOST of it can, and that a strict line can be drawn between the crazy parts and the other parts. That is, there is a hope that for pedagogical purposes, all concepts and theorems can be classified and clearly labeled in all literature as "definitely non-crazy" or "possibly crazy", and most students (including most professional mathematician) can learn the non-crazy stuff, and skip the possibly crazy stuff, unless they are in the mood and have some extra time for craziness.

An alternate motivation is simplicity; regardless of its benefits for new learners, simplicity probably also helps experts (in another field, software engineering, this is certainly thought to be the case).

todo

https://en.wikipedia.org/wiki/Zermelo_set_theory

According to https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory , one of the objections to Zermelo's original set theory axiomitization was that it couldn't prove the existence of the cardinal Aleph-w, or of the set {Z, P(Z), P(P(Z)), ...}. Perhaps those with finitist leanings should investigate Zermelo's original theory. According to https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory#Criticisms , all of mainstream mathematics can be done in Zermelo's theory plus AC.

According to https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory#Criticisms , the axioms of New Foundations admit the existence of a universal set.

http://homotopytypetheory.org/book/

Like intuitionism except that the excluded middle is allowed for \Delta_0^2 formulas.

not really foundational, in a sense, since in logic we expect to be able to go to higher orders

todo talk about Peano, PRA, EFA, etc

"Finite automata can decide Presburger arithmetic formulae" -- http://cstheory.stackexchange.com/questions/14811/what-is-the-enlightenment-im-supposed-to-attain-after-studying-finite-automata/14818#14818

Working in the continuum, https://en.wikipedia.org/wiki/Smooth_function s seem to be a logic endpoint of avoiding monstrosities such as the everywhere continuous but nowhere differentiable https://en.wikipedia.org/wiki/Weierstrass_function .

But relating this to countable stuff, it would seem that e.g. a piecewise linear function is a simple object, but this may not be smooth. So we have some trouble bridging the continuous and discrete worlds in a sensible manner.

Similarly, sets of measure zero seem offensive in the setting of the continuum; but if one is thinking discretely, then it's the sets NOT of measure zero which are problematic.

Perhaps there is some sort of thing like a homomorphism connecting discrete and continuous mathematics that formalizes this sort of thing?

ok these arent really alternative foundations in the same sense but it's past 3am and i just want to write down a note or two before i go to sleep.

one can construct the real starting with the naturals, then passing to the integers, then to the rationals, then to the algebraic numbers, and then to the definable trancendentals, then we say geez can't we find a representation that would let us easily and intuitively compute which of two of these numbers is bigger, and then we get the decimal expansion, and then if we allow our decimal expansions to be of countably infinite length (or taking the limits of other things), we get the reals.

one can also construct the reals starting with via the surreal route. After finite 'generation' steps we get the dyadic rationals, and then if we allow countably infinite 'generation' steps, we get the reals.

Note that before we get to the reals, the surreals cannot give us even simple rationals like 1/3.

This might be taken as an argument for the reality of the reals, since the surreal construction seems so sensible, as does the other progression. On the other hand, it might be taken as an argument against the reality of the reals, because it takes two constructions that are so obviously different and makes them behave the same.

Another point against the reality of the reals is that there are so many reals that not only are most of them not computable, most of them are not even definable.

Conceptions of the Continuum by Solomon Feferman

"The predicativist will object that the power-set operation is not meaningful. And even the classical mathematician will admit that there are some obscure features of the power-set operation. The independence of the continuum hypothesis illustrates one such obscurity." -- http://plato.stanford.edu/entries/logic-higher-order/

http://plato.stanford.edu/entries/set-theory-constructive/#ResPow

https://en.wikipedia.org/wiki/Controversy_over_Cantor%27s_theory

http://math.stanford.edu/~feferman/papers/relationships.pdf

i guess what really bothers me is indefinables, that is, classes for which you would need infinite amounts of information in order to be able to distinguish each of their members. but i guess that's the same as saying that i don't like the cardinality of the continuum, Beth-2?

if one doesn't like the idea of considering an aggregate as a thing, even for the purpose of proving properties about all of its members or about the existence of some member, just because one can't reach, with finite information, every member of that aggregate, then i probably don't like higher-order logic, either. but that seems problematic, because then how do you do metamathematics, e.g. proofs about the properties of predicates that might exist over specific kinds of universes?

i have a vague intuition that what i want is to say something like 'predicates are real things only in respect to this finite system that we have for talking and reasoning about them'. Perhaps i need to learn more about Kleene realizers.

also, should learn what the definitions of formalist and realism are w/r/t math. i guess one opinion is that e.g. uncountable cardinalities are 'real' in the sense that they are specific mechanisms in our formal system and that those mechanisms have real logical and computational consequences as to how the rest of our system works, but they do not denote actual numbers in the same way that finite numbers, and probably countable cardinalities, do. so e.g. independence results are GREAT, because they show where the consequences of the part of our system that we consider to be right for intuitive reasons peter out; beyond this point, the system does not say whether certain propositions about these weird objects are true or false, and that's fine, because we have no reason for believing that those objects are real objects and not just artifacts of our formal system, anyhow; and it's great because then we don't have to bother with that stuff.

i take the same attitude towards complex and even non-positive numbers and i suppose towards the decimal expansions of trancendentals. Those things aren't really numbers in the sense of "here are two sheep", but they are clever ways of stuffing some useful logical computation into our notation that let's us not have to hold so much in our mind as we do math, thereby allowing us to go further, faster, than we otherwise could given the pathetically small number of things we can hold in our mind simultaneously.

i'm guessing that's the prototypical formalist point of view but i'm not sure. it's certainly not realist.

see http://plato.stanford.edu/entries/formalism-mathematics/ . A quick skim of that convinces me that my position is probably Hilbertian formalism. See http://plato.stanford.edu/entries/hilbert-program/ .

One nuance of my position is that i don't really seem to have a problem with countable transfinite ordinals. For example, if you took an infinite sheet of graph paper and considered all of its grid points, these are points of the form of pairs (x,y) where x and y are integers. If you want to have a total ordering on these pairs, you need w2 (i think), which is a transfinite ordinal bigger than mere w. But as we see from this example, w2 isn't so crazy.

Just as various proofs that people give that seem intuitively reasonable formally require induction up to w, various proofs that people give that seem intuitively reasonable formally require transfinite induction on transfinite but countable ordinals. This makes me think that i'm cool with transfinite induction on countable ordinals, and maybe even some form of countably infinitary logic.

It is unclear to me whether this feeling of mine extends to all countable ordinals or only to some of them. I should take a closer look at Feferman's predicativity programme which appears to be based on going up to the Feferman–Schutte? ordinal only. Feferman has talked about his programme as 'Hilbert's Program Relativized' [4], which seems to be what i'm aiming at here. I am not positive that Feferman's ideas haven't evolved over time, and am not sure if all these things i say about 'feferman's programme' refer to the same programme.

mb should read http://math.stanford.edu/~feferman/papers/DraftIntroFEM.pdf which is relatively recent (2012)

https://en.m.wikipedia.org/wiki/Finitism https://en.m.wikipedia.org/wiki/Potential_infinity https://en.m.wikipedia.org/wiki/Absolute_Infinite

ordinal vs cardinal infinities: i havent seen this anywhere, but it strikes me that another reasonable position might be to believe in all of the countably infinite ordinals

todo this is a repetition of the above: here's a simple example that shows why you might want multiple countably infinite ordinals, without wanting uncountable cardinals: consider a 2D sheet of graph paper, infinite in one direction in each dimension (eg if you go far enough up and to the left you eventually come to a corner, but if you go down or to the right you do not). Each grid cell is labeled by its position; the cell in the upper-left corner is labeled 0,0; the cell to its right is labeled 0,1; the cell below it is labeled 1,0; the cell down and to its right is labeled 1,1; etc. Now, considering all of the grid cells in row 0, we already have the ordinal omega (ω). But what if you want to impose an ordering on the sheet of paper such that any cell in a higher-indexed vertical row is greater than every cell in all lower-indexed row? So eg 2,0 > 100,0? I think (todo) this ordering is ω2, which is a different (larger) ordinal from ω. But what is the cardinality of all of the grid cells on the sheet of paper? It's still aleph_0. The whole point of ordinals is to distinguish equivalence classes of orderings, so from this perspective it's not surprising that there might be multiple 'valid' ways to order some sets of a given cardinality.

However, note that ω_1 (sometimes written Ω) is the first uncountable ordinal, corresponding to Aleph_1 (see https://en.wikipedia.org/wiki/First_uncountable_ordinal ), which corresponds to the set of countable ordinals. So if you count all of the countable ordinals, you end up with an uncountable number of them. So if you want to believe in all of the countable ordinals, and you want to believe in the cardinality of the set of things you believe in, then you must believe in an uncountable number. So if you want to believe in some countable ordinals, and you want to believe in the cardinality of the set of things you believe in, then you should have some stopping criterion the prevents you from believing in all of the countable ordinals. https://en.wikipedia.org/wiki/Large_countable_ordinal seems like the sort of thing to look into here. Two interesting ordinals from that page (candidate stopping points) are the Feferman–Schütte? ordinal (the smallest impredicative ordinal, in some sense), and the Church–Kleene? ordinal, which is the first non-recursive ordinal (and the set of all recursive ordinals). My money's on Feferman–Schütte? (but i'm biased, because i took some classes from Feferman).

" Conceptions of the Continuum • There is no unique concept of the continuum but rather several related ones. (Feferman 2009) • To clear the way as to whether CH is a genuine mathematical problem one should avoid the tendency to conflate these concepts, especially those that we use in describing physical reality. • (i)The Euclidean continuum, (ii) The Hilbertian continuum, (iii) The Dedekind real line, (iv) The Cauchy-Cantor real line, (v) The set 2 N , (vi) the set of all subsets of N, S(N). " -- http://math.stanford.edu/~feferman/papers/Conceptual_Structuralism.pdf

" Conceptions of the Continuum (Cont’d) • Not included are physical conceptions of the continuum , since our only way of expressing them is through one of the conceptions via geometry or the real numbers. • Which continuum is CH about? Their identity as to cardinality assumes impredicative set theory. • Set theory erases the conceptual distinction between sets and sequences . • CH as a proposition about subsets of S(N) and possible functions (one-one sets of ordered pairs "

" I shall be relatively brief about each of thes e since I have expanded on them in Feferman ( 2009a ). (i) The Euclidean continuum . Th e conception is semi - structural. Straight lines are conceived of as lying in the plane or in space. They are perfectly straight and have no breadth. Points are perfectly fine; they are conceived of as the objectification of pure locations. A point may lie on a line, but the line does not consist of the set of its points. The idea of arbitrary subset of a line or of the removal of some points from a line is foreign to Euclidean geometry. (ii) The Hilbertian continuum . The conception is structural: on e has points, lines, planes, incidence, betweenness and equidistance relations. Continuity is expressed set - theoretically following Dedekind. (iii) The Dedekind real line . This is a hybrid (arithmetical/geometric) notion that can be expressed in struc tural terms relative to the rationals. Continuity is expressed by the Dedekind cut condition. (iv) The Cauchy - Cantor real line . This is again a hybrid structural notion relative to Q. Continuity is expressed by the Cauchy convergence condition, used by Cantor to “construct” the reals.

17 (v) The set 2 N , i.e. the set of infinite sequences of 0’s and 1’s, i.e. all paths in the full binary tree. (vi) The set of all subsets of N, S(N). Not included here are physical conceptions of the continuum, since o ur only way of expressing them is through one of the mathematical conceptions via geometry or the real numbers. Euclidean geometry aside, s o far as CH is concerned, set theory erases the distinctions between the notions in (ii) - (vi) by identifying sequenc es with sets and by considering only the cardinality of the various continua. But there is also a basic conceptual difference between 2 N and S(N), with the elements of 2 N pictured as the result of an unending sequence of choices, 0 or 1 (left or right) wh ile the elements of S(N) are the result of sprinkling 1s through the natural numbers in some simultaneous manner and then attaching 0s to the rest . Of course, with each set is associated a sequence as its characteristic function and vice versa, but that r equires a bit of reasoning ⎯ the equivalence of these notions is not conceptually immediate. " -- http://logic.harvard.edu/EFI_Feferman_IsCHdefinite.pdf

http://mathoverflow.net/questions/125626/conceptual-structuralism-and-continuum-hypothesis

but see http://logic.harvard.edu/EFI_Feferman_comments.pdf

" Conceptions of Sets • Sets are supposed to be definite totalities, determined solely by which objects are in the membership relation (∈) to them, and independently of how they may be defined, if at all. • A is a definite totality iff the logical operation of quantifying over A, (∀x∈A) P(x), has a determinate truth value for each definite property P(x) of elements of A. •A⊆B means (∀x∈A) (x∈B) •Extensionality: A⊆B∧B⊆A→A? = B.

The Structure of “all” Sets • (V,∈), where V is the universe of “all” sets. •V itself is not a definite totality, so unbounded quantification over V is not justified on this conception. Indeed, it is essentially indefinite. •If the operation S( . ) is conceived to lead from sets to sets, that justifies the power set axiom Pow. • At most, this conception justifies KPω+Pow+AC, with classical logic only for bounded statements (Feferman, t.a.) " -- http://math.stanford.edu/~feferman/papers/Conceptual_Structuralism.pdf

" The Status of CH • But--I believe--the assumption of S(N), S(S(N)) as definite totalities is philosophically justified only on platonistic grounds. • From the point of view of conceptual structuralism, the conception of the totality of arbitrary subsets of any given set is essentially indefinite (or inherently vague). • For, any effort to make it definite violates the idea of what it is supposed to be. "

" A proposed logical framework for what’s definite (and what’s not) According to the finitists , the natural numbers form an inc ompleted or indefinite totality and the general operations of universal and existential quantification ov er the natural numbers are not to be admitted in reasoning about them except in bounded form. The intuitionists share the finitists’ general point of view about the natural numbers but regard 23 unbounded quantification over them as meaningful though not whe n combined with classical logic. According to the predicativists, the natural numbers form a definite totality, but not the collection of “all” sets of natural numbers. Nevertheless systems of predicative analysis have been formulated using quantificatio n with respect to variables for such sets within classical logic. Finally, we have the case of set theory, in which according to practically all points of view ⎯ including that of the mathematical practitioners from the very beginning to the present as well as both the philosophical defenders and critics ⎯ sets in general form an indefinite totality, otherwise the universe of all sets would be a set and thus give rise to Russell’s Paradox. All of this poses questions about the proper formulation of axiomatic systems in which some of the domains involved are conceived to form indefinite totalities, while others, or parts of them, are considered to be definite totalities. There has been much interesting philosophical discussion in recent years about the proble ms raised by absolute gen erality (cf. Rayo and Uzquiano 2006 ) both in its unrestricted sense and more specifically as applied to set theory. " -- http://logic.harvard.edu/EFI_Feferman_IsCHdefinite.pdf

" My main concern here is rather to see what precisely can be said about certain ways of construing in formal terms the distinction between definite and indefinite concepts. One way of saying of a statement φ that it is definite is that it is true or false; on a deflationary account of truth that’s the same as saying that the Law of Excluded Middle (LEM) holds of φ , i.e. one has φ ∨ ¬ φ . Since LEM is rejected in intuitionistic logic as a basic principle, that su ggests the slogan, “What’s definite is the domain of classical logic, what’s not is that of intuitionistic logic.” In the case of predicativity, this would lead us to consider systems in which quantification over the natural numbers is governed by classic al logic while only intuitionistic logic may be used to treat quantification over sets of natural numbers or sets more generally. And in the case of set theory, where every set is conceived to be a definite totality, we would have classical logic for boun ded quantification while intuitionistic logic is to be used for unbounded quantification. The formal study of systems of the latter kind goes back at least to a Wolf(1974 ) and 24 Friedman (1980 ) and has most recently been carried on in the paper, Feferman (20 10b ). 12 The general pattern of the studies there is that we start with a system T formulated in fully classical logic, then consider an associated system SI - T formulated in a mixed, semi - intuitionistic logic, and ask whether there is any essential loss in proof - theoretical strength when passing from T to SI - T. In the cases that are studied, it turns out that there is no such loss, and moreover, there can be an advantage in going to such an SI - T; namely, we can beef it up to a semi - constructive system SC - T without changing the proof - theoretical strength, by the adjunction of certain principles that go beyond what is admitted in SI - T, because they happened to be verified in a certain kind of functional interpretation of the intuitionistic logic. For example , if one starts with S equal to the classical system KP ω of admissible set theory (including the Axiom of Infinity), the associated system SI - KP ω has the same axioms as KP ω , and is based on intuitionistic logic plus the law of excluded middle for all bound ed (i.e. Δ 0 ) formulas. But the beefed up system SC - KP ω proves the Full Axiom of Choice Scheme for sets, ∀ x ∈ a ∃ y φ (x,y) → ∃ r [Fun(r) ∧ ∀ x ∈ a φ (x, r(x))], where φ (x, y,...) is an arbitrary formula of the language of set theory. That in turn implie s the Full Collection Axiom Scheme, ∀ x ∈ a ∃ y φ (x,y) → ∃ b ∀ x ∈ a ∃ y ∈ b φ (x,y) for φ an arbitrary formula, while this holds only for ∑ 1 formulas in SI - KP ω . In addition, SC - KP ω contains some other non - intuitionistic principles that can, nevertheless, be gi ven a semi - constructive interpretation. The main result in Feferman ( 2010b ) is that all of these systems are of the same proof - theoretical strength, KP ω ≡ SI - KP ω ≡ SC - KP ω . " -- http://logic.harvard.edu/EFI_Feferman_IsCHdefinite.pdf

"Descriptive Set Theory (DST, the study of definable sets of reals and of other topological spaces)" -- http://logic.harvard.edu/EFI_Feferman_IsCHdefinite.pdf

"

5. Revised Hilbert Programs

Even if no finitary consistency proof of arithmetic can be given, the question of finding consistency proofs is nevertheless of value: the methods used in such proofs, although they must go beyond Hilbert's original sense of finitism, might provide genuine insight into the constructive content of arithmetic and stronger theories. What Gödel's result showed was that there can be no absolute consistency proof of all of mathematics; hence work in proof theory after Gödel concentrated on relative results, both: relative to the system for which a consistency proof was given, and relative to the proof methods used.

Reductive proof theory in this sense has followed two traditions: the first, mainly carried out by proof theorists following Gentzen and Schütte, has pursued a program of what is called ordinal analysis, and is exemplified by Gentzen's first consistency proof of PA by induction up to ε0. ε0 is a certain transfinite (though countable) ordinal, however, “induction up to ε0” in the sense used here is not a genuinely transfinite procedure. Ordinal analysis does not operate with infinite ordinal numbers, but rather with ordinal notation systems which themselves can be formalized in very weak (essentially, finitary) systems. An ordinal analysis of a system T is given if: (a) one can produce an ordinal notation system which mimics the ordinals less than some ordinal αT so that (b) it can be proved finitarily that the formalization TI(αT) of the principle of induction up to αT implies the consistency of T (i.e., S ⊢ TI(αT)→Con T) and (c) T proves TI(β) for all β < αT (S is a theory formalizing finitary metamathematics and is generally a weak sub-theory of T). To have any foundational significance it is also required that one can give a constructive argument for transfinite induction up to αT. As mentioned above, this was done for by Gentzen and Takeuti for ε0, the proof theoretic ordinal of PA, but becomes more difficult and of progressively questionable philosophical significance for stronger theories.

A philosophically more satisfactory continuation of Hilbert's Program in proof theoretic terms has been suggested by Kreisel (1983; 1968) and Feferman (Feferman, 1988; Feferman, 1993a). This work proceeds from a wider conception of Hilbert's Program as an attempt to justify ideal mathematics by restricted means. In this conception, the aim of Hilbert's proof theory was to show that, at least as far as a certain class of real propositions is concerned, ideal mathematics does not go beyond real mathematics. A finitary consistency proof of the kind envisaged by Hilbert would have accomplished this: if ideal mathematics proves a real proposition, then this proposition is already provable by real (i.e., finitary) methods. In a sense this reduces ideal mathematics to real mathematics. A proof-theoretic reduction of a theory T to a theory S shows that, as far as a certain class of propositions is concerned, if T proves a proposition, then S proves it too, and the proof of this fact is itself finitary. Hilbert's proof theoretic program can then be seen to be a search for a proof theoretic reduction of all of mathematics to finitary mathematics; in a relativized program one looks for reductions of theories weaker than all of classical mathematics to theories often stronger than finitary mathematics. Proof theorists have obtained a number of such results, including reductions of theories which on their face require a significant amount of ideal mathematics for their justification (e.g., subsystems of analysis) to finitary systems. (Feferman, 1993b) has used such results in combination with other results that show that most, if not all, of scientifically applicable mathematics can be carried out in systems for which such reductions are available to argue against the indispensability argument in the philosophy of mathematics. The philosophical significance of such proof theoretic reductions is currently the subject of debate (Hofweber, 2000; Feferman, 2000).

The program of so-called reverse mathematics developed by, in particular, Friedman and Simpson, is another continuation of Hilbert's program. In the face of Gödel's results showing that not all of classical mathematics can be reduced to the finitary, they seek to answer the question: how much of classical mathematics can be so reduced? Reverse mathematics seeks to give a precise answer to this question by investigating which theorems of classical mathematics are provable in weak subsystems of analysis which are reducible to finitary mathematics (in the sense discussed in the preceding paragraph). A typical result is that the Hahn-Banach theorem of functional analysis is provable in a theory known as WKL0 (for “weak König lemma”); WKL0 is conservative over PRA for Π02 sentences (i.e., sentences of the form ∀x∃yA(x, y). (See Simpson 1988 for an overview and Simpson 1999 for a technical treatment.) " -- http://plato.stanford.edu/entries/hilbert-program/#1.3

http://en.wikipedia.org/wiki/Reverse_mathematics#The_big_five_subsystems_of_second_order_arithmetic notes five subsystems, ascending in power, of second-order arithmetic (see also http://en.wikipedia.org/wiki/Second-order_arithmetic#Subsystems_of_second-order_arithmetic ). They are somewhat independent, but sometimes people implicitly refer to one to mean that one, plus the ones beneath it, which is what i will do (i think; i am copying some statements from elsewhere so perhaps i'll make a mistake). Perhaps we should choose one of those.

RCA_0 is computable mathematics, which seems philosophically pretty nice.

WKL_0 also seems feasible, "The subsystem WKL0 consists of RCA0 plus a weak form of König's lemma, namely the statement that every infinite subtree of the full binary tree (the tree of all finite sequences of 0's and 1's) has an infinite path. "

Both RCA_0 and WKL_0 have proof-theoretic ordinals w^w. This is the same as the ordinal of Primitive Recursive Arithmetic (PRA). The next one up is ACA_0, with ordinal \epsilon_0. "ACA0 allows us to form the set of natural numbers satisfying an arbitrary arithmetical formula (one with no bound set variables, although possibly containing set parameters). Actually, it suffices to add to RCA0 the comprehension scheme for Σ1 formulas in order to obtain full arithmetical comprehension.".

ACA_0 (Arithmetical comprehension axiom) is the last predicative one. ACA_0 is necessary for some elementary results that you hear about in required undergraduate analysis courses, such as Bolzano–Weierstrass? and Ascoli's theorem. ACA_0 is "conservative over Peano arithmetic for arithmetical sentences". ACA_0's ordinal \epsilon_0 is the same as Peano Arithmetic's ordinal.

The consistency of ACA_0 can be proved in the next one, ATR_0 (Arithmetical transfinite recursion). "The system ATR0 adds to ACA0 an axiom which states, informally, that any arithmetical functional (meaning any arithmetical formula with a free number variable n and a free class variable X, seen as the operator taking X to the set of n satisfying the formula) can be iterated transfinitely along any countable well ordering starting with any set." ATR_0's ordinal is \gamma_0, "the supremum of that of predicative systems.", see http://en.wikipedia.org/wiki/Feferman%E2%80%93Sch%C3%BCtte_ordinal . ATR_0 is "conservative over Feferman's system IR for Π_1^1 sentences". ATR_0 is needed to prove some theorems that i haven't heard of yet. \gamma_0 is the same ordinal as for "Martin-Löf type theory with arbitrarily many finite level universes".

Beyond that we have a system with ordinal http://en.wikipedia.org/wiki/Psi0%28Omega_omega%29 .

I wonder what ordinal goes with Coq's logic.

So, knowing nothing else but this, it seems to me that ACA_0 is a good place to start. It sounds like many people think that e_0 can be philosophically justified, and it's predicative. Maybe you'd want to go one more step, to ATR_0, to prove ACA_0.

I should learn more about the third, Kreisel-Feferman programme; see also http://math.stanford.edu/~feferman/book98.html , Feferman, Solomon, 1993a, “What rests on what? The proof-theoretic analysis of mathematics”, in Philosophy of Mathematics. Proceedings of the Fifteenth International Wittgenstein-Symposium, Part 1, Johannes Czermak, ed., Vienna: Hölder-Pichler-Tempsky, 147-171, Feferman, Solomon, 1993b, “Why a little bit goes a long way: Logical foundations of scientifically applicable mathematics”, PSA 1992, 2: 442-455. Reprinted in Feferman (1998, Ch. 14, 284-298).

... in http://web.archive.org/web/20120206233919/http://math.stanford.edu/~feferman/papers/psa1992.pdf , Feferman talks about a system W which is at least as powerful at ACA_0.

Some advocate using classical logic for quantification over natural numbers, but intuitionistic logic for quantification over sets of natural numbers: http://web.archive.org/web/20111219144534/http://math.stanford.edu/~feferman/papers/whatsdef.pdf (semi-intuitionism, semi-constructivism)

In http://web.archive.org/web/20111130031429/http://math.stanford.edu/~feferman/papers/newaxioms.pdf , Feferman advocates using classical mathematics practically, but from a philosophical point of view notes that all mathematics that he's found to be applicable to science, with the exception of certain speculative approaches to the foundations of quantum field theory, are conservative extensions of PA (i think, not sure if i understood).

Feferman presents another way of looking at finitism in http://web.archive.org/web/20111219144522/http://math.stanford.edu/~feferman/papers/UnfoldFA.pdf , whose power is equivalent to PA or PRA depending on some choices.

Feferman is working on a book which appears to be his current-best-proposal for metamathematics on mathematical foundations: math.stanford.edu/~feferman/papers/DraftIntroFEM?.pdf

http://www.ltg.unibe.ch/research/Foundations%20of%20Explicit%20Mathematics

An interesting "natural" theorem that is unprovable using just Peano arithmetic: http://en.wikipedia.org/wiki/Goodstein%27s_theorem

I am unclear about the meaning of impredicative. As soon as one moved beyond computable functions, one has uncomputable functions, so i assume that somewhere around here you get the halting function. Can you only construct halting function-like things in theories beyond \Gamma_0? Or is the circularity needed to construct the halting function a different thing than whatever makes people say that theories with proof-theoretic ordinals beyond \Gamma_0 are impredicative? TODO TOASK

http://ncatlab.org/nlab/show/predicative+mathematics

"Conjecture: All (or almost all) scienti cally applicable analysis can be carried out in W" -- Relationships between Constructive, Predicative and Classical Systems of Analysis by Solomon Feferman

Explicit mathematics (Feferman) eg http://math.stanford.edu/~feferman/papers/LangAxsExplMaths.pdf

"I am convinced that the platonism which underlies Cantorian set theory > is utterly unsatisfactory as a philosophy of our subject, despite the > apparent coherence of current set-theoretical conceptions and methods. To echo Weyl, platonism is the medieval metaphysics of mathematics; surely we can do better." -- Infinity in Mathematics: Is Cantor Necessary? by Solomon Feferman

a review of "In the Light of Logic" by Solomon Feferman PDF but without listing of sources of book chapters

" Suppose we accept — with Weyl — the natural number system N as a completed totality, therefore allowing unrestricted quantification over N as meaningful. Then, any property of natural numbers expressible by a first-order formula of arbitrary quantifier complexity is well- defined, and thus determines a subset of N . In turn, the collection of subsets one allows determin es the strength of the corresponding induction principle. In this manner, one can proceed through a number of stages, where at each stage one allows properties expressible by quant ifying over previously determined collections of properties. As independently discovered by Feferman and Schutte, this process gives out at the ordinal Γ0 , which has since come to be regarde d as the ordinal characterizing predicativity." -- a review of "In the Light of Logic" by Solomon Feferman PDF but without listing of sources of book chapters

" proof-theoretical (or foundational ) reduction. This kind of reduction moves in the opposite direction fro m the other one: a stronger theory is reduced to a weaker one by establishing certain conservativity results. Feferman refers to the task of establishing foundational reductions of this kind as a relativized Hilbert program . The basic idea of a proof-theoretical reduction of a theory T 1 to a theory T 2 , for a class of formulas Φ, is that every proof of a formula φ ∈ Φin T 1 can be computably translated into a proof of φ in T 2 , and moreover this very fact can be represented in the weaker theory T 2 itself. Perhaps the first example of such a re duction, due to Ackermann, is the reducibility of first-order arithmetic with the quantifier-free induction schema to primitive recursive arithmetic. This early result has been strengthened many times in many different directions; particularly interesting is the case in which a s econd-order theory is reduced to a first-order one. The easiest and most representative result of this kind is the fact that arithmetic with a comprehension principle for arithmetica lly definable sets and the second-order induction axiom is reducible to the first-or der theory of Peano Arithmetic. The conceptual import of these results is that fairly strong arithmetical systems including various second-order comprehension principles and various forms of induction can be justified on the basis of finitistically (in the case of primitive recursive arithmetic) or, in any case, predicativistically (in the case of Peano arithmetic) acceptable frameworks.

This fact can be used to carry out a critical assessment of the the so-called G ̈ odel- doctrine: the idea, first formulated by G ̈ odel in a footnote to his incompleteness paper, that in order to decide more and more arithmetical propositions, one has to ascend the (cumulative) type hierarchy well into the transfinite. The G ̈ odel-doctrine is often invoked as an argument in favor of embracing the “Cantorian transfinite.” In particular, a number of results beginning with the famous Paris-Harri ngton theorem, and culminating with Harvey Friedman’s recent work, have purported to show that the “higher infinite” is necessary for ordinary mathematical practice. The main idea here is that a finite combinatorial statement is produced which is ( a ) of independent interest for the “working mathematician;” and ( b )not settled by some “standard” theory in which math ematical practice is formalized. In the case of the Paris-Harrington theorem, the statem ent in question is a finite version of Ramsey’s theorem, and it is shown to be independent of Peano arithmetic. But Friedman’s recent work, especially on Boolean Relation Theory, has pushed this much further, by producing statements that appear more and more ‘natural’ from the point of view of the working mathematician (‘natural’ in the same sense in which G ̈ odel’s undecidable sentence might appear contrived and ad hoc), and whose proofs r equire stronger and stronger principles well beyond the reach of Zermelo-Fraenkel set theor y, in particular, large cardinal hypotheses. (The reader interested in keeping up with Friedman’s ongoing research in this direction could usefully consult the archive of the “Foundations of Mathematics” ( FoM? ) discussion list, at http://www.math.psu.edu/simpson/fom/ .)

Feferman has two rejoinders to these claim s. First, referring among other things to his own work, Feferman shows that (in at least some initial cases of the Paris-Harrington type) ascent of the type hierarchy (objectio nable in his own view because it presupposes a well-defined notion of power-set), can be replaced by ascent of another, less ontologically committed kind. This alternative ascent is achieved by adjoining to a give theory either a truth-predicate or appropriate reflection principles. In both cases, one succeeds in going be- yond Peano arithmetic without committing to an intrinsically uncountable framework. More importantly, Feferman’s second re joinder questions Friedman’s claim that the combinatorial principles are natural and readily understandable — and that therefore the intrinsic necessity of strong systems for everyday finitary mathematics has been established. On closer scrutiny one sees that Friedman’s results (important an d difficult as they are) establish the equiv- alence of the combinatorial statements not with the large cardinal hypohteses themselves, but with their 1-consistency, i.e., the claim that all purely existential number-theoretical statements provable from the hypotheses are true. The leap from 1-consistency to truth is perhaps not insormountable, but only if one i s already committed to their being a fact of the matter as to the truth of the large cardinal hypotheses. Moreover, contrary to the cases of the Paris-Harrington type, the combinatorial statements themselves cannot be established by ordinary mathematical reas oning, but only under the assumption of the 1-consistency of the large cardinal hypotheses. To turn around and claim that the combinatorial statements provide evidence for those hypotheses is, for Feferman, and evident petitio principii. . " -- a review of "In the Light of Logic" by Solomon Feferman PDF but without listing of sources of book chapters

"Feferman’s system W of variable types (with a non-constructive least number search operator)" -- a review of "In the Light of Logic" by Solomon Feferman PDF but without listing of sources of book chapters

"system W is proof-theoretically reducible to Peano arithmetic, of which it is a conservative extension." -- a review of "In the Light of Logic" by Solomon Feferman PDF but without listing of sources of book chapters

"W is proof-theoretically reducible to PA and is a conservative extension of PA." -- [http://math.stanford.edu/~feferman/papers/psa1992.pdf[Why a little bit goes a long way: Logical foundations of scientifically applicable mathematics] by Solomon Feferman

"There are, indeed, bits of mathematics that cannot be represented in W, e.g., those that refer in an essential way to non-measurable objects or non-separable Hilbert spaces. But their use in contemporary physics is controversial, and they might in fact not be needed at all" -- a review of "In the Light of Logic" by Solomon Feferman PDF but without listing of sources of book chapters

I am also unclear about diagonalization. Are any of the is the "big five" subsystems of second order logic mentioned above powerful enough to prove the existence of an uncountable cardinal? (according to http://mathforum.org/kb/message.jspa?messageID=7918208 , yes, even RCA_0 is)

maybe see http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.150.3719&rep=rep1&type=pdf

"The mathematical meaning of the term "actual" in actual infinity is synonymous with definite, completed, extended or existential,[1] but not to be mistaken for physically existing. The question of whether natural or real numbers form definite sets is therefore independent of the question of whether infinite things exist physically in nature."

https://en.wikipedia.org/wiki/Actual_infinity

note: imo the turing machine gives an example of the usefulness of potential infinity in definitions; one is always having to qualify any discussion of anything by saying, 'of course computers aren't REALLY Turing machines, they only have finite memory, but if one imagined a family of computer-like devices with ever-increasing memory..'; it seems like if Turing machine memory were just defined as a 'potential infinity' then we could have some linguistic rules to let us call computers Turing machines, where the definition of Turing machine as potential infinity would implicitly imply the qualifying statements so you don't have to say them each time.

https://en.wikipedia.org/wiki/Hyperreal_number

" The idea of the hyperreal system is to extend the real numbers R to form a system *R that includes infinitesimal and infinite numbers, but without changing any of the elementary axioms of algebra. Any statement of the form "for any number x..." that is true for the reals is also true for the hyperreals. ...However, statements of the form "for any set of numbers S ..." may not carry over....The transfer principle, however, doesn't mean that R and *R have identical behavior. For instance, in *R there exists an element ω such that

1<\omega, \quad 1+1<\omega, \quad 1+1+1<\omega, \quad 1+1+1+1<\omega, \ldots.

but there is no such number in R. (In other words, *R is not Archimedean.) This is possible because the nonexistence of ω cannot be expressed as a first order statement.

" -- https://en.wikipedia.org/wiki/Hyperreal_number#The_transfer_principle

http://en.wikipedia.org/wiki/G%C3%B6del%27s_first_incompleteness_theorem#Second_incompleteness_theorem shows that no consistent theory at least as powerful as first-order logic plus Peano arithmetic can be complete.

http://en.wikipedia.org/wiki/G%C3%B6del%27s_second_incompleteness_theorem#Second_incompleteness_theorem shows that no consistent theory at least as powerful as first-order logic plus Peano arithmetic can prove its own consistency (I think).

http://en.wikipedia.org/wiki/Gentzen%27s_consistency_proof proves the consistency of Peano Arithmetic (PA). It requires a theory which is neither stronger nor weaker than Peano arithmetic, namely Primitive Recursive Arithmetic (PRA) plus the axiom of quantifier-free transfinite induction up to \epsilon_0.

http://m-phi.blogspot.com/2011/03/completeness-of-pa-with-omega-rule.html says that Peano Arithmetic "closed" under the omega-rule is complete. I don't understand how that squares with Godel. Is it inconsistent? Does this "closing" operation not lead to a real theory? TODO TOASK

"One idea proposed by Stephen Read and Alan Weir (among others) is to enrich the proof-system with non-recursive rules (specifically, the omega-rule), so as to avoid Gödel’s result. However, it strikes me as unclear what the consequences of adding infinitary rules will be for inferentialist semantics." -- http://inferential.wordpress.com/2008/02/11/carnap-and-gentzen/#comment-316 " Carnap adds an ω-rule, but it is one of his consequence rules, not his derivation rules. They are in good company I guess."

so omega rules are exempt from Godel because they allow infinitely long propositions? See also http://philosophy.stackexchange.com/questions/7201/what-happens-when-we-drop-the-condition-that-proofs-are-finite-strings-of-infere http://www.hss.cmu.edu/philosophy/techreports/34_Ignjatovic.pdf

https://en.wikipedia.org/wiki/Aczel's_anti-foundation_axiom

Russel's paradox

Russel's paradox for anti-foundation (for every set X there exists a set Y such that Y \notin X: Y = {z \in X

z \notin z}; b/c in Y \in X, then if either Y \in Y or Y \notin Y, we have a contradiction. |