5 ms·

Here's how I interpret Gödel's landmark result: > semantic properties, except for the most trivial systems, can't be inferred from syntactic properties. E.g.

Here's how I interpret Gödel's landmark result: > semantic properties, except for the most trivial systems, can't be inferred from syntactic properties. E.g. you can't type a program by seeing everything is using the correct literals and syntactic objects: you need to, sooner or later, know what the program /actually does/. But the problem is that mathematicians do, in fact, reason about semantics. So saying that "it's uncomputable" ignores the elephant in the room, which is that mathematicians compute theorems for a living. What do mathematicians have that enables them to compute the uncomputable: well-aligned chakras, magic, coffee grounds, the zodiac, etc...?

dwohnitmok 6y ago
Argh... this is the nuance I was talking about in another post. Godel's Completeness Theorem (which applies to many systems that Godel's Incompleteness Theorem also applies to) shows that in a sense semantic properties coincide with syntactic properties and so in fact can exactly be inferred from syntactic properties. What instead Godel's Incompleteness Theorems show is that you cannot exhaustively list all the semantic properties of what you care about, but combined with Godel's Completeness Theorems, only the ones "relevant" to your syntactic axioms.
- Konohamaru 6y ago
  This interpretation can't be correct, because Rice's Theorem says that no semantic property of any computer program is computable.
  - dwohnitmok 6y ago
    More nuance is needed; Rice's Theorem says that there is no formula for deciding any semantic property of an arbitrary computer program. Restricted classes of computer programs are totally fine, and in some sense that is exactly what a logical system is: a description of a restricted class of programs. But this is also getting a bit confusing because there are many different interpretations of how to tie computability to a logical system. For example the proof system of first-order logic can be interpreted as a single Turing machine program, not a family of ones, for which it is very possible to make all sorts of judgments about its semantic consequences.
    - Konohamaru 6y ago
      But that's ignoring the main thrust, which is that mathematicians compute /all sorts/ of uncomputable systems, with no apparent restriction. It's undecidable to have a general compression algorithm, but people compress data (e.g. their core values) to their theoretical limits all the time. If there's a landmark theorem that states "all mathematics greater than or equal to number theory is uncomputable, " and mathematicians make a living computing these systems, then I must conclude either a) mathematics is a Sokal affair on a cosmic scale b) something is wrong with the hidden presuppositions behind my theorem.
      - xyzzyz 6y ago
        > which is that mathematicians compute /all sorts/ of uncomputable systems, with no apparent restriction You are flattering us, but that's not actually true. We already have lots of trouble with proving (which is the same as computing, essentially) many computable things as it is. It is only occasionally that we can make progress on some uncomputable problem, and it's always because of making use of some properties very specific to said problem. The point of Rice theorem is that there's no universal method to solve any problem without any concern for the guts of that problem, and that's true: when mathematicians or computer scientists are proving that some computer program halts, they don't apply the same general machine, but instead they try to figure out some "tricks" based on the particular situation at hand, which will not generalize to every conceivable problem.
      - dwohnitmok 6y ago
        > all mathematics greater than or equal to number theory is uncomputable That's not what Godel's Incompleteness Theorem says though. Nor would I agree that "mathematicians compute /all sorts/ of uncomputable systems, with no apparent restriction." It is hard to describe the behavior of real-world mathematicians since that is the realm of psychology rather than logic or mathematics, but if we stick to the realm of idealized proofs, it's clear that we are only ever computing over computable descriptions of uncomputable systems (which is totally fine and something we do all the time!). For example, the first-order theory of the real numbers (real closed fields) is a classic example of a complete and decidable theory. Every first-order statement in that theory can be proved or disproved in an automated fashion. Yet how can this situation persist for the real numbers, entities which we clearly know are non-computable? Well the theory of real closed fields is capable of only describing a subset of the properties of the real numbers. It is worth emphasizing that this is a subset! Those properties in the theory of real closed fields apply perfectly fine to the real numbers. They just don't capture all its properties. So what about the other properties of the real numbers that, for example, make up the field of analysis? Well we can prove those in a larger theory, e.g. ZFC. And again the proofs in ZFC are computable objects, although ZFC itself is no longer decidable. So again the description of the real numbers is a computable thing, even if now we don't know how to computably enumerate all of its consequences (but again we know how to enumerate subsets of them!). Now does ZFC completely describe the reals? This depends on whether you're a mathematical Platonist or not. Do you believe in the notion of the one, true set of real numbers that exist on a Platonic plane independently of our axioms about them? That is there are no "independent" theorems, only theorems for which we haven't found the best way of grasping their Platonic truth? Then no ZFC does not completely describe the reals either as a result of Godel's incompleteness theorem. Alternatively do you believe that the real numbers are an artificial mathematical construction which can have different properties depending on which axioms you are willing to admit? Then there will be properties of the real numbers which are independent of ZFC as a result of Godel's incompleteness theorems.
pvarangot 6y ago
I may be wrong here, but don't mathematicians sometimes "compute" in a meta-language that's sometimes more powerful, or less formal, than the system they are inferring things about? Hence why they need results reviewed and a community to agree upon what's acceptable as a proof. Otherwise reviewing a proof would be an automatic process, if everything was done in the world of syntactic symbols with clear rules that tie one statement to the next.
- schoen 6y ago
  > Hence why they need results reviewed and a community to agree upon what's acceptable as a proof. Otherwise reviewing a proof would be an automatic process, if everything was done in the world of syntactic symbols with clear rules that tie one statement to the next. Nonetheless, we may still get to the second case because there are a couple of large projects that are trying to formalize all of mathematics in a way that a computer can verify. http://us.metamath.org/ http://us.metamath.org/ https://arxiv.org/abs/1910.09336 https://arxiv.org/abs/1910.09336 If these catch on and become a deeper part of the mathematics research process, mathematicians would still discuss "what's acceptable" in terms of their views of axioms, and they would presumably still discover proofs for theorems, but review for formal correctness of inferences could be an automatic process. Note that some pretty impressively complex and abstract theorems have successfully been formalized in these systems (and their proofs checked by machine), even starting from quite small axiom systems. Edit: In the mathlib paper they mention a much wider set of efforts along these lines: > In this section, we compare and contrast mathlib with other substantial formal libraries for mathematics, including libraries for Mizar [9,28], HOL Light [35], Isabelle/HOL [49], Coq/SSReflect [10,46], and Metamath [47]. Our goal here is not to provide detailed comparisons of the various de-sign choices, but, rather to sketch the design space in broad strokes, situate mathlib within it, and explain some of the decisions we have made. Our choice of comparisons is not meant to be exhaustive: there are also substantial mathematical libraries in HOL4 [55], ACL2 [42], PVS [50], and NuPRL [17], as well as notable libraries built on standard Coq, such as the Coquelicot analysis library [14].
- redvenom 6y ago
  There are two separate statements here: 1. Mathematicians often use relatively powerful systems, like reasoning in ZFC about Peano arithmetic. The consistency and completeness of axiomatic systems is what this article is about 2. Mathematicians pretty much exclusively use informal systems (compared to formal logic) for reasoning. The reason why that is is because it is just infeasible to reason typical mathematics using formal logic for most cases. However, it's important to realize that these two are orthogonal.

dwohnitmok 6y ago

Argh... this is the nuance I was talking about in another post. Godel's Completeness Theorem (which applies to many systems that Godel's Incompleteness Theorem also applies to) shows that in a sense semantic properties coincide with syntactic properties and so in fact can exactly be inferred from syntactic properties. What instead Godel's Incompleteness Theorems show is that you cannot exhaustively list all the semantic properties of what you care about, but combined with Godel's Completeness Theorems, only the ones "relevant" to your syntactic axioms.

Konohamaru 6y ago
This interpretation can't be correct, because Rice's Theorem says that no semantic property of any computer program is computable.
- dwohnitmok 6y ago
  More nuance is needed; Rice's Theorem says that there is no formula for deciding any semantic property of an arbitrary computer program. Restricted classes of computer programs are totally fine, and in some sense that is exactly what a logical system is: a description of a restricted class of programs. But this is also getting a bit confusing because there are many different interpretations of how to tie computability to a logical system. For example the proof system of first-order logic can be interpreted as a single Turing machine program, not a family of ones, for which it is very possible to make all sorts of judgments about its semantic consequences.
  - Konohamaru 6y ago
    But that's ignoring the main thrust, which is that mathematicians compute /all sorts/ of uncomputable systems, with no apparent restriction. It's undecidable to have a general compression algorithm, but people compress data (e.g. their core values) to their theoretical limits all the time. If there's a landmark theorem that states "all mathematics greater than or equal to number theory is uncomputable, " and mathematicians make a living computing these systems, then I must conclude either a) mathematics is a Sokal affair on a cosmic scale b) something is wrong with the hidden presuppositions behind my theorem.
    - xyzzyz 6y ago
      > which is that mathematicians compute /all sorts/ of uncomputable systems, with no apparent restriction You are flattering us, but that's not actually true. We already have lots of trouble with proving (which is the same as computing, essentially) many computable things as it is. It is only occasionally that we can make progress on some uncomputable problem, and it's always because of making use of some properties very specific to said problem. The point of Rice theorem is that there's no universal method to solve any problem without any concern for the guts of that problem, and that's true: when mathematicians or computer scientists are proving that some computer program halts, they don't apply the same general machine, but instead they try to figure out some "tricks" based on the particular situation at hand, which will not generalize to every conceivable problem.
    - dwohnitmok 6y ago
      > all mathematics greater than or equal to number theory is uncomputable That's not what Godel's Incompleteness Theorem says though. Nor would I agree that "mathematicians compute /all sorts/ of uncomputable systems, with no apparent restriction." It is hard to describe the behavior of real-world mathematicians since that is the realm of psychology rather than logic or mathematics, but if we stick to the realm of idealized proofs, it's clear that we are only ever computing over computable descriptions of uncomputable systems (which is totally fine and something we do all the time!). For example, the first-order theory of the real numbers (real closed fields) is a classic example of a complete and decidable theory. Every first-order statement in that theory can be proved or disproved in an automated fashion. Yet how can this situation persist for the real numbers, entities which we clearly know are non-computable? Well the theory of real closed fields is capable of only describing a subset of the properties of the real numbers. It is worth emphasizing that this is a subset! Those properties in the theory of real closed fields apply perfectly fine to the real numbers. They just don't capture all its properties. So what about the other properties of the real numbers that, for example, make up the field of analysis? Well we can prove those in a larger theory, e.g. ZFC. And again the proofs in ZFC are computable objects, although ZFC itself is no longer decidable. So again the description of the real numbers is a computable thing, even if now we don't know how to computably enumerate all of its consequences (but again we know how to enumerate subsets of them!). Now does ZFC completely describe the reals? This depends on whether you're a mathematical Platonist or not. Do you believe in the notion of the one, true set of real numbers that exist on a Platonic plane independently of our axioms about them? That is there are no "independent" theorems, only theorems for which we haven't found the best way of grasping their Platonic truth? Then no ZFC does not completely describe the reals either as a result of Godel's incompleteness theorem. Alternatively do you believe that the real numbers are an artificial mathematical construction which can have different properties depending on which axioms you are willing to admit? Then there will be properties of the real numbers which are independent of ZFC as a result of Godel's incompleteness theorems.

pvarangot 6y ago

I may be wrong here, but don't mathematicians sometimes "compute" in a meta-language that's sometimes more powerful, or less formal, than the system they are inferring things about? Hence why they need results reviewed and a community to agree upon what's acceptable as a proof. Otherwise reviewing a proof would be an automatic process, if everything was done in the world of syntactic symbols with clear rules that tie one statement to the next.

schoen 6y ago
> Hence why they need results reviewed and a community to agree upon what's acceptable as a proof. Otherwise reviewing a proof would be an automatic process, if everything was done in the world of syntactic symbols with clear rules that tie one statement to the next. Nonetheless, we may still get to the second case because there are a couple of large projects that are trying to formalize all of mathematics in a way that a computer can verify. http://us.metamath.org/ http://us.metamath.org/ https://arxiv.org/abs/1910.09336 https://arxiv.org/abs/1910.09336 If these catch on and become a deeper part of the mathematics research process, mathematicians would still discuss "what's acceptable" in terms of their views of axioms, and they would presumably still discover proofs for theorems, but review for formal correctness of inferences could be an automatic process. Note that some pretty impressively complex and abstract theorems have successfully been formalized in these systems (and their proofs checked by machine), even starting from quite small axiom systems. Edit: In the mathlib paper they mention a much wider set of efforts along these lines: > In this section, we compare and contrast mathlib with other substantial formal libraries for mathematics, including libraries for Mizar [9,28], HOL Light [35], Isabelle/HOL [49], Coq/SSReflect [10,46], and Metamath [47]. Our goal here is not to provide detailed comparisons of the various de-sign choices, but, rather to sketch the design space in broad strokes, situate mathlib within it, and explain some of the decisions we have made. Our choice of comparisons is not meant to be exhaustive: there are also substantial mathematical libraries in HOL4 [55], ACL2 [42], PVS [50], and NuPRL [17], as well as notable libraries built on standard Coq, such as the Coquelicot analysis library [14].
redvenom 6y ago
There are two separate statements here: 1. Mathematicians often use relatively powerful systems, like reasoning in ZFC about Peano arithmetic. The consistency and completeness of axiomatic systems is what this article is about 2. Mathematicians pretty much exclusively use informal systems (compared to formal logic) for reasoning. The reason why that is is because it is just infeasible to reason typical mathematics using formal logic for most cases. However, it's important to realize that these two are orthogonal.