< 1514075368 212343 :sleffy!~sleffy@c-24-7-67-0.hsd1.ca.comcast.net JOIN :#esoteric < 1514076423 998348 :augur!~augur@2600:380:465d:158e:705c:407b:bac3:1e06 QUIT :Remote host closed the connection < 1514077473 366239 :moony!~moony@unaffiliated/moonythedwarf JOIN :#esoteric < 1514077968 6834 :moonythedwarf!~moony@unaffiliated/moonythedwarf JOIN :#esoteric < 1514078115 369981 :moony!~moony@unaffiliated/moonythedwarf QUIT :Ping timeout: 256 seconds < 1514078639 342274 :hppavilion[1]!~dosgmowdo@58-0-174-206.gci.net JOIN :#esoteric < 1514078868 397473 :trout!~variable@freebsd/developer/variable NICK :function < 1514080227 464077 :oerjan!~oerjan@hagbart.nvg.ntnu.no QUIT :Quit: Nite < 1514080533 93794 :sleffy!~sleffy@c-24-7-67-0.hsd1.ca.comcast.net QUIT :Ping timeout: 264 seconds < 1514081922 781692 :jaboja!~jaboja@jaboja.pl JOIN :#esoteric < 1514082971 217360 :function!~variable@freebsd/developer/variable QUIT :Quit: Found 1 in /dev/zero < 1514084159 794009 :jaboja!~jaboja@jaboja.pl QUIT :Ping timeout: 248 seconds < 1514087425 354125 :hppavilion[1]!~dosgmowdo@58-0-174-206.gci.net QUIT :Ping timeout: 248 seconds < 1514088285 120208 :variable!~variable@freebsd/developer/variable JOIN :#esoteric < 1514090877 656463 :zzo38!~zzo38@24-207-13-153.eastlink.ca PRIVMSG #esoteric :GURPS has "alternative abilities" where you can switch between them, because there are different modes of one thing. I saw once also mention of "alternating abilities", where they must be used in order, and then after the last one is used, the first one becomes available again. Someone said it is silly, but I think it can be interesting if the costs, time to use, and other requirements are significant! < 1514090881 421939 :zzo38!~zzo38@24-207-13-153.eastlink.ca PRIVMSG #esoteric :What is your opinion of this? < 1514091447 739368 :heroux!sandroco@gateway/shell/insomnia247/x-smyjdonxgaesfyko QUIT :Ping timeout: 240 seconds < 1514091605 569078 :heroux!sandroco@gateway/shell/insomnia247/x-asndbqinxeuvbrdf JOIN :#esoteric < 1514091793 435800 :sleffy!~sleffy@c-24-7-67-0.hsd1.ca.comcast.net JOIN :#esoteric < 1514093001 251772 :variable!~variable@freebsd/developer/variable QUIT :Quit: /dev/null is full < 1514095087 388462 :variable!~variable@freebsd/developer/variable JOIN :#esoteric < 1514098703 768946 :doesthiswork!~Adium@207.55.82.87 QUIT :Quit: Leaving. < 1514099457 386618 :sdfgsdfg!~sdfgsdfg@unaffiliated/sdfgsdfg JOIN :#esoteric < 1514099653 979202 :sdfgsdfg!~sdfgsdfg@unaffiliated/sdfgsdfg QUIT :Remote host closed the connection < 1514099671 682194 :sdfgsdfg!~sdfgsdfg@unaffiliated/sdfgsdfg JOIN :#esoteric < 1514102361 132162 :variable!~variable@freebsd/developer/variable QUIT :Quit: /dev/null is full < 1514102446 209737 :variable!~variable@freebsd/developer/variable JOIN :#esoteric < 1514102454 881874 :variable!~variable@freebsd/developer/variable QUIT :Client Quit < 1514102484 101616 :variable!~variable@freebsd/developer/variable JOIN :#esoteric < 1514102500 840322 :variable!~variable@freebsd/developer/variable QUIT :Client Quit < 1514103266 436197 :sleffy!~sleffy@c-24-7-67-0.hsd1.ca.comcast.net QUIT :Ping timeout: 252 seconds < 1514103659 176183 :sleffy!~sleffy@c-24-7-67-0.hsd1.ca.comcast.net JOIN :#esoteric < 1514105146 416768 :ais523!~ais523@unaffiliated/ais523 JOIN :#esoteric < 1514105311 912003 :moonythedwarf!~moony@unaffiliated/moonythedwarf QUIT :Ping timeout: 248 seconds < 1514106147 731367 :sleffy!~sleffy@c-24-7-67-0.hsd1.ca.comcast.net QUIT :Ping timeout: 240 seconds < 1514106579 396461 :Taneb!~Taneb@2001:41c8:51:10d:: PRIVMSG #esoteric :Does the infinite sum of x/(2^x) converge? < 1514107011 381709 :Taneb!~Taneb@2001:41c8:51:10d:: PRIVMSG #esoteric :Actually, I care about (x/2)/(2^x) but I think if one converges then so will the other < 1514107102 316318 :Taneb!~Taneb@2001:41c8:51:10d:: PRIVMSG #esoteric :I think they converge at 1 and 0.5 respectively but don't know how to prove it < 1514107131 153873 :Taneb!~Taneb@2001:41c8:51:10d:: PRIVMSG #esoteric :2 and 1, not 1 and 0.5 < 1514109119 760289 :erkin!~erkin@unaffiliated/erkin JOIN :#esoteric < 1514110936 168113 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :Taneb: x/(2^x) obviously converges because past a certain point, each element of the sequence is smaller than 1/(1.5^x) (exponential beats linear) < 1514110948 608259 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :although that sort of argument doesn't tell you what number it converges at < 1514112044 432830 :ais523!~ais523@unaffiliated/ais523 QUIT :Ping timeout: 252 seconds < 1514112348 40269 :danieljabailey!~danieljab@cpc75709-york6-2-0-cust725.7-1.cable.virginm.net QUIT :Ping timeout: 272 seconds < 1514112397 339721 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Taneb: for the former, you can show that sum[i=0 to n] i/2^i = 2 - (n+2)/2^n < 1514112496 187377 :danieljabailey!~danieljab@cpc75709-york6-2-0-cust725.7-1.cable.virginm.net JOIN :#esoteric < 1514112663 335691 :int-e!~noone@int-e.eu PRIVMSG #esoteric :there's also the cute idea of rewriting sum[i=0 to inf] i/2^i = sum[i=0 to inf] sum[j=1 to i] 1/2^i as sum[j=1 to inf] sum[i=j to inf] 1/2^i = sum[j=1 to inf] 2/2^j = 2. < 1514112741 922254 :Taneb!~Taneb@2001:41c8:51:10d:: PRIVMSG #esoteric :int-e, that's pretty neat < 1514112747 531532 :Taneb!~Taneb@2001:41c8:51:10d:: PRIVMSG #esoteric :Thank you < 1514112834 793388 :int-e!~noone@int-e.eu PRIVMSG #esoteric :And then there's generating functions: x/(1-x)^2 = x(1/(1-x))' = x(1+x+x^2+...+x^i+...)' = x(1 + 2x + 3x^2 + ... + ix^(i-1)) = x + 2x^2 + ... + ix^i + ..., and x/(1-x)^2 =2 for x = 1/2. < 1514112863 844253 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(I should probably reverse those equations...) < 1514112979 985279 :int-e!~noone@int-e.eu PRIVMSG #esoteric :And I should perhaps note that I'm building on top of the knowledge that the series is (absolutely) convergent, which justifies reordering terms, and replacing 1+x+x^2+... by 1/(1-x). < 1514113221 93654 :danieljabailey!~danieljab@cpc75709-york6-2-0-cust725.7-1.cable.virginm.net QUIT :Ping timeout: 264 seconds < 1514113413 430813 :danieljabailey!~danieljab@cpc75709-york6-2-0-cust725.7-1.cable.virginm.net JOIN :#esoteric < 1514116116 49357 :xkapastel!uid17782@gateway/web/irccloud.com/x-btknicgrsdolbhao QUIT :Quit: Connection closed for inactivity < 1514116862 405420 :danieljabailey!~danieljab@cpc75709-york6-2-0-cust725.7-1.cable.virginm.net QUIT :Ping timeout: 252 seconds < 1514117011 258750 :danieljabailey!~danieljab@cpc75709-york6-2-0-cust725.7-1.cable.virginm.net JOIN :#esoteric < 1514117560 195399 :sprocklem!~sprocklem@unaffiliated/sprocklem JOIN :#esoteric < 1514118084 297745 :sdfgsdf!~sdfgsdfg@unaffiliated/sdfgsdfg JOIN :#esoteric < 1514118120 970002 :sdfgsdfg!~sdfgsdfg@unaffiliated/sdfgsdfg QUIT :Read error: Connection reset by peer < 1514118386 299632 :sdfgsdf!~sdfgsdfg@unaffiliated/sdfgsdfg QUIT :Ping timeout: 260 seconds < 1514119169 131405 :sdfgsdfg!~sdfgsdfg@unaffiliated/sdfgsdfg JOIN :#esoteric < 1514119434 137367 :erkin!~erkin@unaffiliated/erkin QUIT :Read error: Connection reset by peer < 1514119485 149850 :sdfgsdfg!~sdfgsdfg@unaffiliated/sdfgsdfg QUIT :Ping timeout: 264 seconds < 1514119523 920482 :erkin!~erkin@unaffiliated/erkin JOIN :#esoteric < 1514119891 270652 :ais523!~ais523@unaffiliated/ais523 JOIN :#esoteric < 1514120345 680124 :FreeFull!~freefull@defocus/sausage-lover QUIT : < 1514122963 8034 :jaboja!~jaboja@jaboja.pl JOIN :#esoteric < 1514124029 855755 :doesthiswork!~Adium@207.55.82.87 JOIN :#esoteric < 1514125744 186763 :oerjan!~oerjan@hagbart.nvg.ntnu.no JOIN :#esoteric < 1514126289 95714 :sprocklem!~sprocklem@unaffiliated/sprocklem QUIT :Ping timeout: 264 seconds < 1514126915 920936 :moony!~moony@unaffiliated/moonythedwarf JOIN :#esoteric < 1514128720 411735 :boily!~alexandre@modemcable225.73-200-24.mc.videotron.ca JOIN :#esoteric < 1514128755 82280 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :afternoily < 1514129031 766235 :boily!~alexandre@modemcable225.73-200-24.mc.videotron.ca PRIVMSG #esoteric :BØN MATIRJAN! < 1514129058 816886 :boily!~alexandre@modemcable225.73-200-24.mc.videotron.ca PRIVMSG #esoteric :
ACTION is older today! ^^
< 1514129074 907229 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 JOIN :#esoteric < 1514129091 193112 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :Suppose there's a program H1 that can answer whether a program P stops. < 1514129109 501230 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :Then suppose there exists a program Q = IF H1(Q) THEN loop(); ELSE stop(); < 1514129119 710062 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :Thus H1 would get the answer wrong for Q < 1514129160 45715 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :Thus we know that H1 gets the answer incorrect for Q < 1514129192 203721 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :Assume that H1 will answer with "YES" for Q < 1514129211 943462 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :This allows us to construt an H2(P) = IF P = Q THEN "NO" ELSE H1(P) < 1514129219 189874 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :which would get the answer correct for Q < 1514129287 369592 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :or similar if H1 answers with "NO" < 1514129380 182677 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :in the "NO" case we could even tell this because then Q actually stops in a finite amount of time < 1514129455 108712 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :if Q exists we can create an H2 that will detect Q and answer correspondingly or else invoke H1 < 1514129498 899439 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :you could construct a Q2 = IF H2(Q) THEN loop(); ELSE STOP(); < 1514129510 493129 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :at which point you can create an H3 that detects this case as well < 1514129511 684971 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :and so on. < 1514129540 818228 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but you can do this more generically < 1514129565 995391 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :for any Hx it can detect whether it is invoked during execution of the program < 1514129586 698949 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :thus you don't need H1, H2, H3, H4... but only an Hx for the generic case. < 1514129594 360708 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :boily: happy birthday! < 1514129622 618156 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :thus this Hx should get the answer correct for all Qx < 1514129635 411341 :laerling!~laerling@unaffiliated/laerling JOIN :#esoteric < 1514129702 484998 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :which would mean that the existence of a Q does not mean that no such H can exist. < 1514129731 282821 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :which makes me even more convinced that the halting problem does not exist. < 1514129771 78012 :erkin!~erkin@unaffiliated/erkin QUIT :Quit: Ouch! Got SIGABRT, dying... < 1514129783 875553 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :besides what I've already mentioned that proving H can't exist also proves Q can't exist which means that neither H can exist nor can a program exist that would break H < 1514129815 881516 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :two problems there < 1514129826 69803 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :first, how do you compare programs for equality? < 1514129833 431694 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :second, and more importantly, programs are finite < 1514129844 138299 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :your hypothetical Hx is infinite; you can't just take the limit and say it exists < 1514129849 531588 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :mroman: the source code of Q is a function of the source code of H. didn't you get this explained the other day? < 1514129957 959106 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :the point is, there is indeed no Q that works to disprove all Hs, but for every H there is a Q that disproves it. < 1514130006 305387 :jaboja!~jaboja@jaboja.pl QUIT :Ping timeout: 260 seconds < 1514130119 103992 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :compare programs? Reduce them to some normal form I guess. < 1514130142 215317 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :which we can do if the program stops in a finite amount of time < 1514130175 184763 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :or compare source codes < 1514130177 610674 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :that's not even true < 1514130180 515159 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :or whatever representation you have for programs < 1514130193 725820 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :and comparing representation works, but there are infinitely many possible representations of equivalent programs < 1514130209 391657 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :I guess that doesn't make things any worse < 1514130215 648211 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :because your Hx still needs to be infinite anyway < 1514130246 782958 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :if two LC terms are semantically the same they'd evaluate to the same final form eventually < 1514130258 488420 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :otherwise you'd have a non-deterministic eval < 1514130261 567436 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :mroman: not if neither halts < 1514130272 425367 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :yes < 1514130272 837175 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :and we definitely can't assume that they halt here < 1514130281 686406 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but H would halt. < 1514130284 153852 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :any H would halt < 1514130293 879449 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :but we're talking about Q < 1514130299 374891 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :you're comparing programs to Q, which may not halt < 1514130369 807103 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :also even in LC, you can have two programs which halt on all inputs and give the same results on all inputs < 1514130373 719412 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :but don't reduce to the same normal form < 1514130376 8138 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :well then you'd have to proof first that there's a program R that is semantically identical to Q but which can't be reduced to Q in a finite amount of time. < 1514130380 281738 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :because you need the input in order to reduce them < 1514130401 416018 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :you can't compare programs by semantics < 1514130404 188598 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :as in proof that Q is not unique under reduction < 1514130408 617322 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :no < 1514130411 169850 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :or whatever that is called in CS terms. < 1514130419 4303 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :you have it backward < 1514130428 36775 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :in order for your argument to be valid, you need a proof that Q *is* unique under reduction < 1514130436 805001 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :which you won't find < 1514130467 447026 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :there might be a R = IF H(P) == !true THEN ... < 1514130469 166450 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :or whatever < 1514130477 427170 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but that R would be reducable to Q in a finite amount of time < 1514130493 925753 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :actually wait consider this < 1514130525 3851 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :R(P) = if (some condition on P) then Q(P) else Q(P) < 1514130527 428785 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :this doesn't reduce to Q < 1514130530 911444 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :until you provide an input P < 1514130543 259206 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :inputs are cheating. < 1514130546 817924 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :not at all < 1514130550 495992 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :all these programs have inputs < 1514130561 325167 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :they don't have meaning without inputs < 1514130580 323483 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :try formalizing it < 1514130676 233875 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :I mean ultimately < 1514130694 681811 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :the input is known before H is invoked < 1514130700 417483 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :since H only takes a program < 1514130704 757657 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :not a program PLUS input < 1514130709 295791 :garit!~garit@94.197.121.194.threembb.co.uk JOIN :#esoteric < 1514130709 342331 :garit!~garit@94.197.121.194.threembb.co.uk QUIT :Changing host < 1514130709 342355 :garit!~garit@unaffiliated/garit JOIN :#esoteric < 1514130714 864215 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :that's not how it's usually specified < 1514130723 360186 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :I know. < 1514130725 980314 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :the halting problem is to determine if a given program halts *on a given input* < 1514130728 55758 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but I don't care about the I/O case. < 1514130746 745422 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :I want the non I/O case :) < 1514130755 822704 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :passing parameters counts as I/O < 1514130764 58271 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :you're thinking at too high a level here < 1514130793 487482 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :H can only somehow measure if P stops or not. < 1514130800 217134 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :I mean < 1514130809 494824 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :without communicating with P in any other way < 1514130812 40065 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :you can look at the input as a program+input combination < 1514130815 658313 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :H doesn't even get the output of P < 1514130820 718199 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :and then you "don't have I/O" < 1514130826 624776 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :turing machines don't have output < 1514130829 992220 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :besides ACCEPT/REJECT < 1514130834 426793 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :it's not actually a big difference if you disallow I/O there, it can be hardcoded. < 1514130837 46740 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :again, you're thinking at too high a level < 1514130846 249403 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :I/O is not a concept in turing machines < 1514130861 666720 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :there are modified Turing Machine definitions that do have I/O < 1514130863 909816 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :normally using a separate tape < 1514130869 706647 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :yeah < 1514130870 373821 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :but the original definition doesn't < 1514130881 162004 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :I accept the halting problem in the I/O case. < 1514130884 159629 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :That makes sense. < 1514130889 143037 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :mroman: there is no "I/O case" though < 1514130892 338436 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :ultimately < 1514130929 16541 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :Q = IF H(P) ... is inherently an I/O bound action. < 1514130942 267828 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :because it calls a foreign program that is not within Q < 1514130945 53668 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :no < 1514130950 120466 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :that's not how turing machines work < 1514130955 301836 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :H is embedded in Q < 1514130963 237897 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :it's not "foreign" < 1514130964 799042 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :there is no I/O < 1514130972 630179 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :it's like a subroutine < 1514130995 106890 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :mroman: i told you, the source code of Q contains the source code of H. < 1514131008 182164 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :it _is_ within. < 1514131068 938875 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but then Q = IF H(Q) doesn't work < 1514131079 218269 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :because you're only passing Q < 1514131080 8923 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :not H. < 1514131084 428637 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :of course it does, you use a quining technique. < 1514131087 368523 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :^ < 1514131098 855120 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :which isn't mentioned in the proof anywhere < 1514131103 717972 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :because < 1514131115 204719 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :H is a machine which takes an encoded representation of a Turing machine, right? < 1514131122 174133 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :like, the input to H is source code < 1514131124 370882 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :mroman: you may have read a bad version of the proof. < 1514131130 78042 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :you just assume that you can embed H like that. < 1514131146 819754 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :mroman: the fact that you can embed H like that is well established < 1514131153 199855 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :turing machines are universal < 1514131158 22358 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :of course, i cannot say clearly that i've read it, i just consider it obvious since i _do_ know how to write a quine. < 1514131169 803778 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :I know how to write a quine too. < 1514131188 271674 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :(\x.xx)(\x.xx) being the most obvious one < 1514131193 212742 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :mroman: so the way it works from a technical point of view is < 1514131229 823329 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :H is a turing machine whose input is a description of turing machine < 1514131232 230012 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :(that is not a quine) < 1514131246 829004 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :the description doesn't need to be specified specifically, because we're trying to prove H doesn't exist < 1514131267 750449 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :so we can assume that there is some way to go from (Turing Machines) -> (input format for H) < 1514131303 990411 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :Q embeds H as a subroutine < 1514131318 364600 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :(it's not too hard to show how to do this, though I can explain it more if you need) < 1514131345 692478 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :so now we apply our mapping to Q, and we get Q in the input format to H < 1514131348 957775 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :then we feed this to Q < 1514131354 101641 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :which in turn passes it on to H < 1514131421 390551 :laerling!~laerling@unaffiliated/laerling QUIT :Quit: Leaving < 1514131546 457476 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :I mean you could have a turing machine with a Quine operator right? < 1514131554 44407 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :that shouldn't violate the laws of turing machines. < 1514131569 828056 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :presumably. but they can already do quines so why bothere < 1514131573 233665 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :*-e < 1514131584 513881 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :so you could write a program IF H(myself) THEN loop(); else halt(); < 1514131599 364680 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :where myself is a builtin that is replaced with the source code of the program itself. < 1514131644 988977 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :then to be more specific... the program would look like `H(p) := ....; Main := IF H(myself) THEN loop(); ELSE halt();` < 1514131682 809834 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :hm < 1514131698 745336 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :it's officially christmas in norway, time to open the first nutella ball... < 1514131699 549743 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :Not quite, a program can't quine itself < 1514131709 41632 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :because it doesn't have a copy of its source code < 1514131720 952548 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :... < 1514131721 458619 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :at least not in the general case < 1514131734 53629 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :quines operate at a meta level < 1514131737 902384 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :oerjan: what day is it celebrated? and what time does it start? I assume if it's officially Christmas now, it has been for several hours < 1514131747 476373 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :today is Christmas Eve in the UK and insanely busy in all the shops as a consequences < 1514131750 251499 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :*consequence < 1514131777 93376 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :hmm, maybe I should write a better BuzzFizz interp so that I can look into whether it can write a quine < 1514131784 79025 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :I'd be surprised if it couldn't, but it seems really painful < 1514131803 948629 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :ais523: 17 on Dec 24 is when the church bells start ringing < 1514131832 453035 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :that is an oddly specific Christmas tradition < 1514131848 661188 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :here it starts at midnight between 24 and 25 in theory, or mid-September in practice :-P < 1514131850 473430 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :well you could have some a regular computer with infinite memory where the program sits in memory itself so it can surely access itself < 1514131858 246576 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :although the TM would technically be that computer than < 1514131860 100421 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but anyway < 1514131860 538514 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :mroman: sure, but that's not a turing machine < 1514131881 174827 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but it's equivalent to turing machines? < 1514131909 399777 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :or it's at least as good as a turing machine < 1514131913 911205 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :equivalent in computational power, but I guess the equivalent for a real computer < 1514131924 77532 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :would be like trying to have the processor output a copy of its own circuitry < 1514131942 229118 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :most processors can do that just fine, especially as they don't need to output the data defining that circuitry too < 1514131952 312747 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but theoretically a turing machine could produce a representation of itself somehow? < 1514131956 254638 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :ais523: how would they do that without access to a copy of the schematic? < 1514131980 903714 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :mroman: Any such machine would either have to be specifically designed to do so, or take enough information to do so in the input, or some mix of the two < 1514131988 719154 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :I'm assuming they have memory, even if it's just cache < 1514131990 353911 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :like, a machine which just adds two numbers together couldn't < 1514131994 149598 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :for a more direct example, see https://codegolf.stackexchange.com/a/100114 < 1514131996 680628 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :because it just adds numbers together < 1514132004 379258 :laerling!~laerling@unaffiliated/laerling JOIN :#esoteric < 1514132012 819879 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :oh, you're talking about "not all programs are quines" rather than "some programs are quines" < 1514132065 792282 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :all normal forms are basically quines. < 1514132078 161223 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :no < 1514132085 840149 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :you're confusing two things there < 1514132108 625249 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :I mean, I guess if you define the output of a computation to be normal form, then yes < 1514132115 482243 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :\x.y evaluates to \x.y < 1514132145 356969 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :the original definition of turing machine has no output other than ACCEPT/REJECT though < 1514132148 406254 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :don't remember what it was caled < 1514132149 771119 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :so quines are impossible under that definition < 1514132150 784301 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :beta normal form? < 1514132160 573205 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :alercah: it could leave a description of itself on the tape < 1514132165 745044 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :ais523: true < 1514132177 2640 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :ais523: there's a radio program playing sounds from church bells all over the country at this time (and also church choirs) < 1514132183 593904 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :but that does require a slightly different definition < 1514132193 169337 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :and the shops close a couple hours earlier at least. < 1514132194 821790 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :incidentally, I'm upset that nobody else took up the challenge to create a circuit that output a specification of itself, it was a really interesting idea < 1514132198 422335 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but either way < 1514132212 309812 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :oerjan: over here most shops close at 9pm on Christmas Eve < 1514132223 70470 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :apparently, even if it's a Sunday (which means that they end up opening /longer/ than they normally would…) < 1514132248 220922 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :The one liner proof is if H exists with said properties then a Q = IF H(Q) THEN loop(); else halt(); exists thus no H can exist with such properties. < 1514132265 285254 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :and this one is really easy to understand. < 1514132296 910432 :boily!~alexandre@modemcable225.73-200-24.mc.videotron.ca QUIT :Quit: EXPLODING CHICKEN < 1514132319 39329 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :a normal form program is basically a literal-only program < 1514132325 27724 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :those normally aren't considered quines < 1514132326 227004 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :similarily if you had two programs A and B that can each answer correctly for a subset of programs < 1514132327 970883 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :> < 1514132329 363523 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :err < 1514132329 808023 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric : : error: not an expression: ‘’ < 1514132330 804942 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :> ` < 1514132332 307217 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :> 1 < 1514132332 870519 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric : :1:1: error: parse error on input ‘`’ < 1514132334 689415 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric : 1 < 1514132336 732063 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :there we go < 1514132338 847193 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :you could combine A and B into a new program < 1514132346 416276 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :"1" is not normally considered a quine in ghci < 1514132351 910053 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :probably < 1514132354 173595 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :because it's just a literal that's printed literally < 1514132356 381490 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :mroman: you can do that, yeah < 1514132358 633633 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :but it meets some definitions < 1514132368 426794 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :mroman: there are definitely subsets of programs for which it can be answered < 1514132414 956259 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but you'd have to make some assumption < 1514132430 393253 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :such as saying that if A can't decide it loops forever and if B can't decide then B loops forever < 1514132475 542512 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :thus you can create a C(P) = PAR { A(P) ; B(P); } < 1514132498 820193 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :yeah < 1514132501 275041 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :which evaluates A and B in parallel and since either A or B eventually terminates C terminates < 1514132512 180372 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :or if neither can decide, then C doesn't terminate < 1514132513 379901 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but then you could create D = IF C(P) THEN loop() ELSE halt() < 1514132535 37741 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :and C(D) would be wrong < 1514132541 801215 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :or nonterminating < 1514132553 71066 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :so we know that no finite amount of programs combined can answer correctly for every P < 1514132557 290630 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :right < 1514132560 201608 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :(in a finite amount of time) < 1514132567 630796 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :you mean bounded, not finite < 1514132575 552045 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :err wait < 1514132577 183584 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :no I'm wrong < 1514132582 663422 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :got it backwards because I'm tired < 1514132585 925074 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :ignore me >_> < 1514132586 207975 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :I don't know what you mean by bounded vs finite < 1514132595 962631 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :ok good pretend I didn't say the stupid thing and move on then < 1514132624 600616 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :oh. bounded is used for quantities < 1514132625 708944 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :I see. < 1514132663 859110 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :in this context bounded usually means there's a single upper bound, so like "there is a number X such that the problem can always be decided in less than X time" < 1514132678 466553 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :vs "the problem is always decided in finite time, but may take arbitrarily long" < 1514132687 230486 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but that still leaves one unanswered question < 1514132693 602875 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :since neither C nor D can exist < 1514132698 240067 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :what do we do with that? < 1514132701 892377 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :philosophically < 1514132720 358237 :jaboja!~jaboja@jaboja.pl JOIN :#esoteric < 1514132741 399548 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :you think that's bad, how about the algorithms that we know exist but that we can't prove them correct < 1514132833 992013 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :suppose A exists but if A exists a B must exist but the existence of B means A can't exist thus A does not exist but since A does not exist neither does B exist so neither A nor B actually exist. < 1514132863 369653 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :ais523: in norway sundays in december can have longer opening hours by law, but not today. < 1514132865 182115 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :which for the halting problem would mean that there doesn't exist a program where H would answer incorrectly. < 1514132879 641858 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :because the existence of that program is bound to the existence of H. < 1514132883 637448 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :and we know H doesn't exist. < 1514132931 140182 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :which sounds more like the halting problem is undecidable < 1514132935 252874 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :I mean, notwithstanding that you're not quite right about A and B < 1514132935 417398 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :rather than saying it exists. < 1514132941 272429 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :that's just how proof by contradiction works < 1514132953 481120 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :you take one impossibility, and build on it < 1514132956 156342 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :not really < 1514132964 297415 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :many of the intermediate constructions you make will be equally impossible < 1514132972 217553 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :because they rely on the first impossibility < 1514132972 264037 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :like the proof for the irationality of sqrt(2) is a proof by contradiction right? < 1514132982 467493 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :that's one approach < 1514132987 904090 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but sqrt(2) actually exists. < 1514132990 636659 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :that's totally different. < 1514133005 775076 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :ok, fine, proofs of non-existence by contradiction < 1514133013 235178 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :which is not what the proof about sqrt(2) is < 1514133031 737411 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :it'd be like saying H exists < 1514133032 75388 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :try, say, the proof that there are no functions continuous at all rational points but discontinuous at all irrational ones < 1514133038 461889 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but it doesn't have a property you say it have < 1514133039 42715 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :like < 1514133055 913257 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :H(x) is a program, suppose H(x) had the property that it answers correctly for all P < 1514133066 172165 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :you could then proof that H can't have that property < 1514133070 642069 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :yeah < 1514133076 255764 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :that's another, equally valid way < 1514133079 286306 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :because Q = IF H(Q) THEN ... would break that property < 1514133087 432225 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :for sqrt(2) < 1514133088 649829 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but this means that H actually exists. < 1514133101 484904 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :you could prove that there is no number x for which x is rational and x^2 = 2 < 1514133188 994272 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :which would leave the question what property that H has then. < 1514133193 473661 :jaboja!~jaboja@jaboja.pl QUIT :Remote host closed the connection < 1514133268 529878 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :you could say P is the set of all programs < 1514133280 699849 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :and H is the property of a program to answer the correctly whether some other program halts. < 1514133288 912375 :propumpkin!~copumpkin@haskell/developer/copumpkin JOIN :#esoteric < 1514133303 713935 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :well.. P is the set of all programs that take another program as input and answer with a yes or no < 1514133341 362564 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :you could then show that no program in that set has the property H. < 1514133415 687556 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but they all exist. < 1514133422 281071 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :they just don't have the property H < 1514133436 307671 :contrapumpkin!~copumpkin@haskell/developer/copumpkin QUIT :Ping timeout: 260 seconds < 1514133440 378782 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :it's just a question of how you define existence < 1514133441 546679 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :I'd accept that as a valid proof. < 1514133459 792271 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :because it avoids the circular argument. < 1514133476 434329 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :you can't embed a program that doesn't exist < 1514133485 574688 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :but you're assuming it does < 1514133493 522585 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :yes but still < 1514133500 852052 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :I'm assuming H(P) exists < 1514133516 125425 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :a consequence of that assumption is that you can construct Q < 1514133518 285661 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :which allows me to define Q=IF H(Q) THEN loop(); else halt(); < 1514133523 773302 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :right < 1514133529 235501 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but I can only construct Q if H exists. < 1514133534 66410 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :because if H doesn't exist < 1514133535 530886 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :but you assumed thta it does < 1514133535 613812 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :then Q doesn't. < 1514133541 232901 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :if H doesn't exist, you don't need Q < 1514133545 19240 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :because you're already done the proof < 1514133545 391656 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :so the chain of proof is < 1514133569 678294 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :if H exists then Q exists and the existence OF Q proofs that H doesn't exist. < 1514133575 571172 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but this invalidates my assumption that Q exists < 1514133579 29934 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :no < 1514133581 505612 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :and if Q doesn't exist < 1514133582 443639 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :Q existing is not an assumption < 1514133585 478667 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :I can't proof that H doesn't exist. < 1514133602 332428 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :because to prove that H doesn't exist I need that Q to exist. < 1514133613 903172 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :Q existing is a consequence of H existing < 1514133617 784682 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :If Q exists < 1514133620 40702 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :then H must exist. < 1514133621 262529 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :you have made only one assumption < 1514133623 825210 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :which is that H exists < 1514133650 589337 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :The existence of Q proves that H exists. < 1514133665 12198 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :yes, but that's only valid in the logical context < 1514133669 493416 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :which is of an assumption that H exists < 1514133702 485967 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :there's no need for Q to exist if H doesn't exist < 1514133711 130903 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :meh :D < 1514133719 263262 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :I can't accept such kind of proofs. < 1514133722 265675 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :they're illogical. < 1514133734 421595 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :no, they're quite logical < 1514133746 168540 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :exists H => exists Q => not exists H. < 1514133763 797509 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :since I now know H does not exist. < 1514133772 132783 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :you never proved Q exists < 1514133777 793924 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :you proved that "if H exists, Q exists" < 1514133781 920636 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :I have false => exists Q => not exists H. < 1514133794 153916 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :and false => X is not a valid proof. < 1514133808 514905 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :no < 1514133810 596676 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :that step doesn't hold < 1514133837 870783 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :(A => B) is true if either A is false OR B is true < 1514133863 618609 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :so (H exists => Q exists) is true even if H doesn't exist < 1514133877 91715 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :well formally < 1514133892 303591 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but we know Q can't exist because Q embeds H. < 1514133897 379602 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :so either awy < 1514133898 865928 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :that's fine < 1514133911 131140 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :we don't need Q to exist on its own < 1514133915 370238 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but yes < 1514133920 404363 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :we only need it to exist if H exists < 1514133924 527126 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :wrong => true statement is technically true < 1514133932 877678 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but a true statement can't follow from a wrong statement. < 1514133944 730200 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :yeah < 1514133951 892132 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :so if we were trying to prove Q exists that would be a problem < 1514133957 232374 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :fortunately we're trying to prove it doesn't exist < 1514133970 870823 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :no, you're trying to prove H doesn't exist < 1514133980 437959 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :well yes < 1514133991 969123 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :and your proof only works if Q exists. < 1514133999 385567 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :because you're using Q as a counter example < 1514133999 432070 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :no < 1514134003 364236 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :that's not true < 1514134058 266316 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :you mentioned the proof that sqrt(2) is irrational, right? < 1514134063 672738 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :yes < 1514134075 140921 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :the first line is "suppose sqrt(2) is rational, then there exist a and b in lowest terms such that a/b = sqrt(2)" < 1514134081 429802 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :those a and b don't exist < 1514134084 388563 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :they cannot < 1514134103 643036 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :well < 1514134111 697573 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :the combination of a/b = sqrt(2) doesn't exist < 1514134142 225794 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :you assume that a are natural numbers < 1514134147 683104 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :*that a and b < 1514134160 930605 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :I'm asserting that some numbers with some properties exist < 1514134167 256902 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :saying they exist without those properties is meaningless < 1514134178 902989 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :and just pointless philosophizing over the definition of "exist" < 1514134197 152584 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :natural numbers exist < 1514134211 986900 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :you just can't find a combination of two natural numbers a and b such that a/b = sqrt(2) < 1514134217 56924 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :sure, but the pair (a, b) such that a/b is in lowest terms and equal to sqrt(2) does not exist < 1514134233 468725 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :you're just trying to draw some arbitrary definition of mathematical objects that do exist, and ones that don't < 1514134235 860743 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :any pair of two natural numbers exist < 1514134243 117285 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :as oerjan said, you could also look at Q as a function < 1514134248 117422 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :Q(H) = ... < 1514134252 84071 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :they just don't have the property that a/b = sqrt(2) < 1514134255 208100 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :or, well, Q(H)(P) < 1514134258 976815 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :in that case, Q absolutely exists < 1514134303 82925 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :or in other terms < 1514134311 371241 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :sqrt(2) is not member of the set N < 1514134324 53790 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :eh < 1514134324 965745 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :set Q < 1514134336 86043 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :like I said, this is pointless philosophizing with no logical meaning < 1514134347 889461 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :that's not pointless < 1514134351 590475 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :if H exists < 1514134355 357790 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :the logical steps are perfectly well defined < 1514134356 737630 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :and correct < 1514134368 740413 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :H can't be a member of the sets of all turing machine-ish programs < 1514134374 425685 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :you're trying to lift Q's existence outside the hypothetical "H exists" < 1514134381 283654 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :which is logically invalid, and correctly so < 1514134389 377539 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :but you're complaining that this means it can't exist in the hypothetical < 1514134390 944667 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :which isn't true < 1514134416 788515 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :let's call the set of all turing machines T < 1514134424 393095 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :then H is not member of that set. < 1514134445 954325 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :that follows from the halting problem proof. < 1514134451 726097 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :right < 1514134465 652517 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but Q is member of that set. < 1514134470 50000 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :no < 1514134489 80908 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :it isn't < 1514134501 113763 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :so Q itself isn't a set of T < 1514134509 658881 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :do you mean member? < 1514134510 380159 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :so you can't use the existence of Q to proof anything < 1514134513 951803 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :because it's not even within T < 1514134521 870920 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but the question is whether H can answer it correctly for members of T < 1514134524 870109 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but if Q isn't member of T < 1514134529 480705 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :but < 1514134530 866918 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :then Q isn't a counter example. < 1514134534 798774 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :if we suppose H exists < 1514134537 7010 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :i.e. < 1514134538 384297 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :H \in T < 1514134541 521176 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :then Q can be defined < 1514134543 397714 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :and Q \in T < 1514134560 452268 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but Q can only be in T if H is in T < 1514134565 664458 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :but we assume H is in T < 1514134569 161400 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :that follows from the definition of H. < 1514134570 446998 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :so it's a logically valid step < 1514134570 537693 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :eh. < 1514134572 768569 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :definition of Q < 1514134706 901256 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :I think you're getting hung up on "existence" here < 1514134716 499563 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :because the logical step of picking a and b in the proof of sqrt(2) is no different < 1514134723 561651 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :it's a step which is only logically valid if the statement is false < 1514134727 563753 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :that's how proof by contradiction works < 1514134737 827381 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :I don't think it's the existence per se but the fact that a proof should be valid if up update it with new information. < 1514134745 913928 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :*you update < 1514134750 177248 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :but then the sqrt(2) proof is equally invalid < 1514134756 791043 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :why? < 1514134761 69301 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :because once we prove that sqrt(2) is irrational < 1514134766 691095 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :suppose sqrt(2) is a member of Q < 1514134767 984785 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :we know that the step of picking a and b was invalid < 1514134784 291504 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :by your argumen < 1514134788 809310 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :then there would exist an a,b both member of N such that sqrt(2) = a/b. < 1514134793 343751 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :right < 1514134795 665956 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :well < 1514134802 581289 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :if we include the fact that sqrt(2) is positive < 1514134806 884004 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :otherwise they could be negative < 1514134809 893180 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :but generally yeah < 1514134833 12574 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :more specifically, you cand find a pair of a,b with the property of a/b = sqrt(2) < 1514134841 770489 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric : a^2/b^2 = 2 < 1514134850 869274 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :right < 1514134874 765285 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :yada yada so we know for that to be true both a and b would have to be even numbers. < 1514134890 234180 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :yeah you can leave out hte details < 1514134963 576617 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :I skipped one assumption tho < 1514134969 817120 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :that a and b don't have common factors < 1514134985 865084 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :yeah, that's fine, I'm familiar with the proof < 1514135002 866266 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :we assumed that we can find a pair a,b with no common factors such that a/b = sqrt(2) < 1514135009 813663 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :no < 1514135013 142346 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but this is wrong. < 1514135013 986979 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :we assumed that sqrt(2) \in Q < 1514135028 472389 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :since both a and b have to be even if a/b = sqrt(2) < 1514135123 592857 :xkapastel!uid17782@gateway/web/irccloud.com/x-umjxzayhmsnstokm JOIN :#esoteric < 1514135124 665499 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :so this is a contradiction < 1514135132 295405 :alercah!~alercah@unaffiliated/alercah PRIVMSG #esoteric :right < 1514135147 180033 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :thus we know there's no such pair of a,b as we assumed < 1514135206 423274 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :hm i see < 1514135210 30147 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :now we know that a and b must have at least a common factor of 2 < 1514135225 434923 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :now we go back < 1514135307 307799 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :mroman: hm i think i have a hunch where you're getting hung up, and the sqrt(2) proof is just simple enough to avoid it. but what about the proof of the infinitude of primes? < 1514135395 770671 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :maybe we can find a,b with common factors such that a/b = sqrt(2) < 1514135398 207163 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :it seems to have the same H => P => no such H thing < 1514135405 950352 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :*structure < 1514135432 939420 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :(well, perhaps i should wait to see if you _are_ hung up on sqrt(2) first) < 1514135464 383828 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :so we divide by two repeat < 1514135471 27097 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but you'll always end up with the same thing. < 1514135504 70578 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :
ACTION had some washing to do
< 1514135523 601377 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :so we know that if a/b = sqrt(2) then both a and b can endlessly be divided by two. < 1514135623 370132 :laerling!~laerling@unaffiliated/laerling QUIT :Ping timeout: 265 seconds < 1514135633 791909 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :so sqtr(2) = x*2^infinity < 1514135851 959500 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :which is nonsense < 1514135872 602307 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :because you can't do that within Q < 1514135906 161778 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :you mean there's no largest prime? < 1514135957 395984 :zzo38!~zzo38@24-207-13-153.eastlink.ca PRIVMSG #esoteric :Is there a quick algorithm to figure out both the squarefree core of a number as well as the square root of the rest, at the same time? < 1514135999 408311 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :Assume there's a number with the property of being prime such that you can not find a number larger than that also having the property of being prime. < 1514136049 767572 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :assume p = p1*p2*p3*p4*p5*...*pn has this property < 1514136098 618865 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :+1 < 1514136114 879769 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :(otherwise it wouldn't be prime) < 1514136156 141144 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :then q = p1*p2*p3*p4*p5*...*pn*p+1 would also be prime < 1514136162 811626 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :thus p doesn't have the property < 1514136192 805411 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :which now we go back as well < 1514136207 699423 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :we know that p doesn't have the property < 1514136211 578827 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but we know that p is prime < 1514136258 80327 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :p doesn't need to have the property for the proof to work < 1514136258 171311 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :p doesn't need to have the property for the proof to work < 1514136326 241609 :h0rsep0wer!~h0rsep0we@unaffiliated/h0rsep0wer JOIN :#esoteric < 1514136352 655496 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :so the fact that p doesn't have the property doesn't invalidate the fact that q is a larger prime than p < 1514136373 656547 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :so q disproves that p has the property. < 1514136381 989967 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :which is logically consistent. < 1514136392 891742 :Taneb!~Taneb@2001:41c8:51:10d:: PRIVMSG #esoteric :Help my scrollback is full of proof and I do not know what is going on (I missed the beginning) < 1514136439 749280 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :mroman: i wanted to explain it in a different way, to highlight the similarity. < 1514136450 743233 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :Taneb: I reject the halting problem proof on the grounds that you assume and H exists and then create a counter example Q = IF H(Q) THEN loop(); ELSE halt(); to prove that H does not exist. < 1514136456 979715 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :assume there are finitely many primes, let H be the list of all of them. < 1514136471 66294 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but if you come back with this new knowledge of H not existing you'll find that Q (your counter example) can't exist as well < 1514136478 147839 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :thus your counter example doesn't exist < 1514136479 998273 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :thus your proof sucks :D < 1514136501 419773 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :now if H exists, then let Q be the product of all the numbers in H. < 1514136520 662907 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :continue as you did. from the existence of Q we deduce that H cannot exist. < 1514136537 759346 :augur!~augur@c-73-125-61-197.hsd1.fl.comcast.net JOIN :#esoteric < 1514136548 522234 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :now you have the exact same structure as for the point you disagree with in the halting problem. < 1514136556 955528 :Taneb!~Taneb@2001:41c8:51:10d:: PRIVMSG #esoteric :mroman, so... proof by contradiction? < 1514136696 880871 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :zzo38: i don't think you can find the squarefree core of a number without prime factorization < 1514136716 73231 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :Taneb: I'm fine with proofs by contradiction. < 1514136827 740911 :augur!~augur@c-73-125-61-197.hsd1.fl.comcast.net QUIT :Ping timeout: 268 seconds < 1514136867 395890 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :Taneb: he's having trouble with proofs of the form H exists => Q exists, Q exists => H doesn't exist, ergo H doesn't exist < 1514136894 792554 :Taneb!~Taneb@2001:41c8:51:10d:: PRIVMSG #esoteric :oerjan, I see < 1514136894 908752 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :so i'm trying to show a different one, but i think i chose a bad time. < 1514136899 982478 :Taneb!~Taneb@2001:41c8:51:10d:: PRIVMSG #esoteric :I think I'll sit this one out < 1514136966 988901 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :Taneb: The reason is because your proof gives you new knowledge and if you update your proof with this new knowledge you'll find that Q can't exist and thus you don't have a counter example anymore. < 1514136980 625004 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :The counter example you used to proof the non-existence of H does itself not exist to begin with. < 1514136998 938547 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :counter examples inherently need to exist < 1514137005 685000 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :an argument based on a non-existing counter example is < 1514137007 51372 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :well < 1514137007 214766 :Taneb!~Taneb@2001:41c8:51:10d:: PRIVMSG #esoteric :mroman, what about a counterexample scheme < 1514137010 387466 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :I consider it non-sense < 1514137022 451902 :Taneb!~Taneb@2001:41c8:51:10d:: PRIVMSG #esoteric :A function from example to counter-example < 1514137047 401727 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :mroman: grmble. ok let's reformulate the original instead, i think it can be done. < 1514137058 825221 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but you can reformulate the proof < 1514137072 925363 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :to show that no program in the sets of all programs can have the property of answering stuff correctly < 1514137116 297027 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :let H be a program deciding _something_ about other programs. let Q = if H(Q) then loop(); else halt() < 1514137142 466739 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :as in. Let M be the set of all programs taking a program as input and answer yes or no then we can certainly show that no program in this set answers correctly for all programs. < 1514137204 967722 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :Meaning that no such program exists in the set of all programs. < 1514137211 808160 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :... < 1514137219 876277 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :(no program that answer correctly for all programs) < 1514137221 843743 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :whatever. < 1514137266 972724 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but the program itself exists < 1514137273 448413 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :it just doesn't have the property you assumed it does < 1514137341 376588 :variable!~variable@freebsd/developer/variable JOIN :#esoteric < 1514137343 936822 :Taneb!~Taneb@2001:41c8:51:10d:: PRIVMSG #esoteric :There isn't a fundamental difference between the two arguments here to me < 1514137348 743886 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :int-e: I was going to tell you that SSR is 75% off but I forgot you already played it. < 1514137394 295384 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Right. I'm stuck. The Witless is also available at a reasonable price. < 1514137423 804114 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :Taneb: not in the outcome. < 1514137424 445131 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :Let M be the set of all programs of the form A(B) = true/false For every program P in M we can construct a program Q = IF P(Q) THEN loop(); ELSE halt(); which would imply that P does not answer correctly for Q. < 1514137435 220857 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but there's a slight difference here < 1514137440 606111 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :namely the fact that P exists < 1514137445 167507 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :which means Q exists < 1514137451 885353 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :which means we can use Q as a counter example < 1514137456 966466 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :because Q exists < 1514137464 726197 :Taneb!~Taneb@2001:41c8:51:10d:: PRIVMSG #esoteric :mroman, I think we have a difference in mathematical philosphy here < 1514137466 495778 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :thus making the proof logical. < 1514137472 1649 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :Taneb: It appears so. < 1514137552 93695 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but this proof makes sense to me. < 1514137554 206377 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :the other doesn't. < 1514137559 532883 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :int-e: Any other good jams? < 1514137584 740304 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but if my reformulation of the proof is correct < 1514137590 338476 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :then I can accept the halting problem to be true < 1514137625 895911 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :otherwise I have to continue looking :D < 1514137665 34362 :Taneb!~Taneb@2001:41c8:51:10d:: PRIVMSG #esoteric :mroman, so... the form you don't like is (\exists x \in S => ¬ \exists x \in S) => ¬ \exists x \in S < 1514137681 560339 :Taneb!~Taneb@2001:41c8:51:10d:: PART #esoteric :"Leaving" < 1514137686 636697 :Taneb!~Taneb@2001:41c8:51:10d:: JOIN :#esoteric < 1514137712 541969 :Taneb!~Taneb@2001:41c8:51:10d:: PRIVMSG #esoteric :But the form you do like is \forall x \in T => (P(x) => ¬P(x)) => ¬P(x) < 1514137718 232778 :Taneb!~Taneb@2001:41c8:51:10d:: PRIVMSG #esoteric :Is this right? < 1514137813 208261 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :\exists X \in S => \exists Y \in S => \not \exists X \in S <- I don't accept this. < 1514137841 190602 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :because the existence of Y \in S is tied to the existence of X \in S < 1514137846 41038 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :which you later proof to be wrong. < 1514137857 602111 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :like < 1514137864 997479 :Taneb!~Taneb@2001:41c8:51:10d:: PRIVMSG #esoteric :I am not sure where that Y is coming from here, the counter example for the halting problem is not in the set of halting oracles < 1514137867 259693 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :travelling in time shouldn't invalidet proofs. < 1514137872 536953 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :*invalidate < 1514137880 874560 :int-e!~noone@int-e.eu PRIVMSG #esoteric :shachaf: I don't know. I finished The Night of the Rabbit today (which I started last year... I took a break which saved me using a walkthrough) which I liked quite a lot. < 1514137899 822613 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :well Q is a counter-example to H. < 1514137905 979942 :int-e!~noone@int-e.eu PRIVMSG #esoteric :But of course it's a point&click adventure, so completely different genre. < 1514137915 608676 :Taneb!~Taneb@2001:41c8:51:10d:: PRIVMSG #esoteric :It's a witness that the existence of H is inconsistent < 1514137924 142047 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but Q contains H < 1514137936 540989 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :Q = IF H <- see. H is contained within Q. < 1514137965 976083 :Taneb!~Taneb@2001:41c8:51:10d:: PRIVMSG #esoteric :All proofs by contradiction do something like that, though < 1514137976 863437 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :not really. < 1514137990 771996 :int-e!~noone@int-e.eu PRIVMSG #esoteric :yes, really. < 1514138016 515515 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :Assume 9 is even. If 9 were even then sqrt(9) had to be even since 9 is a perfect square. sqrt(9) = 3 which is odd thus our assumption that 9 was even must be wrong thus 9 must be odd. < 1514138047 767237 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :int-e: Did you jam Recursed? < 1514138058 920766 :Taneb!~Taneb@2001:41c8:51:10d:: PRIVMSG #esoteric :You make a proof that 3 is even using a proof that 9 is even < 1514138065 965288 :int-e!~noone@int-e.eu PRIVMSG #esoteric :mroman: yes, so you've constructed an *even* square root of 9, which is something that doesn't really exist. < 1514138074 781856 :propumpkin!~copumpkin@haskell/developer/copumpkin NICK :contrapumpkin < 1514138075 744216 :Taneb!~Taneb@2001:41c8:51:10d:: PRIVMSG #esoteric :But then use this to prove that 9 is odd, so the proof that 3 is even cannot exist < 1514138092 422707 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :well 3 isn't even. < 1514138095 80931 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :I don't see the problem there. < 1514138126 589481 :int-e!~noone@int-e.eu PRIVMSG #esoteric :The only objection I have is that a proof of contradiction is not necessary in this case... never mind involving square roots. < 1514138127 545056 :Taneb!~Taneb@2001:41c8:51:10d:: PRIVMSG #esoteric :I can't see why you're happy with that and unhappy with expressing Q in terms of H < 1514138155 128563 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :Taneb: because it's still consistent. < 1514138206 452573 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :my assumption that 9 is even turned to be wrong < 1514138211 950095 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :so now I know that 9 is odd. < 1514138226 306167 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but no statement is invalidated in this proof by 9 being odd. < 1514138238 765042 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :nothing in that proof depends on 9 being odd. < 1514138239 166475 :int-e!~noone@int-e.eu PRIVMSG #esoteric :The Q constructed in the halting problem proof does exist for any given H as well; it just fails to halt if and only if it doesn't halt, because that property relies on the assumption on H. < 1514138245 795184 :Taneb!~Taneb@2001:41c8:51:10d:: PRIVMSG #esoteric :I don't understand your argument here < 1514138257 604801 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :it's like uhm < 1514138258 747435 :Taneb!~Taneb@2001:41c8:51:10d:: PRIVMSG #esoteric :I'm going to wander off < 1514138305 216734 :int-e!~noone@int-e.eu PRIVMSG #esoteric :This is quite analogous to the square root of 9. It exists, it equals 3, it just happens not to be even after all. < 1514138468 85193 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :Assue 9 is even. If 9 is even then 9+0 is even. Since 9+0 is even then .\ < 1514138488 813770 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :now you somehow end up showing that 9 is not even. < 1514138501 58955 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :then isn't valid anymore. < 1514138549 441063 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :or if would show that 9 is odd. < 1514138553 695222 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :that just doesn't work logically. < 1514138571 376693 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Anyway, I'm with Taneb here, I don't understand what your problem is. < 1514138642 249854 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :whatever you conclude from 9+0 is even < 1514138646 403348 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :is only valid if 9+0 is even < 1514138710 477313 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric ::( < 1514138725 111328 :int-e!~noone@int-e.eu PRIVMSG #esoteric :shachaf: nay on recursed < 1514138746 282559 :int-e!~noone@int-e.eu PRIVMSG #esoteric :mroman: this is just basic logic < 1514138780 290861 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :int-e: It's a cute game and also on sale < 1514138794 161543 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Starts off a bit slowly but there are some fun levels. < 1514139008 581409 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :int-e: yeah... but it's a big difference whether you say it doesn't exist or whether you say it doesn't have a certain property. < 1514139039 260098 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :you can certainly say that H doesn't have the property of answering correctly for all programs < 1514139043 585643 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :as it inevitably fails on Q. < 1514139076 697972 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :and that's valid. < 1514139107 402614 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :because if H exists then Q can exist and if Q can exist then Q shows that H doesn't have the right properties. < 1514139137 78317 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :thus your proof remains valid. < 1514139252 316977 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :because you can call/embed programs that exist. < 1514139621 430299 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :whatever :D < 1514139633 151059 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :I'm just not accepting spooky exists proofs. < 1514139898 37178 :int-e!~noone@int-e.eu PRIVMSG #esoteric :shachaf: hmm, might be fun < 1514140337 374948 :FreeFull!~freefull@defocus/sausage-lover JOIN :#esoteric < 1514141397 123740 :jaboja!~jaboja@jaboja.pl JOIN :#esoteric < 1514142615 668925 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :the other question is whether the halting problem is only undecidable for programs that invoke H. < 1514142627 154140 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :and very decidable for programs that do not invoke H. < 1514142660 351688 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :if it were only undecidable for for programs invoking H < 1514142673 305802 :Taneb!~Taneb@2001:41c8:51:10d:: PRIVMSG #esoteric :mroman, how do you determine if a program invokes H? < 1514142686 196474 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :No idea. < 1514142687 806715 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but indirectly < 1514142696 649532 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :if you can't tell if the program halts or not it would contain H. < 1514142712 321056 :Taneb!~Taneb@2001:41c8:51:10d:: PRIVMSG #esoteric :I think "invokes H" is either ill-defined or itself undecidable (by Rice's theorem) < 1514142722 727361 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :if the assumption is correct that all undecidable programs invoke H. < 1514142760 610515 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :so far we just know that programs of the form IF H(myself) THEN ... are undecidable. < 1514142780 168847 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :so it might be that we can write an a program that answers _correctly_ with yes/no/undecidable < 1514142801 156767 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :is there a proof that shows that you can't do that either? < 1514142821 875647 :sleffy!~sleffy@c-24-7-67-0.hsd1.ca.comcast.net JOIN :#esoteric < 1514142832 739903 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :trivially as mentioned you can write an H2 that detects a specific Q and respond with undecidable < 1514142848 611753 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :so a program can surely for some instances tell whether the program halts, doesn't or whether it's undecidable. < 1514142863 403383 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :so in specific cases it's decidable whether it's undecidable :D < 1514142881 183741 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :the bigger question is whether it's decidable in the generic case. < 1514142930 144676 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :specifically... < 1514142954 637510 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :the actual question would be whether a program can detect that the termination of another program is dependent on itself. < 1514142978 723549 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :because if H can conclude that the termination of P depends on the output of H < 1514142986 572345 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :then it can answer with undecidable and would do so correctly. < 1514143027 515448 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :which means the sets of programs that halt and don't halt would be well defined < 1514143037 752959 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :and there would be a subset of programs that are undecidable < 1514143041 670557 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :knowingly undecidable < 1514143049 236953 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :because the outcome depends on H itself. < 1514143120 892563 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :trivially for IF H(myself) THEN loop(); ELSE halt(); you can conclude perfectly fine that the outcome depends on H < 1514143149 198028 :Taneb!~Taneb@2001:41c8:51:10d:: PRIVMSG #esoteric :mroman, not if you don't have the program in that form < 1514143154 867897 :Taneb!~Taneb@2001:41c8:51:10d:: PRIVMSG #esoteric :If H is inlined you're lost < 1514143170 175499 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric : is there a proof that shows that you can't do that either? <-- yes, because any undecidable program doesn't halt, so you could trivially turn that program into one that decides halting itself. < 1514143195 739654 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :hu? < 1514143200 956035 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :why do undecidable programs not halt? < 1514143222 51242 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :if it did it would be decidable < 1514143230 687664 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :simply run it until it halts, there's your proof it halts < 1514143246 81587 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :I mean undecidable as in it's decidable that it depends on H < 1514143254 395013 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :as in < 1514143256 700645 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :like < 1514143258 245042 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :uhm. < 1514143261 737492 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :"This sentence is false". < 1514143277 506398 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :I _know_ that this sentence is neither true nor false within this boolean logic. < 1514143328 464759 :jaboja!~jaboja@jaboja.pl QUIT :Ping timeout: 252 seconds < 1514143331 495415 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :so I know that for IF H(Q) then loop(); else halt(); the outcome is depends on H < 1514143364 361854 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :so H could detect that the outcome depends on the answer it gave the first time < 1514143366 884667 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :hypothetically < 1514143374 976078 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :I mean < 1514143380 124134 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :I assume turing machines are as smart as humans < 1514143381 424697 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :kinda < 1514143392 810179 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :humans can tell that this program is a "paradox" < 1514143402 401192 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :(at least as smart) < 1514143452 409081 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :what if H runs the program Q < 1514143462 364663 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :deliberatily answering with a specific "yes" or "no" < 1514143466 654148 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :to cause it to either terminate or not < 1514143473 288821 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :then revising it's answer for the actual output of H. < 1514143478 515040 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :*its < 1514143498 941138 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :mroman: ok i didn't interpret undecidable the same way you do. but like others i'm not sure whether your version is well-defined (although it might be an interesting concept if it is.) < 1514143560 531928 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :oerjan: I mean it as in could an H detect that the halting state of a program depends on H and then answer with a third answer. < 1514143592 303657 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :the problem is that there's almost surely a way to hide H in a program such that H cannot detect it. < 1514143596 894578 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :which I guess boils down to H being able to detect itself in the program it's given? < 1514143606 137843 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :*its < 1514143641 856597 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :for one thing, rice theorem says that it's undecidable whether a program is equivalent to H. < 1514143646 929138 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :*rice's < 1514143719 198381 :h0rsep0wer!~h0rsep0we@unaffiliated/h0rsep0wer QUIT :Quit: Leaving < 1514143777 98488 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :it's like the halting theorem on steroids: you cannot decide _anything_ about a program that is preserved under equivalence. < 1514143849 40014 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :you could do statistical tests though. < 1514143866 147913 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but that's uninteresting. < 1514143901 898154 :moony!~moony@unaffiliated/moonythedwarf QUIT :Remote host closed the connection < 1514143902 400234 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :so < 1514143909 641822 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :if we assume there's H1 and H2 < 1514143918 695808 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :which are semantically identical < 1514143934 268472 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :they both answer yes/no/dependent < 1514143941 488474 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :(let's call it dependent instead of undecidable) < 1514143966 536717 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :then what happens if we feed Q = IF H2(Q) THEN loop(); ELSE halt(); to H1. < 1514144021 797218 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :H1 can detect it's own presence. < 1514144023 856849 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :so < 1514144034 719470 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :inevatibly IF H2(Q) THEN loop(); ELSE halt(); gets fed through H2 < 1514144038 974328 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :and H2 can detect it's own presence < 1514144044 918039 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :so H2 would detect itself in there? < 1514144076 463420 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :so if H1 would just eval this < 1514144084 25713 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :H2 would say dependent < 1514144107 170438 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :well actually we need switch-case now :D < 1514144124 4312 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :since a simple if is just true/false < 1514144161 656990 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :Q = CASE H2(Q) OF TRUE -> loop(); FALSE -> halt(); DEPENDENT -> .... END < 1514144188 247870 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :even if we feed hat to H2 < 1514144196 663761 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :H2 is going to answer DEPENDENT < 1514144207 625400 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :so if we put DEPENDENT -> stops(); in there < 1514144214 378045 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :then DEPENDENT would be wrong. < 1514144219 220009 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :because it stops. < 1514144240 406077 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :thus H2 would get that wrong. < 1514144241 853489 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :meh. < 1514144244 894603 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :game over :D < 1514144297 716830 :int-e!~noone@int-e.eu PRIVMSG #esoteric :H2 doesn't exist. < 1514144375 208431 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I'd say you're overthinking this. You seem to be constantly amazed by the fact that *under a false assumption*, you can prove both a statement and its negation, but in fact this is true for any statement at all. < 1514144442 27850 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but you could loosen it < 1514144452 583974 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :and say H2 just answers whether it's dependent on itself. < 1514144453 685829 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :nothing else. < 1514144468 984703 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :so the program might terminate but H2 will answer dependent < 1514144488 348055 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :so dependent would just mean "dependent on myself". < 1514144578 170920 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :int-e: not in all forms of logic < 1514144597 406173 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :some people in my department have put a lot of effort into logics where (x and not x) does not imply y < 1514144838 868073 :int-e!~noone@int-e.eu PRIVMSG #esoteric :ais523: please let's not go there < 1514144884 173323 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :int-e: my thesis was heavily based round forms of logic where (x and not x) is a syntax error < 1514144914 67274 :sebbu!~sebbu@unaffiliated/sebbu QUIT :Ping timeout: 272 seconds < 1514144914 855283 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I know that there's work on paraconsistent logics and for the time being I'm pretty happy to keep my knowledge of such logics on that level. < 1514144917 843352 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :so I have some experience with weird logics generally < 1514145506 953488 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :`? paraconsistent < 1514145508 220355 :HackEgo!~HackEgo@162.248.166.242 PRIVMSG #esoteric :paraconsistent? ¯\(°​_o)/¯ < 1514145549 713061 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :`le/rn paraconsistent//There has been a lot of work on paraconsistent logics, although there hasn't been a lot of work on them. < 1514145551 723149 :HackEgo!~HackEgo@162.248.166.242 PRIVMSG #esoteric :Learned 'paraconsistent': There has been a lot of work on paraconsistent logics, although there hasn't been a lot of work on them. < 1514146111 929665 :sleffy!~sleffy@c-24-7-67-0.hsd1.ca.comcast.net QUIT :Ping timeout: 248 seconds < 1514146792 398683 :sleffy!~sleffy@c-24-7-67-0.hsd1.ca.comcast.net JOIN :#esoteric < 1514146805 39829 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :nothing follows from a contradiction. < 1514146848 905042 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :(x => y) y might be true if it's independent from x < 1514146850 942789 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :as in < 1514146872 78895 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :9 is even => there are an infinite number of primes < 1514146895 629424 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :it's true that there are an infinite number of primes < 1514146912 743739 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but it's wrong to follow that from the assumption that 9 is even. < 1514146987 560330 :Taneb!~Taneb@2001:41c8:51:10d:: PRIVMSG #esoteric :9 is even => 7 is even < 1514147100 192212 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :if X exists then Y exists. < 1514147109 531372 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :If X doesn't exist you've just proven that Y doesn't exist. < 1514147122 299194 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :That's an acceptable conclusion. < 1514147135 499035 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :if X exists then Y exists. If Y exists then Z exists. < 1514147149 897192 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :If X doesn't exist then Z doesn't exist. < 1514147154 329830 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :That's an invalid conclusion. < 1514147166 188561 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :Z might exist independently < 1514147182 61894 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :if X exists then Y exists. If Y exists then Z exists. If Z exists then X doesn't exist. < 1514147233 928755 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :Z only exists if and only if Y exists and Y only exists if and only if X exist. They might exist independently of course, but you'd have to prove that independently. < 1514147274 575456 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :Since X doesn't exist if Z exists but Z exists if X exists < 1514147319 128016 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :That just can't possibly work. < 1514147364 367603 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :it can work if it follows directly < 1514147422 20364 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :that's like uhm < 1514147463 211122 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :if a > b then c > d if c > d then a < b < 1514147508 523210 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but if a < b then you don't know whether c > d thus you can't know whether a < b < 1514147547 240968 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :you can only show that a < b if you know for certain that c > d < 1514147548 995780 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :but you don't < 1514147559 186317 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :because c > d is only valid if a > b < 1514147586 726006 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :in essence < 1514147593 774696 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :you know nothing about whether a > b or a < b < 1514147646 709878 :jix!~jix@jixco.de QUIT :Quit: leaving < 1514147665 723993 :jix!~jix@jixco.de JOIN :#esoteric < 1514147980 107491 :int-e!~noone@int-e.eu PRIVMSG #esoteric :shachaf: so apparently, the recursion achievement is unlocked by unlocking the recursion achievement. that's good to know. < 1514148274 54058 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :int-e: sounds obvious in hindsight < 1514148406 965039 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :yeah this sounds wrong. < 1514148410 198157 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :i need a better example. < 1514148451 735894 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :the argument doesn't work there. < 1514148465 137604 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :it certainly allows you to conclude that a > b can't be true. < 1514148637 424514 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :if were true then there would exist showing ! < 1514148640 883599 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Not the corecursion achievement? < 1514148643 35857 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :thus isn't true. < 1514148681 894069 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :if exists then there would exist showing does not exist. < 1514148717 260335 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :hm. < 1514148721 135064 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :you guys were right. < 1514148724 116259 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :this is the same thing. < 1514148780 790231 :APic!apic@apic.name PRIVMSG #esoteric :But in any Case, whether anything would exist or not, there still would be the pointed Brackets < 1514148786 710658 :APic!apic@apic.name PRIVMSG #esoteric :Metadata > Data < 1514148823 798133 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :it just sounds weird < 1514148831 369341 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :because the word exists makes my brain jump to physical things < 1514148841 325947 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :and it's hard to convince your brain about hypothetical physical things that do not exist < 1514148859 351230 :APic!apic@apic.name PRIVMSG #esoteric :Brains are physical, but Spirit is not necessarily < 1514148879 265572 :APic!apic@apic.name PRIVMSG #esoteric :Also, You have an infinite Number of Heads < 1514148933 272641 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :the existence of H would prove its own inexistence. < 1514148949 721135 :APic!apic@apic.name PRIVMSG #esoteric :This is proven in Robert Anton Wilson's „Quantum Psychology“ < 1514148973 289540 :APic!apic@apic.name PRIVMSG #esoteric :But i got two different Instances of the Book, and both disappeared < 1514148993 154141 :APic!apic@apic.name PRIVMSG #esoteric :Then last Year i tried to order one additional Copy as a Gift for my Sister < 1514148999 257544 :APic!apic@apic.name PRIVMSG #esoteric :It did not arrive < 1514149012 354158 :APic!apic@apic.name PRIVMSG #esoteric :So maybe we actually all have zero Heads ☺ < 1514149075 755828 :APic!apic@apic.name PRIVMSG #esoteric :https://xkcd.com/1782/ < 1514149282 731325 :erkin!~erkin@unaffiliated/erkin JOIN :#esoteric < 1514149770 466449 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :well < 1514149774 677475 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :it's still better than slack. < 1514149814 58520 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :you can't be in multiple teams in the same tab in slack < 1514149815 362198 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 PRIVMSG #esoteric :that's weak < 1514149843 242039 :mroman!b2c5e91e@gateway/web/freenode/ip.178.197.233.30 QUIT :Quit: well good night anyway < 1514149990 518467 :ais523!~ais523@unaffiliated/ais523 QUIT :Quit: quit < 1514150188 496394 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric : But i got two different Instances of the Book, and both disappeared <-- that sounds like a non-unitary evolution to me, are you sure it's quantum? < 1514150554 167225 :int-e!~noone@int-e.eu PRIVMSG #esoteric :oerjan: it was a way of telling shachaf that I've obtained a copy of "Recursed". < 1514150700 738713 :FreeFull!~freefull@defocus/sausage-lover QUIT :Read error: Connection reset by peer < 1514151840 165708 :oerjan!~oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :. o O ( curses, foiled again ) < 1514152359 70904 :ais523!~ais523@unaffiliated/ais523 JOIN :#esoteric < 1514152387 298745 :FreeFull!~freefull@defocus/sausage-lover JOIN :#esoteric < 1514152864 57960 :sebbu!~sebbu@unaffiliated/sebbu JOIN :#esoteric < 1514153109 921155 :erkin!~erkin@unaffiliated/erkin QUIT :Quit: Ouch! Got SIGABRT, dying... < 1514154031 675690 :jaboja!~jaboja@jaboja.pl JOIN :#esoteric < 1514154583 925091 :h0rsep0wer!~h0rsep0we@unaffiliated/h0rsep0wer JOIN :#esoteric < 1514154733 357150 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :int-e: Did you get the achievement? < 1514154769 48631 :int-e!~noone@int-e.eu PRIVMSG #esoteric :well, yes. < 1514155966 209491 :variable!~variable@freebsd/developer/variable QUIT :Quit: Found 1 in /dev/zero < 1514157834 102424 :ais523!~ais523@unaffiliated/ais523 QUIT :Ping timeout: 272 seconds < 1514158354 440849 :h0rsep0wer!~h0rsep0we@unaffiliated/h0rsep0wer QUIT :Remote host closed the connection < 1514158932 33441 :h0rsep0wer!~h0rsep0we@unaffiliated/h0rsep0wer JOIN :#esoteric < 1514158984 403707 :h0rsep0wer!~h0rsep0we@unaffiliated/h0rsep0wer QUIT :Remote host closed the connection < 1514159344 501490 :h0rsep0wer!~h0rsep0we@unaffiliated/h0rsep0wer JOIN :#esoteric < 1514159396 389059 :h0rsep0wer!~h0rsep0we@unaffiliated/h0rsep0wer QUIT :Client Quit < 1514159425 452829 :sleffy!~sleffy@c-24-7-67-0.hsd1.ca.comcast.net QUIT :Ping timeout: 248 seconds < 1514159591 732313 :h0rsep0wer!~h0rsep0we@unaffiliated/h0rsep0wer JOIN :#esoteric < 1514159682 334711 :h0rsep0wer!~h0rsep0we@unaffiliated/h0rsep0wer QUIT :Remote host closed the connection < 1514159706 238054 :h0rsep0wer!~h0rsep0we@unaffiliated/h0rsep0wer JOIN :#esoteric < 1514159772 368571 :h0rsep0wer!~h0rsep0we@unaffiliated/h0rsep0wer QUIT :Remote host closed the connection < 1514159795 245876 :h0rsep0wer!~h0rsep0we@unaffiliated/h0rsep0wer JOIN :#esoteric < 1514159862 323170 :h0rsep0wer!~h0rsep0we@unaffiliated/h0rsep0wer QUIT :Remote host closed the connection