Philosophy Discussion Forums | A Humans-Only Club for Open-Minded Discussion & Debate

[ChanceIsChange]

One of the main positions held during the foundational crisis of mathematics was formalism, one of whose most prominent proponents was David Hilbert. According to the formalist philosophy of mathematics, all unproven assumptions must be explicitly stated as axioms, and all deductions must be made according to logical axioms and well-defined inference rules. Thus, I understand that formalism is a kind of foundationalism.

However, I see some problems with formalism and with foundationalism in general. Consider the following example.

The fact that the angle sum of a triangle is 180° is not considered to be an absolute truth according to formalism, but rather a logical consequence of the parallel postulate and the other axioms of Euclidean geometry. Because the parallel postulate is an axiom, it is not questioned further, and thus it might seem that formalism has avoided infinite regress. However, what about the fact that “the angle sum of a triangle is 180°” is a logical consequence of the parallel postulate and the other Euclidean axioms? Where does that follow from? According to formalism, it follows from the axioms of classical logic. But then, from which axioms does it follow that the axioms of classical logic imply the fact that “the angle sum of a triangle is 180°” is a logical consequence of the axioms of Euclidean geometry?

As you can see, we could continue asking such questions, leading to an infinite regress. Formalism seems to have failed at preventing infinite regress, contrary to its claim.

Let’s consider another aspect of formalism. On the most basic level, formalism constitutes a philosophy where mathematics is reduced to manipulations of finite strings of symbols. All mathematical objects and concepts are nothing more than the symbols that represent them. Here, I see a hypocritical claim of formalism, namely that everything is reduced to symbols. Why? Because formalism is based on two concepts, that of finiteness and that of strings (i.e. sequences of symbols, i.e. functions from subsets of the set of the natural numbers to an alphabet), which are themselves not formalized, i.e. reduced to symbols, because they are the basis of formalism and therefore prior to it. Nonetheless, sets are defined formally and then natural numbers and finiteness in terms of sets as if they were reducible to symbols, when in fact they are fundamental to formalism itself. To me, that looks like formalist hypocrisy.

What I have said does not mean that I am entirely against formalism. In fact, I very much appreciate the freedom that formalism bestows upon the mathematician, but I think that this freedom is to be interpreted as the freedom to explore whatever real mathematical realm one wishes rather than a symbol game with no further meaning.

I would like to ask how a formalist would counter my arguments, and whether formalism is indeed hypocritical.

[ThalesOfAthens]

I don’t believe I totally understand your questions, so forgive me if I am misinterpreting them. Formalism was in part constructed to make a foundational theory of mathematics which allows for:

Proofs to be checkable through “automated process” (to make sure that there were mathematical truths that were verifiably true)

Proofs to be defined on a set of axioms, and different sets of axioms lead to different proofs (and truths within that axiomatic set).

In order for the proofs to be understandable by humans, or machines, they have to be finite in length. That is to say, one could construct a proof which consisted of an endless applications of inference rules. However, such a rule would fall outside of formalism, because of its infinite nature. One could define such a set of theorems as “infinite theorems” which would have truths to them, but would not be provable through an automated process, nor through a human checking the validity, for this process would never end. Further, it would be difficult to publish such theorems, for they would involve an infinite number of inferences.

So I don’t think that disproves formalism, but rather contains it to a smaller domain than is possible to imagine.

I don’t believe that everything being reducible to symbols is necessarily hypocritical, but rather, another constraint of formalism. It can’t deal with mathematical notions, or theorems, which cannot be reduced to symbols. Those mathematical ideas are outside the realm of formalism. (And some would say, therefore outside of foundational mathematics).

Sets being defined formally with a set of symbols I don’t believe necessarily means that formalism is in a hypocritical position. Formalism is defining a basis for communicating mathematical ideas using symbols, the absence of a symbology would be a different form of mathematics, and a different paradigm. That is to say, it wouldn’t be formalism anymore, but something else.

[-1-]

According to the formalist philosophy of mathematics, all unproven assumptions must be explicitly stated as axioms, and all deductions must be made according to logical axioms and well-defined inference rules. Thus, I understand that formalism is a kind of foundationalism.

This system boils down to useless. "I assume that my theorem is true, which is that (X is Y) (for instance) or (X is Z) (for a different theorem) or (whatever you can dream up)." In this case X can't be anything but Y or Z or the dream, as the case might be, as this is an assumption, which is an axiomatic truth.

All you need to prove anything in math can be done by naming the theorem an "axiom" or assumed truth.

I don't know if "useless" in my terminology is equivalent to your "hypocritical". I leave that for the philosophers to decide.

[ChanceIsChange]

Here is a clearer version of my questions regarding the triangle. (The improved clarity is partly due to a more symbolic representation, ironically illustrating the usefulness of formalism in a thread criticizing formalism.)

Let
“∧” denote conjunction, i.e. (A ∧ B) means “A and B”,
“∨” denote disjunction, i.e. (A ∨ B) means “A or B (or both)”,
“⇒” denote implication, i.e. (A ⇒ B) means “A implies B”,
“⇔” denote equivalence, i.e. (A ⇔ B) means “A is equivalent to B”, i.e. “A implies B and B implies A”,
“:=” denote defined identity, i.e. (A := B) means “A is defined to be identical to B”, and
“:⇔”denote defined equivalence, i.e. (A := B) means “A is defined to be equivalent to B”.

Now define
A :⇔ the angle sum of a triangle is 180°,
E :⇔ the conjunction of all the axioms of Euclidean geometry,
C :⇔ the conjunction of all the axioms of Classical Logic.

My questions to the formalist and their possible answers run as follows:

Me: Why A?
Formalist: Because of E.
Me: Why E?
Formalist: That’s an axiom.
Me: Why E ⇒ A?
Formalist: Because of C.
Me: Why C?
Formalist: That’s an axiom, too.
Me: Why (E ∧ (E ⇒ A)) ⇒ A?
Formalist: Because of modus ponens, an inference rule of classical logic.
Me: Why C ⇒ (E ⇒ A)?

How would the formalist continue, and for how long? When will this regress end? Will it ever end at all?

… So I don’t think that disproves formalism, but rather contains it to a smaller domain than is possible to imagine.

The problem I see is that the concept of finiteness is fundamental to formalism and therefore not formalized itself (please correct me if I’m wrong). Of course, finiteness of sets can be formally defined, but at that point, we have already entered the formal realm and thereby accepted a concept of finiteness which underlies formalism and is therefore not formal itself.

Also, is there a formal proof for the proposition that a proof has to have finite length in order to be understandable by a machine?

I don’t believe that everything being reducible to symbols is necessarily hypocritical, but rather, another constraint of formalism.

You would be right if everything having to do with formalism were indeed reduced to symbols, but that’s not the case in my opinion. Why? Because the notion of formalism itself, as well as the notion of symbol string, are themselves not reduced to symbols. At least, that is how it appears to me. What I call hypocritical is that formalism nonetheless asserts that everything is reduced to symbols.

Sets being defined formally with a set of symbols I don’t believe necessarily means that formalism is in a hypocritical position.

Sets being defined in terms of a set of symbols is circular, isn’t it?

Formalism is defining a basis for communicating mathematical ideas using symbols, the absence of a symbology would be a different form of mathematics, and a different paradigm. That is to say, it wouldn’t be formalism anymore, but something else.

That’s right. What I’m saying is that formalism doesn’t go far enough. It tries to reduce everything to symbols and claims to be successful, but still relies on concepts such as finiteness, symbol and string that are not formalized. It also relies on laws that are not stated as axioms, contrary to its own spirit. For example, it relies on the fact that the symbol ‘x’ is the symbol ‘x’, an instance of the law of identity. However, this law is not always stated as an axiom, when in fact it should be. That would in turn contradict the tenet of formalism that we are free to choose our axioms. Being compelled to accept a certain axiom (such as the law of identity) would also mean that not everything follows just from the axioms, for example, the fact that we are compelled to accept that axiom follows from something else.

All you need to prove anything in math can be done by naming the theorem an "axiom" or assumed truth.

That is indeed possible in principle, but such a system of axioms would not be taken seriously. Only axiom systems that represent something “useful” will be taken seriously, such as the axiom system of ZFC. What is important is that everything is (supposedly) explicit and transparent. For example, you could not hide the fact that the axiom system you proposed (the one with the X) is not very useful, and a set theoretician could not claim results about sets to be true without them being verifiable by everyone.

I don't know if "useless" in my terminology is equivalent to your "hypocritical".

They are not equivalent. What you call useless is the arbitrariness by which axioms can be chosen, but I consider that aspect of formalism self-regulating and valuable for the freedom of the mathematician.

What I call hypocritical is the supposed explicitness of formal systems when they are in fact based on hidden, implicit concepts like finiteness and string, the supposed freedom of choice of axioms when in fact you are forced to accept certain assertions, such as the law of identity and the necessity of finiteness in proofs, and the supposed universal reducibility to symbols when in fact notions such as formalism and symbol are themselves not reduced to symbols.

[-1-]

"""What I call hypocritical is the supposed explicitness of formal systems when they are in fact based on hidden, implicit concepts like finiteness and string, the supposed freedom of choice of axioms when in fact you are forced to accept certain assertions, such as the law of identity and the necessity of finiteness in proofs, and the supposed universal reducibility to symbols when in fact notions such as formalism and symbol are themselves not reduced to symbols.""""

The axioms chosen have the restriction of creating something useful or transparent.

I had no idea those two restrictions existed, but they do.

So why is one restriction hypocritical and the other not?

Also, the quality of being hypocritical is a moral failure. "Do as I say but I am exempt from my own rules." Exceptions that apply to everyone do not make hypocritical people if the rulers who make the rules also obey the rules and the exceptions.

I am not saying you're not saying something; but your choice of qualifying your criticism in one word is perhaps ill-chosen. A system can't be hypocritical, because it is not a person capable of being morally judged or having ethical expectations to meet.

I think your problem could be solved by accepting that "Formalism is (...) but it is not recursive."

By (...) I meant whatever and however you define formalism. I sense (am I correct?) that your beef with your perception of formalism is that it can't be expressed as a symbol, and symbols can't be reduced to symbols.

So... formalism's not recursive. That makes it "hypocritical" in a sense, but then again... why is that an issue? It's not recursive, great, or too bad, but that's how the "rule-makers" made it.

--------

Let me ask you a question: can you design a system which is formalist and uses symbols reduced to symbols, and formalism reduced to a symbol? This is not a rhetorical question, but a real genuine information seeking question. What would this application involve in a sense of usefulness that could not be created in any other way?

If you can't come up with a useful system that uses recursive formalism, then I show you the mirror of your criticism of my perception of your description of formalism: here's looking at you, kid. "No usefulness, then you may as well discard the tool."

If, however, you come up with a system that uses recursive formalism, and it has real, useful applications, then you ought to win the Nobel prize, and I ain't joking. Or the equivalent in math prizes to the N.P.

[ChanceIsChange]

The axioms chosen have the restriction of creating something useful or transparent.

Actually, the axioms don’t have to represent anything useful; they only have to be consistent and transparent. The first property ensures that they represent anything at all, and the second one allows everyone to decide for themselves whether what is represented is useful or not.

So why is one restriction hypocritical and the other not?

What exactly do you mean?

Also, the quality of being hypocritical is a moral failure. […]A system can't be hypocritical, because it is not a person capable of being morally judged or having ethical expectations to meet.

My description of formalism as hypocritical is to be understood metaphorically. I argue that formalism has a property analogous in some respects to the ethical quality of hypocrisy:

"Do as I say but I am exempt from my own rules."

That is what formalism says; it decrees that everything should be reduced to symbols while not being reducible to symbols itself without appealing to a “meta-formalism”. This meta-formalism would in turn require a “meta-meta-formalism”, and so on.

I sense (am I correct?) that your beef with your perception of formalism is that it can't be expressed as a symbol, and symbols can't be reduced to symbols.

You are close to the truth. That formalism is not recursive is not a problem in itself, but it becomes one once formalism lays claim to being the foundation of mathematics, because if formalism is taken as the foundation of mathematics, it would preclude mathematical inquiry from being applied to formalism and thereby restrict it. Also, just as an explanation that can’t explain itself needs another one to explain it and is thereby not ultimate, so a foundation not based on itself can’t be taken as an ultimate foundation.

Let me ask you a question: can you design a system which is formalist and uses symbols reduced to symbols, and formalism reduced to a symbol?

I can’t design such a system at the moment, and I believe it to be impossible. If that is true, then formalism is not entitled to be the foundation of mathematics in my opinion.