00:00:01 oerjan, yeah one of the excercise was: solve the following equation x^2+1
00:00:06 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:10 fax, BWUH?
00:00:11 that's not an equation
00:00:16 oops
00:00:17 =0
00:00:18 fax: is your definition of "one of the atheist people" "someone who doesn't believe in god"
00:00:26 nice smiley :D
00:00:30 * Sgeo_ is an atheist person.
00:00:33 fax: (set it equal to 0 and tell him he's lame)
00:00:59 do you believe in angels?
00:01:06 dixon: uuuh - i need to study your reference to sponge constructions
00:01:12 -!- zzo38 has joined.
00:01:21 of course, and I beleive in paralell lines too
00:01:23 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:31 hi zzo73
00:01:41 rapido: http://sponge.noekeon.org/
00:01:49 oerjan, hm
00:01:49 http://sponge.noekeon.org/SpongeFunctions.pdf
00:01:50 i could believe in god and still find the concept of god to be impossible
00:01:54 such is believe
00:02:19 although if you are inside the complex numbers to start with, you don't really need to go outside them
00:02:29 dixan: ah, thanks!
00:02:41 rapido: They're cryptographic hashes, however.
00:03:03 dixon: cryptographic hashes are the only ones i'm considering
00:03:35 what if you believe in angels but don't believe in god?
00:03:48 * Sgeo_ pokes alise
00:04:04 rapido: But yes, by definition they're surjective when useful and thus have collisions.
00:04:19 Sgeo what abou gravity
00:04:23 it's supernatural
00:04:24 lament: Then you must've seen my girlfriend.
00:04:26 lament: then you would be a flying lunatic with wings
00:04:30 Sgeo_: hi
00:04:44 fax, lolwhat?
00:04:50 * Sgeo_ blinks a few times
00:04:54 nobody has explained it yet
00:05:05 it's like ghosts or ufos or whatever
00:05:25 fax: gravity is a scam by scientists. intelligent falling is the truth!
00:05:39 It exists, as demonstratably as possible.
00:05:57 it's God's Hand Pushing us Down From Eden
00:06:00 well intelligent falling is a much better explanation by occams razor but it does leave some key questions open
00:06:01 Ghosts and UFOs have not been observed by any measurements.
00:06:13 dixon: all that i want is a naming service that is scalable
00:06:28 rapido, let the name of the proof be the content of the proof.
00:06:31 Oranjer: no that would be more the coriolis force. eden is in the east, iirc
00:06:37 Sgeo - oh that's true I guess
00:06:43 What doe sthat mean, intelligent falling??
00:06:46 fax, it is not a better explanation by occams razor
00:06:56 "Playing with Coq in Jack" -- paper title
00:07:00 The reason otyugh attack with only two tentacles is because one tentacle has three eyes.
00:07:00 Sgeo_: but proofs can be huge - think of computer generated proofs
00:07:02 occams razor refers to the amount of assumptions an explanation requires
00:07:12 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 alise: That cannot be demonstratable
00:07:25 alise... how you have possibly managed to find a coq paper I haven't read O_O
00:07:38 Mostly because it doesn't work.
00:08:06 zzo38: http://en.wikipedia.org/wiki/Intelligent_falling
00:08:08 If you want to say God invented gravity, that's different however. Still not provable, though
00:08:19 falsifiable
00:08:24 I get the feeling that I should learn Coq
00:08:28 Using bigger words make you sound smarter.
00:08:31 fax: googling for unrelated things
00:08:40 zzo38: IT WORKS!!!!
00:08:46 now how do I do nested theorems in coq
00:08:53 See, we don't fall off the earth!
00:09:03 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 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:33 *is
00:09:41 Sgeo it's nothing very deep
00:09:46 alise: What I mean is the proof desn't work.
00:09:52 s/desn't/doesn't/
00:09:53 Sgeo -- just a notationally similarity between proof systems and type systems
00:09:59 notational
00:10:03 * oerjan has _never_ masturbated to the curry-howard isomorphism. should i try it?
00:10:14 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 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 alise: on facebook: Jack Coq Hardi
00:15:06 Jack Coq Hardi
00:15:07 Not the Jack Coq Hardi you were looking for? Search more Â»
00:15:47 Jacking off Coqs in Jack
00:16:20 guh, constructing a sigma is a bitch in a coq proof
00:16:43 the coq sigma stigma
00:16:46 a sigma algebra?
00:17:00 alise just give the value and prove it correct using tactics
00:17:12 yeah but I want to give the value using proof syntax
00:17:20 a sigma algebra?
00:17:28 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 and it's all fffffffffff
00:17:40 dixon: unlikely.
00:17:53 He couldn't have meant a series?
00:17:58 not that i'm _sure_ alise doesn't know what that is, but...
00:18:47 well, for one thing alise only does constructivist things, i doubt sigma algebras qualify
00:19:21 you know constructivism isn't some crazy fringe philosophy :)
00:19:29 yes it is :P
00:19:30 Yes it is.
00:19:45 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 dixon: but it's very useful for masturbating to the curry-howard isomorphism, i hear
00:21:47 * oerjan ducks
00:22:04 I lol'd
00:23:06 Next all he has to say is he's a finitist
00:23:13 It may be boring and old but who cares?
00:23:21 * pikhq masturbates to finite sequences
00:23:24 dixon: fax is a finitist
00:23:24 :P
00:23:26 so...
00:23:33 you're looking at the wrong person I'm very much a believer in infinities
00:23:55 Yeah, but I already think fax is an idiot.
00:24:08 Yay! Infinities.
00:24:17 -!- Quadrescence has joined.
00:24:22 now where did you get THAT idea?
00:25:04 Mainly your berating me for not knowing anything 15 minutes after you claimed the exponential function wasn't hypergeometric.
00:25:49 oh fuck off
00:26:04 it was long before that
00:26:55 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:23 :3
00:27:29 Perhaps we are using different definitions of constructivist.
00:27:53 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 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 So basically I reject the law of the excluded middle and correspondingly ~~p -> p.
00:28:06 That isn't really so crazy.
00:29:42 dixon I wasn't berating you for not knowing anything anyway, you were making some ridiculoulsy stretched joke about 'dixons identity'
00:31:54 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 zzo38 have you read any linear logic?
00:32:58 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 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 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 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 alise: There certainly can be things that are neither true nor false.
00:34:24 moral dilemma: I followed a link allegedly to Rick Astley rickrolling someone himself
00:34:29 and it was actually what it claimed to be, rather than a rickroll
00:34:34 alise: Is'nt the law of the excluded middle about statements that can be derived from the axiomatic system in question?
00:34:34 have I been meta-rickrolled?
00:34:36 wow I want to see it!
00:34:57 http://www.youtube.com/watch?v=y4hqv6USkoU
00:35:02 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 Meta-rickrolled?
00:35:05 basically, it was a Thanksgiving Day's parade
00:35:10 alise: Ah.
00:35:12 Okay, then.
00:35:14 and he was hiding on one of the floats, and just came out and started singing live
00:35:21 However, there are things that are neither.
00:35:28 So the law of the excluded middle is fail.
00:35:52 alise: Tell me one such proposition?
00:36:13 pikhq: Consider the Continuum Hypothesis.
00:36:16 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 ZFC + CH is consistent, as is ZFC + ~CH.
00:36:21 ais weird lol
00:36:25 IMO, that's a weaker situation than the law of the excluded middle
00:36:30 I don't think it's a rickroll
00:36:34 With tristate logic things can be true, false, or tristate. Pre(P) is true if P is not tristate.
00:36:38 ais523: p \/ q = (p -> r) -> (q -> r) -> r
00:36:44 fax: well, it did /say/ it was a rickroll at the end
00:36:57 oh
00:36:57 perhaps this is some sort of meta-meta-rickroll
00:36:58 p \/ ~p = (p -> r) -> (~p -> r) -> r
00:37:03 ais523: Answer: No.
00:37:07 oh it is a rickroll
00:37:11 alise: the law of the excluded middle implies that
00:37:17 pikhq: So, then, how, in plain ZFC, is CH true or false?
00:37:19 but, I think it can be true even without
00:37:24 ais523: no, p or q is literally the same thing
00:37:28 as (p->r)->(q->r)->r
00:37:35 proof:
00:38:02 \f g porq. case porq of theone x -> f x; theother x -> g x
00:38:02 and
00:38:05 erm
00:38:10 \porq f g. case porq of theone x -> f x; theother x -> g x
00:38:19 that's p\/q -> (p->r)->(q->r)->r
00:38:23 now the other way:
00:38:31 the other way is the way I care about
00:38:47 (p->r)->(q->r) -> p \/ q
00:39:07 \f. f theone theother
00:39:17 filling in the arguments we get
00:39:22 first is (p -> p \/ anything)
00:39:22 alise: you must have typoed somewhere
00:39:28 alise: you are missing -> r
00:39:28 second is (q -> anything \/ q)
00:39:34 right right
00:39:37 the implementation is right
00:39:38 so
00:39:42 fill in p and q for the respective anythings
00:39:44 and we get p \/ q
00:39:47 Q.E.D.
00:40:09 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 alise: Clearly, the veracity of CH is a boolean.
00:40:15 hmm, I always get confused trying to follow nonstandard models of logic
00:40:33 That the value of the boolean cannot be determined is beside the point.
00:40:36 in one seminar I went to, someone quantified over all systems of logic, which was /really/ confusing
00:40:40 Prelude> let or2f porq f g = case porq of Left x -> f x; Right x -> g x
00:40:40 Prelude> let f2or f = f Left Right
00:40:40 Prelude> :t (or2f, f2or)
00:40:40 (or2f, f2or)
00:40:40 :: (Either t t1 -> (t -> t2) -> (t1 -> t2) -> t2,
00:40:41 ((a -> Either a b) -> (b1 -> Either a1 b1) -> t11) -> t11)
00:40:44 alise: you had an implied forall r in there
00:40:51 ais523: Since I have proved that (P->Q) and (Q->P), P is equivalent to Q.
00:40:54 pikhq: booleans have /nine/ values, 01XLHWZU-
00:40:58 alise: ok
00:41:11 Well, f2or actually needs a more specific type, but.
00:41:20 ANY LANGUAGE IN WHICH BOOLEANS HAVE FEWER THAN NINE POSSIBLE VALUES IS DEFICIENT
00:41:23 ais523: Then we are clearly discussing the law of the excluded 10th.
00:41:25 btw, I'm not sure which one maps to file_not_found
00:41:28 pikhq: haha
00:41:38 alise: Clearly, the veracity of CH is a boolean.
00:41:39 Really?
00:41:41 ((p->(p\/q))->(q->(p\/q))->(p\/q)) -> (p\/q)
00:41:43 fax: have you decided whether that was a rickroll or not yet?
00:41:59 pikhq: ZFC + CH is consistent iff ZFC is consistent. ZFC + ~CH is consistent iff ZFC is consistent.
00:42:08 In ZFC, CH can neither be true nor false.
00:42:18 If we can prove it true, then ZFC + ~CH would be inconsistent.
00:42:23 If we can prove it false, then ZFC + CH would be inconsistent.
00:42:25 In ZFC, CH cannot be shown to be true or false.
00:42:28 I think I've caused a logical gap in rickrollness
00:42:29 It is neither true nor false.
00:42:38 pikhq: But it has some platonic "real truth"?
00:42:49 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 ais523, I am not really sure
00:43:01 You are referring to some platonic space of "ZFC truths" but no such thing exists, just manipulation of the axioms.
00:43:06 Are you sure you want to go down this path>
00:43:10 fax: hmm, so you're metaundecided?
00:43:11 Please explain what the nine boolean values 01XLHWZU- are meant for.
00:43:57 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:07 OK.
00:44:19 VHDL actually implements all these
00:44:21 yes
00:44:38 *path?
00:45:05 alise: It certainly has no "platonic real truth". It just simply can be said to be one of true or false.
00:45:35 pikhq: Okay.
00:45:38 So suppose it is true.
00:45:44 Then ZFC + ~CH is inconsistent.
00:45:47 So suppose it is false.
00:45:50 Then ZFC + CH is inconsistent.
00:45:58 But we know that ZFC plus either CH or ~CH is consistent iff ZFC is.
00:46:00 So it cannot be both true and false.
00:46:04 No.
00:46:06 It cannot be either.
00:46:12 Because *both systems are consistent*.
00:46:13 How so?
00:46:14 (if ZFC is).
00:46:27 pikhq: OK, let us say that in ZFC, we have proved CH.
00:46:34 I didn't know VHDL implements those. But I suppose it is possible.
00:46:41 We know that ZFC + ~CH is consistent iff ZFC is. Yet we have CH and ~CH.
00:46:54 Reverse it to see that it cannot be false, either.
00:47:06 You can keep running around in circles, but the only real solution is to reject the excluded middle.
00:47:26 alise: "We know that ZFC + ~CH is consistent iff ZFC is. Yet we have CH and ~CH." Uh... Wha?
00:47:38 OK, let me spell it out for you.
00:47:52 Near as I can tell, "proving CH in ZFC" would imply that ZFC + ~CH is inconsistent.
00:48:23 And assuming the proof that ZFC + ~CH is consistent is valid, then clearly you cannot prove CH in ZFC.
00:48:54 and if you did both, then it would show ZFC is not consistent.
00:49:03 dixon: Yes.
00:49:03 because that's a contradiction
00:49:15 pikhq:
00:49:16 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 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 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 Therefore, CH cannot be true and it cannot be false.
00:49:44 alise: You have proven that CH cannot be proven in ZFC.
00:49:44 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 Excluded middle is false.
00:49:53 pikhq: No, I made no references to proofs in the above.
00:49:57 Clearly it can be one or the other; you can use it as an axiom.
00:50:01 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