« first day (1627 days earlier)      last day (1485 days later) » 

user21820
user21820
03:37
0
A: Function "evaluation" just means "composition"?

user21820 Is there anything more to evaluation, or can I exactly equate evaluation with composition and forever de-clutter my mind of the term "evaluation"? Frankly, there is no way to non-circularly 'get rid' of the notion of "evaluation". A rose by any other name is still a rose. Even Lawvere's axiomat...

 
11 hours later…
Lost definition
Lost definition
14:58
@Lostdefinition: Smullyan does not disagree with what I wrote. His comments are misleading to beginners. PA has induction and is incomplete. PA− has no induction and is also incomplete. Talking about going beyond first-order induction is in fact not meaningful because there is simply no such thing in reality. Think about it, there is no formal system for second-order PA with full second-order semantics, so it's simply meaningless to ascribe 'force' to the second-order induction axiom in any foundational sense (which is what the incompleteness theorems are really about). [cont] — user21820 54 mins ago
@user21820, yes. I agree with you about the fundamentional issue. But Smullyan also says you could use this Carnap's rule in page 113 of Incompletess book.Then PA+ with this rule would be complete. I don't understand second-order logic, but it makes sense to me that such thing would be complete.
user21820
user21820
@Lostdefinition Please quote the relevant portions or provide a public link, for ease of reference.
In particular, you definitely should read carefully about what full second-order semantics means, because it is quite like scams; it promises a lot but delivers nothing in reality.
Lost definition
Lost definition
21
Q: Computability viewpoint of Godel/Rosser's incompleteness theorem

user21820 How would the Godel/Rosser incompleteness theorems look like from a computability viewpoint? Often people present the incompleteness theorems as concerning arithmetic, but some people such as Scott Aaronson have expressed the opinion that the heart of the incompleteness phenomenon is uncompu...

logic reference-request computability proof-theory incompleteness
I am not use to the chat... sorry, here are the transcripts of the comments of the link:

"In misconceptions: "It is not due to induction". Smullyan disagrees (see Gödel Incompleteness Theorems, p. 112), he says incompleteness is due to lack of induction. It's because first-order "induction doesn't express the full force of mathematical induction""

"@Lostdefinition: Smullyan does not disagree with what I wrote. His comments are misleading to beginners. PA has induction and is incomplete. PA− has no induction and is also incomplete. Talking about going beyond first-order induction is in fac…
user21820
user21820
15:48
@Lostdefinition Sorry I wasn't clear enough; that's not what I meant. I meant that you should quote the relevant parts about "Carnap's rule".
Google tells me this, but then what you said Smullyan wrote seems to be an empty objection to what I stated because that rule simply cannot be achieved in any foundational system! Since I know Smullyan is a real logician, his real point may be more subtle, but it's unclear what it might be from what you quoted.
Lost definition
Lost definition
@user21820 Yes, I will study better this problem with second order. But to put more clear this another issue, this Carnap rule, in first order, is: [ Form (for all x) F(x) you can infer F(0), F(1),... , F(n), ...., infinitily ] . Put this on PA, then you have a complete theory in first order. Then it seems the cause of incompleteness is something about the finite character of proofs in PA.
user21820
user21820
@Lostdefinition Ah so then there is no actual objection; it is merely an issue of different perspective.
My statement about induction in my post is concerning the fact that many people believe (wrongly) that PA is incomplete because it has induction. And this is false.
As per your last clarification, Smullyan's statement is not about that at all, but rather about the fact that one of the things that incompleteness relies on is that proofs in any foundational system are all finite.
That's completely true, of course.
And just to be clear, what we ought to be talking about is of course essential incompleteness (i.e. no computable extension is complete). If one takes away enough axioms from PA, it remains incomplete but may become completable. I think Robinson pointed out that his theory Q has axioms which are all necessary because removing any axiom yields a completable theory.
So one might believe (wrongly) that PA is incomplete because it snuck in some infinitary behaviour via the induction schema. This is false because PA− (or Q) has finitely many axioms and no induction axiom of any kind, and yet is essentially incomplete.
That is all that I was saying in my statement over at my post.
@Lostdefinition: Does that clear things up?
(I just won't use Smullyan's phrasing of "not enough induction", simply because there is no well-defined notion of enough induction. Carnap's rule doesn't count as induction because it's simply not induction; in standard logic texts it is called the ω-rule.) @Lostdefinition: hope this added remark is helpful as well.
Lost definition
Lost definition
16:10
Yes, it clear somethings. I will have to study more of this. I agree we are talking about essential incompleteness. And I agree that PA- and PA are essentially incomplete, it don't matter, the fistr order induction axiom wasn't used for anything in the proof of incompleteness. But it seems Smullyan wants to point that both systems lack the "real" induction, and if you put it something near it we have a non-axiomatizable theory or infinitely long proofs.
yes it is helpful
user21820
user21820
I understand that. Indeed, you basically need something uncomputable to escape incompleteness. I just quibble with still calling it induction. =)
Ah I have another comment that might shed more light on this.
Note that with the ω-rule, basically all quantifiers vanish. Do you see why? Basically you get rid of one quantifier at a time. ∃ on the outside is easy. ∀ on the outside disappears via the ω-rule. So every arithmetical truth can be proven with the ω-rule, even without all the axioms of PA!
So it becomes no longer sensible to think of this as PA plus ω-rule. It is just ω-rule!
Well, almost all the axioms of PA. You still need the basic stuff for the symbols.
In short, the ω-rule is so powerful that it is like a truth-oracle rather than any sort of induction.
Lost definition
Lost definition
"In short, the ω-rule is so powerful that it is like a truth-oracle rather than any sort of induction." Yeah, now I agree.
user21820
user21820
@Lostdefinition Haha okay. =P
 
1 hour later…
Lost definition
Lost definition
17:28
@user21820 And, by the way, I actually get to this post by this other answer:math.stackexchange.com/questions/1002540/… . I have some questions about it too. If I am right you are simulating lambda calculus rules in arithmetic via definitorial expansions. But to do that wouldn't you still have to have the result that computational enumerable (r.e.) predicates are weak representable in PA?
Could you make the same argumentation using the recursion fix-point theorem?
user21820
user21820
@Lostdefinition The idea is absolutely correct. I don't exactly need the full representability theorem. Notice that that full theorem actually gets you Σ1-representation. I do need Godel's β-lemma to encode sequences, but after that I think it's pretty much just as stated in that post.
It's been more than a year since I wrote that post, so I may have missed something on my just now glance through it.
But I think there is no issue; we are not actually simulating full programs, and the syntactic substitutions we need here (same for λ-calculus reduction rules) is not that painful to encode once you have sequence coding.
If you do want to go all the way to get "can reason about programs", then yes you do need to do more work, and that is part of the point I went into some detail about how to encode program execution in a single string in the other post.
@Lostdefinition I think the recursion fix-point theorem is pretty much the same idea too.
Normally, I prefer to think of that fixed-point theorem as a consequence of the Y combinator, because it's easy to remember the Y combinator and I can actually code it to demonstrate to others! =)
 
1 hour later…
Lost definition
Lost definition
19:06
@user21820 Hmmm... very nice!
Yes, Y combinator seems like magic. Thank you for the answers.

« first day (1627 days earlier)      last day (1485 days later) »