Shouldn't you use 2 for a '(' instead of 1?
Nevermind, my mistake
What Gödel Discovered
61–70 of 271 posts
Re: What Gödel Discovered
#62Earlier quoted context omitted.
It implies an infinity of inconsistent statements. I'm not a mathematician, but the way I understand it is to do an analogy with the halting problem: for any programming language that is powerful enough you can build a program where you don't know if it's going to halt or not. About avoiding singularities, the GEB book (Godel,Escher,Bach) mentions at the beginning: mathematicians like Russel tried to avoid paradoxes…
I think the question is a bit more specific in the context of the halting problem We know by contradiction that we cannot write a program that determines if any program halts, if the program being checked also contains the program that determines if itself halts. Is this the only class of program that cannot be determined to halt?
No, is not the only class of program. An easy example is to take any of the unsolved math problems (like the Goldbach conjeture) and write a program for it, if the program halts it proves the conjeture.
Can you tell if the program halts? You can’t without proving the conjeture.
Re: What Gödel Discovered
#63Here'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…
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 seman…
This interpretation can't be correct, because Rice's Theorem says that no semantic property of any computer program is computable.
Re: What Gödel Discovered
#64Very off-topic, but long ago when Albert Einstein went for a car ride with Mr. Gödel to become U.S. citizens, Einstein was trying very hard to think of ways to shut him up about a Constitution loophole he discovered. Things didn't go exactly as planned, and in front of the naturalization examiner, Mr. Gödel started blabbing about how he had found a way the U.S could be transformed into a fascist regime... Sources: ht…
In light of current circumstances this story has actually been on my mind! Has there ever been any more detail revealed about Godel's scheme?
Re: What Gödel Discovered
#65Here'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…
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…
> 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.
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].
Re: What Gödel Discovered
#66Earlier quoted context omitted.
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 seman…
This interpretation can't be correct, because Rice's Theorem says that no semantic property of any computer program is computable.
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.
Re: What Gödel Discovered
#67Earlier quoted context omitted.
Others have explained why you can't wave away inconsistency (principle of explosion) nor incompleteness (adding new axioms just creates a new axiomatic system with its own Godel sentences). However you might also find it interesting what incompletenesses exist in our own mathematical system (ZFC) -- the most well-known example is the Continuum Hypothesis[1]: > There is no set whose cardinality is strictly between tha…
> being able to prove the CH is an incompleteness in ZFC. It's only incompleteness if the CH is true or false at the semantic level, "outside" of the logic system under discussion. But the CH may be neither true or false, semantically, if the meaning of "existence of a set whose cardinality is strictly between that of the integers and the real numbers" strictly depends on the axioms and logic used to define sets and…
[deleted]
Re: What Gödel Discovered
#68Very off-topic, but long ago when Albert Einstein went for a car ride with Mr. Gödel to become U.S. citizens, Einstein was trying very hard to think of ways to shut him up about a Constitution loophole he discovered. Things didn't go exactly as planned, and in front of the naturalization examiner, Mr. Gödel started blabbing about how he had found a way the U.S could be transformed into a fascist regime... Sources: ht…
In light of current circumstances this story has actually been on my mind! Has there ever been any more detail revealed about Godel's scheme?
There is some more information at
https://jeffreykegler.github.io/personal/morgenstern.html
There's also an article about this question at
Re: What Gödel Discovered
#69Very off-topic, but long ago when Albert Einstein went for a car ride with Mr. Gödel to become U.S. citizens, Einstein was trying very hard to think of ways to shut him up about a Constitution loophole he discovered. Things didn't go exactly as planned, and in front of the naturalization examiner, Mr. Gödel started blabbing about how he had found a way the U.S could be transformed into a fascist regime... Sources: ht…
Wait what? Do tell, the links aren't great on my phone.
Re: What Gödel Discovered
#70Loving this so far!
One tiny typo that threw me for a loop for a second was:
> when apples are a fruit, then bananas or applies implies bananas or fruits
which should be:
> when apples are a fruit, then bananas or apples implies bananas or fruits