Talk:Gödel's completeness theorem

This is the talk page for discussing improvements to the Gödel's completeness theorem article.
This is not a forum for general discussion of the article's subject.

Put new text under old text. Click here to start a new topic.
New to Wikipedia? Welcome! Learn to edit; get help.

Article policies

Find sources: Google (books · news · scholar · free images · WP refs) · FENS · JSTOR · TWL

Shouldn't the redirect be the other way around ? User:TraxPlayer

Equivalence to ultrafilter lemma

When you want to claim two theorems of ZFC are equivalent, you need to specify what weaker theory they are equivalent over. Every pair of theorems ZFC is (trivially) provably equivalent over ZFC. So for example, the ultrafilter lemma and the statement 1 + 1 = 2 are equivalent over ZFC.

I believe if you say something is equivalent to a weak form of the axiom of choice it's clear from context that you are working over ZF, except perhaps in some very special situation where there is another obvious candidate around. --Hans Adler 16:50, 14 November 2007 (UTC)[reply]

Also, could somebody give me (in the discussion) a quick sketch of that proof? I don't see it offhand. I suppose that you need something to do the Henkin construction; is that it? —Preceding unsigned comment added by CMummert (talk • contribs)

Henkin construction is one direction, of course. For the other, let F be a filter over some Boolean algebra. Define a language L with predicates U to represent membership in the ultrafilter, and < to represent the order relation on the algebra. Also it should have a constant representing each element of the algebra. Then the axioms of the theory T should include the state graphs of <, U(c) for each c representing an element of F, and U(c) v U(d) for all c and d, with d the complement of c. Then by the completeness theorem, this theory has a model iff it is consistent. But it is consistent iff every finite subset of the axioms is consistent, which is obvious because every such subset is modeled by a finite extension of F. And from any model of the full theory T, an ultrafilter can be constructed. Ben Standeven 04:15, 17 April 2007 (UTC)[reply]

A sketch of the proof would be very helpful. The claim that the completeness theorem is equivalent to the ultrafilter lemma is surprising, since the article on the ultrafilter lemma says the lemma can't be proved from ZF. So that would indicate that the completeness theorem also can't be proved from ZF. Does this basic property of first-order logic depend on powerful set theory axioms outside ZF? Am I missing something? Thanks.

The completeness theorem can of course be proved in ZFC, otherwise it wouldn't be so universally accepted. Obviously you are right that the axiom of choice is outside ZF, but I think most model theorists would reserve the expression "powerful set theory axiom" for things like existence of measurable cardinals. --Hans Adler 16:45, 14 November 2007 (UTC)[reply]

It seems to me that the Ultrafilter Lemma is not needed in any reasonable case, for example if the language is countable, or at least well ordered. Am i wrong? --Cokaban (talk) 14:49, 15 April 2008 (UTC)[reply]

You aren't wrong as such, but the 'reasonable' cases are not the only important ones. For example, model theorists routinely throw uncountable collections of constants around and then apply completeness to the resulting language. Algebraist 13:04, 26 May 2008 (UTC)[reply]

I am still not convinced: if you have to throw in an uncountable collection of constants, why not choose a well-ordered one?

I think it deserves at least mentionning that you can "usually" get away without the AC. --Cokaban (talk) 18:48, 26 May 2008 (UTC)[reply]

Proof trees / pictures

"Common to all deductive systems is the notion of a formal deduction. This is a sequence (or, in some cases, a finite tree) of formulas with a specially-designated conclusion."

It's nice to have a link to an article with beautiful pictures. I think we should only spoil the fun if there is something that actually answers the question: "How are arboreal deductive systems represented?" The article on proof theory ("Proofs are typically presented as inductively-defined data structures [...]") suggests tree (data structure). I am not familiar with the culture of proof theory. (Haven't been in Leeds long enough yet). So I am not sure if this is adequate, and I almost hope it's not. Both articles can remind us that we need more illustrations. For example for this article a scan of the the cover page / title or a typical formula from Gödel's thesis or publication come to mind. (I suppose that would be fair use, someone please correct me if I am wrong.) --Hans Adler (talk) 09:48, 21 November 2007 (UTC)[reply]

I've changed the link to tree to tree structure, which is a bit more general than tree (data structure), and in any case is much better than an article on large woody plants (though without as many nice photographs). 86.136.228.84 (talk) 12:48, 3 January 2008 (UTC)[reply]

A somewhat related matter: I suspect that this article gets a relatively large number of hits from non-mathematicians (coming from the incompleteness theorem, or having mistyped it). I tried to give them a vague understanding of what the theorem is about. Can we put something like this back into the current version (much improved by User:CBM) if we make it absolutely clear that it is not meant to be exact? I am still trying to learn how we handle these mathematicians vs. non-mathemiticians matters. --Hans Adler (talk) 10:06, 21 November 2007 (UTC)[reply]

We just balance correctness, accessibility, and intuition, on a case-by-case basis. Please do feel free to add more content; others will edit it, and eventually a version will be found that most people are happy with. I tried to add some more intuition to the lede this morning. My concern before was that it focused heavily on enumerability of logical validities, which is important but not in my opinion the most important part of the completeness theorem.

I don't know what the copyright status of Gödel's thesis is; if it is still copyrighted, then we wouldn't be allowed to use a scan from it. In general, I don't favor using images of math papers just to show "what they look like" because I think it overemphasizes the difficulty of the notation. It would be like putting an image of extremely complicated sheet music on an article about musical keys - the only effect would be to make the reader think the notation is complicated, and it wouldn't help them understand keys. — Carl (CBM · talk) 14:09, 21 November 2007 (UTC)[reply]

"different meaning of 'completeness'"

The paragraph contrasting with the incompleteness theorem strikes me as misleading. It isn't clear to me that the meaning of "complete" changes for the incompleteness theorems. To put things as simply as possible completeness is just "if truth then proof". For propositional logic and first-order predicate logic the "truths" in the system are basically just tautologies, and every tautology can be proven deductively. For the more expressive systems that are incomplete, however, you get more truths than you can prove. That's the whole point of the Godel sentence; it "says of itself" that it is not derivable, hence is true and not derivable. The relevant difference to emphasize is that the incomplete systems are more expressive, not that there's a different meaning of "complete" involved in the two theories. Also, in the same paragraph "logical consequence" is used in a confusing/unclear way. This paragraph needs to be completely scrapped and rewritten, imo. Maybe I'll come back and do it when I have time. 173.30.27.245 (talk) 16:43, 11 May 2009 (UTC)[reply]

The issue is that every first order theory, including e.g. Peano arithmetic, is complete in the sense that any statement that is true in every model of the theory is provable in the theory. This sense of completeness is a property of first-order logic itself. In another sense of the word "complete", there are sentences that are true in the standard model of Peano arithmetic that are not provable. So the sense in which that is "incompleteness" is indeed different than the sense in which first-order logic is complete. — Carl (CBM · talk) 18:32, 11 May 2009 (UTC)[reply]

So in what model the sentence P="P is not provable in Peano arithmetic" is false? I see why you can add P as an axiom to the system and still get a consistent model, but if you add its negation instead, we have the Peano axioms and another axiom (not P) which states that its negation(P) is provable from the Peano axioms... oops. Bbbbbbbbba (talk) 12:20, 10 November 2010 (UTC)[reply]

Yes, that is possible. It's a consequence of the incompleteness theorems. — Carl (CBM · talk) 13:38, 10 November 2010 (UTC)[reply]

Sorry, but I can't see how your answer makes sense. You said "that is possible" but I didn't (even implicitly) state the impossibility of anything. If I did, then it's the impossibility of a model in which P is false (sorry for mistakenly typing in "true" in the original question; I have corrected it). And how is the existence of such a model justified by the incompleteness theorems? —Preceding unsigned comment added by Bbbbbbbbba (talk • contribs) 13:59, 10 November 2010 (UTC)[reply]

You should read the article Non-standard model of arithmetic. The point is that, because the Goedel sentence ("I am not provable") is not provable, there are indeed models in which it is false, by the completeness theorem. — Carl (CBM · talk) 14:17, 10 November 2010 (UTC)[reply]

But that's where I am confused. Suppose we have a model where the Peano axioms (denoted by Q) are true, and the Godel sentence P is false, then P is provable from the Peano axioms (because P is false). So altogether we have: Q is true, P is false, yet P can be proved from Q. I find that situation weird. Bbbbbbbbba (talk) 14:33, 10 November 2010 (UTC)[reply]

P refers to a formalized provability predicate, which in turn quantifies over natural numbers. In a non-standard model, that quantifier ranges over non-standard numbers. So a non-standard model can think something is "provable" without that thing actually being provable in the real world. It's necessary to keep a firm separation between actual provability, in the metatheory, and formalized provability, in the object theory. — Carl (CBM · talk) 14:38, 10 November 2010 (UTC)[reply]

clarification

Could someone please clarify what "completely effective manner" means in "The completeness theorem and the compactness theorem are two cornerstones of first-order logic. While neither of these theorems can be proven in a completely effective manner" Cheers, 128.232.228.79 (talk) 18:41, 15 January 2010 (UTC)[reply]

It means effective in the sense of computable. The details are in the last paragraph of that section. Algebraist 18:54, 15 January 2010 (UTC)[reply]

I started to tag that statement with 'citation needed' but then read this exchange and the latter part of the section; nonetheless do we need to say something in the article about what sense of 'effective' is meant (i.e. not that "the theorems cannot be proven in a manner that will convince college freshmen") or do we assume sophistication on the part of the reader to know what's meant? BrideOfKripkenstein (talk) 15:30, 5 October 2010 (UTC)[reply]

I don't think we assume sophistication: there are (at least) two senses of effective in which the statement is true, and both are described in that same section. The sentence in question is a summary sentence for the entire section; I don't think it's excessive to ask the reader to actually read the section before asking what is intended there. But the sense meant is not really "computable", it has more to do with constructive proof. The meaning of effective in the last sentence is about computability. — Carl (CBM · talk) 16:39, 5 October 2010 (UTC)[reply]

Is there a little mistake in the abstract of the proof?

Hello! first i don't speak english perfectly, please forgive me for the mistakes...

in the chapter: statement the theorem in the sub chapter: Model existence theorem

It's written:

Alternatively, given Henkin's theorem, the completeness theorem can be proved as follows: If $\Phi \models A$ is valid, then $\Phi \cup \lnot A$ does not have models. By the contrapositive of Henkin's, then $\lnot A$ is an inconsistent formula. But, by the definition of consistency, if $\Phi \cup \lnot A$ is inconsistent then it's possible to build a proof of $\Phi \vdash A$ .

I believe there is a little mistake: should it be written: By the contrapositive of Henkin's, then $\Phi \cup \lnot A$ is an inconsistent formula.

thanks --Nicobzz (talk) 10:27, 26 September 2018 (UTC)[reply]

I guess you are right. Moreover, (the current version of) the article Henkin's theorem requires Henkin witnesses for all existentially quantified formulas which are not necessarily available in the setting of the completeness theorem. - Jochen Burghardt (talk) 12:55, 26 September 2018 (UTC)[reply]

About strong completeness theorem

Should the term "Strong completeness theorem" redirect here? I'm translating some other pages and wonder whether "Strong completeness theorem" and "Gödel's completeness theorem" are the same concept or not. Thanks for helping! Puresnower (talk) 05:04, 14 June 2019 (UTC)[reply]

Do you have a reference? - Jochen Burghardt (talk) 09:09, 14 June 2019 (UTC)[reply]