How foundation of mathematics can be based on a first order logic system?

Question

Let's assume that we have an axiomatic system that utilises the second order logic. Can this system be reformulated in terms of first order logic? I guess, it is not the case, since the second order logic is more expressive that the first order logic. If I am right, how than Zermelo-Fraenkel set theory can be used as foundation of mathematic (it uses only first order logic).

Answer 1

You need to ask yourself what you mean by a "foundation" for mathematics. This is important since claims about the nature of mathematics will carry unstated assumptions of an extra-mathematical character.

Several years ago controversy erupted on Internet sites because two advocates for homotopy type theory attempted to participate in the FOM mailing list started many years ago by Harvey Friedman. The details involve unfortunate personality traits exacerbated by strong differences of opinion. The HOTT advocates left the mailing list disgruntled by the lack of acceptance of their ideas.

Nothing about this story is meant to be critical. Within the HOTT literature you can find the explanation of how a foundation for mathematics is merely an "encoding" of mathematical ideas. In making these claims, HOTT theorists are attempting to place HOTT on the same footing as first-order logic with set theory. But, HOTT differs significantly.

In the discussions which ensued, many interested in HOTT proclaimed how HOTT satisfied their personal intuition for what a foundation for mathematics ought to be, whereas first-order logic with set theory did not.

One reason for this may be the historical account claiming that mathematics is arithmetized. A paper by Reyes sitting on my bookshelf asserts that one of the aims of categorical logic is to introduce a more "geometrical" account of logic.

It is the case that much of what is posted on the FOM mailing list is traditional with respect to arithmetization and Hilbert's arithmetical metamathematics. And, during the controversy Friedman discussed his differences with Lawvere. Of course, HOTT uses Lawvere's category-theoretic notion of set.

Disputes like this are not new. Brouwer's intuitionism declares mathematics to be the product of human creativity. On the other hand, Russell clearly explains that he is crafting an account of mathematics that will exclude the philosophical position called monism. Like Frege, he had been a critic of formalists. The idea that mathematics is extensional comes from the metaphysical motivations held by Frege and Russell.

The introduction of Heyting's "Intuitionism" contains an imaginative discussion among presumed advocates for different views. This kind of text is valuable for understanding that "foundation" means different things to different people.

As yet unmentioned is the rejection of completed infinities by the Russian constructivists. Markov's normal algorithms do not presume the "infinite tape" of Turing machines.

Positions like Brouwer's or the Russian constructivists do not try to portray a foundation as an " encoding" for all of mathematics in the same sense as set theory or HOTT. So, even that metamathematical view may be disputed.

With this said, your question falls in line with the received views concerning logic and mathematics. You should find the links provided by Mr. Allegranza helpful and informative.