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:18 <alise> fax: is your definition of "one of the atheist people" "someone who doesn't believe in god"

00:01:23 <oerjan> fax: adding roots of polynomials in that way is a fundamental tool of galois theory iirc

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:04:04 <dixon> rapido: But yes, by definition they're surjective when useful and thus have collisions.

00:06:00 <fax> well intelligent falling is a much better explanation by occams razor but it does leave some key questions open

00:07:00 <zzo38> The reason otyugh attack with only two tentacles is because one tentacle has three eyes.

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:08:08 <zzo38> If you want to say God invented gravity, that's different however. Still not provable, though

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:24 <dixon> HEY LOOK GUYS I CAN PRETEND I'M A MATHEMATICIAN BECAUSE I CAN WRITE PROOFS IN COQ fapfapfapfapfap etc

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: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:18:47 <oerjan> well, for one thing alise only does constructivist things, i doubt sigma algebras qualify

00:21:35 <oerjan> dixon: but it's very useful for masturbating to the curry-howard isomorphism, i hear

00:25:04 <dixon> Mainly your berating me for not knowing anything 15 minutes after you claimed the exponential function wasn't hypergeometric.

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: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: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: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:34:24 <ais523> moral dilemma: I followed a link allegedly to Rick Astley rickrolling someone himself

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: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:14 <ais523> and he was hiding on one of the floats, and just came out and started singing live

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:34 <zzo38> With tristate logic things can be true, false, or tristate. Pre(P) is true if P is not tristate.

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:36 <ais523> in one seminar I went to, someone quantified over all systems of logic, which was /really/ confusing

00:41:59 <alise> pikhq: ZFC + CH is consistent iff ZFC is consistent. ZFC + ~CH is consistent iff ZFC is consistent.

00:42:49 <alise> That's metaphysical mumbojumbo: you are talking about things in the system that are not from the axioms.

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: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: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: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: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: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: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: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: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:53 <alise> Well, this has taught me something: Never bother trying to talk about excluded middle.

00:55:52 <pikhq> People don't like the implication that you could define the following: ZFC + CH & ~CH. :P

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: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 :)))

02:46:49 <alise> [["Anime is a prime example of why two nukes wasnt enough." - NH Democrat State Rep., Nick Levasseur]]

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

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:04:20 <pikhq> Try more of Pikhqどのはお馬鹿で御座るとお思いになります。(Pikhq dono wa baka de gozaru to o-omoi ni narimasu)

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: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: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: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:17:25 <pikhq> The closest you can get in Japanese is "gaijin". Which... Refers to everyone other than Japanese.

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."

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.

10:34:09 <AnMaster> dixon, it allows you to press that key you made your compose key then press two other keys

10:36:30 <AnMaster> but yeah ~/.XCompose doesn't seem to be used, though docs indicate it should work

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:50:53 <dixon> There difference between a math student and a computer science student is a sense of humor.

13:28:08 <Phantom_Hoover> Unfortunately, my life is now going to be unfulfilled until I acquire or build one.

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: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.

14:11:00 <oklopol> :PPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPP

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:31:28 <alise_> Because I just plugged in the value then told it to shut up and compute S (pred n) and n. :)

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:48 <oklopol> right i don't know anything about tactics. well except that they can magically do things for you

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: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:50:17 <alise_> here's my documentation for auto: "does something helpful, or does something unhelpful, or does nothing".

16:21:36 <alise_> (alwaysbigger : forall x, exists y, y > x) so we get ~(exists x, ~exists y, y > x).

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: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.

17:13:34 <FireFly> `addquote <alise_> man go fuck yourself :P <AnMaster> alise_, hm okay <AnMaster> bbl

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:57 <alise_> "Hereditarily finite set. Strange maths stuff. Makes no sense. Angela 00:52, Oct 2, 2003 (UTC)"

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: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:52 <alise_> dixon: Of course it is very easy to package the fact that ~ n >= S n up into one theorem.

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:25:46 <alise_> You can't just say "this is true" because if you did that nothing would need a proof.

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: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: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: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: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: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:44 <alise_> It is a proof system only in the most pathological sense, and even then it is blatantly inconsistent.

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:11 <uorygl> So a mathematician is a person who invents new fields of mathematics and discovers novel applications of it?

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: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: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:46:32 <Quadrescence> And he knows his shit and moreover has a passion lacking in most mathematicians.

17:49:24 <Sgeo_> VLC: Please stop being an attention whore. You should only be making your window flash when something actually happens

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. "

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: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: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

20:58:38 <alise_> and i don't see how being gay and atheist are not "progressive" for a loose definition

20:59:06 <Sgeo_> alise_, he wrote a program to get information about an SL user's profile, including group stuff

21:19:21 <alise_> oerjan: You can't just say that something sounds kinky, we're talking about sexuality

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:54:24 <oerjan> incidentally the progress party is the most right-wing one in the norwegian parliament

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:01:19 <alise_> wireless mice are horrible; I've tried the worst and the best and they're all just as bad