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?

ThalesOfAthens wrote: … 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?

ThalesOfAthens wrote: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.

ThalesOfAthens wrote: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?

ThalesOfAthens wrote: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.

-1- wrote: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.

-1- wrote: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.