00:00:01 <fax> oerjan, yeah one of the excercise was: solve the following equation x^2+1
00:00:06 <dixon> 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.
00:00:11 <oerjan> that's not an equation
00:00:18 <alise> fax: is your definition of "one of the atheist people" "someone who doesn't believe in god"
00:00:30 * Sgeo_ is an atheist person.
00:00:33 <dixon> fax: (set it equal to 0 and tell him he's lame)
00:00:59 <lament> do you believe in angels?
00:01:06 <rapido> dixon: uuuh - i need to study your reference to sponge constructions
00:01:12 -!- zzo38 has joined.
00:01:21 <fax> of course, and I beleive in paralell lines too
00:01:23 <oerjan> fax: adding roots of polynomials in that way is a fundamental tool of galois theory iirc
00:01:29 * Sgeo_ does not believe in anything that would commonly be considered to be supernatural.
00:01:41 <dixon> rapido: http://sponge.noekeon.org/
00:01:49 <fax> oerjan, hm
00:01:49 <dixon> http://sponge.noekeon.org/SpongeFunctions.pdf
00:01:50 <rapido> i could believe in god and still find the concept of god to be impossible
00:02:19 <oerjan> although if you are inside the complex numbers to start with, you don't really need to go outside them
00:02:41 <dixon> rapido: They're cryptographic hashes, however.
00:03:03 <rapido> dixon: cryptographic hashes are the only ones i'm considering
00:03:35 <lament> what if you believe in angels but don't believe in god?
00:04:04 <dixon> rapido: But yes, by definition they're surjective when useful and thus have collisions.
00:04:19 <fax> Sgeo what abou gravity
00:04:23 <fax> it's supernatural
00:04:24 <dixon> lament: Then you must've seen my girlfriend.
00:04:26 <rapido> lament: then you would be a flying lunatic with wings
00:04:50 * Sgeo_ blinks a few times
00:04:54 <fax> nobody has explained it yet
00:05:05 <fax> it's like ghosts or ufos or whatever
00:05:25 <oerjan> fax: gravity is a scam by scientists. intelligent falling is the truth!
00:05:39 <Sgeo_> It exists, as demonstratably as possible.
00:05:57 <Oranjer> it's God's Hand Pushing us Down From Eden
00:06:00 <fax> well intelligent falling is a much better explanation by occams razor but it does leave some key questions open
00:06:01 <Sgeo_> Ghosts and UFOs have not been observed by any measurements.
00:06:13 <rapido> dixon: all that i want is a naming service that is scalable
00:06:28 <Sgeo_> rapido, let the name of the proof be the content of the proof.
00:06:31 <oerjan> Oranjer: no that would be more the coriolis force. eden is in the east, iirc
00:06:37 <fax> Sgeo - oh that's true I guess
00:06:43 <zzo38> What doe sthat mean, intelligent falling??
00:06:46 <Oranjer> fax, it is not a better explanation by occams razor
00:06:56 <alise> "Playing with Coq in Jack" -- paper title
00:07:00 <zzo38> The reason otyugh attack with only two tentacles is because one tentacle has three eyes.
00:07:00 <rapido> Sgeo_: but proofs can be huge - think of computer generated proofs
00:07:02 <Oranjer> occams razor refers to the amount of assumptions an explanation requires
00:07:12 <alise> zzo38: intelligent falling is the demonstratable fact that gravity is a lie and all things are actually being pushed down by god individually
00:07:24 <zzo38> alise: That cannot be demonstratable
00:07:25 <fax> alise... how you have possibly managed to find a coq paper I haven't read O_O
00:07:38 <zzo38> Mostly because it doesn't work.
00:08:06 <oerjan> zzo38: http://en.wikipedia.org/wiki/Intelligent_falling
00:08:08 <zzo38> If you want to say God invented gravity, that's different however. Still not provable, though
00:08:24 <Sgeo_> I get the feeling that I should learn Coq
00:08:28 <dixon> Using bigger words make you sound smarter.
00:08:31 <alise> fax: googling for unrelated things
00:08:40 <alise> zzo38: IT WORKS!!!!
00:08:46 <alise> now how do I do nested theorems in coq
00:08:53 <pikhq> See, we don't fall off the earth!
00:09:03 <dixon> Sgeo_: I wouldn't bother. You'd be in the same boat as the Haskellingtons masturbating to the Curry-Howard isomorphism.
00:09:13 * Sgeo_ knows a bit of Haskell
00:09:24 <dixon> HEY LOOK GUYS I CAN PRETEND I'M A MATHEMATICIAN BECAUSE I CAN WRITE PROOFS IN COQ fapfapfapfapfap etc
00:09:31 * Sgeo_ should probably learn what the Curry-Howard isomorphism
00:09:41 <fax> Sgeo it's nothing very deep
00:09:46 <zzo38> alise: What I mean is the proof desn't work.
00:09:53 <fax> Sgeo -- just a notationally similarity between proof systems and type systems
00:09:59 <fax> notational
00:10:03 * oerjan has _never_ masturbated to the curry-howard isomorphism. should i try it?
00:10:14 <dixon> 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.
00:10:20 <rapido> look.... the coq has giving me sign - it's hanging low - it's time to go to bed.... later ...
00:10:40 -!- rapido has quit (Quit: rapido).
00:15:06 <fax> alise: on facebook: Jack Coq Hardi
00:15:06 <fax> Jack Coq Hardi
00:15:07 <fax> Not the Jack Coq Hardi you were looking for? Search more »
00:15:47 <alise> Jacking off Coqs in Jack
00:16:20 <alise> guh, constructing a sigma is a bitch in a coq proof
00:17:00 <fax> alise just give the value and prove it correct using tactics
00:17:12 <alise> yeah but I want to give the value using proof syntax
00:17:28 <alise> 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
00:17:30 <alise> and it's all fffffffffff
00:17:53 <dixon> He couldn't have meant a series?
00:17:58 <oerjan> not that i'm _sure_ alise doesn't know what that is, but...
00:18:47 <oerjan> well, for one thing alise only does constructivist things, i doubt sigma algebras qualify
00:19:21 <alise> you know constructivism isn't some crazy fringe philosophy :)
00:19:29 <fax> yes it is :P
00:19:45 <dixon> And it's a boring one, because it's shit that's been done since the 1800's.
00:21:00 -!- jcp has joined.
00:21:35 <oerjan> dixon: but it's very useful for masturbating to the curry-howard isomorphism, i hear
00:23:06 <dixon> Next all he has to say is he's a finitist
00:23:13 <alise> It may be boring and old but who cares?
00:23:21 * pikhq masturbates to finite sequences
00:23:24 <alise> dixon: fax is a finitist
00:23:33 <alise> you're looking at the wrong person I'm very much a believer in infinities
00:23:55 <dixon> Yeah, but I already think fax is an idiot.
00:24:17 -!- Quadrescence has joined.
00:24:22 <fax> now where did you get THAT idea?
00:25:04 <dixon> Mainly your berating me for not knowing anything 15 minutes after you claimed the exponential function wasn't hypergeometric.
00:25:49 <fax> oh fuck off
00:26:04 <fax> it was long before that
00:26:55 <dixon> 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).
00:27:29 <alise> Perhaps we are using different definitions of constructivist.
00:27:53 <alise> 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.
00:27:54 <zzo38> 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)
00:28:03 <alise> So basically I reject the law of the excluded middle and correspondingly ~~p -> p.
00:28:06 <alise> That isn't really so crazy.
00:29:42 <fax> dixon I wasn't berating you for not knowing anything anyway, you were making some ridiculoulsy stretched joke about 'dixons identity'
00:31:54 <zzo38> 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).
00:32:32 <fax> zzo38 have you read any linear logic?
00:32:58 <zzo38> 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.
00:33:09 <alise> 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.
00:33:19 <alise> You cannot prove them true, you cannot prove them false; it is fine to add their negation, it is fine to add them.
00:33:38 <alise> So if you could say it is true, then the negation would be inconsistent, and vice-versa, yet this is not the case.
00:33:53 <zzo38> alise: There certainly can be things that are neither true nor false.
00:34:24 <ais523> moral dilemma: I followed a link allegedly to Rick Astley rickrolling someone himself
00:34:29 <ais523> and it was actually what it claimed to be, rather than a rickroll
00:34:34 <pikhq> alise: Is'nt the law of the excluded middle about statements that can be derived from the axiomatic system in question?
00:34:34 <ais523> have I been meta-rickrolled?
00:34:36 <fax> wow I want to see it!
00:34:57 <ais523> http://www.youtube.com/watch?v=y4hqv6USkoU
00:35:02 <alise> pikhq: It says that for any given proposition P, I will tell you that either P is true, or P is not true.
00:35:05 <ais523> basically, it was a Thanksgiving Day's parade
00:35:14 <ais523> and he was hiding on one of the floats, and just came out and started singing live
00:35:21 <alise> However, there are things that are neither.
00:35:28 <alise> So the law of the excluded middle is fail.
00:35:52 <pikhq> alise: Tell me one such proposition?
00:36:13 <alise> pikhq: Consider the Continuum Hypothesis.
00:36:16 <ais523> alise: would you say that if X implies Y, and not X implies Y, then Y can be considered to be true?
00:36:18 <alise> ZFC + CH is consistent, as is ZFC + ~CH.
00:36:21 <fax> ais weird lol
00:36:25 <ais523> IMO, that's a weaker situation than the law of the excluded middle
00:36:30 <fax> I don't think it's a rickroll
00:36:34 <zzo38> With tristate logic things can be true, false, or tristate. Pre(P) is true if P is not tristate.
00:36:38 <alise> ais523: p \/ q = (p -> r) -> (q -> r) -> r
00:36:44 <ais523> fax: well, it did /say/ it was a rickroll at the end
00:36:57 <ais523> perhaps this is some sort of meta-meta-rickroll
00:36:58 <alise> p \/ ~p = (p -> r) -> (~p -> r) -> r
00:37:03 <alise> ais523: Answer: No.
00:37:07 <fax> oh it is a rickroll
00:37:11 <ais523> alise: the law of the excluded middle implies that
00:37:17 <alise> pikhq: So, then, how, in plain ZFC, is CH true or false?
00:37:19 <ais523> but, I think it can be true even without
00:37:24 <alise> ais523: no, p or q is literally the same thing
00:37:28 <alise> as (p->r)->(q->r)->r
00:38:02 <alise> \f g porq. case porq of theone x -> f x; theother x -> g x
00:38:10 <alise> \porq f g. case porq of theone x -> f x; theother x -> g x
00:38:19 <alise> that's p\/q -> (p->r)->(q->r)->r
00:38:23 <alise> now the other way:
00:38:31 <ais523> the other way is the way I care about
00:38:47 <alise> (p->r)->(q->r) -> p \/ q
00:39:07 <alise> \f. f theone theother
00:39:17 <alise> filling in the arguments we get
00:39:22 <alise> first is (p -> p \/ anything)
00:39:22 <ais523> alise: you must have typoed somewhere
00:39:28 <oerjan> alise: you are missing -> r
00:39:28 <alise> second is (q -> anything \/ q)
00:39:37 <alise> the implementation is right
00:39:42 <alise> fill in p and q for the respective anythings
00:40:09 <zzo38> 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.
00:40:13 <pikhq> alise: Clearly, the veracity of CH is a boolean.
00:40:15 <ais523> hmm, I always get confused trying to follow nonstandard models of logic
00:40:33 <pikhq> That the value of the boolean cannot be determined is beside the point.
00:40:36 <ais523> in one seminar I went to, someone quantified over all systems of logic, which was /really/ confusing
00:40:40 <alise> Prelude> let or2f porq f g = case porq of Left x -> f x; Right x -> g x
00:40:40 <alise> Prelude> let f2or f = f Left Right
00:40:40 <alise> Prelude> :t (or2f, f2or)
00:40:40 <alise> :: (Either t t1 -> (t -> t2) -> (t1 -> t2) -> t2,
00:40:41 <alise> ((a -> Either a b) -> (b1 -> Either a1 b1) -> t11) -> t11)
00:40:44 <oerjan> alise: you had an implied forall r in there
00:40:51 <alise> ais523: Since I have proved that (P->Q) and (Q->P), P is equivalent to Q.
00:40:54 <ais523> pikhq: booleans have /nine/ values, 01XLHWZU-
00:41:11 <alise> Well, f2or actually needs a more specific type, but.
00:41:20 <ais523> ANY LANGUAGE IN WHICH BOOLEANS HAVE FEWER THAN NINE POSSIBLE VALUES IS DEFICIENT
00:41:23 <pikhq> ais523: Then we are clearly discussing the law of the excluded 10th.
00:41:25 <ais523> btw, I'm not sure which one maps to file_not_found
00:41:38 <alise> <pikhq> alise: Clearly, the veracity of CH is a boolean.
00:41:41 <oerjan> ((p->(p\/q))->(q->(p\/q))->(p\/q)) -> (p\/q)
00:41:43 <ais523> fax: have you decided whether that was a rickroll or not yet?
00:41:59 <alise> pikhq: ZFC + CH is consistent iff ZFC is consistent. ZFC + ~CH is consistent iff ZFC is consistent.
00:42:08 <alise> In ZFC, CH can neither be true nor false.
00:42:18 <alise> If we can prove it true, then ZFC + ~CH would be inconsistent.
00:42:23 <alise> If we can prove it false, then ZFC + CH would be inconsistent.
00:42:25 <pikhq> In ZFC, CH cannot be shown to be true or false.
00:42:28 <ais523> I think I've caused a logical gap in rickrollness
00:42:29 <alise> It is neither true nor false.
00:42:38 <alise> pikhq: But it has some platonic "real truth"?
00:42:49 <alise> That's metaphysical mumbojumbo: you are talking about things in the system that are not from the axioms.
00:42:49 -!- BeholdMyGlory has quit (Remote host closed the connection).
00:42:53 <fax> ais523, I am not really sure
00:43:01 <alise> You are referring to some platonic space of "ZFC truths" but no such thing exists, just manipulation of the axioms.
00:43:06 <alise> Are you sure you want to go down this path>
00:43:10 <ais523> fax: hmm, so you're metaundecided?
00:43:11 <zzo38> Please explain what the nine boolean values 01XLHWZU- are meant for.
00:43:57 <ais523> 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
00:44:19 <ais523> VHDL actually implements all these
00:45:05 <pikhq> alise: It certainly has no "platonic real truth". It just simply can be said to be one of true or false.
00:45:38 <alise> So suppose it is true.
00:45:44 <alise> Then ZFC + ~CH is inconsistent.
00:45:47 <alise> So suppose it is false.
00:45:50 <alise> Then ZFC + CH is inconsistent.
00:45:58 <alise> But we know that ZFC plus either CH or ~CH is consistent iff ZFC is.
00:46:00 <pikhq> So it cannot be both true and false.
00:46:06 <alise> It cannot be either.
00:46:12 <alise> Because *both systems are consistent*.
00:46:27 <alise> pikhq: OK, let us say that in ZFC, we have proved CH.
00:46:34 <zzo38> I didn't know VHDL implements those. But I suppose it is possible.
00:46:41 <alise> We know that ZFC + ~CH is consistent iff ZFC is. Yet we have CH and ~CH.
00:46:54 <alise> Reverse it to see that it cannot be false, either.
00:47:06 <alise> You can keep running around in circles, but the only real solution is to reject the excluded middle.
00:47:26 <pikhq> alise: "We know that ZFC + ~CH is consistent iff ZFC is. Yet we have CH and ~CH." Uh... Wha?
00:47:38 <alise> OK, let me spell it out for you.
00:47:52 <pikhq> Near as I can tell, "proving CH in ZFC" would imply that ZFC + ~CH is inconsistent.
00:48:23 <pikhq> And assuming the proof that ZFC + ~CH is consistent is valid, then clearly you cannot prove CH in ZFC.
00:48:54 <dixon> and if you did both, then it would show ZFC is not consistent.
00:49:03 <dixon> because that's a contradiction
00:49:16 <alise> 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.
00:49:18 <alise> 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.
00:49:18 <alise> 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.
00:49:25 <alise> Therefore, CH cannot be true and it cannot be false.
00:49:44 <pikhq> alise: You have proven that CH cannot be proven in ZFC.
00:49:44 <alise> Although we cannot use this to disprove excluded middle from inside ZFC, because it is a meta issue, it is still present.
00:49:48 <alise> Excluded middle is false.
00:49:53 <alise> pikhq: No, I made no references to proofs in the above.
00:49:57 <pikhq> Clearly it can be one or the other; you can use it as an axiom.
00:50:01 <alise> The law of the excluded middle means that ONE must be true.
00:50:19 -!- Quadrescence has quit (Read error: Connection reset by peer).
00:50:21 -!- Quadresce` has joined.
00:50:44 -!- Quadresce` has changed nick to Quadrescence.
00:51:25 <dixon> 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.
00:51:39 <zzo38> Is "false unless contradicted" in a digital circuit like a pull-down resistor?
00:52:01 <pikhq> 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."
00:54:00 <Sgeo_> If ~CH in ZFC, how do you get CH?
00:54:23 <Sgeo_> n/m, I agree with pikhq
00:54:53 <alise> Well, this has taught me something: Never bother trying to talk about excluded middle.
00:55:03 <alise> People are absolutely sure it is true at any cost.
00:55:52 <pikhq> People don't like the implication that you could define the following: ZFC + CH & ~CH. :P
00:57:53 <dixon> Without realizing that proving both at the same time shows ZFC's inconsistency.
01:02:26 <zzo38> Off topic: Have you ever invented any spell/power for D&D game?
01:02:39 -!- FireFly has quit (Quit: Leaving).
01:03:08 <alise> dixon: Of course it does.
01:04:24 <dixon> Then it says nothing about CH...
01:04:49 <dixon> And your whole law of the excluded middle being false idea is inane with that example.
01:05:19 <oklopol> "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
01:06:43 <alise> imagine filling the entire universe with one 16 bit pattern, say
01:07:04 <alise> 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
01:08:27 <oklopol> 1. you would probably be pretty surprised if you suddenly turned into an elephant, too, that's not what physically impossible means
01:09:36 <alise> well i guess i could start enumerating every single way a bit could be flipped :)))
01:14:48 <oklopol> it's pretty stupid to claim computers can't make errors
01:14:50 <zzo38> It is difficult to repair a watch while falling from an airplane.
01:15:09 <oklopol> of course they can make errors
01:15:35 <oklopol> some unicorns can turn bits with their tongues from miles away
01:15:39 <alise> I never claimed that
01:15:58 <oklopol> but if you thought that was true, you might
01:16:09 <oklopol> can't really unclaim that one huh
01:17:37 <zzo38> I recently added something to esolang wiki
01:22:29 -!- zzo38 has quit (Quit: ERR_QUIT).
02:35:16 <oklopol> 02:22… zzo38 has quit IRC (Quit: ERR_QUIT)
02:35:34 <oklopol> it was all sorts of funny stuff
02:35:57 <oklopol> but i actually am going to sleep now ->
02:36:36 <fax> oklopol :)
02:36:49 <fax> I have an idea about this OR thing
02:36:55 <fax> but it's probably wrong
02:36:59 <fax> I'll try it out tommorow
02:37:23 -!- oerjan has quit (Quit: Tomorrow OR not tomorrow, that's the question).
02:46:49 <alise> [["Anime is a prime example of why two nukes wasnt enough." - NH Democrat State Rep., Nick Levasseur]]
02:47:37 * Sgeo_ .. doesn't like nor dislike anime
02:47:57 <alise> That's rather orthogonal to the hilarious extremity of bad taste found in that quote :P
02:47:58 <Sgeo_> It's just another medium, albeit one for which there's a .. website that lets me watch for free
02:57:27 <pikhq> It's just another medium, albeit one which is generally made in a language that I happen to be studying. :P
02:58:22 <dixon> ANATA WA BAKA DESU ZO
02:58:47 <alise> dixon: you violated the syntax anime := desu | anime anime
02:58:51 <pikhq> dixon: That's quite formal of you.
02:58:54 <alise> do not pass go do not collect 200 pounds
02:59:25 <dixon> Why would I collect pounds? I'm an American, we're fat enough.
02:59:44 <pikhq> Try something more like 馬鹿ぜ、あんた！(baka ze, anta
03:00:18 <dixon> Really? I was going for the "You sir, are an idiot!" meme.
03:00:49 <pikhq> Oh, *that's* what you were going for?
03:01:47 <dixon> My Japanese is flaky, but yes.
03:02:58 -!- adu has joined.
03:03:04 <alise> pikhq: Please translate this to exquisitely formal Japanese: "Your asshole is a skyscraper-sized orifice which receives bread daily, fuckwit."
03:03:26 <alise> Someone has to have translated that already, it being such a common insult.
03:03:30 <alise> Is that even an insult? I can't tell.
03:04:16 <dixon> Whoa, he gets free bread?
03:04:20 <pikhq> Try more of Pikhqどのはお馬鹿で御座るとお思いになります。(Pikhq dono wa baka de gozaru to o-omoi ni narimasu)
03:04:27 <pikhq> ... I *think*. My keigo sucks.
03:04:47 <alise> dixon: NO COST AT ALL
03:05:08 <Sgeo_> alise, is that a quote from SL?
03:05:18 <alise> Have you heard it before or something? XD
03:05:35 <Sgeo_> No, but it sounds like the sort of thing a certain character might say
03:05:42 <pikhq> alise: Sadly, I know not the vocab for that.
03:05:48 <Sgeo_> I'm not saying the full name of it in the presence of a minor
03:05:53 <pikhq> alise: I shall let you know when I can translate that, though.
03:06:04 <alise> Sgeo_: Does it have RUDE WORDS in it????
03:06:12 <Sgeo_> It has naked people and sex in it
03:06:17 <alise> OH NOOOOOOOOOOOOOOOO
03:06:42 <alise> 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.
03:06:48 <alise> Anyway, since when do I have Second Life installed?
03:06:56 <Sgeo_> alise, SL != Second Life in this case
03:07:12 <alise> Oh, that webcomic.
03:08:47 <alise> 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
03:08:58 <alise> Again, FORMAL AND POLITE!
03:09:45 <pikhq> alise: "Fuck You".
03:12:50 <pikhq> Fine, I'll give you a shockingly rude statement instead. 私は日本人達を殺したい。なぜ？アジア人が大嫌い！
03:13:41 <pikhq> That is probably the most racist thing I have ever typed, in jest or otherwise.
03:13:58 <Sgeo_> Translate it! Translate IT!
03:14:35 <pikhq> "I want to kill all Japanese. Why? I hate Asians!" Now, alise. Say it to every Japanese person you meet. :P
03:15:08 <pikhq> （watashi wa nihonjintachi wo korositai. naze? ajiajin ga daikirai!）, BTW
03:15:50 <alise> 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.
03:16:22 <pikhq> "Nigger" is untranslatable.
03:16:40 <alise> why not, do all japs love nigs or sth
03:16:54 <pikhq> It is a term that literally only exists in English.
03:17:25 <pikhq> The closest you can get in Japanese is "gaijin". Which... Refers to everyone other than Japanese.
03:17:42 <Sgeo_> I have a friend who ran in a marathon!
03:19:46 <Sgeo_> "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."
03:20:04 <fax> I GET IT!!
03:25:47 <adu> pikhq: 君は日本人ですか？
03:26:17 <pikhq> adu: いいえ。僕は日本語を勉強する人です。
03:27:10 <adu> pikhq: あ、わかた
03:28:12 <pikhq> 今漢字を勉強してます。1810字を知って、232字を勉強するつもりです。
03:28:31 <pikhq> ちょっと難しいです。でも、面白いと思います。
03:28:52 <adu> pikhq: 僕も日本人が大嫌い
03:31:57 <adu> 僕は６年かん日本にすんでいました。
03:33:07 <adu> でも、たくさんわすれた
03:34:06 <pikhq> 4年間高校で日本語を勉強しました。この後、２年間勉強しなくて、いまもっと勉強を始めてます。
03:35:34 <adu> そですか？すごい！がんばってね
03:36:14 <adu> lol i've never seen sed and japanese used together
03:37:15 <adu> どもありがと Mr. ロボト
03:41:07 <pikhq> aduさんがなぜ日本に住んでいましたかな。
03:42:03 <adu> ぶくも, but i've been away for 10 years, so i've forgotten so much
03:42:14 <alise> I'm going to bed now.
03:42:21 <alise> Cheerio, fellows. See you tomorrow.
03:42:22 <adu> alise: night
03:42:25 -!- alise has quit (Quit: Leaving).
03:43:21 <pikhq> 日本語で、「僕も、でも10年間住まなくて、たくさん忘れた」と思います。
03:44:16 <adu> sounds about right
03:47:12 <adu> 僕の日本語は悪いです。
04:01:45 -!- ais523 has set topic: 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.
04:01:50 -!- fax has quit (Quit: Lost terminal).
04:22:15 -!- MizardX has quit (Ping timeout: 276 seconds).
04:46:18 <uorygl> It's incorrect and will remain incorrect forever.
04:53:27 -!- jcp has quit (Quit: I will do anything (almost) for a new router.).
05:29:53 -!- jcp has joined.
05:39:30 -!- adu has quit (Quit: adu).
05:53:08 -!- Oranjer has left (?).
06:55:55 -!- jcp has quit (Quit: I will do anything (almost) for a new router.).
07:04:12 -!- coppro has joined.
07:59:59 -!- clog has quit (ended).
08:00:00 -!- clog has joined.
08:57:45 -!- lifthrasiir has quit (Ping timeout: 258 seconds).
08:59:03 -!- lifthrasiir has joined.
09:04:07 -!- lifthrasiir has quit (Ping timeout: 268 seconds).
09:51:13 -!- ais523 has quit.
10:04:09 -!- Quadrescence has quit (Remote host closed the connection).
10:05:30 <AnMaster> me looks up at the non-latin script
10:05:33 * AnMaster looks up at the non-latin script
10:06:13 <AnMaster> <alise> groan <-- you don't like Discworld books then I assume?
10:06:44 <AnMaster> dixon, sure, but not for it's own sake
10:07:08 <AnMaster> it is very nice when you actually have a reason to use it though
10:08:17 * AnMaster really should try to figure out why mapping pi onto compose p i didn't work out
10:12:24 -!- adam_d has joined.
10:17:06 -!- BeholdMyGlory has joined.
10:31:40 <AnMaster> dixon, you know the compose key?
10:32:12 <dixon> I don't have such a fancy thing.
10:32:41 <AnMaster> well usually you need to enable it in some settings
10:32:51 <AnMaster> also I never seen it on non-*nix systems
10:34:09 <AnMaster> dixon, it allows you to press that key you made your compose key then press two other keys
10:34:41 <AnMaster> (though that specific one is also on altgr-m for me)
10:34:51 <dixon> Yes, I know. I'm running *nix, I just don't use it.
10:35:17 -!- FireFly has joined.
10:35:28 <AnMaster> dixon, thing is I want compose p i to give me the unicode pi
10:35:45 <AnMaster> and well, for some reason something is ignoring my config file for it
10:35:59 <dixon> need to restart X or something?
10:36:11 <AnMaster> dixon, done that since when I added the file
10:36:30 <AnMaster> but yeah ~/.XCompose doesn't seem to be used, though docs indicate it should work
10:37:33 <dixon> leave it up to the X people to not update their docs
10:37:53 <AnMaster> dixon, oh? you found something indicating it works differently nowdays?
10:38:08 <AnMaster> dixon, the weird thing is that it worked for someone else in here (forgot who)
10:38:53 <dixon> Naw, I have no idea why it doesn't work. :\
10:39:16 <dixon> but there is a chance that the docs aren't up to date
10:39:54 -!- oerjan has joined.
10:42:05 <dixon> http://www.mail-archive.com/vague@list.uvm.edu/msg03505.html
10:42:15 <dixon> dunno if that helps
10:45:58 -!- Phantom_Hoover has joined.
10:47:10 <dixon> It's obvious the tape isn't infinitely long.
10:47:13 <dixon> What a piece of shit.
10:47:45 <Phantom_Hoover> And there are around 1000 feet of tape, so it's practically infinite.
10:48:18 <Phantom_Hoover> I.e. if you wanted to do any calculations involving more cells than that you'd really just use a computer.
10:49:16 <dixon> Glad to hear you think 1000 feet is "practically infinite"
10:49:32 <dixon> Means my penis is up there on the list.
10:50:02 -!- Phantom_Hoover has quit (Client Quit).
10:50:53 <dixon> There difference between a math student and a computer science student is a sense of humor.
11:10:09 -!- tombom has joined.
11:24:53 -!- fax has joined.
11:33:45 -!- Phantom_Hoover has joined.
11:50:11 -!- adam_d has quit (Ping timeout: 260 seconds).
12:19:06 -!- oerjan has quit (Quit: leaving).
13:13:50 -!- fax has quit (Quit: Lost terminal).
13:14:20 <oklopol> which one has a sense of humor?
13:15:47 <oklopol> i'm both and i both do and don't have a sense of humor, i think
13:16:07 <oklopol> so in either case, you might be right
13:21:47 -!- cheater2 has joined.
13:23:19 -!- cheater has quit (Ping timeout: 276 seconds).
13:28:06 <oklopol> but it has a bit too much technology in it to be absolutely superawesome
13:28:08 <Phantom_Hoover> Unfortunately, my life is now going to be unfulfilled until I acquire or build one.
13:49:32 -!- Phantom_Hoover has quit (Quit: ChatZilla 0.9.86 [Firefox 3.5.8/20100214235838]).
13:52:43 -!- alise has joined.
13:54:02 <alise> /r/programming is fucking useless; the idiot Ted Dziuba taking the first spot.
13:54:37 <alise> 02:06:44 <AnMaster> dixon, sure, but not for it's own sake
13:54:43 <alise> What, the Japanese or the what?
13:54:47 <Deewiant> I upvoted it for generating discussion, whether or not it's sensible.
13:55:30 <alise> 02:36:30 <AnMaster> but yeah ~/.XCompose doesn't seem to be used, though docs indicate it should work
13:55:33 <alise> you need to do stuff
13:55:52 <alise> Deewiant: Discussion of the most trivial, boring stuff - the kind Dziuba usually generates.
13:56:18 <alise> 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.
13:56:43 <alise> 02:47:10 <dixon> It's obvious the tape isn't infinitely long.
13:56:43 <alise> 02:47:13 <dixon> What a piece of shit.
13:56:54 <alise> You fail; only some Turing machines have infinite tape.
14:01:55 <Slereah> Turing machines have infinite tapes
14:02:02 <Slereah> Otherwise, they would not be Turing machines!
14:04:30 <alise> Hmm, but there are non-universal turing machines, no?
14:04:35 <alise> I guess maybe they have infinite tape anyway.
14:10:42 <oklopol> of course there are non-universal turing machines
14:10:53 <oklopol> for instance the empty turing machine is pretty non-universal
14:11:00 <oklopol> :PPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPP
14:13:02 -!- MigoMipo has joined.
14:24:53 -!- Guest39936 has joined.
14:26:11 -!- Guest39936 has left (?).
14:36:20 <alise> Global tuple space!
14:37:08 <oklopol> i used to love that crazy thing
14:38:41 <alise> global tuple space?
14:40:18 <alise> seems a bit too ... unesoteric for you, i mean in your fun definition of esoteric
14:40:21 <alise> but why don't you love it any more
14:40:37 <alise> K has a global tuplespace... it's hot
14:40:46 <oklopol> i haven't touched one in ages
14:41:01 <oklopol> love fades fast as they say
14:42:32 <alise> i mean i'm just imagining like... one gigantic trie/graph/thing
14:42:32 <alise> and that is everything
14:54:28 -!- alise_ has joined.
14:57:07 -!- alise has quit (Ping timeout: 258 seconds).
15:02:37 -!- MizardX has joined.
15:24:48 <alise_> sometimes I end up with
15:24:50 <alise_> ============================
15:25:00 <alise_> and I'm not entirely sure how it wants me to prove that 1 = 0 is impossible...
15:30:25 <alise_> Today on "ridiculously trivial proofs": There exists a natural n such that S (pred n) <> n (because pred 0 = 0 in Coq).
15:30:27 <alise_> http://pastie.org/892089.txt?key=mjqv5f7o9cbvwfvjih18a
15:30:35 <alise_> apply ex_intro with 0.
15:31:20 <alise_> Really it's a disproof of 1 = 0.
15:31:28 <alise_> Because I just plugged in the value then told it to shut up and compute S (pred n) and n. :)
15:33:47 <alise_> Actually I don't think auto did anything there...
15:36:14 <alise_> Yeah, I could have produced that with just:
15:36:16 <alise_> apply ex_intro with 0.
15:37:54 <alise_> If I used discriminate instead of the more advanced congruence, I'd get:
15:38:11 <alise_> http://pastie.org/892094.txt?key=sygsuuuwz1tnauvsksvw5q
15:38:31 <alise_> (That's from apply ex_intro with 0. compute. intros H. discriminate.)
15:38:55 <alise_> Which can also be produced with:
15:38:58 <alise_> apply ex_intro with 0.
15:39:04 <alise_> So that's the shortest, simplest proof.
15:45:15 <alise_> Now I'm trying to prove (~ exists n, forall m, n >= m); it's surprisingly difficult.
15:45:52 <oklopol> for exists, you need a specific counterexample, so take succ n, then just use succ n > n for all n
15:46:08 <alise_> well of course it is easy, it's just expressing it in the tactics engine
15:46:12 <alise_> without really knowing what tactics to use...
15:46:20 <alise_> I could do it as a lambda expression, probably, with equality induction
15:46:24 <alise_> but it'll be shorter as tactics
15:46:31 <alise_> and lambda expression proofs get unwieldy fast, they're like bytecode
15:46:47 <alise_> H : forall m : nat, 0 >= m
15:46:48 <oklopol> right i don't know anything about tactics. well except that they can magically do things for you
15:46:48 <alise_> ============================
15:46:50 <alise_> nobiggest < apply (H 1).
15:46:50 <alise_> Toplevel input, characters 0-11:
15:46:55 <alise_> Error: Impossible to unify "0 >= 1" with "False".
15:47:08 <alise_> oklopol: basically they search for stuff with certain types in the environment then apply them using various different already-proved theorems
15:47:12 <alise_> to try and prove the current goal
15:47:33 <alise_> 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
15:47:51 <alise_> 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
15:47:59 <alise_> oklopol: one issue is that tactics automatically introduce variables with names they like
15:48:09 <alise_> so reading it without seeing the transcript, random "H3"s just appear out of nowhere :)
15:49:10 <alise_> Maybe I'll prove forall n, exists m, m > n, then prove ~ exists n, forall m, n >= m from that.
15:49:55 <alise_> ============================
15:50:17 <alise_> here's my documentation for auto: "does something helpful, or does something unhelpful, or does nothing".
15:50:27 <alise_> oklopol: it tries to magically prove whatever for you
15:50:29 <alise_> it isn't very good at it
15:50:40 <alise_> apply ex_intro with (S n).
15:50:46 <alise_> fun n : nat => ex_intro (fun m : nat => m > n) (S n) (le_n (S n))
15:50:46 <alise_> : forall n : nat, exists m : nat, m > n
15:52:03 <alise_> H : forall m : nat, x >= m
15:52:03 <alise_> ============================
15:56:47 <alise_> H1 := H (S x) : x >= S x
15:57:18 <alise_> basically... take this object, deconstruct it into its components
15:57:23 <alise_> which depends on what it is
15:57:29 <alise_> in this case I'm destructing the inequality into the environment
15:57:35 <alise_> so that the same implications hold, but it's folded into other things
15:57:39 <alise_> rather than a separate object
15:57:52 <alise_> with e.g. a tuple (x,y) it'd introduce two values, x and y
15:58:01 <alise_> they're tactics... they don't really have precise semantics :)
15:59:37 <alise_> lol disproving x >= S x is so hard
15:59:45 <alise_> there must be some lemma for x >= y -> x <> y
15:59:52 <alise_> then I could use discriminate
16:01:23 <alise_> Theorem gt_Sn_n : forall n, S n > n.
16:01:33 <alise_> Hint Resolve gt_Sn_n: arith v62.
16:04:43 <alise_> H : forall m : nat, x >= m
16:04:43 <alise_> H1 := H (S x) : x >= S x
16:04:43 <alise_> ============================
16:05:03 -!- lament has quit (Ping timeout: 252 seconds).
16:05:15 <alise_> proving False from this is stupidly hard...
16:08:22 -!- lament has joined.
16:08:28 <alise_> now we're getting somewhere
16:20:36 <alise_> I'm just doing it the general abstract nonsense way -
16:20:59 <alise_> Prove (forall x, P x) -> ~(exists x, ~P x)
16:21:35 <alise_> then apply that to alwaysbigger
16:21:36 <alise_> (alwaysbigger : forall x, exists y, y > x) so we get ~(exists x, ~exists y, y > x).
16:21:46 <alise_> fun (A : Type) (P : A -> Prop) (H : forall x : A, P x)
16:21:46 <alise_> (H0 : exists x : A, ~ P x) =>
16:21:46 <alise_> | ex_intro x H1 => let H2 := H x in False_ind False (H1 H2)
16:21:47 <alise_> : forall (A : Type) (P : A -> Prop),
16:21:49 <alise_> (forall x : A, P x) -> ~ (exists x : A, ~ P x)
16:22:00 <alise_> Pretty easy proof, it has to be said.
16:26:55 <alise_> lol auto worked in coqtop but not here...
16:29:17 <dixon> Write it in LaTeX.
16:29:18 <alise_> oh because I inverted it lol
16:33:37 <AnMaster> <alise> you need to do stuff <-- what stuff?
16:35:55 <alise_> Darn, I can't turn ~ exists ~ -> forall.
16:36:44 <alise_> Because that's excluded middle.
16:36:44 <alise_> AnMaster: It's like some sort of include thing and some sort of config file change and thingy; I forget.
16:36:44 <alise_> I have ~ exists n, ~ exists m, m > n which is, you know, close.
16:37:10 -!- Gracenotes has quit (Quit: Leaving).
16:38:17 -!- kar8nga has joined.
16:41:56 <alise_> 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.
16:42:00 <alise_> gawd, why didn't I know of this before
16:50:19 * alise_ looks for (m <= n) -> (m <= S n)
16:52:26 -!- lifthrasiir has joined.
16:52:47 <alise_> H : forall m : nat, S x >= m
16:52:47 <alise_> IHx : (forall m : nat, x >= m) -> False
16:52:48 <alise_> ============================
16:52:51 <alise_> man go fuck yourself :P
16:55:46 <dixon> alise_: Write it in LaTeX without using a tool to do it for you.
16:56:06 <alise_> dixon: But the proof is trivial; all I am trying to do is get used to Coq.
16:56:35 <alise_> Typesetting is not what I am trying to do.
16:57:58 <alise_> H : forall m : nat, 1 >= m
16:57:59 <alise_> ============================
16:57:59 <alise_> forall m : nat, 0 >= m
16:58:04 <alise_> i am doing this all wrong
17:00:16 <alise_> H : forall m : nat, S (S x) >= m
17:00:16 <alise_> IHx : (forall m : nat, S x >= m) -> False
17:00:16 <alise_> IHx0 : (forall m : nat, S x >= m) ->
17:00:16 <alise_> ((forall m : nat, x >= m) -> False) -> False
17:00:16 <alise_> ============================
17:00:20 <alise_> I have a feeling Coq is trying to get me to do an infinite induction manually
17:04:58 -!- lament has quit (Ping timeout: 240 seconds).
17:08:05 -!- adam_d has joined.
17:12:14 <FireFly> <alise_> man go fuck yourself :P
17:12:14 <FireFly> <AnMaster> alise_, hm okay
17:12:16 <alise_> Not using tactics - only partly - though.
17:12:20 <FireFly> What was the syntax for that quote bot?
17:13:12 <alise_> http://pastie.org/892210.txt?key=ir8pgxsvdnexhfoifnvvpg
17:13:17 <alise_> FireFly: `addquote ...
17:13:34 <FireFly> `addquote <alise_> man go fuck yourself :P <AnMaster> alise_, hm okay <AnMaster> bbl
17:14:34 <alise_> Theorem No_biggest_3 : ~ exists n, forall m, n >= m.
17:14:34 <alise_> apply (Not_bigger_than_successor H0).
17:14:39 <alise_> I could fold in Not_bigger_than_successor if I wanted...
17:15:59 <alise_> fun H : exists n : nat, forall m : nat, n >= m =>
17:15:59 <alise_> let H1 := H0 (S x) in let H2 := gt_Sn_n x in le_not_lt (S x) x H1 H2
17:16:00 <alise_> : ~ (exists n : nat, forall m : nat, n >= m)
17:16:27 <alise_> 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.
17:18:52 <alise_> 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.
17:19:10 <alise_> All the 0 people who believe that infinity is a natural number have been thoroughly debunked! Ha!
17:19:16 <alise_> That was such a waste of time.
17:19:27 <uorygl> There are more than 0 people who believe that.
17:19:56 <alise_> From Talk:Hereditarily finite set, archived from Votes for DEletion:
17:19:57 <alise_> "Hereditarily finite set. Strange maths stuff. Makes no sense. Angela 00:52, Oct 2, 2003 (UTC)"
17:20:07 <alise_> Angela being the Wikia founder.
17:20:39 <dixon> wat, u mean I can't just do S(n)
17:20:59 <uorygl> Hey, "hereditarily finite set" alternates vowels and consonants.
17:21:46 <dixon> my proof is shorter. suckaaaaaaaaa
17:21:48 <alise_> but that just gives you n >= S n... so then you have to disprove that
17:21:58 <uorygl> Well, to be fair, when she nominated it for deletion, the article's text was this:
17:22:02 <alise_> which you do by asserting that S n > n, using the existing theorem for that, then using the theorem that contradicts the two
17:22:06 <dixon> ... n can't be >= S(n)
17:22:14 <uorygl> "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$"
17:22:16 <alise_> and there can't be a finite number of primes
17:22:52 <alise_> dixon: Of course it is very easy to package the fact that ~ n >= S n up into one theorem.
17:22:59 <alise_> Theorem Not_bigger_than_successor {n} : ~ n >= S n.
17:23:00 <alise_> assert (H0 : S n > n).
17:23:00 <alise_> apply (le_not_lt (S n) n).
17:23:15 <alise_> 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.
17:23:26 <dixon> Or you could just reference Peano's axioms.
17:24:23 <alise_> Peano's axioms don't actually define greaterthan, less than, etc, for a start.
17:25:28 <dixon> We can define less than using them. If m = S^n(x) for some natural n, then m > x
17:25:37 <alise_> Which is something you have to prove.
17:25:46 <alise_> You can't just say "this is true" because if you did that nothing would need a proof.
17:25:55 <dixon> I can define it as true.
17:25:56 <alise_> Anyway -- if I used "auto with arith" it could do all this automatically.
17:26:07 <alise_> dixon: Then congratulations, you created an axiom.
17:26:21 <alise_> Too lazy to avoid doing work, heh.
17:26:33 <alise_> Anyway, yes, of course, there is a tactic to automatically prove this sort of stuff for you in one statement.
17:26:43 <alise_> But I'm trying to learn how to use Coq, not how to ask Coq to prove everything for me.
17:26:55 <alise_> If you just want to dis Coq as being a verbose waste of time you could just do that directly :P
17:27:25 -!- kar8nga has quit (Remote host closed the connection).
17:27:30 <dixon> 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.
17:27:42 <alise_> Haskell can't even prove things.
17:27:51 <alise_> So lumping it in with Coq is ridiculous.
17:28:09 <alise_> dixon: Well, for a start, it can prove anything (using undefined); for a second, its propositions are boolean-returning functions, not actual types.
17:28:21 <alise_> And Axiom is a computer algebra system, not a proof assistant.
17:28:26 <dixon> Curry-Howard isomorphism.
17:28:53 <dixon> And I'm well-aware what Axiom is, but it has a language packaged with it called Aldor.
17:28:56 <alise_> - is clearly something you know nothing about; it addresses the simply-typed lambda calculus, which has no _|_.
17:28:56 <alise_> So - do you consider the proof of the four-colour theorem "pseudo-math"?
17:29:03 <alise_> Is it pseudo-math just because a computer did it?
17:30:56 -!- jcp has joined.
17:32:40 <dixon> 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.
17:32:59 <alise_> Well, yes, you can prove things in Haskell, but it is an inconsistent system.
17:33:25 <alise_> Yes - you can do `data Z; data S n`, then meticulously define operations on it, then construct values to prove it.
17:33:30 <alise_> But you can prove anything you want: "undefined".
17:33:33 <uorygl> That depends on how you define "a mathematician".
17:33:44 <alise_> It is a proof system only in the most pathological sense, and even then it is blatantly inconsistent.
17:33:51 <alise_> And I never claimed I was a mathematician because I fuck around with Coq.
17:34:06 <dixon> uorygl: Think Newton.
17:34:22 <alise_> 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.
17:34:54 <alise_> If you do not agree then you're just an elitist scared of some random nobody doing anything worthwhile.
17:35:05 -!- Quadrescence has joined.
17:35:11 <uorygl> So a mathematician is a person who invents new fields of mathematics and discovers novel applications of it?
17:35:37 <alise_> Or even just a person who discovers novel results about existing fields.
17:35:43 <AnMaster> uorygl, I would say far from all mathematicians manage to invent a new field of mathematics.
17:35:49 <alise_> A mathematician is someone who explores mathematics and shows up previously unknown things in its depths.
17:35:58 <AnMaster> some could refine an already existing field
17:36:12 <alise_> 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.
17:36:18 <AnMaster> alise_, correction: s/mathematician/successful mathematician/ :P
17:37:13 <AnMaster> (my finger was on enter when your last line arrived)
17:41:26 -!- MigoMipo has quit (*.net *.split).
17:43:09 -!- pikhq has quit (*.net *.split).
17:43:09 -!- yiyus has quit (*.net *.split).
17:43:09 -!- alise_ has quit (*.net *.split).
17:43:09 -!- Gregor has quit (*.net *.split).
17:43:09 -!- olsner has quit (*.net *.split).
17:43:09 -!- adam_d has quit (*.net *.split).
17:43:10 -!- uorygl has quit (*.net *.split).
17:43:10 -!- ineiros has quit (*.net *.split).
17:43:10 -!- tombom has quit (*.net *.split).
17:43:10 -!- mtve has quit (*.net *.split).
17:43:10 -!- SimonRC has quit (*.net *.split).
17:43:10 -!- Quadrescence has quit (*.net *.split).
17:43:10 -!- jix has quit (*.net *.split).
17:43:10 -!- pineapple has quit (*.net *.split).
17:43:10 -!- rodgort has quit (*.net *.split).
17:43:10 -!- chickenzilla has quit (*.net *.split).
17:43:10 -!- jcp has quit (*.net *.split).
17:43:10 -!- EgoBot has quit (*.net *.split).
17:43:10 -!- HackEgo has quit (*.net *.split).
17:43:10 -!- cal153 has quit (*.net *.split).
17:43:11 -!- MaXo2 has quit (*.net *.split).
17:43:11 -!- Leonidas has quit (*.net *.split).
17:43:11 -!- MizardX has quit (*.net *.split).
17:43:11 -!- FireFly has quit (*.net *.split).
17:43:11 -!- wareya has quit (*.net *.split).
17:43:11 -!- myndzi\ has quit (*.net *.split).
17:43:11 -!- bsmntbombdood has quit (*.net *.split).
17:43:11 -!- comex has quit (*.net *.split).
17:43:11 -!- Ilari has quit (*.net *.split).
17:43:11 -!- dixon has quit (*.net *.split).
17:43:11 -!- cheater2 has quit (*.net *.split).
17:43:11 -!- BeholdMyGlory has quit (*.net *.split).
17:43:11 -!- AnMaster has quit (*.net *.split).
17:43:11 -!- oklopol has quit (*.net *.split).
17:43:13 -!- sshc has quit (Ping timeout: 255 seconds).
17:43:42 -!- mycroftiv has quit (Ping timeout: 240 seconds).
17:44:33 -!- sebbu has quit (Ping timeout: 240 seconds).
17:45:34 -!- sshc has joined.
17:45:34 -!- mycroftiv has joined.
17:45:34 -!- Quadrescence has joined.
17:45:34 -!- jcp has joined.
17:45:34 -!- adam_d has joined.
17:45:34 -!- MizardX has joined.
17:45:34 -!- alise_ has joined.
17:45:34 -!- MigoMipo has joined.
17:45:34 -!- cheater2 has joined.
17:45:34 -!- tombom has joined.
17:45:34 -!- FireFly has joined.
17:45:34 -!- BeholdMyGlory has joined.
17:45:34 -!- AnMaster has joined.
17:45:34 -!- oklopol has joined.
17:45:34 -!- pikhq has joined.
17:45:34 -!- wareya has joined.
17:45:34 -!- dixon has joined.
17:45:34 -!- myndzi\ has joined.
17:45:34 -!- yiyus has joined.
17:45:34 -!- mtve has joined.
17:45:34 -!- ineiros has joined.
17:45:34 -!- uorygl has joined.
17:45:34 -!- SimonRC has joined.
17:45:34 -!- EgoBot has joined.
17:45:34 -!- HackEgo has joined.
17:45:34 -!- cal153 has joined.
17:45:34 -!- jix has joined.
17:45:34 -!- pineapple has joined.
17:45:34 -!- rodgort has joined.
17:45:34 -!- chickenzilla has joined.
17:45:34 -!- olsner has joined.
17:45:34 -!- Gregor has joined.
17:45:34 -!- bsmntbombdood has joined.
17:45:34 -!- MaXo2 has joined.
17:45:34 -!- Leonidas has joined.
17:45:34 -!- comex has joined.
17:45:34 -!- Ilari has joined.
17:45:48 <Quadrescence> I will speak to him and leverage what he knows already, and move forward.
17:45:49 -!- sebbu has joined.
17:45:52 <alise_> 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.
17:45:58 -!- adam_d has quit (Ping timeout: 240 seconds).
17:46:04 <alise_> And Zeilberger is a lunatic.
17:46:30 <alise_> Yes, well, so are many people.
17:46:32 <Quadrescence> And he knows his shit and moreover has a passion lacking in most mathematicians.
17:47:51 <alise_> dixon: Is that just a random exclamation or does it have context?
17:48:39 <dixon> alise_: You'd understand if you knew much about Zeilberger.
17:48:56 * Sgeo_ wonders who isn't a lunatic, according to alise_
17:49:24 <Sgeo_> VLC: Please stop being an attention whore. You should only be making your window flash when something actually happens
17:50:26 -!- sshc has quit (Ping timeout: 258 seconds).
17:50:48 <dixon> Sgeo_: VLC said that if you stop watching porn in it, it'll stop flashing you.
17:50:49 -!- sshc has joined.
17:51:02 <dixon> That's what VLC thought.
17:51:21 -!- BeholdMyGlory_ has joined.
17:51:57 -!- AnMaster_ has joined.
17:53:39 -!- jcp has quit (Ping timeout: 258 seconds).
17:54:56 -!- Leonidas has quit (Ping timeout: 258 seconds).
17:54:56 -!- MaXo2 has quit (Ping timeout: 258 seconds).
17:55:01 -!- BeholdMyGlory has quit (Remote host closed the connection).
17:55:02 -!- MaXo2 has joined.
17:55:03 -!- AnMaster has quit (Remote host closed the connection).
17:55:06 -!- mtve has quit (Ping timeout: 246 seconds).
17:55:07 -!- SimonRC has quit (Ping timeout: 246 seconds).
17:55:07 -!- SimonRC has joined.
17:55:39 -!- jcp has joined.
17:55:54 -!- Leonidas_ has joined.
17:55:55 -!- Leonidas_ has quit (Changing host).
17:55:55 -!- Leonidas_ has joined.
17:56:07 -!- sshc has quit (Changing host).
17:56:07 -!- sshc has joined.
17:56:09 -!- AnMaster_ has quit (Changing host).
17:56:09 -!- AnMaster_ has joined.
17:56:09 -!- BeholdMyGlory_ has quit (Changing host).
17:56:09 -!- BeholdMyGlory_ has joined.
17:56:14 -!- jcp has quit (Changing host).
17:56:14 -!- jcp has joined.
17:56:43 -!- cal153 has quit (Ping timeout: 258 seconds).
17:56:46 -!- BeholdMyGlory_ has changed nick to BeholdMyGlory.
17:56:48 -!- cal153 has joined.
17:56:55 -!- uorygl has quit (*.net *.split).
17:56:55 -!- ineiros has quit (*.net *.split).
17:57:58 <alise_> "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. "
17:59:48 -!- uorygl has joined.
18:00:05 -!- uorygl has quit (Read error: Operation timed out).
18:00:22 -!- uorygl has joined.
18:01:10 -!- lifthras1ir has joined.
18:01:12 -!- adam_d has joined.
18:01:12 -!- MizardX- has joined.
18:01:18 -!- sebbu has quit (*.net *.split).
18:01:18 -!- MizardX has quit (*.net *.split).
18:01:41 -!- MizardX- has changed nick to MizardX.
18:01:56 -!- werdan7 has quit (Read error: Connection reset by peer).
18:01:56 -!- lifthrasiir has quit (Remote host closed the connection).
18:02:31 -!- myndzi has joined.
18:02:49 -!- werdan7_ has joined.
18:04:02 -!- mtve has joined.
18:04:03 -!- sebbu has joined.
18:04:07 -!- charlls has joined.
18:05:35 -!- myndzi\ has quit (Ping timeout: 268 seconds).
18:05:43 -!- AnMaster_ has changed nick to AnMaster.
18:06:44 -!- fax has joined.
18:06:45 -!- ineiros has joined.
18:08:55 <alise_> Infinite associative arrays + lazy mapping =
18:08:56 <alise_> :nats / {n} [ n := [ 0 := n ] ]
18:08:56 <alise_> | :nats / {n} [ n := :nats / {m} [ m succ := plus n m succ ] ]
18:09:25 -!- charlls has quit (Ping timeout: 264 seconds).
18:11:50 -!- charlls has joined.
18:12:01 <alise_> If you had succ as a function not a "method" it'd be
18:15:33 -!- MaXo2 has quit (Ping timeout: 240 seconds).
18:15:42 -!- yiyus has quit (*.net *.split).
18:15:49 -!- MaXo2 has joined.
18:16:33 -!- Deewiant has quit (Ping timeout: 240 seconds).
18:17:18 -!- Deewiant has joined.
18:17:55 <alise_> Why hello there... DEEWIANT
18:18:58 <alise_> A little BING noise keeps happening every while on this machine... why grr
18:22:41 -!- yiyus has joined.
18:26:20 -!- pineapple has quit (Ping timeout: 245 seconds).
18:26:22 -!- pineapple has joined.
18:29:50 -!- BeholdMyGlory_ has joined.
18:31:16 -!- BeholdMyGlory has quit (Write error: Broken pipe).
18:41:02 -!- oklofok has joined.
18:42:15 -!- cheater3 has joined.
18:43:19 -!- cheater2 has quit (Write error: Connection reset by peer).
18:45:38 -!- oklopol has quit (Ping timeout: 260 seconds).
18:46:22 -!- BeholdMyGlory_ has quit (Changing host).
18:46:22 -!- BeholdMyGlory_ has joined.
18:46:25 -!- BeholdMyGlory_ has changed nick to BeholdMyGlory.
19:07:19 -!- Oranjer has joined.
19:10:07 <alise_> it's weird that you can prove ~~~~P -> ~~P without LEM...
19:10:46 <fax> no it's not
19:11:18 -!- oerjan has joined.
19:12:07 -!- kar8nga has joined.
19:12:08 <fax> it's just saying ~~~~P -> (P -> False) -> False, so you have hypothesis H : ~~~~P and H' : ~P, but ~P -> ~~~P which immediately contradicts H
19:12:41 <fax> the point is that the negation gives you contra-whatever-it-is which lets you add more ~'s instead of stripping them off
19:12:53 <oerjan> <oklopol> i'm both and i both do and don't have a sense of humor, i think <-- no, that would be the quantum physicists
19:14:22 <alise_> and ~~~P -> ~P for that matter
19:14:24 <alise_> fax: intuitively weird, I mean
19:14:32 <alise_> get into #morphism fax :<
19:14:55 <fax> it's because you're looking at it wrong
19:18:48 <oerjan> ~ may be an antitone galois connection, i think?
19:20:05 <oerjan> or wait, does that require the excluded middle
19:21:07 <oerjan> b -> ~a iff a -> ~b. hm that's obvious really.
19:21:23 <oerjan> so no excluded middle required
19:22:19 <fax> alise_ ????
19:22:50 <fax> I think b -> ~a iff a -> ~b is excluded middle?
19:23:02 <fax> no sorry of course it's not
19:24:09 <oerjan> nah with ~a = a -> false, it's just switching of assumptions
19:28:16 <fax> how to give a geometrical interpretation of Sum[k=1..] (2/3)^k?
19:29:00 <fax> I'm so confused how can 2/3 possibly be less than 1
19:29:13 -!- adam_d_ has joined.
19:31:56 -!- adam_d has quit (Ping timeout: 246 seconds).
19:32:56 * oerjan swats fax to unconfuse em -----###
19:33:27 <fax> I figured it out
19:33:58 <fax> but still can't explain the convergence
19:34:18 <oerjan> it's obvious from the geometric interpretation >:)
19:34:52 <fax> what is the geometric interpretation
19:35:04 <oerjan> well one interpretation
19:35:37 <oerjan> just divide up say a triangle into infinitely many pieces so that each piece is 2/3 of the previous one
19:36:17 <fax> you mean like chop a triangle up somhow
19:36:28 <oerjan> actually chopping up a line segment may be easier
19:36:36 <fax> area of a triangle = 1/2 w h
19:36:46 <oerjan> (then you just need length
19:38:21 <oerjan> fax: take a line segment whose length is x where x = 2/3 + (2/3)*x
19:39:00 <oerjan> chop off the first 2/3, then note how the rest is just the original scaled by 2/3
19:39:28 <fax> that's just solving the equation :(
19:39:41 <oerjan> it's also a geometric interpretation
19:40:30 <oerjan> it's just that you obviously need to solve the equation to find out how long the whole segment should be
19:42:10 <oerjan> if you use triangles you'll need to take the square root of 2/3 to get the right area
19:43:27 <oerjan> <alise_> it's weird that you can prove ~~~~P -> ~~P without LEM...
19:43:44 <oerjan> oh and that is essentially the galois connection stuff again
19:44:26 <alise_> lol I did an induction on an (impossible) natural
19:44:31 <alise_> and it simply gave me no assumptions
19:45:30 -!- adam_d_ has changed nick to adam_d.
19:52:50 -!- hiato has joined.
19:53:26 -!- hiato has quit (Client Quit).
20:11:30 -!- adam_d has quit (Ping timeout: 260 seconds).
20:53:20 <alise_> stack-based term rewriting
20:53:32 <fax> great idea Lindenmayer!
20:53:37 <fax> how did you come up with that
20:54:35 <alise_> basically the same as tree rewriting languages
20:54:44 <alise_> except it just checks the stack every iteration
20:54:59 <alise_> that way... you don't need parens or anything
20:55:16 -!- kar8nga has quit (Ping timeout: 260 seconds).
20:56:50 <Sgeo_> <Andy-> Interesting profile.
20:56:51 <Sgeo_> <Andy-> You appear to be a progressive atheist gay programmer.
20:56:51 <Sgeo_> <Andy-> Possibly a redditor.
20:57:12 <fax> progressive??
20:57:13 <alise_> Well, you learned one new thing about yourself.
20:57:20 <fax> what the fuck is progressive about being a gay atheist
20:57:21 <alise_> fax: fag name for left-winger
20:57:30 <alise_> so wait you hate gays too? :D
20:58:07 <fax> of course not
20:58:15 <fax> how could you even think that
20:58:25 <alise_> well I know you dislike atheism
20:58:38 <alise_> and i don't see how being gay and atheist are not "progressive" for a loose definition
20:58:48 <alise_> and I also don't see that Andy- connected the two
20:58:58 <alise_> so I was assuming you were using {atheist, gay} bad -> not progressive
20:59:01 <alise_> apologies if I am wrong
20:59:06 <Sgeo_> alise_, he wrote a program to get information about an SL user's profile, including group stuff
20:59:08 <fax> uh I thought progressive means like
20:59:15 <Sgeo_> http://www.mancer.org/sgeo.txt
20:59:16 <fax> radical new fresh idea
20:59:18 <fax> or somethin like that
20:59:22 <fax> as opposed to same old shit
20:59:38 <alise_> well gay atheism isn't exactly acceptable in today's society :)))
20:59:41 <oerjan> fax: sure, but compared to the 1950s, not now >:)
20:59:44 <alise_> fax: no it just means liberal anyway because USA sucks
20:59:52 <fax> alise everyone is a gay atheist
21:00:24 <alise_> fax is pulling a fax :D
21:02:48 <alise_> Axiom Too_Lazy : forall P, P. (* Fill in the boring parts of proofs later *)
21:03:54 * oerjan isn't sure whether that is false or tautological
21:04:06 <alise_> consider Too_Lazy False
21:04:23 <alise_> (P : Proposition) -> P
21:04:36 <alise_> P is the proposition, a value of type P is a proof of P
21:05:02 <oerjan> hm would forall x:P, P be a tautology then?
21:05:33 -!- anto_ram has joined.
21:06:06 -!- anto_ram has left (?).
21:06:43 <oerjan> what about forall x:P, x
21:07:42 * oerjan guesses at least the first one is, from what you said
21:08:42 <fax> you can't do forall x:P, x it's a type error
21:08:46 <fax> (assuming P : Prop)
21:08:58 <fax> since x is a 'value'
21:12:13 <Sgeo_> Incidentally, I'm not gay
21:12:27 * fax knew that :P
21:13:24 -!- tombom_ has joined.
21:15:25 -!- tombom has quit (Ping timeout: 264 seconds).
21:15:54 <alise_> <oerjan> hm would forall x:P, P be a tautology then?
21:16:00 <alise_> forall P, forall x:P, P
21:16:06 <alise_> forall x:P, x is wrong yeah
21:16:23 <alise_> but forall a:b,c is the dependent function arrow b-->c where the b is called a
21:16:28 <alise_> so obviously values don't make any sense there
21:16:30 <alise_> Sgeo_: well become gay!
21:16:37 <fax> it's fashionable!
21:16:51 * Sgeo_ somewhat wishes he could choose to become bi
21:17:30 <alise_> Use transsexuals as a bridge!
21:18:42 <Sgeo_> <kick52> 8:46:22 [Foonetic] CTCP PING reply from Sgeo_: 1374.449 seconds
21:18:43 <Sgeo_> <kick52> 22 minutes, Sgeo
21:19:18 -!- hiato has joined.
21:19:21 <alise_> oerjan: You can't just say that something sounds kinky, we're talking about sexuality
21:19:35 <alise_> Therefore no sexual puns can possibly work.
21:20:27 <dixon> Did you really use QED in a conversation?
21:21:28 <alise_> Did I offend you, Q.E.D.?
21:21:59 <dixon> No, you just made yourself look like a bigger pop-culture cargo-cult mathematically inept jackass.
21:22:04 <Sgeo_> Are you saying that it's quite easy to offend dixon? [Although oerjan was probably joking]
21:22:14 <alise_> dixon: You're a cunt. :)
21:45:47 -!- hiato has quit (Quit: underflow).
21:48:09 <oklofok> dixon and alise_ should just have some bittersweet sex and get it over with
21:48:31 <oklofok> two gay atheists in a big pile of progression
21:49:06 <dixon> Sadly I'm a friendly.
21:49:19 <fax> @ pile of progression
21:49:29 <fax> so I still have no clue what progressive means
21:49:38 <fax> probably means something totally specific to americans
21:49:49 <oklofok> it's a buzzword, you don't *know* what it means, you use it
21:51:08 <fax> this is so progressive
21:53:47 <dixon> It generally means liberal.
21:54:24 <oerjan> incidentally the progress party is the most right-wing one in the norwegian parliament
21:59:34 * Sgeo_ wants a wireless mouse
21:59:55 <Sgeo_> 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
22:00:20 <fax> wireless mouse? hahaha
22:00:26 <fax> you mean a mouse that turns off by itsself
22:01:19 <alise_> wireless mice are horrible; I've tried the worst and the best and they're all just as bad
22:01:22 <alise_> Just don't even go there
22:01:38 <Sgeo_> Then I'd like a mouse with a shorter cord
22:06:54 -!- MigoMipo has quit (Quit: Konversation terminated!).
22:13:57 -!- tombom_ has quit (Quit: Leaving).
22:59:45 -!- jcp has quit (Read error: Connection reset by peer).
23:00:57 -!- jcp has joined.
23:10:17 -!- lament has joined.
23:10:26 <lament> the topic is incorrect
23:14:31 -!- coppro has quit (Quit: Reconnecting…).
23:15:07 -!- coppro has joined.
23:22:13 -!- Leonidas_ has changed nick to Leonidas.
23:42:39 -!- MizardX- has joined.
23:43:49 -!- MizardX has quit (Read error: Connection reset by peer).
23:44:08 -!- MizardX- has changed nick to MizardX.
23:50:56 -!- FireFly has quit (Quit: Leaving).