# How can mathematical logic try to model math, when mathematics are used to define mathematical logic?

I've done so far a few courses in logic and formal verification, and I've always wondered: mathematical logic, at least as Hilbert envisioned, tries to model mathematics. Formally define what a "true" statement is, or why proving something (at least in a sound system) makes it true.

But, every logic course uses mathematics in its essence. The use of sets, functions and series' (as with inductive groups, for example) - is already mathematics, in a field that tries to model exactly that.

Isn't that circular logic?

• Interesting question:) Feb 20 at 21:35
• I don't see a contradiction - but I am not an expert for mathematical logic. To "model" need not be circular here, and of course it depends what is meant by this - "to model". In the naive sense, prime numbers model number theory, although number theory is used to define prime numbers. But this is certainly a bad comparison. Feb 20 at 21:41
• Have you seen this and this? If not they're worth having a look at. If they don't answer your doubts, then it will help if you explain what they leave to be desired. I think it's basically a misconception that the whole point of logic is to "build up" maths from the ground up - it's a big field with many different things going on, though that is one part of it. To really grasp the answer takes some "mathematical-philosophical maturity" that you should trust will come with time. Feb 20 at 21:56
• It's all just symbol shunting. Any meaning we ascribe to it is metaphorical. Feb 20 at 22:46
• How can linguistics logic try to model human language, when human language is used to write linguistics? Feb 21 at 6:54

## 1 Answer

It is a common misconception many logic students pass by.

Let us start with an example: Every microprocessor we use has its own design, and we can implement it in different ways: Either physically with silicon wafers, virtually with emulators, or even over Minecraft. Nobody says the design of a microprocessor is circular or contradictory. However, people become confused if a "microprocessor" becomes a "formal theory."

Formal theories, like first-order logic, set theories, or type theories can be viewed as sets of axioms and formal rules. We can implement them as computer programs (like Coq or Lean, which implement a type theory) or over another theory (as a formal theory, an interpretation, or a model.) Mathematical logic handles formal theories as objects implemented over a metatheory, and we can ask what can hold for 'implemented' formal theories.

This line of understanding collides with a common belief that mathematical logic is a field trying to build up mathematics from the ground. It was true that mathematical logic in the early 20th century focused on building a theory ensuring the consistency of mathematics. However, it changed around the advent of Hilbert's program and the incompleteness theorem.

Hilbert formulated a program for defining a complete foundation for mathematics, and he assumed that the 'perfect' foundation should satisfy some desirable properties (like soundness and completeness.) It might be disputable that "we proved a completeness of $$T$$ from a metatheory" ensures "$$T$$ is complete indeed in the reality" (The word "reality" is also quite ambiguous, although it should be clear in the Platonist view.) However, establishing the completeness of $$T$$ over some metatheory is good evidence of the preference of $$T$$ over other theories without any justification.

However, Gödel proved that we cannot formulate a complete theory (more precisely, sound, complete, and recursively axiomatizable extension of $$\mathsf{PA}$$.) Hilbert's program turned out not to work, but Hilbert's view on analyzing a formal theory over mathematics turned out to be useful.

By that tendency, modern logic textbooks teach students about the properties of formal theories over a metatheory, and they do not try to build a formal theory encompassing the entire mathematics.