Formal axiom systems and the finite/infinite sets

[RockyMarciano]

The hereditarily finite sets(a subclass of the Von Neumann universe) are an axiomatic model that corresponds to the usual axioms of set theory but with the axiom of infinity replaced by its negation(showing its independency from the other axioms of set theory).
Some mathematicians (a minority) that are called strict finitists, reject the notion of infinite sets and have this consistent axiom system of hereditarily finite sets model to work with, with which apparently one can do most if not all of what one can do with the usual axiom system at least in the field of applied mathematics in as much as one can model infinity with finite sets approximately(like computers performing analytic tasks that formally require infinite sets with floating points...) or doesn't have to deal with actual infinite sets in applied science.

There is an important foundational issue that would concern both the finitists and non-finitists that has to do with the very distinction between finite and infinite that is vital for set theory(one can read about it here: https://en.wikipedia.org/wiki/Finite_set#Foundational_issues) but I won't dwell on it now unless necessary (it's thorny and can take us too far from my point).

My questions: is this consistent finitist model an example of the flexibility of the Formalist way to see mathematics and axioms. I mean, is the central idea that one can choose different sets of axioms depending on what one intends to do with them as long as they are consistent, and that there is no specific set of axioms that is "truer" or more fundamental and therefore that should be considered "the foundation of mathematics"?

It apears to me that this is the idea behind Formalism, i.e. that there is no single set of axioms that can be considered the foundation of all math(I know that the particular flavor of Hilbert formalism attempted this in the past but it is my understanding that Godel's theorems of incompleteness prevent it). If so, the reason that most mathematicians consider set theory itself and particularly ZF(C) axiomatic set theory as fundamental is that they are not actually formalists, but rather platonists or something else?

 

[SSequence]

To me the strict finitist position is very difficult to defend (unless one insists on taking a view of maths that is very closely tied to physical universe?).
As a matter of analogy, it seems to me somewhat similar to saying that a computer isn't really just a computer but just a finite state machine with finite memory (or alternatively a finite automaton). Once again, this seems (at least to me) to be a sensible comment in a physical sense (that is when we are talking about the actual physical model of the computer) but not so much in the mathematical sense (where one might assume an idealised model with infinite memory).

Some mathematicians (a minority) that are called strict finitists, reject the notion of infinite sets and have this consistent axiom system of hereditarily finite sets model to work with, with which apparently one can do most if not all of what one can do with the usual axiom system at least in the field of applied mathematics...

Do you know a source for this kind of claim? It might be of interest to see.

A somewhat different (but loosely related) point was raised by feferman where he mentioned in the following essay/paper:
http://math.stanford.edu/~feferman/impact.pdf
(you don't have to read or understand all of it :P ... the specific quote is on page-12)
that:
"Even more, I have conjectured and verified to a considerable extent that all of current scientifically
applicable mathematics can be formalized in a system that is proof-theoretically no stronger than PA"

My questions: is this consistent finitist model an example of the flexibility of the Formalist way to see mathematics and axioms. I mean, is the central idea that one can choose different sets of axioms depending on what one intends to do with them as long as they are consistent, and that there is no specific set of axioms that is "truer"...

In my (admittedly limited) knowledge this is a point that is also difficult to defend. I will try to give a specific example in this case, so it is clearer what is being talked about. Well at least I think it is interesting enough to mention.

Now let's consider two systems F1 and F2. In general, they might make many kinds of claims.

Lets restrict ourselves only very specific kinds of claims that F1 and F2 make.
The kind of claim I am talking about is following (here x∈N):
P(x) = Program/Machine with index x halts on the input 0/blank
Also assume that the above statement is either true or false for all input values.

Of course for both F1 and F2 (if they are sound) there will actually be some smallest numbers a1 and a2 where F1 and F2 will fail to prove the statements P(a1) and P(a2) false respectively.
Now if one tried to apply the "relativity" of truth here (that is specifically on the statements of P) and say that there exists no set of axioms that is "truer" (in which case one might also throw away with the notion of soundness I suppose?) one quickly gets into strange situations.

For example, consider just one statement (say P(100)) and try to think about what it might mean to say it is both true and false at the same time? Suppose F1 says P(100) is true and F2 says P(100) is false. Saying P(100) is true means that there is a smallest n (number of steps) where a given program will eventually terminate. Yet saying P(100) is false means there is no such n.

Here if there was actually such an n one would eventually just find it (unless one retreats to a strict finitist sort of position) in a trivial manner. So:
if P(100) is actually true
F2's claim about P(100) can be shown to be false (in a finitary manner***).
if P(100) is actually false
Neither F1 nor F2's claim about P(100) can be shown to be false in a finitary manner.

In which case I might just make a system F3 which, when limited to statements of P, says that all statements P(a) (where a∈N) are true. And I say that since you can't find any inconsistency (in a finitary manner) in claims of F3 there is no such thing as "actual truth" for statements of the form P(x).
Notice how strange the system F3 will be in presence of programs such as:
"while(true) { }"

-----

Now when we are talking about higher level objects and more difficult cases so to speak, formalism certainly does seem to be much more nuanced. I still don't agree with it but nevertheless.*** I have used the phrase "finitary manner" in a specific sense. Note that even from formalist point of view one has to accept certain base rules of "symbolic manipulation" or "number crunching". To evaluate steps of a program is very much the same kind of thing.

 

[RockyMarciano]

To me the strict finitist position is very difficult to defend (unless one insists on taking a view of maths that is very closely tied to physical universe?).

Yes, I'm precisely saying that strict formalism seems to be claiming that no single axiomatic "position" is valid universally to found all of mathematics. For instance from Wikipedia page on formalism:"Many formalists would say that in practice, the axiom systems to be studied are suggested by the demands of the particular science." So it might be said that certain axiomatic systems may be more suited for physics or the natural sciences, and a different one sharing more or less axioms with the former is better suited for some other task or science, but the idea would be that there is no single set of axioms that is universally valid and consistence to found all math. At least that is how I understand the insistence on treating axiom systems as "games" and "strings of symbols", and I think it is a sensible way to approach foundations after Godel and Turing-Church results.

Do you know a source for this kind of claim? It might be of interest to see.

The claim must of course be understood in the way I formulated it. I mean that in the way math is currently axiomatized and within ZFC axioms and set theory formulation, the continuum and analysis are based on completed infinite sets, certainly not on strict finitism. But as far as I understand physics can be also operationally formulated as a finite approximation, since any conceivable measure is by definition finite and every outcome of a prediction and computation in physics must be finite, in the unsurmountable sense that it must have a finite precision. Therefore the use of infinite sets never actually comes up in practice, it is more of a conceptual crutch to justify the notion of continuum that is specific to the currently most commonly axiomatic system used as a foundation of mathematics.

In my (admittedly limited) knowledge this is a point that is also difficult to defend. I will try to give a specific example in this case, so it is clearer what is being talked about.
...

-----

Probably I didn't express myself clearly. Formalism as I understand it, (wich might be wrong and that's why I'm asking people more knowledgeable to clarify) in its more strict form is not concerned with the concept of true or false in general, only with the consistency of certain axiom systems with respect to certain specific purposes (see the sentence from wiki I quoted above). In other words the Godelian idea that if one wants to keep consistency at all costs one must give up completeness or universal validity.

Now when we are talking about higher level objects and more difficult cases so to speak, formalism certainly does seem to be much more nuanced. I still don't agree with it but nevertheless.

One specific doubt that I have is if modern formalism still requires to be built on top of logic(I know Hilbert formalism required it) or is now flexible enough to distance itself from it and develop along with its axioms logics different from the usual propositional and predicative logic based on classical logic. Traditionally this was the view of a different view about foundations of mathematics(intuitionism), but I don't know if nowadays formalism admits this.

I'm thiking of different foundational axiomatic systems like Type theory that doesn't use set theory and can develop its own logic

 

[SSequence]

... Therefore the use of infinite sets never actually comes up in practice, it is more of a conceptual crutch to justify the notion of continuum that is specific to the currently most commonly axiomatic system used as a foundation of mathematics.

Perhaps it is a little pedantic to point this out but there is a lot of mathematics that can be done with just countable infinite sets. I don't think countable infinite sets are just there to justify uncountable infinite sets.

Probably I didn't express myself clearly. Formalism as I understand it, (wich might be wrong and that's why I'm asking people more knowledgeable to clarify) in its more strict form is not concerned with the concept of true or false in general, only with the consistency of certain axiom systems with respect to certain specific purposes (see the sentence from wiki I quoted above).

Well my example was to show how if formalism (taken to an extreme example) can be shown to be a weak view point (though only for that extreme example). The example that I was trying to give with the system F3*** was to show that.

What I was trying to get at was that even when we say that only "consistency" is important and accept certain rules of logic, we have already accepted that "genuine truth "of at least some kinds of statements exist (the statements that assert consistency of a system) and also accepted certain kind of rules for manipulating symbols (ability to do primitive computational steps).
So when F3 says that the following program halts: "while(true) { }" it sounds silly. Or for example when a system F4 says that the following two trivially equivalent programs aren't equivalent. This is even more strange given that consistency statements can be extremely difficult to evaluate (not for specific easy cases but in general).

One specific doubt that I have is if modern formalism still requires to be built on top of logic(I know Hilbert formalism required it) or is now flexible enough to distance itself from it and develop along with its axioms logics different from the usual propositional and predicative logic based on classical logic. Traditionally this was the view of a different view about foundations of mathematics(intuitionism), but I don't know if nowadays formalism admits this.

I'm thiking of different foundational axiomatic systems like Type theory that doesn't use set theory and can develop its own logic

I don't have enough knowledge to know about that.*** I do not know (not enough knowledge) whether a given logical system would usually contain enough in-built "guard mechanism" against a system like F3. But note that many different and obviously absurd examples like F3 can be given (where consistency is preserved but clearly the most trivial true statements (perhaps only one level above 1+1=2) have to be abandoned as "actual truths" and taken as "syntactic truths").

 

[RockyMarciano]

Perhaps it is a little pedantic to point this out but there is a lot of mathematics that can be done with just countable infinite sets. I don't think countable infinite sets are just there to justify uncountable infinite sets.

I wasn't implying anything about what mathematics can be done with uncountable or countable infinite sets, my comment was just about math applied to physics.

Well my example was to show how if formalism (taken to an extreme example) can be shown to be a weak view point (though only for that extreme example). The example that I was trying to give with the system F3*** was to show that.

What I was trying to get at was that even when we say that only "consistency" is important and accept certain rules of logic, we have already accepted that "genuine truth "of at least some kinds of statements exist (the statements that assert consistency of a system) and also accepted certain kind of rules for manipulating symbols (ability to do primitive computational steps).
So when F3 says that the following program halts: "while(true) { }" it sounds silly. Or for example when a system F4 says that the following two trivially equivalent programs aren't equivalent. This is even more strange given that consistency statements can be extremely difficult to evaluate (not for specific easy cases but in general).

*** I do not know (not enough knowledge) whether a given logical system would usually contain enough in-built "guard mechanism" against a system like F3. But note that many different and obviously absurd examples like F3 can be given (where consistency is preserved but clearly the most trivial true statements (perhaps only one level above 1+1=2) have to be abandoned as "actual truths" and taken as "syntactic truths").

I was talking about how general statements about truth seem to not be posible in formalism, there will be of course true or false statement within the domain of validity of the specific axioms at hand for a certain purpose or process, it will just not be generally valid for all possible axiom systems.

 

[Nagase]

Just a quick comment: most strict finitists or ultrafinitists actually work in much weaker systems than (say) Z+the negation of infinity. In fact, they generally work in a version of Robinson arithmetic, since even Peano Arithmetic is too strong for their tastes (it allows induction over impredicatively defined sets). Cf. Edward Nelson's work, especially his Predicative Arithmetic, for details.

 

[RockyMarciano]

Just a quick comment: most strict finitists or ultrafinitists actually work in much weaker systems than (say) Z+the negation of infinity. In fact, they generally work in a version of Robinson arithmetic, since even Peano Arithmetic is too strong for their tastes (it allows induction over impredicatively defined sets). Cf. Edward Nelson's work, especially his Predicative Arithmetic, for details.

That makes sense, such strong restriction must be really hard to work with in practice.
Do you perhaps know whether formalism always implies some form of set theory and must be built on top of classical logic, or is it flexible enough to allow for different syntactic rules and alternatives to set theory?

 

[Nagase]

That makes sense, such strong restriction must be really hard to work with in practice.
Do you perhaps know whether formalism always implies some form of set theory and must be built on top of classical logic, or is it flexible enough to allow for different syntactic rules and alternatives to set theory?

Actually, formalists generally do not use any set theory. Hilbert, for instance, employed a very weak form of arithmetic, enough to code a sufficient amount of syntax. Hilbert did not specify exactly what theory he was employing, but William Tait has argued rather forcefully that it's probably a form of Primitive Recursive Arithmetic, which is what most formalists employ nowadays. Gödel showed that PRA is enough to capture the syntax of any formal theory, so that's generally the exact amount of strength that a formalist would want.

 

[RockyMarciano]

Actually, formalists generally do not use any set theory. Hilbert, for instance, employed a very weak form of arithmetic, enough to code a sufficient amount of syntax. Hilbert did not specify exactly what theory he was employing, but William Tait has argued rather forcefully that it's probably a form of Primitive Recursive Arithmetic, which is what most formalists employ nowadays. Gödel showed that PRA is enough to capture the syntax of any formal theory, so that's generally the exact amount of strength that a formalist would want.

Ok, but surely that minimal syntax follows the usual propositional and predicative logic? Or can one relax those and choose a different logic withing current formalism?

 

[RockyMarciano]

For context, I'm thinking of axioms based maybe on intuitionist logic a la Brouwer, or PerMartin-Lof's Type theory, or axiom systems that introduce fuzzy logic, etc...can such axiomatic systems be framed in modern Formalism?

 

[Nagase]

Ok, but surely that minimal syntax follows the usual propositional and predicative logic? Or can one relax those and choose a different logic withing current formalism?

Since Hilbert wanted to convince Brouwer that classical mathematics was consistent, he actually proposed to employ as a background logic only means that Brouwer accepted. So no, formalists are not tied to classical logic, though, depending on your purposes, that may not be much of a difference (e.g. Gödel and Gentzen independently proved that classical, first-order Peano Arithmetic is equiconsistent with first-order intuitionist arithmetic, so, for purposes of some consistency proofs, it makes no difference which theory you employ).