« first day (479 days earlier)      last day (2332 days later) » 

5:00 AM
@user21820 its effectively a 20x20 truth table
 
Anyway I just proved that the puzzle is false. I ask "Will you say no to the question I am asking now?" and none of the gods can answer truly or falsely.
 
@user21820 negative. Random god can answer
 
Cannot.
See the Wikipedia definition of Random.
He flips a coin, then answers truly or falsely accordingly.
So he too cannot answer.
 
i stand corrected
you're right
although i don't know that that makes the puzzle false
 
As for the da/ja complication, there is a way to reduce to yes/no, so we can assume it's yes/no with our standard meanings.
 
5:04 AM
as you've obstructed yourself from achieving the desired outcome
you've now asked a question and are not any closer to knowing which god is which
 
@DavidReed It makes it false in the sense that the puzzle claims these gods exist, but they can't because there is question that none of them can answer according to the puzzle's claims.
From this I can deduce a contradiction, and hence that I can solve the puzzle without asking any question. =D
 
@DavidReed the part where it disappeared
@user21820 oh god
 
@LeakyNun Har har. Pun intended?
 
@user21820 not intended
 
Lol.
 
5:05 AM
@user21820 I reject that reasoning
 
@DavidReed why?
you follow minimal logic then
 
I don't know what minimal logic is.
 
In classical logic, we have the principle of explosion.
 
I reject it because it simply doesn't make sense to me
 
false |− P.
I'm using that.
 
5:07 AM
> I reject it because it simply doesn't make sense to me
 
using what?
 
be logical
4
@DavidReed exfalso sequitur quodlibet
aha
 
@DavidReed: You want a formal proof? Okay give me a minute.
 
I'm aware of a contradiction proves everything
 
@user21820 there is no proof of axioms
you're just using other axioms
 
5:09 AM
although implicit in that assumption is that the material conditional is an accurate portrayal of the actual conditional
 
disjunction elimination?
 
but also I just don't see a contradiction
 
@DavidReed he just derived a contradiction
 
@LeakyNun Of course. I'm not proving that rule, but the claim I just made that David rejects.
 
Give me the True and give me the false
doesn't have to be formal
 
5:11 AM
In the world which the puzzle describes, the gods will answer any question either truly or falsely. Instantiate that for the question I wrote above. Then contradiction.
 
twin prime conjecture: ∀x∃y[y>x∧(∀a∀b(ab=y−1⟹a=1∨b=1))∧(∀a∀b(ab=y+1⟹a=1∨b=1))]
what is the classification? @user21820
 
@LeakyNun The one you wrote is Π3, however remember that we only count unbounded quantifiers, and here we can bound the quantified a,b.
 
where in the statement does he guaraentee that you will get a response to a question
theres ambiguity in the phrase "always speaks truly/falsely"
 
@user21820 hmm, what is the Π2 version?
 
One could rationally interpret that to mean : If he speaks, he will speak only the truth/not truth"
 
5:14 AM
@DavidReed If you interpret that as saying that the gods may not answer at all, then by unsolvability of the halting problem relative to the gods you will find that you cannot solve the puzzle at all either!!!
Because all three could agree to keep silent to keep you in the dark forever.
 
could $\neq$ will
 
@LeakyNun Just bound the a,b; you know the factors of a number are no greater than the number itself.
@DavidReed But the point is that you cannot prove any solution correct.
Because I can prove that you cannot.
By constructing a model of the puzzle as described above (all 3 silent), I can show you that any purported solution fails.
 
what happens in the instance that all three are not silent>
what if you get a response to each question you ask
 
Then my earlier proof of contradiction applies, since your objection to my interpretation of "always speaks" does not apply.
I'm not sure why you don't understand my reasoning. It's water-tight. It's the puzzle that's flawed.
 
oh
 
5:17 AM
I understand your reasoning
 
Perhaps the only way to save the puzzle is to try finding a middle ground.
 
somehow I read unbounded as unbound and got confused haha
 
But I don't see a way.
 
but i don't see how in the instance you get an answer from all three i have to change my interpretation of always speaks
 
Haha.. bind > bound > bounded. Double past tense.
 
5:19 AM
∀x∃y[y>x∧(∀a∀b(a<y→b<y→ab=y−1→a=1∨b=1))∧(∀a∀b(a<y→b<y→ab=y+1⟹a=1∨b=1))]
English
 
Your objective is to have all three answer your questions. Why would you intentionally ask a question they would not answer>
 
@DavidReed The point is that the puzzle is flawed. Give me a precise version of the puzzle and I'll think about it.
 
what's the complexity now?
 
@LeakyNun Π2, but seems wrong. Your second part bounds a,b by y−1, but it needs to be y+1...
 
@user21820 something tells me there is going to be inherent imprecision in anything that is ever presented to you :)
 
5:21 AM
alright
 
@DavidReed Nah it's just that I dislike puzzles that are presented by people as "world's hardest" or something pompous but are actually so flawed.
If a friend came up with it on his/her own, it would be totally different.
 
I understand
You actually express that sentiment a lot..... a strong dislike of narcissism
 
@LeakyNun Normally you rewrite in Skolem normal form before counting, but it's kind of obvious here.
Yup. Well put.
 
well
 
Oh and adjacent quantifiers of the same kind are always counted as one partly because Cantor pairing allows us to.
Where can I move this conversation to? Logic (intertwining with the other thread)?
 
5:25 AM
do you use "if" or "iff" for definitions? @user21820
 
iff.
 
oh yeah leaky what part of 17.2 were you not following?
 
21 mins ago, by Leaky Nun
@DavidReed the part where it disappeared
 
lol
sry
so I skipped a little because I had sent you 17.1 yesterday
but I will resend it
 
do keep in mind that I'm an idiot
in fact I'm the world's most idiotic person in existence
 
5:27 AM
@LeakyNun What's that supposed to mean.
 
@LeakyNun: If you cannot justify your self-vilification, I'm going to trash it. =)
 
@user21820 well interpretation depends on the domain and the constants and the relations and the functions
@user21820 it's not self-vilification
so your statement is flawed from the antecedent to the consequent
 
18 messages moved from CRUDE
 
it is self-vilificationn
 
5:29 AM
it isn't
 
some would tell you that repeating that to yourself will reinforce that viewpoint in you
 
Hmm it seems we have a disagreement here.
Heh.
 
and you will eventually begin to believe it
 
I'm sure LeakyNun is kidding though.
 
it was obviously a parody of this statement:
 
5:30 AM
Or using some idiosyncratic notion of "idiot".
 
9 mins ago, by user21820
@DavidReed Nah it's just that I dislike puzzles that are presented by people as "world's hardest" or something pompous but are actually so flawed.
 
idiots don't make it this far on the incompleteness theorem
 
@DavidReed I still don't follow 17.2
 
Maybe its because I'm a zombie right now
 
@LeakyNun Actually I don't quite see the link.
 
5:31 AM
but i have no idea what that means
ok let me pull it up for myself and we'll go through it
 
@user21820 well you said you dislike things tagged with "world's ..."
 
@LeakyNun You made an invalid deduction! I said "world's hardest" or something pompous.
 
lol
 
"world's most idiotic person" does not fit that.
=D
Phew. For a moment I thought there was a loop-hole in my statement allowing people to justify self-vilification...
 
5:33 AM
So Q is the closure of those axioms from the pg that says 16.2 minimal arithmetic
Q is the set of all sentences provable from those axioms
 
@DavidReed why don't you just send me the page instead
 
i did
 
you didn't
 
hrm. well i screenshotted. there were a lot of pages. my bad
here it is
 
you only sent me the first few lines of 17.2
 
5:34 AM
 
You two like to argue back and forth like little kids. It is. It isn't. I did. You didn't...
 
Just kidding.
 
Don't wry about the E rudimentary part
just think of Q as the set of all sentences provable from those axioms
 
It's ∃-rudimentary?
And it just means Σ1-sentence, in modern terms.
 
5:36 AM
@DavidReed I just need 17.2
you keep sending me pages
none of those contain the second part of 17.2
 
@user21820 we don't
 
oh, finally you got that page across, lol
 
maybe the connection doesn't like sending a lot of pages at once. Because on my end I scroll up and see that I've sent you like 15 pgs a few min ago
 
5:40 AM
@DavidReed: By the way, are you in your 3rd or 4th year or something?
 
I'm 30
 
so it's "something"
 
why?
 
nvm
@user21820 so somehow soundness is assumed
 
@DavidReed Ah okay. You mentioned being a student last time so I thought you might still be. Are you working or doing research?
 
5:41 AM
Ah.
2006-2010 B.S. math at baylor
2010-2015ish drugs/depression
2015-present prereqs for med school
 
@LeakyNun It must be assumed somewhere, but I don't know what that 17.2 is doing.
@DavidReed Ah I see. All the best.
 
Thanks man
 
Curious that you're so into logic though, since you're now going into med school. Though we need more doctors who are logical...
 
@user21820 17.2 is deriving a contradiction from the fact that there is a formula that determines provability
 
But that's way stronger than Godel used.
 
5:44 AM
I maintained a recreational mathematics curriculum over the last few yrs
Ok
 
@user21820 hmm
 
so earlier the book proves that the relation : there exists a proof of formula A, is semirecursive
 
@LeakyNun In particular, yes that assumption is where soundness is.
You can significantly strengthen the argument simply by not assuming that and proceeding.
 
@user21820 could you explain to me where exactly Con(PA) and Con(PA+Con(PA)) differ?
they are both sentences over the same language
@user21820 to where?
 
The second implies the first but not the other way around?
Wait one question at a time.
 
5:47 AM
ok
 
To clarify, that's not the part of the incomplentess theorem that I sent you, although its in here as well
 
You now know how to construct the sentence ⬜P for any sentence P. Moreover you know how to diagonalize to get the fixed-point lemma.
So construct sentence G such that S |− G⇔¬⬜G.
If S |− G, then S |− ⬜G because S can { reason about programs / prove any Σ1-sentence }, but also S |− ¬⬜G by the property of G.
If S |− ¬G, then S |− ⬜G by property of G, but then clearly S is not sound for { program halting / Σ1-sentences } because S cannot prove G (we're assuming S is consistent).
Done.
 
mmhmm
 
@LeakyNun Let PA* = PA+Con(PA). Then PA* does not prove Con(PA*). Hence PA* cannot prove ( Con(PA) ⇒ Con(PA+Con(PA)) ).
 
But I'm asking what is the difference between the two sentences
 
5:52 AM
Well of course they would be different sentences when you plug them into the machinery, whether using TC or PA−.
I thought you were asking about the qualitative difference.
 
I'm asking about the "of course" part
 
The "of course" is because PA and PA+Con(PA) have different proof verifiers, so the sentence generated will of course be different.
I'm of course using the obvious proof verifiers. It is conceivable that they have the same proof verifier, but the above shows that it is impossible.
 
please expand on the obvious proof verifier
where is the difference?
 
You can write a proof verifier for PA, right?
Now Con(PA) is some sentence. The proof verifier for PA+Con(PA) simply checks whether each step uses a valid deductive rule or an axiom of PA or Con(PA).
Difference is clearly there.
 
thanks, you could have gone there from the beginning
 
5:56 AM
I didn't know it wasn't obvious...
 
I did say I'm asking about the of course part
 
I assumed you knew how to write proof verifiers, and it's obvious by definition of PA+Con(PA).
In general for any first-order theory S and sentence P over S, we have S+P denoting the system generated by axioms of S plus P.
 
is Con(PA) unique?
 
6:13 AM
Well it clearly depends on your chosen proof verifier.
Which depends on your proof style.
And also depends on the specific phrasing of axioms, in the case of a first-order theory.
 
@user21820 so let's say I wrote two different sentences for the consistency of PA
Con1(PA) and Con2(PA)
I think you can guess my question :P
 
Yes I can.
Answer is no.
Wait...
I think it depends.
 
hmm
on what?
 
I'm not sure.
 
@user21820 but it also depends on whether I phrase it positively or negatively though
wait, in English no is always negative
 
6:17 AM
To make clear, you want to ask whether PA proves ( Con1(PA) ⇒ Con2(PA) ).
 
in Chinese no always negates the question
 
Actually, yes it does.
 
wait what
 
Interesting, my intuition was wrong.
I think.
 
how did you know that your intuition was wrong
you must have used intuition
but if your intuition is wrong
then you shouldn't trust your intuition
which makes your judgment non-trustworthy
which makes it trustworthy
assuming the soundness of intuition
ok seriously @user21820 what is the answer
 
6:20 AM
Working in PA, if ¬Con2(PA), then there exists a proof over PA2 (some specific representation of PA) of "false2" (in that representation), and now PA (using induction) can follow that proof (of arbitrary length) and construct a proof over PA1 of "false1", and hence ¬Con1(PA).
I think induction is necessary because it needs to be able to follow any proof of arbitrary length.
 
PA cannot use induction, what if?
 
So for example I think it is not always the case that TC proves ( Con1(TC) ⇒ Con2(TC) ).
 
hmm
that's... absurd
 
6:34 AM
@LeakyNun If you really want to know, I could ask this on Main.
 
@user21820 thanks
 
1
A: The infamous sub(s,c,d)

David ReedNote: Most of these are from Boolos' "Computability and Logic". It is going to be strongly assumed here that one is familiar with properties of recursive functions and relations. I will define these functions and leave it to the reader to verify they are recursive: $ \\ $ quo(x,y) to be the quo...

@user21820 are this persons comments what you would consider "cranky"
 
@DavidReed No? reuns seems to prefer my kind of computability approach, as you yourself noted. So how is it cranky?
 
snotty
"excuse me, but why do you care about these details? I would simply show that.."
 
6:49 AM
By "cranky" I didn't mean anything except "by a (mathematical) crank".
 
"pompous"
 
But you're reading too much into the first comment; it seems neutral to me, an honest comment from someone like myself who does not see why it is of much interest to do it all out.
I may not use the same words though.
I'll just not read and not comment.
 
this is how I would say it....
"Nice post. You know there's an alternative way of developing this that I personally find to be easier...."
Stipulating that I have not seen the "programming language" approach, I will say that the less precise you are in terms of defining your system/computer/program syntantically and semantically the less confident I would expect you to be with your end result/theorem
Anyways I have to get some sleep. Have a good night.
 
7:06 AM
@DavidReed Good night!
@DavidReed That's true, LeakyNun and I faced a similar issue when attempting to literally produce a sentence over TC/PA− by the computability method. We found that there was no going around building essentially a compiler inside the system, so the best might be a minimalist compiler that still supports high-level looping.
@LeakyNun: I hope I'm not missing some obvious trick...
0
Q: Equivalence of different consistency sentences

user21820Take any formal system $S$ that has a proof verifier program and interprets TC or PA$^-$. $ \def\imp{\Rightarrow} \def\con{\text{Con}} $ Then the incompleteness theorems show that $S$ does not prove $\con_1(S)$, where the subscript denotes that it is based on a particular encoding of a particula...

@LeakyNun But if my guess is correct, I don't find it absurd because TC is really too weak to do inductive reasoning; it can only check specific finite sequences, not reason about all finite sequences.
We'll see. I tend to get very little attention for my posts, compared to rubbish like "Is this batman equation real?"
@DavidReed @DavidReed: By the way, I think there is a way to fix the logic puzzle. The fixed version stipulates that the gods will always answer if the question can be justified to be a true/false question about reality. The question I gave is indeed not justifiable (by any reasonable means) to be of that kind, as explained in my post about the paradoxes. This fix is imprecise, but the easiest way to make it precise is to stipulate exactly what sentences are allowed, which kind of spoils the fun.
For instance we would have to say that we can form atomic sentences of the form "A/B/C is True/False/Random" and "da/ja means yes/no" and that we know who A/B/C refer to, and so on. This would really spoil the fun.
 
8:07 AM
This fixed version prevents not only my proof that the puzzle is flawed, but also the 'alternative' solutions given in the Wikipedia article, which are of the same kind of question as mine. For this fixed version, I deduced the same solution as Boolos, which is permitted by the above restrictions. Here is the full explanation:
If every question we ask could be answered by Random, then we are doomed because we get zero information.
Therefore we must figure out how to ask questions to True or False.
First note that we can assume we know which of ja/na is yes/no, because we can append "xor ( ja means no )" and treat "ja" to mean "yes", since the appended proposition is false iff "ja" means "yes".
Next note that we can assume True and False answer truly by appending "xor ( you are False )", since the appended proposition will negate the answer iff you are asking False.
No need for messy truth tables at all!
 
 
4 hours later…
11:42 AM
Let G be a formula such that for all P and X, ⊢[G(P,X,0)⟺Q(X,0)], where P="Q".
Now, let D(P,n) := ¬G(P,P,n).
Assume ⊢D("D",0). Then, ⊢¬G("D","D",0) by def D. Then, ⊢¬D("D",0) by prop G.
Assume ⊢¬D("D",0). Then, ⊢G("D","D",0) by def D. Then, ⊢D("D",0) by prop G.
Therefore no such formula G exists.
---
Let G be a formula such that [⊢G(P,X,0)⟺Bew(P++"(X,0)")] and [⊢G(P,X,1)⟺Bew("¬"++P++"(X,0)")].
Then, for any P and X: let "Q"=P.
Assume ⊢Q(X,0). Then, ⊢Bew("Q(X,0)"). Therefore, ⊢G(P,X,0).
Assume ⊢¬Q(X,0). Then, ⊢Bew("¬Q(X,0)"). Therefore, ⊢G(P,X,1).
@user21820
 
12:18 PM
What is this?
You should have split into two.
@LeakyNun The first section is wrong in the last line. Just because there is a sentence that cannot be proven or disproven does not imply a contradiction.
 
@user21820 oh right
 
@LeakyNun The second section seems wrong in the first line, but it's syntactically malformed so I don't know what it's supposed to mean.
 
what's wrong with the first line?
 
You didn't prove that such a G exists.
 
I'm trying to translate your stronger proof into PA
I don't even know what "halt" means
I assume it has something to do with a finite number
 
12:23 PM
Hmm, don't you know what "program P halts on input X" means?
"exists finite sequence of states such that..."
 
@user21820 yes, but I don't know how to translate it to PA
 
Just use Godel coding and the section in my post about how to code a finite sequence of strings as a single string? Finite string can be coded as a natural, no problem.
But if you want in terms of provability...
That's why I said it feels like the stronger version is not similar to Rosser's trick.
 
hmm
 
You want C to diagonalize against the zero-guessing decider... So C(x) should be equal to 1 iff x(x) = 0 but equal to 0 otherwise. In terms of a 'fixed-point' style, you want C to be represented somehow by a sentence.
 
I'm not even sure what the zero-guessing means
 
12:35 PM
Wait did you read the section using the zero-guessing problem?
 
@user21820 yes
what I mean is
as I've said above
sigh
I'm not sure how to translate zero-guessing to PA
 
You need a 2-parameter sentence for the function C.
Because you need to represent the function's output.
 
55 mins ago, by Leaky Nun
Let G be a formula such that for all P and X, ⊢[G(P,X,0)⟺Q(X,0)], where P="Q".
Now, let D(P,n) := ¬G(P,P,n).
Assume ⊢D("D",0). Then, ⊢¬G("D","D",0) by def D. Then, ⊢¬D("D",0) by prop G.
Assume ⊢¬D("D",0). Then, ⊢G("D","D",0) by def D. Then, ⊢D("D",0) by prop G.
Therefore no such formula G exists.
---
Let G be a formula such that [⊢G(P,X,0)⟺Bew(P++"(X,0)")] and [⊢G(P,X,1)⟺Bew("¬"++P++"(X,0)")].
Then, for any P and X: let "Q"=P.
Assume ⊢Q(X,0). Then, ⊢Bew("Q(X,0)"). Therefore, ⊢G(P,X,0).
Assume ⊢¬Q(X,0). Then, ⊢Bew("¬Q(X,0)"). Therefore, ⊢G(P,X,1).
are you talking about my G?
 
The problem is that it's not clear that it exists by the fixed-point lemma.
 
I mean, is my G above the correct way to phrase the "zero-guessing decider"
 
12:41 PM
As I said I can't tell because you didn't explain what "++" means, but the idea looks correct, though as I said you didn't prove that such a G exists.
It's not just concatenate...
 
not just?
 
And I don't know why you didn't phrase it the same way as the earlier one.
 
oh
well
I should have
 
It's not, because you can't just concatenate the code with "(X,0)".
 
oh, I'm supposed to substitute
 
12:42 PM
That's why "syntactically malformed".
 
good point
but I'm asking whether it's your intended translation of your proof into PA-
 
The first section also is wrong because you didn't use soundness.
@LeakyNun The second section first line is still wrong because you didn't diagonalize.
 
@user21820 your proof didn't diagonalize in the second section
 
It did. C did the diagonalization.
 
@user21820 you said you don't need soundness
 
12:46 PM
@LeakyNun Your first section needs.
 
C isn't even in your proof
 
Mine doesn't.
 
@user21820 which is why I'm asking you for a better translation...
 
Sorry D.
> Let D be the program constructed in the proof that G does not solve the zero-guessing problem.
 
not this section
the section above
 
12:48 PM
@LeakyNun I'm saying you didn't even translate the first section (which mirrors Godel's proof) right.
 
1 min ago, by Leaky Nun
@user21820 which is why I'm asking you for a better translation...
now we're going in circles
by "first section" I mean "Zero-guessing problem"
 
Wait look at my first two messages responding to yours. I was splitting your message into "first section" and "second section".
Next time don't put unrelated things in the same message.
 
unrelated?
 
@LeakyNun <− I'm going to repeat myself; your first section is wrong even if you remove the last line.
 
the first section in my message is "Zero-guessing problem" and the section is "Rosser's incompleteness theorem via the zero-guessing problem"
@user21820 could you just translate the whole thing into PA instead of having me embarrass myself and not getting what you/I want?
 
12:52 PM
Oh sorry I'm the one making the embarrassing mistake.
It's not wrong, but not the argument you want.
> Assume ⊢D("D",0). Then, ⊢¬G("D","D",0) by def D. Then, ⊢¬D("D",0) by prop G.
> Assume ⊢¬D("D",0). Then, ⊢G("D","D",0) by def D. Then, ⊢D("D",0) by prop G.
 
I'm saying, instead of telling me repeatedly that I'm wrong, which I know I am, just translate it to PA correctly
 
You do not want to work in the meta-level.
Do that two lines inside the system.
 
it's inside the system
 
If D("D",0) then ... hence contradiction. If not D("D",0) then ... contradiction.
No you did it outside by saying If |− D("D",0) then ...
Which is why I glanced at it and said there's no contradiction.
But actually if you do it inside you get a contradiction.
 
well I'm doing it inside, I just prefixed everything with ⊢
 
12:56 PM
No that's incorrect.
You are stating something of the form ( If ( S |− P ) then ( S |− Q ) ).
 
that's just a misunderstanding
 
What you want is the stronger ( S |− P ⇒ Q ).
Your notation means the former.
 
well
if you insist
oh, I see it
 
Sorry it's just like that. You'll find it that way in standard books.
It's important to know the distinction.
Because it's strictly stronger if you can prove the implication inside.
 
D("D",0) [assumption]
¬G("D","D",0) [def D]
¬D("D",0) [prop G]
⊢D("D",0)→¬D("D",0)
better?
 
12:58 PM
Yes.
 
move on
 
And similarly for the next one. So that you get |− false.
 
agreed
 
For the next part you wrote:
> Let G be a formula such that [⊢G(P,X,0)⟺Bew(P++"(X,0)")] and [⊢G(P,X,1)⟺Bew("¬"++P++"(X,0)")].
 

« first day (479 days earlier)      last day (2332 days later) »