Talk:Gödel's completeness theorem

From Wikipedia, the free encyclopedia

WikiProject Mathematics
Mathematics Portal
This article is within the scope of WikiProject Mathematics, which collaborates on articles related to mathematics.
Mathematics rating: Start Class Mid Priority  Field: Foundations, logic, and set theory

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

[edit] 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)

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)

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)
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)
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)
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)

[edit] 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)

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)

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)

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)