3 ms·

> Do you really believe that writing a proof checker for Robinson arithmetic, with or without your new axiom, is different in any salient way than writing a pro

> Do you really believe that writing a proof checker for Robinson arithmetic, with or without your new axiom, is different in any salient way than writing a proof checker for PA? No, and this has exactly nothing to do with my point.

lisper 4y ago
Then why did you bring up RA at all? You must think there is some salient difference between RA and PA with respect to my proof or (I presume) you would not have brought it up. What is it? For that matter, what is the point you are trying to make? You originally wrote [1]: > A theory Γ is said to be complete whenever for all sentences we have either Γ ⊨ φ or Γ ⊨ ¬φ. If you recall, at the time I thought this was a simple mistake on your part, and that what you really meant was "Γ ⊢ φ or Γ ⊢ ¬φ", not "Γ ⊨ φ or Γ ⊨ ¬φ". But you never conceded this. So I'm going to ask you again, is that really what you meant? Because that is not the sense in which the term "completeness" is used in Goedel's incompleteness theorem. The word "complete" is used there to mean syntactic completeness. To quote Wikipedia [2]: "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). THIS IS THE NOTION RELEVANT for Gödel's first Incompleteness theorem. It is NOT TO BE CONFUSED WITH SEMANTIC COMPLETENESS, which means that the set of axioms proves all the semantic tautologies of the given language." [emphasis added] I'm trying to give you the benefit of the doubt here, but you really do appear to be confused on this point, particularly since you keep talking about soundness, which is a semantic property, not a syntactic one. --- [1] https://news.ycombinator.com/item?id=33250168 https://news.ycombinator.com/item?id=33250168 [2] https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems#Completeness https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...

lisper 4y ago

Then why did you bring up RA at all? You must think there is some salient difference between RA and PA with respect to my proof or (I presume) you would not have brought it up. What is it? For that matter, what is the point you are trying to make? You originally wrote [1]: > A theory Γ is said to be complete whenever for all sentences we have either Γ ⊨ φ or Γ ⊨ ¬φ. If you recall, at the time I thought this was a simple mistake on your part, and that what you really meant was "Γ ⊢ φ or Γ ⊢ ¬φ", not "Γ ⊨ φ or Γ ⊨ ¬φ". But you never conceded this. So I'm going to ask you again, is that really what you meant? Because that is not the sense in which the term "completeness" is used in Goedel's incompleteness theorem. The word "complete" is used there to mean syntactic completeness. To quote Wikipedia [2]: "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). THIS IS THE NOTION RELEVANT for Gödel's first Incompleteness theorem. It is NOT TO BE CONFUSED WITH SEMANTIC COMPLETENESS, which means that the set of axioms proves all the semantic tautologies of the given language." [emphasis added] I'm trying to give you the benefit of the doubt here, but you really do appear to be confused on this point, particularly since you keep talking about soundness, which is a semantic property, not a syntactic one. --- [1] https://news.ycombinator.com/item?id=33250168 https://news.ycombinator.com/item?id=33250168 [2] https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems#Completeness https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...