Is it possible to formalize mathematics by using a different logic system (higher order, non-classical logics, model theory…)?

Is it possible to formalize mathematics by using a different logic system (higher order, non-classical logics, model theory…)?

Hilbert's dream (against Gödel). The axiomatic system of all mathematical theories. I mean axiomatic formalization or axiomatization in terms of the Hilbert's program, which imply developping a single logical-mathematical language or formal system to formalize every possible mathematical theory (well, or at least, the actual existing ones).

• Why downvote ? Its a reasonable question. Sep 15, 2016 at 0:04
• No, using a different logical system doesn't change much in terms of ability to formalize mathematics. We can already formalize mathematics using the usual systems, and also using other systems. Exactly how much we can formalize depends on which system we use. Could you please expand and clarify the question? Sep 15, 2016 at 0:08
• Please include your question in the body of your post not just in the title. "Hilbert's dream (against Goedel)" isn't a useful question. Sep 15, 2016 at 0:09
• I mean axiomatic formalization or axiomatization in terms of the Hilbert's program, which imply develop a single logical-mathematical language or formal system to formalize every possible mathematical theory (well, or at least, the actual existing ones). Sep 15, 2016 at 0:25
• No, that is impossible, regardless what system you use. Sep 15, 2016 at 0:27

Your question is way too vague to answer properly, so let's try to pin down exactly what you mean.

What is going on when mathematicians claim that all of common mathematics can be grounded in first order logic? Well, it means that there exists interpretations that allow you to identify the structures used in different areas of mathematics with syntactical expressions expressed in the language of set theory.

Are there other alternatives to FOL? Sure. It would be pretty damn surprising if of all formalizations of logical reasoning we had chosen the only one that truly works.

So let's go for the quest of other logic to ground mathematics on! What properties would we like our theory to have?

Well, first of all we would like our theory to be expressive. We want our logic to be able to handle complex mathematical structures like numbers and infinite sets of numbers and groups and categories and whatnot.

On the other hand, we would like our logic to be nicely behaved, in the sense that it is possible to easily compute the logical entailments of the theory.

But it turns out that you cannot get both. By Tarsky's theorem, as soon as you have a system expressive enough to talk about basic arithmetic, undecidability kicks in and you are left with a semidecidable (at best) theory.

There are useful logical theories which are decidable and useful, such as modal provability logic and propositional logic, but they are limited in their scope.

On the other hand, there are also more expressive theories than FOL, such as Higher Order Logic. This comes at the expense of losing semidecidability.

On a personal note, I think that Hilbert's dream is far from dead, and that we should keep trying to come up with a better way of formalizing and automating math. Sure, there will always be undecidability and tricky self referential sentences whose value we are unsure about, but we humans still manage to talk meaningfully about the world and make useful deductions, so why not formalize that powerful intuition?

• You just mentioned "intuition" and I thought about intuitionism, the problem is what is considered a proof of a given mathematical statement. And we can wonder also about superintuitionistic logics or intermediate logics, inside classical logics. But I can't imagine how it would be possible to construct an axiomatic system of all mathematical theories, including at the same time classical-logic-based mathematical theories and non-classical-logic-based mathematical theories. Although model theory seems to be very powerful language. Sep 15, 2016 at 1:25
• The key insight to be had is that you can embed primitive concepts of certain logics into the language of others. Thus we can talk about analysis and probabilities and other concepts all within FOL using appropriate translations between one and the other. TBH once you get a logic capable of defining all computable functions you aren't going to get more expressiveness by adding more stuff, though you could certainly express things more naturally. Also, model theory is not a language, but the study of interpretation in logic. Sep 15, 2016 at 1:36
• Ok, model theory is itself a metalanguage to talk about another formal languages, but of course we are talking about a metalevel here, if a mathematical theory consists of an axiomatic system and all its derived theorems, we are talking about the metatheory of all mathematical theories. I found an interesting approach from paraconsistent logic to avoid inconsistency, but I don´t know how it would affect to decidability, here the link: philosophy.stackexchange.com/questions/7317/… Sep 15, 2016 at 1:48