Therefore we cannot prove a statement that cannot be proven in this axiomatic system is semantically true, and to the extent of our logical method, this new axiomatic system can never be proven incomplete. — simeonz
I couldn't express myself properly, but this is what I meant. I was attempting to construct an axiomatic system, whose undecidable sentences are not amenable to further evaluation by means of metalogic. The idea was to start with incomplete axiomatic system and to import proofs of undecidable statements by continuously adding meta-axioms. There were problems with this approach.These "true but unprovable" statements will appear to use as simply undecidable. — alcontali
If I understand you correctly, there are axiomatic systems which preserve the truth values of all statements of Peano arithmetic, but make previously undecidable statements decidable? It is a curious fact. So, we don't actually have an axiomatic system yet, in which all statements of Peano arithmetic are decidable?Number theory (by default: Dedekind-Peano) is a sub-theory of set theory (by default: ZFC), meaning that every number-theoretical theorem can be proven in set theory, but not the other way around. Now, there really are number-theoretical theorems that are fundamentally undecidable in number theory (=DP), but provable in the larger set theory (=ZFC): — alcontali
Just thinking out loud, I wonder whether we would know if ZFC is semantically complete or not, if it were deductively incomplete? And what would be our course of action if we can't know? And on a related note, I wonder whether a theorem with the same quality as Chaitin's constant for Turing machines can be discovered for ZFC - having definite truth value, but no proof in logic or meta-logic.Now, we may not have fundamentally stronger theories than set theory (=ZFC). In other words, there may not be such larger theory of which set theory would just be a sub-theory. Therefore, when a theorem is undecidable in set theory, it may even be absolutely undecidable. — alcontali
Yes, I think that it is also intuitive that ZFC cannot be weaker than a universal Turing machine. I also thought that it cannot be stronger. Since non-deterministic Turing machines are computationally equivalent to their deterministic counterpart and should be able to simulate successfully any deductive system. I mean - that was my intuition anyhow.One reason why we may not go higher nor further than ZFC, is because ZFC is already at the level of Turing-completeness -- can compute everything that is computable and therefore: can represent all knowledge that can be expressed in language. ZFC is possibly even stronger than that — alcontali
I have wondered about this. I am not intimately familiar with the hypothesis, but it becomes ever more so obvious that material and abstract sciences are intertwined together. There are some implicit assumptions here, like discrete finite state and determinism. If I recall correctly non-determinism cannot produce more computability. But it can produce more outcomes, and I cannot tell whether this can contribute to nature somehow. Analog or infinite state may be unfeasible, as per QM. The hypothesis does depend on a number of assumptions, but may be true nonetheless.On the other hand, Turing Completeness is already a seriously constraining limit:
All known laws of physics have consequences that are computable by a series of approximations on a digital computer. A hypothesis called digital physics states that this is no accident because the universe itself is computable on a universal Turing machine. This would imply that no computer more powerful than a universal Turing machine can be built physically. — alcontali
If I understand you correctly, there are axiomatic systems which preserve the truth values of all statements of Peano arithmetic, but make previously undecidable statements decidable? — simeonz
So, we don't actually have an axiomatic system yet, in which all statements of Peano arithmetic are decidable? — simeonz
I think I understand the nuance. There are undecidable deductively complete theories, so claiming that an undecidable statement makes a theory deductively incomplete sounds strange. Saying that the statement is independent from the axioms, purely as a vocabulary, reduces the confusion.By the way, there is a problem with the terminology. Decidability is about computability:
...
While independence is about provability:
...
The difference between "undecidable" and "independent" seems to depend mostly "on the peculiarities of either formalism" rather than on truly fundamental issues. — alcontali
I find the Curry-Howard Correspondence a little strange. I'm sure it makes sense, but likening axioms to a pre-execution invariant and theorems to a post-execution invariant appears complicated. It may have something to do with formal verification processes, but for me, the relationship between proofs and computation appears to be about enumeration of proofs by turing machines in one direction, and the generation of booleans on the Turing tape for the proven theorems after every inference step in the other direction.Given the Curry-Howard Correspondence, undecidability and independence overlap much stronger than suggested — alcontali
After clearing up my error in understanding, hopefully, I am not very surprised. Indeed, because of Gödel's completeness theorem, if a theory were able to prove a statement of PA that PA iteself couldn't, it would have fewer models. The stronger theory would not simply be deductively stronger, but semantically stronger. I was mistakenly excited that a theory with equivalent semantics (one that is expansion of PA) could cure PA's incompleteness. I was hoping that because the new axioms are not statements of PA itself, but their interpretations, they might result in some completely different configuration, without restricting the model space. But this is apparently not the case, at least for first-order logic.ZFC is not more powerful than PA because it knows more stuff. In fact, that would not be possible. Such theorem (as well as its proof) would still be a Gödel number which PA can also reach. Therefore, PA actually "knows" all possible theorems (and their proofs) that can be expressed in language. Therefore, it also knows all the axioms and all theorems (including their proofs) of all the other systems. The problem is that PA does not "trust" them. — alcontali
I also couldn't clear up if ZFC is decidable, undecidable, or not yet established. Wikipedia indicates that there are only decidable sublanguages, while a stackexchange answer indicates that ZFC is recursively enumerable, which if mu-recursively enumerable, should mean that ZFC is decidable by Turing machines. — simeonz
Since the semantic incompleteness proof holds for the standard model, what is the "intended" interpretation for other theories. — simeonz
I find the Curry-Howard Correspondence a little strange. I'm sure it makes sense, but likening axioms to a pre-execution invariant and theorems to a post-execution invariant appears complicated. It may have something to do with formal verification processes, but for me, the relationship between proofs and computation appears to be about enumeration of proofs by turing machines in one direction, and the generation of booleans on the Turing tape for the proven theorems after every inference step in the other direction. — simeonz
My understanding from the definition was that for a theory to be decidable, it is necessary to have effective enumeration of its theorems, not to have a theorem for every statement or its negation. In that sense, I thought, whether ZFC is decidable is a separate subject matter from its syntactical incompleteness.ZFC is subject to the diagonal lemma, and therefore is syntactically incomplete. Hence, it must necessarily have undecidable statements that can be expressed in first-order logic. — alcontali
I understand, but just to clarify. I wasn't so much curious about Gödel's semantic completeness directly as application with respect to other axiomatic systems, i.e. examples of models that satisfy a statement that is independent of the axioms. I was wondering whether there exists a definition of some kind of "minimal" class of models for every theory. Because, as it stands, I am under the impression that semantic incompleteness says nothing that the syntactic incompleteness and semantic completeness theorems together don't say. If such models were defined and coincided with our "intuitive" definition of interpretation of a theory (similarly to what denotational semantics offers for recursive programs), and Gödel's semantic incompleteness were shown to apply to such models (i.e. they always satisfied a statement that cannot be derived from the axioms), it would make the claim stand on its own.Concerning the implications of Gödel's semantic completeness theorem for other systems than Peano arithmetic, we are talking about advanced model theory, which is an enormous subject in itself. — alcontali
Absolutely. I will look into it on my own when I have the time. Logic is a past time interest for me, so I have gaps in my understanding at the moment. But I am trying to cure them, a piece at a time.It is interesting to work on such explanation by examples, but then again, who else would be interested in reading the results? This discussion on the diagonal lemma is probably already more than what many potential readers would want to handle ... — alcontali
My understanding from the definition was that for a theory to be decidable, it is necessary to have effective enumeration of its theorems, not to have a theorem for every statement or its negation. — simeonz
A theory (set of sentences closed under logical consequence) in a fixed logical system is decidable if there is an effective method for determining whether arbitrary formulas are included in the theory. — Wikipedia
Decidability should not be confused with completeness. For example, the theory of algebraically closed fields is decidable but incomplete, whereas the set of all true first-order statements about nonnegative integers in the language with + and × is complete but undecidable. — Wikipedia
From the definition you quoted, a complete axiomatic theory has a proof for either the statement or its negation. That does not mean that all such proofs or statements can be enumerated by a single effective procedure simultaneously. (PS. According to the previous edit I made, the answer is yes, for the more conventionally axiomatized theories.)Completeness. A set of axioms is (syntactically, or negation-) complete if, for any statement in the axioms' language, that statement or its negation is provable from the axioms (Smith 2007, p. 24). — alcontali
I reason, that for a statement to lack proof implies that it is not part of the axiomatization consequences. Not that it is part of the axiomatization consequences, but those cosequences cannot be computed.First Incompleteness Theorem: "Any consistent formal system F within which a certain amount of elementary arithmetic can be carried out is incomplete; i.e., there are statements of the language of F which can neither be proved nor disproved in F." (Raatikainen 2015) — Wikipedia
This contradicts the summary, by clearly stating that validity is not the subject of the theorem. And finally, the following paragraph shows that the Gödel sentence is merely satisfiable in the standard model, not in every model:The first incompleteness theorem shows that the Gödel sentence GF of an appropriate formal theory F is unprovable in F. Because, when interpreted as a statement about arithmetic, this unprovability is exactly what the sentence (indirectly) asserts, the Gödel sentence is, in fact, true (Smoryński 1977 p. 825; also see Franzén 2005 pp. 28–33). For this reason, the sentence GF is often said to be "true but unprovable." (Raatikainen 2015). However, since the Gödel sentence cannot itself formally specify its intended interpretation, the truth of the sentence GF may only be arrived at via a meta-analysis from outside the system. — Wikipedia
Although the Gödel sentence of a consistent theory is true as a statement about the intended interpretation of arithmetic, the Gödel sentence will be false in some nonstandard models of arithmetic, as a consequence of Gödel's completeness theorem (Franzén 2005, p. 135). — Wikipedia
So, as you stated, if ZFC were complete it would be decidable. But since it is not, does my original question - if it is decidable or not still stand? — simeonz
However, since the Gödel sentence cannot itself formally specify its intended interpretation, the truth of the sentence GF may only be arrived at via a meta-analysis from outside the system. — Wikipedia
This contradicts the summary, by clearly stating that validity is not the subject of the theorem. — simeonz
I see. Thinking about it, semidecidability I imagine will carry a lot of practical utility for applications like automated theorem proving, even though it doesn't guarantee termination. Decidability is probably more crucial to theoretic analysis.I suspect that ZFC is not decidable, but then again, it really depends on the link between completeness and decidability. If there exists a procedure to solve the proof problem, the proof problem is decidable. That means that the theorem is provable from the theory. In that sense, provability is a decidability problem, because a proof is a procedure. — alcontali
I actually don't know how the syntactic incompleteness was proven (through the same meta-logical argument as its semantic counterpart or not), but it seems that you shouldn't need a lot of semantics in order to demonstrate that some statement is independent. If the statement's derivation involves circularity (like the Gödel sentence), it should be entirely a deductive property if this circularity can be eliminated or not. But I might be wrong.I think that it is the semantic completeness theorem that throws a spanner in the works: For a statement deemed true by the system, some proof must exist within the system. — alcontali
I actually don't know how the syntactic incompleteness was proven (through the same meta-logical argument as its semantic counterpart or not), but it seems that you shouldn't need a lot of semantics in order to demonstrate that some statement is independent. If the statement's derivation involves circularity (like the Gödel sentence), it should be entirely a deductive property if this circularity can be eliminated or not. But I might be wrong. — simeonz
I am not familiar either, considering that I didn't understand its significance before yesterday. But from what I understand, it essentially states that inference and semantics are equivalent in a first order theory. If the theory knows something, it is true in all models (i.e. true for all interpretations consistent with the axioms), and if something is true in all models, the theory knows it. I don't find this surprising, as it makes intuitive sense. What I find more surprising is that it doesn't hold for higher order logics, as elaborated here:I am not familiar enough with Gödel's semantic completeness theorem. The explanation does not contain elaborate examples to illustrate the details of what they are talking about. It would be quite a job to inject examples in the right places. — alcontali
The completeness theorem is a central property of first-order logic that does not hold for all logics. Second-order logic, for example, does not have a completeness theorem for its standard semantics (but does have the completeness property for Henkin semantics), and the set of logically-valid formulas in second-order logic is not recursively enumerable. The same is true of all higher-order logics. It is possible to produce sound deductive systems for higher-order logics, but no such system can be complete. — Wikipedia
A ring is "almost" a field -- it just lacks inverses (it is not closed under division) -- but that's the little I understand of why this ring is still a model (=σf-structure) of a field ... I hope that Wikipedia will manage to better elaborate on this subject. — alcontali
Get involved in philosophical discussions about knowledge, truth, language, consciousness, science, politics, religion, logic and mathematics, art, history, and lots more. No ads, no clutter, and very little agreement — just fascinating conversations.