< 1269734401 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oerjan, yeah one of the excercise was: solve the following equation x^2+1 < 1269734406 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :Although those are more useful for stream ciphers than actual hashes. I'm sure their proofs of security are only for a finite amount of output before they hit a cycle or something. < 1269734410 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :fax, BWUH? < 1269734411 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :that's not an equation < 1269734416 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oops < 1269734417 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :=0 < 1269734418 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: is your definition of "one of the atheist people" "someone who doesn't believe in god" < 1269734426 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :nice smiley :D < 1269734430 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :ACTION is an atheist person. < 1269734433 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :fax: (set it equal to 0 and tell him he's lame) < 1269734459 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :do you believe in angels? < 1269734466 0 :rapido!unknown@unknown.invalid PRIVMSG #esoteric :dixon: uuuh - i need to study your reference to sponge constructions < 1269734472 0 :zzo38!~zzo38@h24-207-48-53.dlt.dccnet.com JOIN :#esoteric < 1269734481 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :of course, and I beleive in paralell lines too < 1269734483 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :fax: adding roots of polynomials in that way is a fundamental tool of galois theory iirc < 1269734489 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :ACTION does not believe in anything that would commonly be considered to be supernatural. < 1269734491 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :hi zzo73 < 1269734501 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :rapido: http://sponge.noekeon.org/ < 1269734509 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oerjan, hm < 1269734509 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :http://sponge.noekeon.org/SpongeFunctions.pdf < 1269734510 0 :rapido!unknown@unknown.invalid PRIVMSG #esoteric :i could believe in god and still find the concept of god to be impossible < 1269734514 0 :rapido!unknown@unknown.invalid PRIVMSG #esoteric :such is believe < 1269734539 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :although if you are inside the complex numbers to start with, you don't really need to go outside them < 1269734549 0 :rapido!unknown@unknown.invalid PRIVMSG #esoteric :dixan: ah, thanks! < 1269734561 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :rapido: They're cryptographic hashes, however. < 1269734583 0 :rapido!unknown@unknown.invalid PRIVMSG #esoteric :dixon: cryptographic hashes are the only ones i'm considering < 1269734615 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :what if you believe in angels but don't believe in god? < 1269734628 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :ACTION pokes alise  < 1269734644 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :rapido: But yes, by definition they're surjective when useful and thus have collisions. < 1269734659 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo what abou gravity < 1269734663 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :it's supernatural < 1269734664 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :lament: Then you must've seen my girlfriend. < 1269734666 0 :rapido!unknown@unknown.invalid PRIVMSG #esoteric :lament: then you would be a flying lunatic with wings < 1269734670 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo_: hi < 1269734684 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :fax, lolwhat? < 1269734690 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :ACTION blinks a few times < 1269734694 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :nobody has explained it yet < 1269734705 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :it's like ghosts or ufos or whatever < 1269734725 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :fax: gravity is a scam by scientists. intelligent falling is the truth! < 1269734739 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :It exists, as demonstratably as possible. < 1269734757 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :it's God's Hand Pushing us Down From Eden < 1269734760 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :well intelligent falling is a much better explanation by occams razor but it does leave some key questions open < 1269734761 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :Ghosts and UFOs have not been observed by any measurements. < 1269734773 0 :rapido!unknown@unknown.invalid PRIVMSG #esoteric :dixon: all that i want is a naming service that is scalable < 1269734788 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :rapido, let the name of the proof be the content of the proof. < 1269734791 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :Oranjer: no that would be more the coriolis force. eden is in the east, iirc < 1269734797 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo - oh that's true I guess < 1269734803 0 :zzo38!unknown@unknown.invalid PRIVMSG #esoteric :What doe sthat mean, intelligent falling?? < 1269734806 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :fax, it is not a better explanation by occams razor < 1269734816 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :"Playing with Coq in Jack" -- paper title < 1269734820 0 :zzo38!unknown@unknown.invalid PRIVMSG #esoteric :The reason otyugh attack with only two tentacles is because one tentacle has three eyes. < 1269734820 0 :rapido!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo_: but proofs can be huge - think of computer generated proofs < 1269734822 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :occams razor refers to the amount of assumptions an explanation requires < 1269734832 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :zzo38: intelligent falling is the demonstratable fact that gravity is a lie and all things are actually being pushed down by god individually < 1269734844 0 :zzo38!unknown@unknown.invalid PRIVMSG #esoteric :alise: That cannot be demonstratable < 1269734845 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise... how you have possibly managed to find a coq paper I haven't read O_O < 1269734858 0 :zzo38!unknown@unknown.invalid PRIVMSG #esoteric :Mostly because it doesn't work. < 1269734886 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :zzo38: http://en.wikipedia.org/wiki/Intelligent_falling < 1269734888 0 :zzo38!unknown@unknown.invalid PRIVMSG #esoteric :If you want to say God invented gravity, that's different however. Still not provable, though < 1269734899 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :falsifiable < 1269734904 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :I get the feeling that I should learn Coq < 1269734908 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :Using bigger words make you sound smarter. < 1269734911 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: googling for unrelated things < 1269734920 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :zzo38: IT WORKS!!!! < 1269734926 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :now how do I do nested theorems in coq < 1269734933 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :See, we don't fall off the earth! < 1269734943 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo_: I wouldn't bother. You'd be in the same boat as the Haskellingtons masturbating to the Curry-Howard isomorphism. < 1269734953 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :ACTION knows a bit of Haskell < 1269734964 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :HEY LOOK GUYS I CAN PRETEND I'M A MATHEMATICIAN BECAUSE I CAN WRITE PROOFS IN COQ fapfapfapfapfap etc < 1269734971 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :ACTION should probably learn what the Curry-Howard isomorphism < 1269734973 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :*is < 1269734981 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo it's nothing very deep < 1269734986 0 :zzo38!unknown@unknown.invalid PRIVMSG #esoteric :alise: What I mean is the proof desn't work. < 1269734992 0 :zzo38!unknown@unknown.invalid PRIVMSG #esoteric :s/desn't/doesn't/ < 1269734993 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo -- just a notationally similarity between proof systems and type systems < 1269734999 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :notational < 1269735003 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ACTION has _never_ masturbated to the curry-howard isomorphism. should i try it? < 1269735014 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo_: It says if you can make a type to represent a theorem and then find a value that satisfies the type, you prove the theorem. < 1269735020 0 :rapido!unknown@unknown.invalid PRIVMSG #esoteric :look.... the coq has giving me sign - it's hanging low - it's time to go to bed.... later ... < 1269735040 0 :rapido!unknown@unknown.invalid QUIT :Quit: rapido < 1269735306 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise: on facebook: Jack Coq Hardi < 1269735306 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :Jack Coq Hardi < 1269735307 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :Not the Jack Coq Hardi you were looking for? Search more » < 1269735347 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Jacking off Coqs in Jack < 1269735380 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :guh, constructing a sigma is a bitch in a coq proof < 1269735403 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :the coq sigma stigma < 1269735406 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :a sigma algebra? < 1269735420 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise just give the value and prove it correct using tactics < 1269735432 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :yeah but I want to give the value using proof syntax < 1269735440 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :a sigma algebra? < 1269735448 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so I put it in another top-level theorem, which is a bitch. and then I have to do it all separately in another theorem < 1269735450 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :and it's all fffffffffff < 1269735460 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :dixon: unlikely. < 1269735473 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :He couldn't have meant a series? < 1269735478 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :not that i'm _sure_ alise doesn't know what that is, but... < 1269735527 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :well, for one thing alise only does constructivist things, i doubt sigma algebras qualify < 1269735561 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :you know constructivism isn't some crazy fringe philosophy :) < 1269735569 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :yes it is :P < 1269735570 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :Yes it is. < 1269735585 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :And it's a boring one, because it's shit that's been done since the 1800's. < 1269735660 0 :jcp!~jw@bzflag/contributor/javawizard2539 JOIN :#esoteric < 1269735695 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :dixon: but it's very useful for masturbating to the curry-howard isomorphism, i hear < 1269735707 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ACTION ducks < 1269735724 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :I lol'd < 1269735786 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :Next all he has to say is he's a finitist < 1269735793 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :It may be boring and old but who cares? < 1269735801 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :ACTION masturbates to finite sequences < 1269735804 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :dixon: fax is a finitist < 1269735804 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric ::P < 1269735806 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so... < 1269735813 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :you're looking at the wrong person I'm very much a believer in infinities < 1269735835 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :Yeah, but I already think fax is an idiot. < 1269735848 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :Yay! Infinities. < 1269735857 0 :Quadrescence!~quad@unaffiliated/quadrescence JOIN :#esoteric < 1269735862 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :now where did you get THAT idea? < 1269735904 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :Mainly your berating me for not knowing anything 15 minutes after you claimed the exponential function wasn't hypergeometric. < 1269735949 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oh fuck off < 1269735964 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :it was long before that < 1269736015 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :Granted being a constructivist and finitist would've just made me think you were a Zeilberger clone, and then I'd have to decide if you were thinking for yourself (in which case you would've been cool) or if you were just a copycat (in which case you would be an idiot). < 1269736043 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric ::3 < 1269736049 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Perhaps we are using different definitions of constructivist. < 1269736073 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I merely believe that an object must be constructed in some formal language to be proved to exist; or in the case of a proposition, a demonstration of it. < 1269736074 0 :zzo38!unknown@unknown.invalid PRIVMSG #esoteric :Looking at the page I found a lot of other things and links to pages about quantum mechanics, and so on. I have a lot of my own ideas about quantum mechanics, some of which are different from other ones. (But some ideas are similar, and have been figured out independently by me but other people generally figure it out more in the past, because they are scientists and I'm not) < 1269736083 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :So basically I reject the law of the excluded middle and correspondingly ~~p -> p. < 1269736086 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :That isn't really so crazy. < 1269736182 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :dixon I wasn't berating you for not knowing anything anyway, you were making some ridiculoulsy stretched joke about 'dixons identity' < 1269736314 0 :zzo38!unknown@unknown.invalid PRIVMSG #esoteric :I also reject the law of excluded middle but only in some contexts. You can use tristate logic with quantum superposition/entanglement and with presuppose (so for some proposition P you could make Pre(P)) and a new kind of imply operator, distinct from the old one (but both of which are used, for different purposes). < 1269736352 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :zzo38 have you read any linear logic? < 1269736378 0 :zzo38!unknown@unknown.invalid PRIVMSG #esoteric :There are then three truth values instead of two values. The standard operators still act in the standard way when dealing with only standard truth values. < 1269736389 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :zzo38: I reject the law of the excluded middle because I believe that axioms not in the current system that nevertheless are fine to add are neither true nor false. < 1269736399 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :You cannot prove them true, you cannot prove them false; it is fine to add their negation, it is fine to add them. < 1269736418 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :So if you could say it is true, then the negation would be inconsistent, and vice-versa, yet this is not the case. < 1269736433 0 :zzo38!unknown@unknown.invalid PRIVMSG #esoteric :alise: There certainly can be things that are neither true nor false. < 1269736464 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :moral dilemma: I followed a link allegedly to Rick Astley rickrolling someone himself < 1269736469 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and it was actually what it claimed to be, rather than a rickroll < 1269736474 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :alise: Is'nt the law of the excluded middle about statements that can be derived from the axiomatic system in question? < 1269736474 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :have I been meta-rickrolled? < 1269736476 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :wow I want to see it! < 1269736497 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :http://www.youtube.com/watch?v=y4hqv6USkoU < 1269736502 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: It says that for any given proposition P, I will tell you that either P is true, or P is not true. < 1269736505 0 :zzo38!unknown@unknown.invalid PRIVMSG #esoteric :Meta-rickrolled? < 1269736505 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :basically, it was a Thanksgiving Day's parade < 1269736510 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :alise: Ah. < 1269736512 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Okay, then. < 1269736514 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and he was hiding on one of the floats, and just came out and started singing live < 1269736521 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :However, there are things that are neither. < 1269736528 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :So the law of the excluded middle is fail. < 1269736552 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :alise: Tell me one such proposition? < 1269736573 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: Consider the Continuum Hypothesis. < 1269736576 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise: would you say that if X implies Y, and not X implies Y, then Y can be considered to be true? < 1269736578 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ZFC + CH is consistent, as is ZFC + ~CH. < 1269736581 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ais weird lol < 1269736585 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :IMO, that's a weaker situation than the law of the excluded middle < 1269736590 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I don't think it's a rickroll < 1269736594 0 :zzo38!unknown@unknown.invalid PRIVMSG #esoteric :With tristate logic things can be true, false, or tristate. Pre(P) is true if P is not tristate. < 1269736598 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: p \/ q = (p -> r) -> (q -> r) -> r < 1269736604 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :fax: well, it did /say/ it was a rickroll at the end < 1269736617 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oh < 1269736617 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :perhaps this is some sort of meta-meta-rickroll < 1269736618 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :p \/ ~p = (p -> r) -> (~p -> r) -> r < 1269736623 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Answer: No. < 1269736627 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oh it is a rickroll < 1269736631 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise: the law of the excluded middle implies that < 1269736637 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: So, then, how, in plain ZFC, is CH true or false? < 1269736639 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :but, I think it can be true even without < 1269736644 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: no, p or q is literally the same thing < 1269736648 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :as (p->r)->(q->r)->r < 1269736655 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :proof: < 1269736682 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :\f g porq. case porq of theone x -> f x; theother x -> g x < 1269736682 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :and < 1269736685 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :erm < 1269736690 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :\porq f g. case porq of theone x -> f x; theother x -> g x < 1269736699 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :that's p\/q -> (p->r)->(q->r)->r < 1269736703 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :now the other way: < 1269736711 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :the other way is the way I care about < 1269736727 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(p->r)->(q->r) -> p \/ q < 1269736747 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :\f. f theone theother < 1269736757 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :filling in the arguments we get < 1269736762 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :first is (p -> p \/ anything) < 1269736762 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise: you must have typoed somewhere < 1269736768 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :alise: you are missing -> r < 1269736768 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :second is (q -> anything \/ q) < 1269736774 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :right right < 1269736777 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :the implementation is right < 1269736778 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so < 1269736782 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fill in p and q for the respective anythings < 1269736784 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :and we get p \/ q < 1269736787 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Q.E.D. < 1269736809 0 :zzo38!unknown@unknown.invalid PRIVMSG #esoteric :If there is no present king of France, the statement "The present king of France has stopped robbing banks" cannot be true or false, because it presupposes that there is a king of France. < 1269736813 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :alise: Clearly, the veracity of CH is a boolean. < 1269736815 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hmm, I always get confused trying to follow nonstandard models of logic < 1269736833 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :That the value of the boolean cannot be determined is beside the point. < 1269736836 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :in one seminar I went to, someone quantified over all systems of logic, which was /really/ confusing < 1269736840 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Prelude> let or2f porq f g = case porq of Left x -> f x; Right x -> g x < 1269736840 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Prelude> let f2or f = f Left Right < 1269736840 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Prelude> :t (or2f, f2or) < 1269736840 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(or2f, f2or) < 1269736840 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : :: (Either t t1 -> (t -> t2) -> (t1 -> t2) -> t2, < 1269736841 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : ((a -> Either a b) -> (b1 -> Either a1 b1) -> t11) -> t11) < 1269736844 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :alise: you had an implied forall r in there < 1269736851 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Since I have proved that (P->Q) and (Q->P), P is equivalent to Q. < 1269736854 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: booleans have /nine/ values, 01XLHWZU- < 1269736858 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise: ok < 1269736871 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Well, f2or actually needs a more specific type, but. < 1269736880 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ANY LANGUAGE IN WHICH BOOLEANS HAVE FEWER THAN NINE POSSIBLE VALUES IS DEFICIENT < 1269736883 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Then we are clearly discussing the law of the excluded 10th. < 1269736885 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :btw, I'm not sure which one maps to file_not_found < 1269736888 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: haha < 1269736898 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : alise: Clearly, the veracity of CH is a boolean. < 1269736899 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Really? < 1269736901 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :((p->(p\/q))->(q->(p\/q))->(p\/q)) -> (p\/q) < 1269736903 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :fax: have you decided whether that was a rickroll or not yet? < 1269736919 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: ZFC + CH is consistent iff ZFC is consistent. ZFC + ~CH is consistent iff ZFC is consistent. < 1269736928 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :In ZFC, CH can neither be true nor false. < 1269736938 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :If we can prove it true, then ZFC + ~CH would be inconsistent. < 1269736943 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :If we can prove it false, then ZFC + CH would be inconsistent. < 1269736945 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :In ZFC, CH cannot be shown to be true or false. < 1269736948 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I think I've caused a logical gap in rickrollness < 1269736949 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :It is neither true nor false. < 1269736958 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: But it has some platonic "real truth"? < 1269736969 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :That's metaphysical mumbojumbo: you are talking about things in the system that are not from the axioms. < 1269736969 0 :BeholdMyGlory!unknown@unknown.invalid QUIT :Remote host closed the connection < 1269736973 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ais523, I am not really sure < 1269736981 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :You are referring to some platonic space of "ZFC truths" but no such thing exists, just manipulation of the axioms. < 1269736986 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Are you sure you want to go down this path> < 1269736990 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :fax: hmm, so you're metaundecided? < 1269736991 0 :zzo38!unknown@unknown.invalid PRIVMSG #esoteric :Please explain what the nine boolean values 01XLHWZU- are meant for. < 1269737037 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :zzo38: 0 = false, 1 = true, X = both false and true, L = false unless contradicted, H = true unless contradicted, W = somewhere between true and false, Z = no truth value at all, U = as yet unknown, - = irrelevant < 1269737047 0 :zzo38!unknown@unknown.invalid PRIVMSG #esoteric :OK. < 1269737059 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :VHDL actually implements all these < 1269737061 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :yes < 1269737078 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :*path? < 1269737105 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :alise: It certainly has no "platonic real truth". It just simply can be said to be one of true or false. < 1269737135 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: Okay. < 1269737138 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :So suppose it is true. < 1269737144 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Then ZFC + ~CH is inconsistent. < 1269737147 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :So suppose it is false. < 1269737150 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Then ZFC + CH is inconsistent. < 1269737158 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :But we know that ZFC plus either CH or ~CH is consistent iff ZFC is. < 1269737160 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :So it cannot be both true and false. < 1269737164 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :No. < 1269737166 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :It cannot be either. < 1269737172 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Because *both systems are consistent*. < 1269737173 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :How so? < 1269737174 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(if ZFC is). < 1269737187 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: OK, let us say that in ZFC, we have proved CH. < 1269737194 0 :zzo38!unknown@unknown.invalid PRIVMSG #esoteric :I didn't know VHDL implements those. But I suppose it is possible. < 1269737201 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :We know that ZFC + ~CH is consistent iff ZFC is. Yet we have CH and ~CH. < 1269737214 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Reverse it to see that it cannot be false, either. < 1269737226 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :You can keep running around in circles, but the only real solution is to reject the excluded middle. < 1269737246 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :alise: "We know that ZFC + ~CH is consistent iff ZFC is. Yet we have CH and ~CH." Uh... Wha? < 1269737258 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :OK, let me spell it out for you. < 1269737272 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Near as I can tell, "proving CH in ZFC" would imply that ZFC + ~CH is inconsistent. < 1269737303 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :And assuming the proof that ZFC + ~CH is consistent is valid, then clearly you cannot prove CH in ZFC. < 1269737334 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :and if you did both, then it would show ZFC is not consistent. < 1269737343 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :dixon: Yes. < 1269737343 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :because that's a contradiction < 1269737355 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: < 1269737356 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :By the law of the excluded middle, we know that in ZFC, either CH is true or ~CH is true. I will demonstrate that it cannot be either. < 1269737358 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Let us assume that CH is true. It has been proved at the meta-level that ZFC + ~CH is consistent iff ZFC is. Since we are working in ZFC, we assume its consistency. But then ZFC + ~CH cannot be consistent, for we have CH and ~CH. But ZFC + ~CH has been proved to be consistent. Contradiction; CH cannot be true. < 1269737358 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Let us assume that CH is false. It has been proved at the meta-level that ZFC + CH is consistent iff ZFC is. Since we are working in ZFC, we assume its consistency. But then ZFC + CH cannot be consistent, for we have CH and ~CH. But ZFC + CH has been proved to be consistent. Contradiction; CH cannot be false. < 1269737365 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Therefore, CH cannot be true and it cannot be false. < 1269737384 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :alise: You have proven that CH cannot be proven in ZFC. < 1269737384 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Although we cannot use this to disprove excluded middle from inside ZFC, because it is a meta issue, it is still present. < 1269737388 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Excluded middle is false. < 1269737393 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: No, I made no references to proofs in the above. < 1269737397 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Clearly it can be one or the other; you can use it as an axiom. < 1269737401 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :The law of the excluded middle means that ONE must be true. < 1269737419 0 :Quadrescence!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1269737421 0 :Quadresce`!~quad@unaffiliated/quadrescence JOIN :#esoteric < 1269737444 0 :Quadresce`!unknown@unknown.invalid NICK :Quadrescence < 1269737485 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :And you use ZFC's consistency as an axiom. Again, if you prove ZFC + ~CH and ZFC + CH iff ZFC is consistent, it means ZFC is not consistent. Hello mathematical logic. < 1269737499 0 :zzo38!unknown@unknown.invalid PRIVMSG #esoteric :Is "false unless contradicted" in a digital circuit like a pull-down resistor? < 1269737521 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :alise: Fine. I shall start using a form of limited law of excluded middle. "Any proposition which can be reasoned about in an axiomatic system must be either true or false in that axiomatic system." < 1269737525 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric ::P < 1269737640 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :If ~CH in ZFC, how do you get CH? < 1269737645 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :erm < 1269737663 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :n/m, I agree with pikhq < 1269737693 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Well, this has taught me something: Never bother trying to talk about excluded middle. < 1269737703 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :People are absolutely sure it is true at any cost. < 1269737752 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :People don't like the implication that you could define the following: ZFC + CH & ~CH. :P < 1269737873 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :Without realizing that proving both at the same time shows ZFC's inconsistency. < 1269738146 0 :zzo38!unknown@unknown.invalid PRIVMSG #esoteric :Off topic: Have you ever invented any spell/power for D&D game? < 1269738159 0 :FireFly!unknown@unknown.invalid QUIT :Quit: Leaving < 1269738188 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :dixon: Of course it does. < 1269738264 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :Then it says nothing about CH... < 1269738289 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :And your whole law of the excluded middle being false idea is inane with that example. < 1269738319 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :"alise: For one, you can have RAM with so much error checking that it is physically impossible for it not to detect an error for the computation you are doing..." <<< may i see this article < 1269738386 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: wut < 1269738403 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :imagine filling the entire universe with one 16 bit pattern, say < 1269738424 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I'd be highly surprised if it was physically possible for all those bits to spontaneously flip in the certain maximum time it takes to do a given computation < 1269738507 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :1. you would probably be pretty surprised if you suddenly turned into an elephant, too, that's not what physically impossible means < 1269738510 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :2. oh, you linked it < 1269738576 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :well i guess i could start enumerating every single way a bit could be flipped :))) < 1269738888 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :it's pretty stupid to claim computers can't make errors < 1269738890 0 :zzo38!unknown@unknown.invalid PRIVMSG #esoteric :It is difficult to repair a watch while falling from an airplane. < 1269738909 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :of course they can make errors < 1269738935 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :some unicorns can turn bits with their tongues from miles away < 1269738939 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I never claimed that < 1269738958 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :but if you thought that was true, you might < 1269738969 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :can't really unclaim that one huh < 1269738973 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i should go to sleep < 1269739057 0 :zzo38!unknown@unknown.invalid PRIVMSG #esoteric :I recently added something to esolang wiki < 1269739349 0 :zzo38!unknown@unknown.invalid QUIT :Quit: ERR_QUIT < 1269743582 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :err bye < 1269743678 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :bye < 1269743687 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :wait what < 1269743716 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :02:22… zzo38 has quit IRC (Quit: ERR_QUIT) < 1269743716 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :04:32… oklopol: err bye < 1269743734 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :it was all sorts of funny stuff < 1269743757 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :but i actually am going to sleep now -> < 1269743796 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oklopol :) < 1269743809 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I have an idea about this OR thing < 1269743815 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :but it's probably wrong < 1269743819 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I'll try it out tommorow < 1269743843 0 :oerjan!unknown@unknown.invalid QUIT :Quit: Tomorrow OR not tomorrow, that's the question < 1269744409 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :[["Anime is a prime example of why two nukes wasn’t enough." - NH Democrat State Rep., Nick Levasseur]] < 1269744411 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Oh, America. < 1269744457 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :ACTION .. doesn't like nor dislike anime < 1269744477 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :That's rather orthogonal to the hilarious extremity of bad taste found in that quote :P < 1269744478 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :It's just another medium, albeit one for which there's a .. website that lets me watch for free < 1269745047 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :It's just another medium, albeit one which is generally made in a language that I happen to be studying. :P < 1269745102 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :ANATA WA BAKA DESU ZO < 1269745127 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :dixon: you violated the syntax anime := desu | anime anime < 1269745131 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :dixon: That's quite formal of you. < 1269745134 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :do not pass go do not collect 200 pounds < 1269745165 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :Why would I collect pounds? I'm an American, we're fat enough. < 1269745181 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: thanx. < 1269745184 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Try something more like 馬鹿ãœã€ã‚ã‚“ãŸï¼(baka ze, anta < 1269745186 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :) < 1269745218 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :Really? I was going for the "You sir, are an idiot!" meme. < 1269745249 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Oh, *that's* what you were going for? < 1269745307 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :My Japanese is flaky, but yes. < 1269745378 0 :adu!~ajr@pool-74-96-89-29.washdc.fios.verizon.net JOIN :#esoteric < 1269745384 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: Please translate this to exquisitely formal Japanese: "Your asshole is a skyscraper-sized orifice which receives bread daily, fuckwit." < 1269745406 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Someone has to have translated that already, it being such a common insult. < 1269745410 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Is that even an insult? I can't tell. < 1269745420 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :SL? < 1269745456 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :Whoa, he gets free bread? < 1269745460 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Try more of Pikhqã©ã®ã¯ãŠé¦¬é¹¿ã§å¾¡åº§ã‚‹ã¨ãŠæ€ã„ã«ãªã‚Šã¾ã™ã€‚(Pikhq dono wa baka de gozaru to o-omoi ni narimasu) < 1269745467 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :... I *think*. My keigo sucks. < 1269745487 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :dixon: NO COST AT ALL < 1269745508 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :alise, is that a quote from SL? < 1269745515 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo_: Schawhat? < 1269745518 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Have you heard it before or something? XD < 1269745535 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :No, but it sounds like the sort of thing a certain character might say < 1269745542 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :alise: Sadly, I know not the vocab for that. < 1269745548 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :I'm not saying the full name of it in the presence of a minor < 1269745553 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :alise: I shall let you know when I can translate that, though. < 1269745564 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo_: Does it have RUDE WORDS in it???? < 1269745572 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :It has naked people and sex in it < 1269745577 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :OH NOOOOOOOOOOOOOOOO < 1269745602 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :My beacon-of-light emitting orifices will all be brutally penetrated by its hostile influence of filth and putridness, such that I may never lay claim to someone of sound mind again. < 1269745608 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Anyway, since when do I have Second Life installed? < 1269745616 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :alise, SL != Second Life in this case < 1269745632 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Oh, that webcomic. < 1269745637 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :Yes >.> < 1269745727 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: Okay, translate this too when you can: "My beacon-of-light emitting orifices will all be brutally penetrated by its hostile influence of filth and putridness, such that I may never lay claim to someone of sound mind again." :P < 1269745738 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Again, FORMAL AND POLITE! < 1269745785 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :alise: "Fuck You". < 1269745797 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :"No" < 1269745970 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Fine, I'll give you a shockingly rude statement instead. ç§ã¯æ—¥æœ¬äººé”を殺ã—ãŸã„。ãªãœï¼Ÿã‚¢ã‚¸ã‚¢äººãŒå¤§å«Œã„ï¼ < 1269746021 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :That is probably the most racist thing I have ever typed, in jest or otherwise. < 1269746038 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :Translate it! Translate IT! < 1269746075 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :"I want to kill all Japanese. Why? I hate Asians!" Now, alise. Say it to every Japanese person you meet. :P < 1269746108 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :(watashi wa nihonjintachi wo korositai. naze? ajiajin ga daikirai!), BTW < 1269746150 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Fags should die, naturally: we should have killed them all at the start. But niggers, niggers are the worst. We should relegate all the niggers to their own country so we can bomb the place. Put the asians there too, the fucking worthless pieces of shit. But the only thing worse than a nigger is a nigger fag. < 1269746156 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :RACISM CONTEST < 1269746182 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :"Nigger" is untranslatable. < 1269746193 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :>:| < 1269746200 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :why not, do all japs love nigs or sth < 1269746214 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :It is a term that literally only exists in English. < 1269746245 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :The closest you can get in Japanese is "gaijin". Which... Refers to everyone other than Japanese. < 1269746262 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :I have a friend who ran in a marathon! < 1269746285 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Is he a nigger?! < 1269746386 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :"Rincewind had always been happy to think of himself as a racist. The One Hundred Meters, the Mile, the Marathon -- he'd run them all." < 1269746401 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :hehe < 1269746404 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I GET IT!! < 1269746405 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :groan < 1269746747 0 :adu!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: å›ã¯æ—¥æœ¬äººã§ã™ã‹ï¼Ÿ < 1269746777 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :adu: ã„ã„ãˆã€‚僕ã¯æ—¥æœ¬èªžã‚’勉強ã™ã‚‹äººã§ã™ã€‚ < 1269746830 0 :adu!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: ã‚ã€ã‚ã‹ãŸ < 1269746892 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :今漢字を勉強ã—ã¦ã¾ã™ã€‚1810字を知ã£ã¦ã€232字を勉強ã™ã‚‹ã¤ã‚‚ã‚Šã§ã™ã€‚ < 1269746911 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :ã¡ã‚‡ã£ã¨é›£ã—ã„ã§ã™ã€‚ã§ã‚‚ã€é¢ç™½ã„ã¨æ€ã„ã¾ã™ã€‚ < 1269746932 0 :adu!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: 僕も日本人ãŒå¤§å«Œã„ < 1269746960 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :ãªã‚‹ã»ã©ã€‚w < 1269746985 0 :adu!unknown@unknown.invalid PRIVMSG #esoteric :ãœã‚“ãœã‚“ < 1269747017 0 :adu!unknown@unknown.invalid PRIVMSG #esoteric :jk < 1269747039 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :分ã‹ã£ãŸã€‚^_^ < 1269747117 0 :adu!unknown@unknown.invalid PRIVMSG #esoteric :僕ã¯ï¼–å¹´ã‹ã‚“日本ã«ã™ã‚“ã§ã„ã¾ã—ãŸã€‚ < 1269747163 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :ã‚〜。 < 1269747187 0 :adu!unknown@unknown.invalid PRIVMSG #esoteric :ã§ã‚‚ã€ãŸãã•ã‚“ã‚ã™ã‚ŒãŸ < 1269747220 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :desu < 1269747225 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :desuuuuu < 1269747231 0 :adu!unknown@unknown.invalid PRIVMSG #esoteric :lol < 1269747246 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :4年間高校ã§æ—¥æœ¬èªžã‚’勉強ã—ã¾ã—ãŸã€‚ã“ã®å¾Œã€ï¼’年間勉強ã—ãªãã¦ã€ã„ã¾ã‚‚ã£ã¨å‹‰å¼·ã‚’始ã‚ã¦ã¾ã™ã€‚ < 1269747267 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :s/ã„ã¾/今/ < 1269747334 0 :adu!unknown@unknown.invalid PRIVMSG #esoteric :ãã§ã™ã‹ï¼Ÿã™ã”ã„ï¼ãŒã‚“ã°ã£ã¦ã­ < 1269747367 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :ã©ã†ã‚‚ã‚ã‚ŠãŒã¨ã†ã”ã–ã„ã¾ã™ã€‚ < 1269747374 0 :adu!unknown@unknown.invalid PRIVMSG #esoteric :lol i've never seen sed and japanese used together < 1269747383 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :w < 1269747435 0 :adu!unknown@unknown.invalid PRIVMSG #esoteric :ã©ã‚‚ã‚ã‚ŠãŒã¨ Mr. ロボト < 1269747456 0 :adu!unknown@unknown.invalid PRIVMSG #esoteric ::) < 1269747462 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :w < 1269747667 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :aduã•ã‚“ãŒãªãœæ—¥æœ¬ã«ä½ã‚“ã§ã„ã¾ã—ãŸã‹ãªã€‚ < 1269747723 0 :adu!unknown@unknown.invalid PRIVMSG #esoteric :ã¶ãã‚‚, but i've been away for 10 years, so i've forgotten so much < 1269747734 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I'm going to bed now. < 1269747741 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Cheerio, fellows. See you tomorrow. < 1269747742 0 :adu!unknown@unknown.invalid PRIVMSG #esoteric :alise: night < 1269747745 0 :alise!unknown@unknown.invalid QUIT :Quit: Leaving < 1269747801 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :日本語ã§ã€ã€Œåƒ•ã‚‚ã€ã§ã‚‚10å¹´é–“ä½ã¾ãªãã¦ã€ãŸãã•ã‚“忘れãŸã€ã¨æ€ã„ã¾ã™ã€‚ < 1269747856 0 :adu!unknown@unknown.invalid PRIVMSG #esoteric :sounds about right < 1269748032 0 :adu!unknown@unknown.invalid PRIVMSG #esoteric :僕ã®æ—¥æœ¬èªžã¯æ‚ªã„ã§ã™ã€‚ < 1269748220 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :ãªã‚‹ã»ã©ã€‚ < 1269748256 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :勉強ã™ã‚‹ã¤ã‚‚ã‚Šã˜ã‚ƒãªã„ã‚“ã§ã™ã‹ã€‚ < 1269748402 0 :adu!unknown@unknown.invalid PRIVMSG #esoteric :勉強ã—ãŸããªã„ < 1269748504 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :残念ã§ã™ã­ã€‚ < 1269748905 0 :ais523!unknown@unknown.invalid TOPIC #esoteric :this topic is incorrect today but will be correct tomorrow | last topic change: 1 day ago | http://tunes.org/~nef/logs/esoteric/?C=M;O=D < 1269748910 0 :fax!unknown@unknown.invalid QUIT :Quit: Lost terminal < 1269749021 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :ACTION brainmelts < 1269750135 0 :MizardX!unknown@unknown.invalid QUIT :Ping timeout: 276 seconds < 1269751578 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :It's incorrect and will remain incorrect forever. < 1269751600 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :So will 1+1=2 < 1269751602 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :erm, 3 < 1269752007 0 :jcp!unknown@unknown.invalid QUIT :Quit: I will do anything (almost) for a new router. < 1269754193 0 :jcp!~jw@bzflag/contributor/javawizard2539 JOIN :#esoteric < 1269754770 0 :adu!unknown@unknown.invalid QUIT :Quit: adu < 1269755588 0 :Oranjer!unknown@unknown.invalid PART #esoteric :? < 1269759355 0 :jcp!unknown@unknown.invalid QUIT :Quit: I will do anything (almost) for a new router. < 1269759852 0 :coppro!~coppro@unaffiliated/coppro JOIN :#esoteric < 1269763199 0 :clog!unknown@unknown.invalid QUIT :ended < 1269763200 0 :clog!unknown@unknown.invalid JOIN :#esoteric < 1269766665 0 :lifthrasiir!unknown@unknown.invalid QUIT :Ping timeout: 258 seconds < 1269766743 0 :lifthrasiir!~lifthrasi@haje12.kaist.ac.kr JOIN :#esoteric < 1269767047 0 :lifthrasiir!unknown@unknown.invalid QUIT :Ping timeout: 268 seconds < 1269769873 0 :ais523!unknown@unknown.invalid QUIT : < 1269770649 0 :Quadrescence!unknown@unknown.invalid QUIT :Remote host closed the connection < 1269770716 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :what? < 1269770730 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :me looks up at the non-latin script < 1269770732 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :err < 1269770733 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ACTION looks up at the non-latin script < 1269770749 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :Unicode++ < 1269770773 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric : groan <-- you don't like Discworld books then I assume? < 1269770782 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ah wait he isn't here atm < 1269770804 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :dixon, sure, but not for it's own sake < 1269770828 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :it is very nice when you actually have a reason to use it though < 1269770897 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ACTION really should try to figure out why mapping pi onto compose p i didn't work out < 1269770942 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :wat < 1269771144 0 :adam_d!~Adam@aatl83.neoplus.adsl.tpnet.pl JOIN :#esoteric < 1269771426 0 :BeholdMyGlory!~behold@unaffiliated/beholdmyglory JOIN :#esoteric < 1269772300 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :dixon, you know the compose key? < 1269772332 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :I don't have such a fancy thing. < 1269772361 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :well usually you need to enable it in some settings < 1269772371 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :also I never seen it on non-*nix systems < 1269772449 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :dixon, it allows you to press that key you made your compose key then press two other keys < 1269772452 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :to write some letter < 1269772469 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :like µ (compose m u) < 1269772481 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :(though that specific one is also on altgr-m for me) < 1269772491 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :Yes, I know. I'm running *nix, I just don't use it. < 1269772504 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ah right < 1269772517 0 :FireFly!~firefly@unaffiliated/firefly JOIN :#esoteric < 1269772528 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :dixon, thing is I want compose p i to give me the unicode pi < 1269772545 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :and well, for some reason something is ignoring my config file for it < 1269772550 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :weird < 1269772559 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :need to restart X or something? < 1269772571 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :dixon, done that since when I added the file < 1269772590 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :but yeah ~/.XCompose doesn't seem to be used, though docs indicate it should work < 1269772653 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :leave it up to the X people to not update their docs < 1269772673 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :dixon, oh? you found something indicating it works differently nowdays? < 1269772688 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :dixon, the weird thing is that it worked for someone else in here (forgot who) < 1269772733 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :Naw, I have no idea why it doesn't work. :\ < 1269772756 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :but there is a chance that the docs aren't up to date < 1269772794 0 :oerjan!~oerjan@hagbart.nvg.ntnu.no JOIN :#esoteric < 1269772844 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :true < 1269772899 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :lies! < 1269772925 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :http://www.mail-archive.com/vague@list.uvm.edu/msg03505.html < 1269772935 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :dunno if that helps < 1269773158 0 :Phantom_Hoover!~chatzilla@cpc3-sgyl21-0-0-cust116.sgyl.cable.virginmedia.com JOIN :#esoteric < 1269773168 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :http://aturingmachine.com/ < 1269773170 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :I want one. < 1269773216 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :That's just dumb. < 1269773228 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :But it's cool. < 1269773230 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :It's obvious the tape isn't infinitely long. < 1269773233 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :What a piece of shit. < 1269773241 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :Yes, but it's still cool. < 1269773265 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :And there are around 1000 feet of tape, so it's practically infinite. < 1269773298 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :I.e. if you wanted to do any calculations involving more cells than that you'd really just use a computer. < 1269773356 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :Glad to hear you think 1000 feet is "practically infinite" < 1269773366 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :Read my second post. < 1269773372 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :Means my penis is up there on the list. < 1269773384 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :And by that logic, normal computers are dumb. < 1269773392 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :After all, they have finite memory. < 1269773402 0 :Phantom_Hoover!unknown@unknown.invalid QUIT :Client Quit < 1269773453 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :There difference between a math student and a computer science student is a sense of humor. < 1269773456 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :-re < 1269774609 0 :tombom!tombom@wikipedia/Tombomp JOIN :#esoteric < 1269775493 0 :fax!~none@unaffiliated/fax JOIN :#esoteric < 1269776025 0 :Phantom_Hoover!~chatzilla@cpc3-sgyl21-0-0-cust116.sgyl.cable.virginmedia.com JOIN :#esoteric < 1269777011 0 :adam_d!unknown@unknown.invalid QUIT :Ping timeout: 260 seconds < 1269778746 0 :oerjan!unknown@unknown.invalid QUIT :Quit: leaving < 1269782030 0 :fax!unknown@unknown.invalid QUIT :Quit: Lost terminal < 1269782060 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :which one has a sense of humor? < 1269782147 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i'm both and i both do and don't have a sense of humor, i think < 1269782167 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :so in either case, you might be right < 1269782501 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: Your sense of humour must be quantum. < 1269782507 0 :cheater2!~cheater@ip-80-226-15-2.vodafone-net.de JOIN :#esoteric < 1269782535 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :I still maintain the Turing machine was cool, though. < 1269782599 0 :cheater!unknown@unknown.invalid QUIT :Ping timeout: 276 seconds < 1269782860 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :it was totally awesome < 1269782886 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :but it has a bit too much technology in it to be absolutely superawesome < 1269782888 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :Unfortunately, my life is now going to be unfulfilled until I acquire or build one. < 1269784172 0 :Phantom_Hoover!unknown@unknown.invalid QUIT :Quit: ChatZilla 0.9.86 [Firefox 3.5.8/20100214235838] < 1269784363 0 :alise!~alise___@212.183.140.21 JOIN :#esoteric < 1269784442 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :/r/programming is fucking useless; the idiot Ted Dziuba taking the first spot. < 1269784477 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :02:06:44 dixon, sure, but not for it's own sake < 1269784483 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :What, the Japanese or the what? < 1269784487 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :My stuff maybe? < 1269784487 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :I upvoted it for generating discussion, whether or not it's sensible. < 1269784530 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :02:36:30 but yeah ~/.XCompose doesn't seem to be used, though docs indicate it should work < 1269784533 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :you need to do stuff < 1269784552 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant: Discussion of the most trivial, boring stuff - the kind Dziuba usually generates. < 1269784578 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Professional social network manipulator by way of simply being a gigantic asshole with stupid opinions. Hey, sounds like me, apart from the social network part. < 1269784603 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :02:47:10 It's obvious the tape isn't infinitely long. < 1269784603 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :02:47:13 What a piece of shit. < 1269784614 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :You fail; only some Turing machines have infinite tape. < 1269784689 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Coq is awesome < 1269784910 0 :Slereah!unknown@unknown.invalid PRIVMSG #esoteric :alise : Lies < 1269784915 0 :Slereah!unknown@unknown.invalid PRIVMSG #esoteric :Turing machines have infinite tapes < 1269784922 0 :Slereah!unknown@unknown.invalid PRIVMSG #esoteric :Otherwise, they would not be Turing machines! < 1269785070 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Hmm, but there are non-universal turing machines, no? < 1269785075 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I guess maybe they have infinite tape anyway. < 1269785442 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :of course there are non-universal turing machines < 1269785453 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :for instance the empty turing machine is pretty non-universal < 1269785460 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric ::PPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPP < 1269785582 0 :MigoMipo!~migomipo@84-217-9-23.tn.glocalnet.net JOIN :#esoteric < 1269785641 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric ::PPPPPPPPPPPP < 1269786293 0 :Guest39936!~mirwais_g@77.69.196.133 JOIN :#esoteric < 1269786371 0 :Guest39936!unknown@unknown.invalid PART #esoteric :? < 1269786980 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Global tuple space! < 1269787028 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i used to love that crazy thing < 1269787108 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :what thing < 1269787121 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :global tuple space? < 1269787170 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :yes < 1269787218 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :seems a bit too ... unesoteric for you, i mean in your fun definition of esoteric < 1269787221 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :but why don't you love it any more < 1269787237 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :K has a global tuplespace... it's hot < 1269787246 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i haven't touched one in ages < 1269787261 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :love fades fast as they say < 1269787276 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :wat < 1269787331 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :wat wat < 1269787352 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :i mean i'm just imagining like... one gigantic trie/graph/thing < 1269787352 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :and that is everything < 1269787360 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :wat < 1269787410 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :wat wat wat < 1269787466 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :oko < 1269788068 0 :alise_!~alise___@212.183.140.35 JOIN :#esoteric < 1269788227 0 :alise!unknown@unknown.invalid QUIT :Ping timeout: 258 seconds < 1269788557 0 :MizardX!~MizardX@unaffiliated/mizardx JOIN :#esoteric < 1269789884 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :the thing with coq is < 1269789888 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :sometimes I end up with < 1269789889 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : H : 1 = 0 < 1269789890 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : ============================ < 1269789890 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : False < 1269789900 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :and I'm not entirely sure how it wants me to prove that 1 = 0 is impossible... < 1269790225 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Today on "ridiculously trivial proofs": There exists a natural n such that S (pred n) <> n (because pred 0 = 0 in Coq). < 1269790227 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :http://pastie.org/892089.txt?key=mjqv5f7o9cbvwfvjih18a < 1269790233 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Tactics used: < 1269790235 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :apply ex_intro with 0. < 1269790235 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :compute in |- *. < 1269790235 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :intros H. < 1269790235 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :auto. < 1269790235 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :congruence. < 1269790280 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Really it's a disproof of 1 = 0. < 1269790288 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Because I just plugged in the value then told it to shut up and compute S (pred n) and n. :) < 1269790427 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Actually I don't think auto did anything there... < 1269790574 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Yeah, I could have produced that with just: < 1269790576 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :apply ex_intro with 0. < 1269790578 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :congruence. < 1269790674 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :If I used discriminate instead of the more advanced congruence, I'd get: < 1269790691 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :http://pastie.org/892094.txt?key=sygsuuuwz1tnauvsksvw5q < 1269790701 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Which is simpler. < 1269790711 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :(That's from apply ex_intro with 0. compute. intros H. discriminate.) < 1269790735 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Which can also be produced with: < 1269790738 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :apply ex_intro with 0. < 1269790739 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :discriminate. < 1269790744 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :So that's the shortest, simplest proof. < 1269791066 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :ooh, coqolf < 1269791115 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Now I'm trying to prove (~ exists n, forall m, n >= m); it's surprisingly difficult. < 1269791152 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :for exists, you need a specific counterexample, so take succ n, then just use succ n > n for all n < 1269791155 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :how can that be hard? < 1269791162 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i should learn cow < 1269791164 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :*coq < 1269791168 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :well of course it is easy, it's just expressing it in the tactics engine < 1269791171 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :*example < 1269791172 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :without really knowing what tactics to use... < 1269791180 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I could do it as a lambda expression, probably, with equality induction < 1269791184 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :but it'll be shorter as tactics < 1269791191 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :and lambda expression proofs get unwieldy fast, they're like bytecode < 1269791204 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :currently I'm up to: < 1269791207 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : H : forall m : nat, 0 >= m < 1269791208 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :right i don't know anything about tactics. well except that they can magically do things for you < 1269791208 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : ============================ < 1269791209 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : False < 1269791210 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :nobiggest < apply (H 1). < 1269791210 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Toplevel input, characters 0-11: < 1269791211 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :> apply (H 1). < 1269791213 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :> ^^^^^^^^^^^ < 1269791215 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Error: Impossible to unify "0 >= 1" with "False". < 1269791228 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: basically they search for stuff with certain types in the environment then apply them using various different already-proved theorems < 1269791232 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :to try and prove the current goal < 1269791253 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :so like if you have "1 = 0" you can use "discriminate" and it'll look for an equality, then it'll examine the constructors, find out that they're different, and derive a contradiction for you < 1269791266 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :right, cool < 1269791271 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :you can use "apply F" to apply a function/implication in the environment automatically filling in the arguments it can, giving subgoals automatically if this reduces the problem < 1269791279 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: one issue is that tactics automatically introduce variables with names they like < 1269791289 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :so reading it without seeing the transcript, random "H3"s just appear out of nowhere :) < 1269791350 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Maybe I'll prove forall n, exists m, m > n, then prove ~ exists n, forall m, n >= m from that. < 1269791395 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : ============================ < 1269791395 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : S n > n < 1269791400 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :auto time :P < 1269791417 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :here's my documentation for auto: "does something helpful, or does something unhelpful, or does nothing". < 1269791418 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :what's auto? < 1269791423 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :this time it worked! < 1269791427 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :cool < 1269791427 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: it tries to magically prove whatever for you < 1269791429 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :it isn't very good at it < 1269791440 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :intros n. < 1269791440 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :apply ex_intro with (S n). < 1269791441 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :auto. < 1269791441 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :-> < 1269791444 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :alwaysbigger = < 1269791446 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fun n : nat => ex_intro (fun m : nat => m > n) (S n) (le_n (S n)) < 1269791446 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : : forall n : nat, exists m : nat, m > n < 1269791521 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : x : nat < 1269791523 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : H : forall m : nat, x >= m < 1269791523 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : x0 : nat < 1269791523 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : H0 : x0 > x < 1269791523 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : ============================ < 1269791523 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : False < 1269791523 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :that's better < 1269791669 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : H0 : x0 > x < 1269791670 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : H1 := H x0 : x >= x0 < 1269791671 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cuntradiction < 1269791805 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :destruct H0 < 1269791806 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :then I get < 1269791807 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : H1 := H (S x) : x >= S x < 1269791824 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :destruct? < 1269791838 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :basically... take this object, deconstruct it into its components < 1269791843 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :which depends on what it is < 1269791849 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :in this case I'm destructing the inequality into the environment < 1269791855 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :so that the same implications hold, but it's folded into other things < 1269791859 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :rather than a separate object < 1269791872 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :with e.g. a tuple (x,y) it'd introduce two values, x and y < 1269791881 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :they're tactics... they don't really have precise semantics :) < 1269791882 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :kinda cool < 1269791886 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :yeah i get it < 1269791977 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :lol disproving x >= S x is so hard < 1269791985 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :there must be some lemma for x >= y -> x <> y < 1269791992 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :then I could use discriminate < 1269792083 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Theorem gt_Sn_n : forall n, S n > n. < 1269792093 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Hint Resolve gt_Sn_n: arith v62. < 1269792282 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : x : nat < 1269792283 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : H : forall m : nat, x >= m < 1269792283 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : H1 := H (S x) : x >= S x < 1269792283 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : ============================ < 1269792303 0 :lament!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1269792315 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :proving False from this is stupidly hard... < 1269792315 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :obviously ~ x >= S x < 1269792502 0 :lament!~lament@S0106001b63f462cc.vc.shawcable.net JOIN :#esoteric < 1269792505 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : H1 := H x : x >= x < 1269792508 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :now we're getting somewhere < 1269793236 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I'm just doing it the general abstract nonsense way - < 1269793259 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Prove (forall x, P x) -> ~(exists x, ~P x) < 1269793295 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :then apply that to alwaysbigger < 1269793296 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :(alwaysbigger : forall x, exists y, y > x) so we get ~(exists x, ~exists y, y > x). < 1269793296 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I'll go from there. < 1269793305 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :forallnotexists2 = < 1269793306 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fun (A : Type) (P : A -> Prop) (H : forall x : A, P x) < 1269793306 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : (H0 : exists x : A, ~ P x) => < 1269793306 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :match H0 with < 1269793306 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :| ex_intro x H1 => let H2 := H x in False_ind False (H1 H2) < 1269793306 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :end < 1269793307 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : : forall (A : Type) (P : A -> Prop), < 1269793309 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : (forall x : A, P x) -> ~ (exists x : A, ~ P x) < 1269793318 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :if anyone cares. < 1269793320 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Pretty easy proof, it has to be said. < 1269793615 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :lol auto worked in coqtop but not here... < 1269793637 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :in emacs < 1269793757 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :Write it in LaTeX. < 1269793758 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oh because I inverted it lol < 1269794017 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric : you need to do stuff <-- what stuff? < 1269794052 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :(context: composite key= < 1269794056 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :s/=/)/ < 1269794155 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Darn, I can't turn ~ exists ~ -> forall. < 1269794204 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Because that's excluded middle. < 1269794204 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: It's like some sort of include thing and some sort of config file change and thingy; I forget. < 1269794204 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :dixon: latex coq < 1269794204 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I have ~ exists n, ~ exists m, m > n which is, you know, close. < 1269794230 0 :Gracenotes!unknown@unknown.invalid QUIT :Quit: Leaving < 1269794297 0 :kar8nga!~kar8nga@91.35.72-86.rev.gaoland.net JOIN :#esoteric < 1269794516 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :This tactic applies to any goal. assert (H : U) adds a new hypothesis of name H asserting U to the current goal and opens a new subgoal U3. The subgoal U comes first in the list of subgoals remaining to prove. < 1269794520 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :gawd, why didn't I know of this before < 1269795019 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ACTION looks for (m <= n) -> (m <= S n) < 1269795146 0 :lifthrasiir!pLkLl8ot@haje12.kaist.ac.kr JOIN :#esoteric < 1269795167 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : x : nat < 1269795167 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : H : forall m : nat, S x >= m < 1269795167 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : IHx : (forall m : nat, x >= m) -> False < 1269795168 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : ============================ < 1269795169 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : False < 1269795171 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :man go fuck yourself :P < 1269795306 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise_, hm okay < 1269795309 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :bbl < 1269795346 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :alise_: Write it in LaTeX without using a tool to do it for you. < 1269795366 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :dixon: But the proof is trivial; all I am trying to do is get used to Coq. < 1269795395 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Typesetting is not what I am trying to do. < 1269795403 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :i c < 1269795478 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : H : forall m : nat, 1 >= m < 1269795479 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : ============================ < 1269795479 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : forall m : nat, 0 >= m < 1269795479 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :lol < 1269795484 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :i am doing this all wrong < 1269795615 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : x : nat < 1269795616 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : H : forall m : nat, S (S x) >= m < 1269795616 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : IHx : (forall m : nat, S x >= m) -> False < 1269795616 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : IHx0 : (forall m : nat, S x >= m) -> < 1269795616 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : ((forall m : nat, x >= m) -> False) -> False < 1269795616 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : ============================ < 1269795617 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : False < 1269795620 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I have a feeling Coq is trying to get me to do an infinite induction manually < 1269795898 0 :lament!unknown@unknown.invalid QUIT :Ping timeout: 240 seconds < 1269796085 0 :adam_d!~Adam@aatl83.neoplus.adsl.tpnet.pl JOIN :#esoteric < 1269796323 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Well, I proved it. < 1269796334 0 :FireFly!unknown@unknown.invalid PRIVMSG #esoteric : man go fuck yourself :P < 1269796334 0 :FireFly!unknown@unknown.invalid PRIVMSG #esoteric : alise_, hm okay < 1269796334 0 :FireFly!unknown@unknown.invalid PRIVMSG #esoteric : bbl < 1269796336 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Not using tactics - only partly - though. < 1269796339 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric ::D < 1269796340 0 :FireFly!unknown@unknown.invalid PRIVMSG #esoteric :What was the syntax for that quote bot? < 1269796392 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :http://pastie.org/892210.txt?key=ir8pgxsvdnexhfoifnvvpg < 1269796397 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :FireFly: `addquote ... < 1269796414 0 :FireFly!unknown@unknown.invalid PRIVMSG #esoteric :`addquote man go fuck yourself :P alise_, hm okay bbl < 1269796427 0 :FireFly!unknown@unknown.invalid PRIVMSG #esoteric :`quote < 1269796429 0 :FireFly!unknown@unknown.invalid PRIVMSG #esoteric :Hmm < 1269796474 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Theorem No_biggest_3 : ~ exists n, forall m, n >= m. < 1269796474 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : intros H. < 1269796474 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : destruct H. < 1269796474 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : set (H0 := H (S x)). < 1269796474 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : apply (Not_bigger_than_successor H0). < 1269796475 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Qed. < 1269796475 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :tada < 1269796479 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I could fold in Not_bigger_than_successor if I wanted... < 1269796532 0 :HackEgo!unknown@unknown.invalid PRIVMSG #esoteric :No output. < 1269796532 0 :HackEgo!unknown@unknown.invalid PRIVMSG #esoteric :No output. < 1269796558 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :No_biggest_4 = < 1269796559 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fun H : exists n : nat, forall m : nat, n >= m => < 1269796559 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :match H with < 1269796559 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :| ex_intro x H0 => < 1269796559 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : let H1 := H0 (S x) in let H2 := gt_Sn_n x in le_not_lt (S x) x H1 H2 < 1269796559 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :end < 1269796560 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : : ~ (exists n : nat, forall m : nat, n >= m) < 1269796560 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Success! < 1269796587 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Proof: intros H. destruct H. set (H0 := H (S x)). assert (H1 : S x > x). apply gt_Sn_n. apply (le_not_lt (S x) x). assumption. assumption. < 1269796732 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Thus proving the incredibly obvious truth that there is no natural number n such that for all natural numbers m, n is either greater than or equal to m. < 1269796750 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :All the 0 people who believe that infinity is a natural number have been thoroughly debunked! Ha! < 1269796756 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :That was such a waste of time. < 1269796767 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :There are more than 0 people who believe that. < 1269796785 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Shaddup. < 1269796796 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :From Talk:Hereditarily finite set, archived from Votes for DEletion: < 1269796797 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :"Hereditarily finite set. Strange maths stuff. Makes no sense. Angela 00:52, Oct 2, 2003 (UTC)" < 1269796807 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Angela being the Wikia founder. < 1269796819 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :Heh. < 1269796839 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :wat, u mean I can't just do S(n) < 1269796859 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :Hey, "hereditarily finite set" alternates vowels and consonants. < 1269796866 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :dixon: wut < 1269796877 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :*Deletion < 1269796888 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :let m = S(n) < 1269796895 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :well yeah exactly < 1269796906 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :my proof is shorter. suckaaaaaaaaa < 1269796908 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :but that just gives you n >= S n... so then you have to disprove that < 1269796918 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :Well, to be fair, when she nominated it for deletion, the article's text was this: < 1269796922 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :which you do by asserting that S n > n, using the existing theorem for that, then using the theorem that contradicts the two < 1269796926 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :... n can't be >= S(n) < 1269796930 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :of course it can't < 1269796934 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :"A set A is called 'Heredity finite' if it is is in $V_\omega$, or on other word, if it is in $V_n$ for some natural number $n$" < 1269796936 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :and there can't be a finite number of primes < 1269796937 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :you have to prove it < 1269796972 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :dixon: Of course it is very easy to package the fact that ~ n >= S n up into one theorem. < 1269796979 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Theorem Not_bigger_than_successor {n} : ~ n >= S n. < 1269796980 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : intros n H. < 1269796980 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : assert (H0 : S n > n). < 1269796980 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : apply gt_Sn_n. < 1269796980 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : apply (le_not_lt (S n) n). < 1269796980 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : assumption. < 1269796982 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : assumption. < 1269796984 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Qed. < 1269796995 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Either I just didn't find it in Coq's library or nobody thought to combine the two yet, because there's ~ n > S n. < 1269797006 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :Or you could just reference Peano's axioms. < 1269797063 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Peano's axioms don't actually define greaterthan, less than, etc, for a start. < 1269797065 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Just equality. < 1269797119 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :So... yeah. < 1269797128 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :We can define less than using them. If m = S^n(x) for some natural n, then m > x < 1269797137 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Which is something you have to prove. < 1269797145 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :No I don't. < 1269797146 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :You can't just say "this is true" because if you did that nothing would need a proof. < 1269797155 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :I can define it as true. < 1269797156 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Anyway -- if I used "auto with arith" it could do all this automatically. < 1269797159 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :But I was too lazy. < 1269797167 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :dixon: Then congratulations, you created an axiom. < 1269797181 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Too lazy to avoid doing work, heh. < 1269797193 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Anyway, yes, of course, there is a tactic to automatically prove this sort of stuff for you in one statement. < 1269797203 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :But I'm trying to learn how to use Coq, not how to ask Coq to prove everything for me. < 1269797215 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :If you just want to dis Coq as being a verbose waste of time you could just do that directly :P < 1269797245 0 :kar8nga!unknown@unknown.invalid QUIT :Remote host closed the connection < 1269797250 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :I don't think Coq is a waste of time, I think computer-based pseudo-math using Coq, Haskell, Axiom, etc is a waste of time. < 1269797262 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Haskell can't even prove things. < 1269797268 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :Yes it can. < 1269797271 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :So lumping it in with Coq is ridiculous. < 1269797289 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :dixon: Well, for a start, it can prove anything (using undefined); for a second, its propositions are boolean-returning functions, not actual types. < 1269797292 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :So no, it cannot. < 1269797301 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :And Axiom is a computer algebra system, not a proof assistant. < 1269797306 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :Curry-Howard isomorphism. < 1269797333 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :And I'm well-aware what Axiom is, but it has a language packaged with it called Aldor. < 1269797336 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :- is clearly something you know nothing about; it addresses the simply-typed lambda calculus, which has no _|_. < 1269797336 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :So - do you consider the proof of the four-colour theorem "pseudo-math"? < 1269797343 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Is it pseudo-math just because a computer did it? < 1269797389 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :FireFly, hah at that quote < 1269797456 0 :jcp!~jw@bzflag/contributor/javawizard2539 JOIN :#esoteric < 1269797560 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :alise_: Coming from the one saying you can't prove things in Haskell, you seem to be the one in the dark. And I think fooling around with Coq, Haskell, etc and thinking it makes you a mathematician is pseudo-math, not being a mathematician who happens to use Coq to construct a proof of e.g., the FCT. < 1269797579 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Well, yes, you can prove things in Haskell, but it is an inconsistent system. < 1269797605 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Yes - you can do `data Z; data S n`, then meticulously define operations on it, then construct values to prove it. < 1269797610 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :But you can prove anything you want: "undefined". < 1269797613 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :That depends on how you define "a mathematician". < 1269797624 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :It is a proof system only in the most pathological sense, and even then it is blatantly inconsistent. < 1269797631 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :And I never claimed I was a mathematician because I fuck around with Coq. < 1269797646 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :uorygl: Think Newton. < 1269797662 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :But are you imposing some sort of elitism on "mathematician" above someone who does mathematics? Surely if some amateur constructed a new kind of object and proved useful things about it with Coq, e would be a "real" mathematician. < 1269797694 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :If you do not agree then you're just an elitist scared of some random nobody doing anything worthwhile. < 1269797705 0 :Quadrescence!~quad@unaffiliated/quadrescence JOIN :#esoteric < 1269797711 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :So a mathematician is a person who invents new fields of mathematics and discovers novel applications of it? < 1269797737 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Or even just a person who discovers novel results about existing fields. < 1269797743 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :uorygl, I would say far from all mathematicians manage to invent a new field of mathematics. < 1269797749 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :A mathematician is someone who explores mathematics and shows up previously unknown things in its depths. < 1269797758 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :some could refine an already existing field < 1269797772 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :They're even a mathematician if they only try and do this without succeeding as long as they have the competence to potentially do it. < 1269797778 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise_, correction: s/mathematician/successful mathematician/ :P < 1269797805 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :hm < 1269797821 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :(for the one before) < 1269797833 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :(my finger was on enter when your last line arrived) < 1269798086 0 :MigoMipo!unknown@unknown.invalid QUIT :*.net *.split < 1269798189 0 :pikhq!unknown@unknown.invalid QUIT :*.net *.split < 1269798189 0 :yiyus!unknown@unknown.invalid QUIT :*.net *.split < 1269798189 0 :alise_!unknown@unknown.invalid QUIT :*.net *.split < 1269798189 0 :Gregor!unknown@unknown.invalid QUIT :*.net *.split < 1269798189 0 :olsner!unknown@unknown.invalid QUIT :*.net *.split < 1269798189 0 :adam_d!unknown@unknown.invalid QUIT :*.net *.split < 1269798190 0 :uorygl!unknown@unknown.invalid QUIT :*.net *.split < 1269798190 0 :ineiros!unknown@unknown.invalid QUIT :*.net *.split < 1269798190 0 :tombom!unknown@unknown.invalid QUIT :*.net *.split < 1269798190 0 :mtve!unknown@unknown.invalid QUIT :*.net *.split < 1269798190 0 :SimonRC!unknown@unknown.invalid QUIT :*.net *.split < 1269798190 0 :Quadrescence!unknown@unknown.invalid QUIT :*.net *.split < 1269798190 0 :jix!unknown@unknown.invalid QUIT :*.net *.split < 1269798190 0 :pineapple!unknown@unknown.invalid QUIT :*.net *.split < 1269798190 0 :rodgort!unknown@unknown.invalid QUIT :*.net *.split < 1269798190 0 :chickenzilla!unknown@unknown.invalid QUIT :*.net *.split < 1269798190 0 :jcp!unknown@unknown.invalid QUIT :*.net *.split < 1269798190 0 :EgoBot!unknown@unknown.invalid QUIT :*.net *.split < 1269798190 0 :HackEgo!unknown@unknown.invalid QUIT :*.net *.split < 1269798190 0 :cal153!unknown@unknown.invalid QUIT :*.net *.split < 1269798191 0 :MaXo2!unknown@unknown.invalid QUIT :*.net *.split < 1269798191 0 :Leonidas!unknown@unknown.invalid QUIT :*.net *.split < 1269798191 0 :MizardX!unknown@unknown.invalid QUIT :*.net *.split < 1269798191 0 :FireFly!unknown@unknown.invalid QUIT :*.net *.split < 1269798191 0 :wareya!unknown@unknown.invalid QUIT :*.net *.split < 1269798191 0 :myndzi\!unknown@unknown.invalid QUIT :*.net *.split < 1269798191 0 :bsmntbombdood!unknown@unknown.invalid QUIT :*.net *.split < 1269798191 0 :comex!unknown@unknown.invalid QUIT :*.net *.split < 1269798191 0 :Ilari!unknown@unknown.invalid QUIT :*.net *.split < 1269798191 0 :dixon!unknown@unknown.invalid QUIT :*.net *.split < 1269798191 0 :cheater2!unknown@unknown.invalid QUIT :*.net *.split < 1269798191 0 :BeholdMyGlory!unknown@unknown.invalid QUIT :*.net *.split < 1269798191 0 :AnMaster!unknown@unknown.invalid QUIT :*.net *.split < 1269798191 0 :oklopol!unknown@unknown.invalid QUIT :*.net *.split < 1269798193 0 :sshc!unknown@unknown.invalid QUIT :Ping timeout: 255 seconds < 1269798222 0 :mycroftiv!unknown@unknown.invalid QUIT :Ping timeout: 240 seconds < 1269798273 0 :sebbu!unknown@unknown.invalid QUIT :Ping timeout: 240 seconds < 1269798334 0 :sshc!~sshc@unaffiliated/sshc JOIN :#esoteric < 1269798334 0 :mycroftiv!~ircguy@h69-128-47-242.mdsnwi.dedicated.static.tds.net JOIN :#esoteric < 1269798334 0 :Quadrescence!~quad@unaffiliated/quadrescence JOIN :#esoteric < 1269798334 0 :jcp!~jw@bzflag/contributor/javawizard2539 JOIN :#esoteric < 1269798334 0 :adam_d!~Adam@aatl83.neoplus.adsl.tpnet.pl JOIN :#esoteric < 1269798334 0 :MizardX!~MizardX@unaffiliated/mizardx JOIN :#esoteric < 1269798334 0 :alise_!~alise___@212.183.140.35 JOIN :#esoteric < 1269798334 0 :MigoMipo!~migomipo@84-217-9-23.tn.glocalnet.net JOIN :#esoteric < 1269798334 0 :cheater2!~cheater@ip-80-226-15-2.vodafone-net.de JOIN :#esoteric < 1269798334 0 :tombom!tombom@wikipedia/Tombomp JOIN :#esoteric < 1269798334 0 :FireFly!~firefly@unaffiliated/firefly JOIN :#esoteric < 1269798334 0 :BeholdMyGlory!~behold@unaffiliated/beholdmyglory JOIN :#esoteric < 1269798334 0 :AnMaster!~AnMaster@unaffiliated/anmaster JOIN :#esoteric < 1269798334 0 :oklopol!~oklopol@a91-153-122-35.elisa-laajakaista.fi JOIN :#esoteric < 1269798334 0 :pikhq!~pikhq@75-106-123-198.cust.wildblue.net JOIN :#esoteric < 1269798334 0 :wareya!~wareya@cpe-74-70-140-214.nycap.res.rr.com JOIN :#esoteric < 1269798334 0 :dixon!~dixon@unaffiliated/reikon JOIN :#esoteric < 1269798334 0 :myndzi\!myndzi@tengototen.net JOIN :#esoteric < 1269798334 0 :yiyus!1242712427@je.je.je JOIN :#esoteric < 1269798334 0 :mtve!~mtve@65.98.99.53 JOIN :#esoteric < 1269798334 0 :ineiros!~itniemin@james.ics.hut.fi JOIN :#esoteric < 1269798334 0 :uorygl!~Warrigal@rrcs-70-63-156-144.midsouth.biz.rr.com JOIN :#esoteric < 1269798334 0 :SimonRC!~sc@fof.durge.org JOIN :#esoteric < 1269798334 0 :EgoBot!~EgoBot@codu.xen.prgmr.com JOIN :#esoteric < 1269798334 0 :HackEgo!~HackEgo@codu.xen.prgmr.com JOIN :#esoteric < 1269798334 0 :cal153!~cal@c-69-181-46-213.hsd1.ca.comcast.net JOIN :#esoteric < 1269798334 0 :jix!~jix@cyb0rg.org JOIN :#esoteric < 1269798334 0 :pineapple!~pineapple@cpc3-aztw11-0-0-cust24.aztw.cable.virginmedia.com JOIN :#esoteric < 1269798334 0 :rodgort!~rodgort@li14-39.members.linode.com JOIN :#esoteric < 1269798334 0 :chickenzilla!~chicken@olol.eu JOIN :#esoteric < 1269798334 0 :olsner!~salparot@c83-252-161-133.bredband.comhem.se JOIN :#esoteric < 1269798334 0 :Gregor!~gregor@65.183.185.22 JOIN :#esoteric < 1269798334 0 :bsmntbombdood!~gavin@97-118-247-81.hlrn.qwest.net JOIN :#esoteric < 1269798334 0 :MaXo2!~dwili@esp64-1-82-243-172-27.fbx.proxad.net JOIN :#esoteric < 1269798334 0 :Leonidas!~Leonidas@unaffiliated/leonidas JOIN :#esoteric < 1269798334 0 :comex!comex@c-98-210-192-54.hsd1.ca.comcast.net JOIN :#esoteric < 1269798334 0 :Ilari!~user@2002:5870:32ae::1 JOIN :#esoteric < 1269798348 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :I will speak to him and leverage what he knows already, and move forward. < 1269798349 0 :sebbu!~sebbu@ADijon-152-1-30-184.w83-194.abo.wanadoo.fr JOIN :#esoteric < 1269798352 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Well, you could have just stated - as I suspected - that it was a philosophical objection to all this rag at the start; then we'd know it's a philosophical disagreement and could have stopped wasting our time sooner. < 1269798358 0 :adam_d!unknown@unknown.invalid QUIT :Ping timeout: 240 seconds < 1269798364 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :And Zeilberger is a lunatic. < 1269798376 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :He's a smart lunatic. < 1269798390 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Yes, well, so are many people. < 1269798392 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :And he knows his shit and moreover has a passion lacking in most mathematicians. < 1269798413 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :Masterpieces. < 1269798471 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :dixon: Is that just a random exclamation or does it have context? < 1269798519 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :alise_: You'd understand if you knew much about Zeilberger. < 1269798536 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :ACTION wonders who isn't a lunatic, according to alise_  < 1269798545 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :dixon: lol. < 1269798564 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :VLC: Please stop being an attention whore. You should only be making your window flash when something actually happens < 1269798626 0 :sshc!unknown@unknown.invalid QUIT :Ping timeout: 258 seconds < 1269798648 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo_: VLC said that if you stop watching porn in it, it'll stop flashing you. < 1269798649 0 :sshc!~sshc@174-19-197-100.bois.qwest.net JOIN :#esoteric < 1269798655 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :lol < 1269798662 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :That's what VLC thought. < 1269798681 0 :BeholdMyGlory_!~behold@d83-183-183-70.cust.tele2.se JOIN :#esoteric < 1269798717 0 :AnMaster_!~AnMaster@cl-394.sto-01.se.sixxs.net JOIN :#esoteric < 1269798819 0 :jcp!unknown@unknown.invalid QUIT :Ping timeout: 258 seconds < 1269798896 0 :Leonidas!unknown@unknown.invalid QUIT :Ping timeout: 258 seconds < 1269798896 0 :MaXo2!unknown@unknown.invalid QUIT :Ping timeout: 258 seconds < 1269798901 0 :BeholdMyGlory!unknown@unknown.invalid QUIT :Remote host closed the connection < 1269798902 0 :MaXo2!~dwili@esp64-1-82-243-172-27.fbx.proxad.net JOIN :#esoteric < 1269798903 0 :AnMaster!unknown@unknown.invalid QUIT :Remote host closed the connection < 1269798906 0 :mtve!unknown@unknown.invalid QUIT :Ping timeout: 246 seconds < 1269798907 0 :SimonRC!unknown@unknown.invalid QUIT :Ping timeout: 246 seconds < 1269798907 0 :SimonRC!~sc@fof.durge.org JOIN :#esoteric < 1269798939 0 :jcp!~jw@c-98-202-196-76.hsd1.ut.comcast.net JOIN :#esoteric < 1269798954 0 :Leonidas_!~Leonidas@chronon.pointtec.de JOIN :#esoteric < 1269798955 0 :Leonidas_!unknown@unknown.invalid QUIT :Changing host < 1269798955 0 :Leonidas_!~Leonidas@unaffiliated/leonidas JOIN :#esoteric < 1269798967 0 :sshc!unknown@unknown.invalid QUIT :Changing host < 1269798967 0 :sshc!~sshc@unaffiliated/sshc JOIN :#esoteric < 1269798969 0 :AnMaster_!unknown@unknown.invalid QUIT :Changing host < 1269798969 0 :AnMaster_!~AnMaster@unaffiliated/anmaster JOIN :#esoteric < 1269798969 0 :BeholdMyGlory_!unknown@unknown.invalid QUIT :Changing host < 1269798969 0 :BeholdMyGlory_!~behold@unaffiliated/beholdmyglory JOIN :#esoteric < 1269798974 0 :jcp!unknown@unknown.invalid QUIT :Changing host < 1269798974 0 :jcp!~jw@bzflag/contributor/javawizard2539 JOIN :#esoteric < 1269799003 0 :cal153!unknown@unknown.invalid QUIT :Ping timeout: 258 seconds < 1269799006 0 :BeholdMyGlory_!unknown@unknown.invalid NICK :BeholdMyGlory < 1269799008 0 :cal153!~cal@c-69-181-46-213.hsd1.ca.comcast.net JOIN :#esoteric < 1269799015 0 :uorygl!unknown@unknown.invalid QUIT :*.net *.split < 1269799015 0 :ineiros!unknown@unknown.invalid QUIT :*.net *.split < 1269799078 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :"dd/dd is something based on dd/sh but different. It is based on the UNIX 'dd' command, but it doesn't use 'dd' command, actually, because it is different. " < 1269799188 0 :uorygl!~Warrigal@rrcs-70-63-156-144.midsouth.biz.rr.com JOIN :#esoteric < 1269799205 0 :uorygl!unknown@unknown.invalid QUIT :Read error: Operation timed out < 1269799222 0 :uorygl!~Warrigal@rrcs-70-63-156-144.midsouth.biz.rr.com JOIN :#esoteric < 1269799270 0 :lifthras1ir!M58WNbag@haje12.kaist.ac.kr JOIN :#esoteric < 1269799272 0 :adam_d!~Adam@aatl83.neoplus.adsl.tpnet.pl JOIN :#esoteric < 1269799272 0 :MizardX-!~MizardX@unaffiliated/mizardx JOIN :#esoteric < 1269799278 0 :sebbu!unknown@unknown.invalid QUIT :*.net *.split < 1269799278 0 :MizardX!unknown@unknown.invalid QUIT :*.net *.split < 1269799301 0 :MizardX-!unknown@unknown.invalid NICK :MizardX < 1269799316 0 :werdan7!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1269799316 0 :lifthrasiir!unknown@unknown.invalid QUIT :Remote host closed the connection < 1269799351 0 :myndzi!myndzi@tengototen.net JOIN :#esoteric < 1269799369 0 :werdan7_!~w7@freenode/staff/wikimedia.werdan7 JOIN :#esoteric < 1269799442 0 :mtve!~mtve@65.98.99.53 JOIN :#esoteric < 1269799443 0 :sebbu!~sebbu@ADijon-152-1-30-184.w83-194.abo.wanadoo.fr JOIN :#esoteric < 1269799447 0 :charlls!charlls@166.237.157.220 JOIN :#esoteric < 1269799535 0 :myndzi\!unknown@unknown.invalid QUIT :Ping timeout: 268 seconds < 1269799543 0 :AnMaster_!unknown@unknown.invalid NICK :AnMaster < 1269799604 0 :fax!~none@unaffiliated/fax JOIN :#esoteric < 1269799605 0 :ineiros!~itniemin@james.ics.hut.fi JOIN :#esoteric < 1269799735 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Infinite associative arrays + lazy mapping = < 1269799735 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :plus := < 1269799736 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : :nats / {n} [ n := [ 0 := n ] ] < 1269799736 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :| :nats / {n} [ n := :nats / {m} [ m succ := plus n m succ ] ] < 1269799736 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :; < 1269799765 0 :charlls!unknown@unknown.invalid QUIT :Ping timeout: 264 seconds < 1269799910 0 :charlls!charlls@166.237.157.220 JOIN :#esoteric < 1269799921 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :If you had succ as a function not a "method" it'd be < 1269799924 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :succ (plus n m) < 1269800133 0 :MaXo2!unknown@unknown.invalid QUIT :Ping timeout: 240 seconds < 1269800142 0 :yiyus!unknown@unknown.invalid QUIT :*.net *.split < 1269800149 0 :MaXo2!~dwili@esp64-1-82-243-172-27.fbx.proxad.net JOIN :#esoteric < 1269800193 0 :Deewiant!unknown@unknown.invalid QUIT :Ping timeout: 240 seconds < 1269800238 0 :Deewiant!~deewiant@kekkonen.cs.hut.fi JOIN :#esoteric < 1269800275 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Why hello there... DEEWIANT < 1269800288 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Wellhello < 1269800338 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :A little BING noise keeps happening every while on this machine... why grr < 1269800561 0 :yiyus!1242712427@je.je.je JOIN :#esoteric < 1269800780 0 :pineapple!unknown@unknown.invalid QUIT :Ping timeout: 245 seconds < 1269800782 0 :pineapple!~pineapple@cpc3-aztw11-0-0-cust24.aztw.cable.virginmedia.com JOIN :#esoteric < 1269800990 0 :BeholdMyGlory_!~behold@d83-183-183-70.cust.tele2.se JOIN :#esoteric < 1269801076 0 :BeholdMyGlory!unknown@unknown.invalid QUIT :Write error: Broken pipe < 1269801662 0 :oklofok!~oklopol@a91-153-122-35.elisa-laajakaista.fi JOIN :#esoteric < 1269801735 0 :cheater3!~cheater@ip-80-226-15-2.vodafone-net.de JOIN :#esoteric < 1269801799 0 :cheater2!unknown@unknown.invalid QUIT :Write error: Connection reset by peer < 1269801938 0 :oklopol!unknown@unknown.invalid QUIT :Ping timeout: 260 seconds < 1269801982 0 :BeholdMyGlory_!unknown@unknown.invalid QUIT :Changing host < 1269801982 0 :BeholdMyGlory_!~behold@unaffiliated/beholdmyglory JOIN :#esoteric < 1269801985 0 :BeholdMyGlory_!unknown@unknown.invalid NICK :BeholdMyGlory < 1269803239 0 :Oranjer!~HP_Admini@adsl-71-7-92.cae.bellsouth.net JOIN :#esoteric < 1269803407 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :it's weird that you can prove ~~~~P -> ~~P without LEM... < 1269803446 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :no it's not < 1269803478 0 :oerjan!~oerjan@hagbart.nvg.ntnu.no JOIN :#esoteric < 1269803527 0 :kar8nga!~kar8nga@91.35.72-86.rev.gaoland.net JOIN :#esoteric < 1269803528 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :it's just saying ~~~~P -> (P -> False) -> False, so you have hypothesis H : ~~~~P and H' : ~P, but ~P -> ~~~P which immediately contradicts H < 1269803561 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :the point is that the negation gives you contra-whatever-it-is which lets you add more ~'s instead of stripping them off < 1269803573 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric : i'm both and i both do and don't have a sense of humor, i think <-- no, that would be the quantum physicists < 1269803662 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :and ~~~P -> ~P for that matter < 1269803664 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: intuitively weird, I mean < 1269803672 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :get into #morphism fax :< < 1269803695 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :it's because you're looking at it wrong < 1269803928 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :~ may be an antitone galois connection, i think? < 1269804005 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :or wait, does that require the excluded middle < 1269804067 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :b -> ~a iff a -> ~b. hm that's obvious really. < 1269804083 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :so no excluded middle required < 1269804139 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise_ ???? < 1269804170 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I think b -> ~a iff a -> ~b is excluded middle? < 1269804182 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :no sorry of course it's not < 1269804232 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :whoa, flood < 1269804233 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :all at once < 1269804235 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :sorry guyz < 1269804249 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :nah with ~a = a -> false, it's just switching of assumptions < 1269804496 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :how to give a geometrical interpretation of Sum[k=1..] (2/3)^k? < 1269804540 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I'm so confused how can 2/3 possibly be less than 1 < 1269804553 0 :adam_d_!~Adam@aath39.neoplus.adsl.tpnet.pl JOIN :#esoteric < 1269804716 0 :adam_d!unknown@unknown.invalid QUIT :Ping timeout: 246 seconds < 1269804776 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ACTION swats fax to unconfuse em -----### < 1269804807 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I figured it out < 1269804830 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :good, good < 1269804838 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :but still can't explain the convergence < 1269804858 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :it's obvious from the geometric interpretation >:) < 1269804892 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :what is the geometric interpretation < 1269804904 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :well one interpretation < 1269804937 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :just divide up say a triangle into infinitely many pieces so that each piece is 2/3 of the previous one < 1269804954 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :what < 1269804977 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :you mean like chop a triangle up somhow < 1269804988 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :actually chopping up a line segment may be easier < 1269804996 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :area of a triangle = 1/2 w h < 1269805006 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :(then you just need length < 1269805007 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :) < 1269805101 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :fax: take a line segment whose length is x where x = 2/3 + (2/3)*x < 1269805140 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :chop off the first 2/3, then note how the rest is just the original scaled by 2/3 < 1269805168 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :that's just solving the equation :( < 1269805181 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :it's also a geometric interpretation < 1269805230 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :it's just that you obviously need to solve the equation to find out how long the whole segment should be < 1269805330 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :if you use triangles you'll need to take the square root of 2/3 to get the right area < 1269805407 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric : it's weird that you can prove ~~~~P -> ~~P without LEM... < 1269805424 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :oh and that is essentially the galois connection stuff again < 1269805466 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :lol I did an induction on an (impossible) natural < 1269805471 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :and it simply gave me no assumptions < 1269805473 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :empty induction! < 1269805488 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :(-> P 0) < 1269805530 0 :adam_d_!unknown@unknown.invalid NICK :adam_d < 1269805970 0 :hiato!~fdulu@41.132.216.79 JOIN :#esoteric < 1269806006 0 :hiato!unknown@unknown.invalid QUIT :Client Quit < 1269807090 0 :adam_d!unknown@unknown.invalid QUIT :Ping timeout: 260 seconds < 1269809597 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ACTION has a cool idea < 1269809600 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :stack-based term rewriting < 1269809612 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :great idea Lindenmayer! < 1269809617 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :how did you come up with that < 1269809665 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fuck you :D < 1269809671 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :no but I mean < 1269809675 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :basically the same as tree rewriting languages < 1269809684 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :except it just checks the stack every iteration < 1269809699 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :that way... you don't need parens or anything < 1269809701 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :really simple impl < 1269809716 0 :kar8nga!unknown@unknown.invalid QUIT :Ping timeout: 260 seconds < 1269809717 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :but yet# < 1269809717 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :yet < 1269809720 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :you can do prefix ops < 1269809721 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :and t t < 1269809722 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :-> < 1269809723 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :and < 1269809724 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :and t < 1269809727 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :and t t REWRITE LOL < 1269809728 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :t < 1269809810 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric : Interesting profile. < 1269809811 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric : You appear to be a progressive atheist gay programmer. < 1269809811 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric : Possibly a redditor. < 1269809832 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :progressive?? < 1269809833 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Well, you learned one new thing about yourself. < 1269809840 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :what the fuck is progressive about being a gay atheist < 1269809841 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: fag name for left-winger < 1269809850 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :so wait you hate gays too? :D < 1269809865 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo_: context? < 1269809887 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :of course not < 1269809895 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :how could you even think that < 1269809905 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :well I know you dislike atheism < 1269809918 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :and i don't see how being gay and atheist are not "progressive" for a loose definition < 1269809928 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :and I also don't see that Andy- connected the two < 1269809938 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :so I was assuming you were using {atheist, gay} bad -> not progressive < 1269809941 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :apologies if I am wrong < 1269809946 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :alise_, he wrote a program to get information about an SL user's profile, including group stuff < 1269809948 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :uh I thought progressive means like < 1269809955 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :http://www.mancer.org/sgeo.txt < 1269809956 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :radical new fresh idea < 1269809958 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :or somethin like that < 1269809962 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :as opposed to same old shit < 1269809975 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :SL ?? < 1269809978 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :well gay atheism isn't exactly acceptable in today's society :))) < 1269809979 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :second life < 1269809981 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :fax: sure, but compared to the 1950s, not now >:) < 1269809984 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: no it just means liberal anyway because USA sucks < 1269809992 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise everyone is a gay atheist < 1269810024 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax is pulling a fax :D < 1269810168 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Axiom Too_Lazy : forall P, P. (* Fill in the boring parts of proofs later *) < 1269810234 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ACTION isn't sure whether that is false or tautological < 1269810243 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :false, naturally < 1269810246 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :consider Too_Lazy False < 1269810249 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :: False < 1269810260 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :to spell it out < 1269810263 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :(P : Proposition) -> P < 1269810276 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :P is the proposition, a value of type P is a proof of P < 1269810302 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :hm would forall x:P, P be a tautology then? < 1269810333 0 :anto_ram!anto_ram@85.136.223.42.dyn.user.ono.com JOIN :#esoteric < 1269810366 0 :anto_ram!unknown@unknown.invalid PART #esoteric :? < 1269810403 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :what about forall x:P, x < 1269810462 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ACTION guesses at least the first one is, from what you said < 1269810522 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :you can't do forall x:P, x it's a type error < 1269810526 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :(assuming P : Prop) < 1269810538 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :since x is a 'value' < 1269810561 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ok < 1269810733 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :Incidentally, I'm not gay < 1269810747 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ACTION knew that :P < 1269810804 0 :tombom_!tombom@wikipedia/Tombomp JOIN :#esoteric < 1269810925 0 :tombom!unknown@unknown.invalid QUIT :Ping timeout: 264 seconds < 1269810954 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : hm would forall x:P, P be a tautology then? < 1269810954 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :yes < 1269810956 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :well < 1269810960 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :forall P, forall x:P, P < 1269810966 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :forall x:P, x is wrong yeah < 1269810969 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :since x : P < 1269810982 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric ::P < 1269810983 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :but forall a:b,c is the dependent function arrow b-->c where the b is called a < 1269810988 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :so obviously values don't make any sense there < 1269810990 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo_: well become gay! < 1269810997 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :it's fashionable! < 1269811011 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :ACTION somewhat wishes he could choose to become bi < 1269811050 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Use transsexuals as a bridge! < 1269811082 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :sounds kinky < 1269811122 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric : 8:46:22 [Foonetic] CTCP PING reply from Sgeo_: 1374.449 seconds < 1269811123 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric : 22 minutes, Sgeo < 1269811158 0 :hiato!~fdulu@41.132.216.79 JOIN :#esoteric < 1269811161 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: You can't just say that something sounds kinky, we're talking about sexuality < 1269811175 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Therefore no sexual puns can possibly work. < 1269811176 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Q.E.D. < 1269811227 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :Did you really use QED in a conversation? < 1269811238 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :quite easily done < 1269811280 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :dixon: Yes, Q.E.D. < 1269811288 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Did I offend you, Q.E.D.? < 1269811319 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :No, you just made yourself look like a bigger pop-culture cargo-cult mathematically inept jackass. < 1269811324 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :Are you saying that it's quite easy to offend dixon? [Although oerjan was probably joking] < 1269811334 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :dixon: You're a cunt. :) < 1269811377 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :Quite. < 1269812747 0 :hiato!unknown@unknown.invalid QUIT :Quit: underflow < 1269812889 0 :oklofok!unknown@unknown.invalid PRIVMSG #esoteric :dixon and alise_ should just have some bittersweet sex and get it over with < 1269812911 0 :oklofok!unknown@unknown.invalid PRIVMSG #esoteric :two gay atheists in a big pile of progression < 1269812946 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :Sadly I'm a friendly. < 1269812956 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :lol < 1269812959 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :@ pile of progression < 1269812969 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :so I still have no clue what progressive means < 1269812978 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :probably means something totally specific to americans < 1269812989 0 :oklofok!unknown@unknown.invalid PRIVMSG #esoteric :it's a buzzword, you don't *know* what it means, you use it < 1269813024 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :it means democrat < 1269813068 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :this is so progressive < 1269813227 0 :dixon!unknown@unknown.invalid PRIVMSG #esoteric :It generally means liberal. < 1269813264 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :incidentally the progress party is the most right-wing one in the norwegian parliament < 1269813574 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :ACTION wants a wireless mouse < 1269813595 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :Right now, I'm wrapping the mouse cord around the monitor so it doesn't hang off the table, because hanging off the table results in a pull < 1269813620 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :wireless mouse? hahaha < 1269813626 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :you mean a mouse that turns off by itsself < 1269813640 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :..what? < 1269813654 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :battry < 1269813679 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :wireless mice are horrible; I've tried the worst and the best and they're all just as bad < 1269813682 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Just don't even go there < 1269813692 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :Hm < 1269813698 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :Then I'd like a mouse with a shorter cord < 1269813701 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :Much shorter < 1269813710 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :Fledermausversuch < 1269814014 0 :MigoMipo!unknown@unknown.invalid QUIT :Quit: Konversation terminated! < 1269814437 0 :tombom_!unknown@unknown.invalid QUIT :Quit: Leaving < 1269817185 0 :jcp!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1269817257 0 :jcp!~jw@bzflag/contributor/javawizard2539 JOIN :#esoteric < 1269817817 0 :lament!~lament@S0106001b63f462cc.vc.shawcable.net JOIN :#esoteric < 1269817826 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :the topic is incorrect < 1269818071 0 :coppro!unknown@unknown.invalid QUIT :Quit: Reconnecting… < 1269818107 0 :coppro!~coppro@unaffiliated/coppro JOIN :#esoteric < 1269818533 0 :Leonidas_!unknown@unknown.invalid NICK :Leonidas < 1269819759 0 :MizardX-!~MizardX@unaffiliated/mizardx JOIN :#esoteric < 1269819829 0 :MizardX!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1269819848 0 :MizardX-!unknown@unknown.invalid NICK :MizardX < 1269820256 0 :FireFly!unknown@unknown.invalid QUIT :Quit: Leaving