2
$\begingroup$

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?

$\endgroup$
7
  • $\begingroup$ Interesting question:) $\endgroup$ Feb 20 at 21:35
  • $\begingroup$ 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. $\endgroup$ Feb 20 at 21:41
  • 4
    $\begingroup$ 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. $\endgroup$ Feb 20 at 21:56
  • $\begingroup$ It's all just symbol shunting. Any meaning we ascribe to it is metaphorical. $\endgroup$ Feb 20 at 22:46
  • 2
    $\begingroup$ How can linguistics logic try to model human language, when human language is used to write linguistics? $\endgroup$ Feb 21 at 6:54

1 Answer 1

3
$\begingroup$

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.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .