Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It only takes a minute to sign up.
Sign up to join this community
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).
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?
