The Coq mailing list

[Ken Kubota <mail AT kenkubota.de>]

My general criticism of the existing presentations of Goedel's theorems is that it is never discussed that defining truth in terms of a metatheory itself is a (usually tacit) philosophical assumption, which can be challenged.

While it is clear that Goedel's theorems are formally correct, the underlying assumption of a distinction between syntax and semantics in the common understanding of the proofs is a philosophical ingredient outside of the mathematical proofs presented by Goedel.

Another approach would be a purely syntactical approach, in which mathematical meaning is obtained by syntactical reasoning only, in other words, syntax is identical with semantics (which is my approach).

Then it would be impossible to call this "incompleteness," since completeness is obtained automatically by the identity of syntax and semantics, and Goedel's theorems boil down to the conclusion that within calculi of the strength of Peano arithmetic it is possible to construct well-formed formulae which are neither provable nor refutable.

Simply being grammatically correct doesn't mean being meaningful, as I have argued earlier with a syntactically well-formed, but nonsensical example sentence of natural language "Mathematics is liquid" at

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-July/msg00029.html

Then, although the formal statements of Goedel's theorems are correct, the term "incompleteness" is inaccurate and Goedel's theorems don't have the philosophical relevance usually associated with them.

This criticism would also apply to the post by Kevin Buzzard, who wrote:

We all know Goedel proved that there are true maths statements that aren't provable, so true != provable.

https://twitter.com/XenaProject/status/1363537114265247746

His article

Where is the fashionable mathematics?

https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/

generally is nearest to my position, however, the Pi operator in Lean should be replaced by type abstraction (thus avoiding introducing meta-theoretical elements into the syntax), as mentioned at

https://groups.google.com/g/metamath/c/Fgn0qZEzCko/m/bvVem1BZCQAJ (linked at https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/#comment-1005).

Kind regards,

Ken Kubota

____________________________________________________

Ken Kubota
https://doi.org/10.4444/100

Am 22.06.2021 um 12:15 schrieb Andrei Popescu <andrei.h.popescu AT gmail.com>:

Greetings,

I think a main problem with the formulations of Gödel's incompleteness
theorems from the literature is that they are either too concrete
(focussing on a particular setting, e.g., extensions of Peano
arithmetic within classic FOL) or too abstract (e.g., at the level of
provability logic). I've recently written a paper with Dmitriy Traytel
https://www.andreipopescu.uk/pdf/Goedel_JAR_2021.pdf
where we "distill" the amount of structure and properties needed for
being able to formulate these theorems. Particular attention is paid
to the notion of truth in a standard model and to the avoidance of
unnecessary assumptions (e.g., classical reasoning) about the object
logics.

Best wishes,
Andrei