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

3:49 AM
4 messages moved to trash
 
hello there
 
@LeakyNun You just have to observe that the proof of D1 can be internalized inside the system itself if it interprets TC/PA− + induction.
Then you get D3.
@DavidReed: Hello!
 
Still haven't slept
 
@user21820 what if I don't have induction?
 
Then you're in trouble.
@DavidReed Then go and sleep.
 
3:51 AM
I thought you don't need induction to prove incompleteness
 
@DavidReed: Seriously. 7 hours of sleep per day is the target.
@LeakyNun We don't. I didn't need the formal system to have induction in my linked post.
However, if you want to go via provability logic, then it appears you do.
 
heh?
 
@user21820 It's been a strange 36 hrs
that's for sure
 
By the way, I noticed you thought your chat messages are gone once it's too long. Click "full transcript" and you can see the whole lot. Except those that are moved elsewhere.
 
About 3/4 of my conversation today have been moved to trash
 
3:53 AM
@LeakyNun Namely, if you want to show that S satisfies D3 you do need induction.
D1 does not need induction, because it's literally the same as saying that S can reason about programs.
 
can you go the PA- pathway without induction?
 
PA is stronger than you need for incompleteness
you don't need induction
 
@DavidReed Please read my comments carefully. You need S to support induction to show that S satisfies D3.
 
@user21820 well, please read his comments carefully :P he's saying you don't need induction for incompleteness
 
@LeakyNun I read it, but we're talking about D3. And I already said earlier that my post only assumes reasoning about programs, not induction.
@LeakyNun You simply can't get the derivability conditions for PA−. At least it's not known.
4
Q: Derivability conditions for Robinson arithmetic

Charles StewartTwo pieces of hearsay I have encountered about Robinson's Q: Q fails to satisfy the Löb derivability conditions; Pudlák criticised the Löb derivability conditions and suggested rival, weaker conditions. Which leads to three questions, if the above are right: Which derivability condition(s) ...

 
3:59 AM
@user21820 then how do you prove incompleteness in PA-?
 
You still have not read my post?
PA− is equivalent to TC.
In the sense that you can translate sentences over TC into PA−.
And they would prove the same theorems modulo that translation.
 
but is there a translated version
 
I don't get you; what translated version? Godel did his proof for a system S that interprets PA, but Robinson noticed that his argument only needs S to interpret Q (which is equivalent to PA−).
In the same manner, the proof I gave for systems that can reason about programs works for PA−, and the "reason about programs" part is where Godel's trick (β-function) comes in.
The trick is unnecessary for TC, but anytime you want to use PA− for string manipulation you will have to use that trick or something equally powerful.
Unless all you're asking is about the trick.
 
@user21820 have you ever studied digital logic design?
 
In mathematical logic, Gödel's β function is a function used to permit quantification over finite sequences of natural numbers in formal theories of arithmetic. The β function is used, in particular, in showing that the class of arithmetically definable functions is closed under primitive recursion, and therefore includes all primitive recursive functions. == Definition == The β function takes three natural numbers as arguments. It is defined as β(x1, x2, x3) = rem(x1, 1 + (x3 + 1) · x2) = rem(x1, (x3 · x2 + x2 + 1) ) where rem(x, y) denotes the remainder after integer division of x by y (Mendelson...
 
4:05 AM
the proof via curry's paradox is so elegant though
 
@DavidReed Not that much. I know roughly how gates work physically, and how to make rather complex circuits. But that's about it.
@LeakyNun Yes it is elegant, which is just too bad it requires induction.
 
my notes on david's notes on fixed-point theorem:
 
It's always like this, the more you assume the more you can prove.
Lob's theorem apparently requires induction.
 
??
what notes
 
Patience, @DavidReed
I have barely started typing
 
4:07 AM
And now he has to start over again.
 
there's a reason it ends in a colon
 
=P
 
@user21820 oh I always copy it before I type anything else
 
@user21820 I think you'd enjoy it. You'd enjoy assembly and compiler design as well
 
I do the same. I was just joking.
 
4:08 AM
I just don't remember giving any notes other than sub(s,c,d)
 
@DavidReed just
 
Claude Elwood Shannon (April 30, 1916 – February 24, 2001) was an American mathematician, electrical engineer, and cryptographer known as "the father of information theory". Shannon is noted for having founded information theory with a landmark paper, A Mathematical Theory of Communication, that he published in 1948. He is, perhaps, equally well known for founding digital circuit design theory in 1937, when—as a 21-year-old master's degree student at the Massachusetts Institute of Technology (MIT)—he wrote his thesis demonstrating that electrical applications of Boolean algebra could construct...
the most remarkable man you've never heard of
 
@DavidReed I once learnt MIPS assembly, and no I do not enjoy it. And I am not patient enough to build a compiler.
 
interesting. ok
 
@LeakyNun Sometimes, I do it twice, and later realize that I lost the first copied text.
 
4:12 AM
Let " ":WFF→ω be the encoding function. It is injective.
Let Diag(x,y) be a sentence that is true iff y encodes (∃a)(a=x∧P), where "P"=x.
e.g. if "0=0"=5 and "(∃a)(a=5∧0=0)"=6, then Diag(5,6) is true.
Now, let A(a) := (∃y)(Diag(a,y)∧φ(y)) where φ is any formula.
Let G := (∃a)(a="A(a)"∧A(a)).
Then, ⊢ Diag("A(a)","G") from the definition of G and Diag.
Also:
⊢ G ⟺ A("A(a)")
⊢ G ⟺ (∃y)(Diag("A(a)",y)∧φ(y))
⊢ G ⟺ φ("G")
 
Something is very wrong with your Diag.
It's supposed to Diag-onalize.
 
"P" = x is not correct
get rid of that and replace P with P(x)
 
@DavidReed that's just notation
 
the idea is that if t is an actual term then A(t) is equivalent to $\exists x x=t \land A(x)$
granted you don't have to write P as P(x)
but what you can definitely not do is write P = x
 
4:15 AM
Diag(x,y) is supposed to mean "y is the code of the sentence x(x)."
 
@user21820 hmm
I kind of see the issue
 
for example...
let A: 3 + x = 5
then A(2) is 3+2 = 5
which is equivalent to there exists an x such that x= 2 and 3 + x = 5
A(2) logically equiv to $\exists x x=2 \land A(x)$
$(\exists x)(x = 2 \land A(x)$
 
Let " ":WFF→ω be the encoding function. It is injective.
Let Diag(x,y) be a sentence that is true iff y encodes (∃a)(a=x∧P(a))), where "P"=x.
Now, let A(a) := (∃y)(Diag(a,y)∧φ(y)) where φ is any formula.
Let G := (∃a)(a="A"∧A(a)).
Then, ⊢ Diag("A","G") from the definition of G and Diag.
Also:
⊢ G ⟺ A("A")
⊢ G ⟺ (∃y)(Diag("A",y)∧φ(y))
⊢ G ⟺ φ("G")
 
this part should disappear: "where "P" = x"
 
No it has to stay.
 
4:22 AM
....
 
But in the way it's written, the existential is useless.. It's just y encodes x(x).
 
P = formula, x = variable,
 
Or rather, y encodes P(x) where x codes for P.
He is identifying strings with numbers.
 
@user21820 are you sure I can rewrite the whole thing without existential?
 
So "P" is a string encoded by x.
 
4:23 AM
oh wait
 
@user21820 I wouldn't say that
note how I defined " "
 
quotations means godel number of
 
everybody skipped the first line outright
 
@LeakyNun Only when you expand the substitution function then you need to rephrase.
At the high-level it's just what I wrote.
 
@user21820 I can do the substitution outside
 
4:24 AM
Yes I skipped the first line because it's equivalent.
 
by outside I mean inside the system but outside the child-system
 
To treat every string as a number is the same as what your quotes are doing.
@LeakyNun The point is, there is nothing wrong with what I wrote.
2 mins ago, by user21820
Or rather, y encodes P(x) where x codes for P.
 
I didn't say there is :P
 
There is no existential.
 
what we say are not incompatible
 
4:25 AM
I'm just saying that there is no need to complicate it when you're at the high-level now.
 
So those pages I sent you last night.....the incompleteness theorem is 2 pages after
would you like me to just send those as well
 
Let " ":WFF→ω be the encoding function. It is injective.
Let Diag(x,y) be a sentence that is true iff y encodes P(x), where "P"=x.
Now, let A(a) := (∃y)(Diag(a,y)∧φ(y)) where φ is any formula.
Let G := A("A").
Then, ⊢ Diag("A","G") from the definition of G and Diag.
Also:
⊢ G ⟺ A("A")
⊢ G ⟺ (∃y)(Diag("A",y)∧φ(y))
⊢ G ⟺ φ("G")
you still need existential in A
@DavidReed yes, by all means
 
whats wrong with having existential>
 
I'm stuck in the ⊢¬G part in the incompleteness
@DavidReed nothing is wrong with existential
 
ok.
I'll upload some other relevant things here as well.
 
4:28 AM
@LeakyNun Because that part needs soundness for program halting.
You're doing Godel's way, so you can't escape that.
 
i.e. omega-consistency?
 
Yes he used ω-consistency, but actually you only need Σ1-soundness.
 
alright
 
But whichever you pick, you're going to have to go back and analyze the complexity of all your formulae.
Otherwise you can't ensure that your Godel sentence is Σ1.
Haha it's coming back to bite you...
 
let's just say
that Löb's theorem is the most beautiful theorem in existence
apart from Theorema Egregium
 
4:30 AM
Löl.
I differ. The unsolvability of the halting problem is better.
 
but it's depressing
incompleteness theorems are depressing
 
LOL.
 
(⊢Bew("P")→P)⟹(⊢P)
 
Then you like ACF[p]?
RCF? DLO?
 
I know second incompleteness is a straightforward corollary of Loeb
 
4:32 AM
Ok
 
All nice complete theories.
 
@user21820 oh I like ACF
don't forget TFDAG
 
As long as you don't care about natural numbers.
What is TFDAG?
 
torsion-free divisible abelian groups
 
Oh.
I had to prove QE for that one as a homework exercise some years ago.
 
4:33 AM
and DLO is really DLOWE
 
Most authors are lazy and omit the "WE".
 
just two keystrokes
 
40% discount!
 
oh god
 
Perspective matters... =P
 
4:35 AM
have I asked you about the decidability of $e+\pi\in \Bbb Q$?
 
@LeakyNun Not sure. There is a high-rep user who is so extremely stubborn that he/she does not want to fix a wrong post claiming that it is true if undecidable.
 
@user21820 so if it's false then it's decidable?
wait
what's the truth now
 
do the complete axiomatiziable theory part first
i basically uploaded those in the order you should read them
 
4:40 AM
@LeakyNun The truth is not known.
 
but if it's true then it must be decidable...
wait that means if it's undecidable then it's false, lol
 
@user21820 I noticed you were quoting bolos in some of the dialogue that person sent me from the other day
@user21820 are you familiar with his generalization of the world's hardest logic problem?
 
@DavidReed Yes I was. It was only because I got fed up with people refusing to even listen to reason when I explained clearly what was circular in the common justification of the replacement schema. So I did a Google search and found that both Menzel and Boolos said the same as I had.
And then people stopped responding. Clever, aren't they; stop when they know they can't win, but still don't admit.
 
@user21820 ironic given your distaste for his book
 
@DavidReed Show me a quote where I said it. I don't have a distaste for his book.
I just prefer free material.
 
4:50 AM
"bad book"
 
I think I said I was joking... no?
 
although now that I think about it it was because the sub(s,c,d) was an excersize
 
I just meant that it was a tedious exercise and in my opinion not much use to go through all the details.
So the book was 'bad' in making students do it...
 
Anyhow, this is a generalization of smullyans logic problem....
The Hardest Logic Puzzle Ever is a logic puzzle so called by American philosopher and logician George Boolos and published in The Harvard Review of Philosophy in 1996. Boolos' article includes multiple ways of solving the problem. A translation in Italian was published earlier in the newspaper La Repubblica, under the title L'indovinello più difficile del mondo. It is stated as follows: Three gods A, B, and C are called, in no particular order, True, False, and Random. True always speaks truly, False always speaks falsely, but whether Random speaks truly or falsely is a completely random matter...
 
I guess I saw it before, but too lazy to try.
 
4:54 AM
@DavidReed p.222 doesn't even follow from p.221...??
 
clarify
theres several pg 221's for some reason
you man theorem 17.2?
 
yes
 
@user21820 it would be easier to go through the classification of all finite simple groups
so 17.1 was the diagonal lemma i sent you earlier
which part of 17.2 are you not following?
 
@DavidReed You're talking about the puzzle? No I'm sure if I wanted I could solve it. I certainly can't do the classification of finite simple groups...
 
@user21820 yes was a joke. The classification of all finite simple groups numbers in the thousands of pages
but if you look at Wikipedia article
you can see that HUGE binary table
and you immediately lost interest in trying to solve it
 
4:59 AM
@DavidReed I didn't look down. I only looked at the puzzle statement.
 

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