Some questions about Godel's Results

  • Thread starter Thread starter Asmodeus
  • Start date Start date
AI Thread Summary
The discussion revolves around clarifying concepts related to Gödel's Completeness theorem and the self-reference lemma in mathematical logic. Equivalence classes are essential for proving completeness in systems that include equality, as they ensure that equality behaves correctly within the domain. The self-reference lemma, also known as Gödel's Fixed-Point lemma, is crucial for demonstrating the first incompleteness theorem, allowing for the construction of sentences that reference their own provability. Participants also explore the distinction between completeness and incompleteness, particularly in different contexts. The conversation highlights the complexities of these concepts and the importance of precise definitions in mathematical logic.
Asmodeus
Messages
3
Reaction score
0
I'm in Mathematical Logic course. I just wanted to tie a few loose ends.

In our logic text, ("A Friendly Introduction to Mathematical Logic" -C. Leary) he uses the Henkin axioms to prove Godel's Completeness theorem. I understand the whole proof, except the last part that requires equivalence classes. Can anyone spell this out for me.


Further, can someone explain the self-reference lemma to me? For instance, our text uses v=4. Why is this so? Is it because 4 = 2^2, which is not a godel number?

What is the precise difference between the completeness in the first sense, and (in)completeness in the second sense?

Any explanations or good links would be greatly appreciated.
 
Physics news on Phys.org
"A friendly introduction to ML"? Oh God...

Well, I don't know this text, so I cannot comment on how its author does things, but Henkin-style completness proofs are the pretty much standard these days. But there is one thing: equivalence classes are necessary if you are proving completness for the calculus with equality, and they appear right at the beggining, in the definition of the domain (the canonical, or Herbrand, domain is defined out of the language's closed terms and, if you have equality, them you must group them in equivalence classes, so that equality really behaves like equality, not something weaker), not at the end: the last part is, usually, the proof that there is a maximal consistent set of a particular type.

Is it possible that the author proves completness for the calculus without equality (which doesn't require equivalence classes), and then treats the equality case? And, perhaps, says that the major change in the proofs is precisely in the domains' definition?

I'll take that the self-reference lemma is the (more usually called) Gödel's Fixed-Point lemma: if you have an arithmetizable (so that you may code any formula) and sufficiently powerful theory (capable of representing the partial recursive functions, for example), then this lemma states that, given a formula A(x), with x free, then tere is a sentence B, with code #B, such that B <->A(#B) is provable.

You need this lemma in the proof of the first incompletness theorem, where you apply it to the A(x) = Prov(x) (or Bew(x)) predicate.

Informally, the lemma states that the sentence B has the property A, iff B is the case.

Are you sure you are asking about the difference between completness and incompletness? This is almost obvious. Or are you asking about incompletness in the first and second senses?
 
JSuarez said:
"A friendly introduction to ML"? Oh God...

Well, I don't know this text, so I cannot comment on how its author does things, but Henkin-style completness proofs are the pretty much standard these days. But there is one thing: equivalence classes are necessary if you are proving completness for the calculus with equality, and they appear right at the beggining, in the definition of the domain (the canonical, or Herbrand, domain is defined out of the language's closed terms and, if you have equality, them you must group them in equivalence classes, so that equality really behaves like equality, not something weaker), not at the end: the last part is, usually, the proof that there is a maximal consistent set of a particular type.

Is it possible that the author proves completness for the calculus without equality (which doesn't require equivalence classes), and then treats the equality case? And, perhaps, says that the major change in the proofs is precisely in the domains' definition?

I'll take that the self-reference lemma is the (more usually called) Gödel's Fixed-Point lemma: if you have an arithmetizable (so that you may code any formula) and sufficiently powerful theory (capable of representing the partial recursive functions, for example), then this lemma states that, given a formula A(x), with x free, then tere is a sentence B, with code #B, such that B <->A(#B) is provable.

You need this lemma in the proof of the first incompletness theorem, where you apply it to the A(x) = Prov(x) (or Bew(x)) predicate.

Informally, the lemma states that the sentence B has the property A, iff B is the case.

Are you sure you are asking about the difference between completness and incompletness? This is almost obvious. Or are you asking about incompletness in the first and second senses?

I had my mathematical logic exam last night, so I had to figure out all these things myself.

Yes, it was the difference between the two senses of completeness, notice the "in" was in parentheses.

"Is it possible that the author proves completness for the calculus without equality (which doesn't require equivalence classes), and then treats the equality case?"

Exactly the case.
 
I was reading documentation about the soundness and completeness of logic formal systems. Consider the following $$\vdash_S \phi$$ where ##S## is the proof-system making part the formal system and ##\phi## is a wff (well formed formula) of the formal language. Note the blank on left of the turnstile symbol ##\vdash_S##, as far as I can tell it actually represents the empty set. So what does it mean ? I guess it actually means ##\phi## is a theorem of the formal system, i.e. there is a...
Back
Top