00:04:07 -!- sacje has quit (Ping timeout: 264 seconds). 00:25:41 I wish dvorakbot were here. 00:25:47 He really brightened up this channel. 00:25:51 -!- dvorakbot has joined. 00:25:55 * tswett sighs wistfully. 00:28:11 dvorakbot: what did you do again? 00:28:22 Same thing as la_fen. 00:28:39 $u a 00:28:40 U+0061 LATIN SMALL LETTER A (a) 00:29:10 List of dvorakbot's commands: http://pastie.org/8095682 00:29:21 $newcard oerjan 00:29:22 Card 1: oerjan 00:29:33 Congratulations on being a card. 00:29:45 eek 00:29:59 $moveallto deck 00:29:59 Cards moved. 00:30:06 $draw 00:30:07 No cards in draw pile. 00:30:14 Whoops. 00:30:16 $moveallto draw 00:30:16 Cards moved. 00:30:18 $draw 00:30:19 Card drawn. 00:30:23 I wonder what card it is! 00:30:50 $newcard orson 00:30:51 Card 2: orson 00:32:56 what happens to these cards? 00:33:02 where are they? 00:33:07 $where 1 00:33:08 In pile: tswett's hand 00:33:10 $where 2 00:33:11 Nowhere 00:33:16 $where 3 00:33:17 KeyError: 3 (file "/Users/tswett/Documents/Hobbies/Programming/Python/phenny/modules/dvorak.py", line 139, in where_card) 00:33:32 dvorakbot handles all errors gracefully. 00:35:31 aha, now i know ur local username! 00:36:15 Uh oh. Now you can )(4xx0r4t3 me. 00:39:10 >:D, i am so 1337 at that 00:40:13 s;top 00:41:50 only you can stop them elliott 00:42:27 or was it forest fires, i'm not sure 00:42:28 actually that was directed specifically at bike hth 00:42:41 `factor 1337 00:42:43 1337: 7 191 00:42:48 hmm, wasn't it oerjan who could stop forest fires? 00:42:55 pretty sure it was oerjan. 00:43:08 i'm pretty sure i've never tried stopping a forest fire 00:43:34 though I'm sure fungot could say that to lots of people if it wanted to 00:43:35 olsner: you should do it. thanks for pointing out a pro ( or con). modulo a b) 00:43:57 modular arguments 00:47:04 ‮"oof" < 00:47:58 ‮.rof si retcarahc siht tahw erus toN 00:49:45 Hm. "The right-to-left override, for example, can be used to force a part number made of mixed English, digits and Hebrew letters to be written from right to left." 00:53:45 would you mind to reactivate bike elliott? 00:55:00 -!- Lumpio- has quit (Ping timeout: 256 seconds). 00:55:52 $newcard clog 00:55:53 Card 3: clog 00:55:54 $newcard EgoBot 00:55:56 Card 4: EgoBot 00:56:02 $newcard fngot 00:56:03 Card 5: fngot 00:56:06 Whoops. 00:56:28 $delete 5 00:56:29 Card deleted. 00:56:31 $newcard fungot 00:56:31 tswett: the best explanation of what he meant 00:56:32 Card 6: fungot 00:56:32 dvorakbot: but if i start generating absurd amounts of money from my sick leave and i have 0.8.6 running on this computer 00:56:33 -!- Lumpio- has joined. 00:56:56 This channel has a lot of bots. 00:57:05 $newcard HackEgo 00:57:06 Card 7: HackEgo 00:57:07 $newcard lambdabot 00:57:08 Card 8: lambdabot 00:57:11 $moveallto draw 00:57:12 Cards moved. 00:57:13 $shuffle draw 00:57:15 Pile shuffled: Draw pile. 00:57:47 tswett: can you also define rules? or are they defined someway? 00:58:02 Nope, the rules are just whatever you've previously agreed on. 00:58:43 The bot is unfinished, but it's also usable. It can do almost everything DvorakMUSH, I think it was, can do. 00:59:49 ahh.. i think i know that one 01:05:15 tswett: is dvorak a popular game where in the US? 01:05:35 Nope, I think it's completely obscure worldwide. 01:06:16 oh if it's the game i know it's spoken "durak" and means "fool" in russian 01:06:59 and it's quite popular in germany ..so 01:07:06 -!- Koen_ has joined. 01:09:56 -!- DHeadshot has quit (Remote host closed the connection). 01:13:24 -!- ggherdov has quit (Ping timeout: 240 seconds). 01:14:25 -!- hagb4rd has changed nick to noloveinwaikiki. 01:22:47 * oerjan suddenly recalls a silly norwegian children's song about a many-headed monster remembering his love affair in hawaii 01:23:07 :) 01:23:54 do you think you can find a version on the net? 01:25:04 okay.. it's not that important 01:25:14 don't mean to waste your time 01:25:47 "not available in your country" :/ 01:25:55 yt video? 01:26:26 oh there http://www.youtube.com/watch?v=9Htk_XLPuWs 01:26:48 great <3 01:28:30 -!- noloveinwaikiki has changed nick to hagb4rd. 01:34:23 turns out that video was recorded in trondheim 01:34:29 <- there 01:34:51 oerjan: can I come visit 01:34:53 *mysticwindblowing* 01:34:58 :P 01:35:51 elliott: you can come to trondheim but we can never meet there hth 01:35:58 oerjan: but what if I bring taneb 01:36:14 hm, tricky 01:43:48 http://distractionware.com/games/flash/vvvvvvproto/ 01:44:03 This music doesn't seem to be in PPPPPP or VVVVVV 01:51:49 kmc, http://www.souleye.se/adventure has songs that are on VVVVVV 2 but not 1 (I didn't even know there was a 2) 01:53:02 is... is there a reason kmc is pinged 01:54:10 maybe because he's interested in that stuff 01:54:29 or because sgeo is evil 01:54:47 01:55:07 Because kmc has expressed liking of PPPPPP previously 01:55:25 and here i was going with the sgeo is evil hypothesis 01:55:44 WHY NOT BOTH hth 01:56:15 hth hth hth hth 01:56:19 monoids hth monoids hth monoids 01:56:49 ok 01:57:06 -!- elliott has set topic: The channel for helpful people | http://underhanded.xcott.com/?page_id=5 | logs: http://codu.org/logs/_esoteric and http://tunes.org/~nef/logs/esoteric/?C=M;O=D. 01:57:15 > fix ("monoids hth" <>) 01:57:16 "monoids hthmonoids hthmonoids hthmonoids hthmonoids hthmonoids hthmonoids ... 01:57:19 oops 01:57:22 hthmonoids 01:57:43 `? monoids 01:57:46 Monoids are the easy version of categories. 01:58:58 `learn hthmonoids hthmonoids hthmonoids hthmonoids hthmonoids hthmonoids ... 01:59:02 I knew that. 01:59:49 `run mv wisdom/hthmonoid{s,} # hth 01:59:52 No output. 01:59:59 -!- sprocklem has joined. 02:00:30 i think this hth and monoids thing is getting a little out of hand. 02:00:55 easy hth hand 02:01:09 i think it's gotten a lot out of hand & has gone from being kind of ««««ironically»»»» silly to just silly & also poop dumb 02:01:55 Bike: but. 02:02:09 Butt 02:02:18 Bike: going further than is reasonable until it starts being funny again is arguably the whole idea here!! 02:02:21 hth. 02:02:33 that has never worked ever 02:02:49 maybe you just haven't tried enough, hth 02:09:02 seriously? it's not as bad as it sounds..and maybe a direct consequence of that long-year-relationships grown in this channel.. but there's a lot of "insider" jokes or references made here.. they're cool sure, but may in worst case (which is not a tragedy) keep newcomers out.. 02:09:37 but it's really not a problem 02:09:48 i think 02:10:13 most newbie are welcomed and always given a chance here 02:10:19 *newbies 02:13:08 on the other hand that is what makes a good community..development and preservation of culture 02:14:39 -!- Phantom_Hoover has quit (Remote host closed the connection). 02:17:01 shit i don't have any skin.. hope you can make any sense of this 02:17:05 -!- sprocklem has quit (Remote host closed the connection). 02:17:33 ...not the last line, no 02:17:48 development of culture? 02:18:00 "shit i don't have any skin" 02:18:06 oh this part 02:18:07 :) 02:18:22 oerjan don't be so intolerant, if we can have bicycles we can have horrific jumbles of flesh and bone 02:18:37 i don't have a lymphatic system :) 02:18:55 I don't have an emphatic system 02:19:01 the joke is Bike sux 02:19:30 that one didn't really work so well :( 02:20:10 -!- Nisstyre has quit (Quit: Leaving). 02:20:43 bike jokes are tired and flat 02:20:51 -!- Nisstyre-laptop has joined. 02:21:01 ... 02:24:37 -!- sacje has joined. 02:28:20 wow 02:29:21 mnoqy: now what 02:29:40 yeah 02:30:16 AOL is a commonly recognized root CA? 02:30:31 if you say so 02:33:44 -!- Nisstyre-laptop has quit (Ping timeout: 246 seconds). 02:37:17 -!- Koen_ has quit (Quit: Koen_). 03:14:18 -!- ggherdov has joined. 03:27:47 and now for something completely different 03:28:41 yes 03:32:35 -!- oerjan has quit (Quit: Good night). 03:38:00 -!- mnoqy has quit (Quit: hello). 03:50:23 -!- nooodl has quit (Ping timeout: 268 seconds). 04:36:30 -!- zzo38 has joined. 04:42:51 -!- NihilistDandy has joined. 05:42:03 -!- Bike has quit (Ping timeout: 260 seconds). 05:42:23 -!- Bike has joined. 06:00:38 Quoting from a message on Chess Variants: "What is the interface of Chess and reality? Is Chess the unreal? Or the other way around. ... If Chess existed first, why not invent a Reality to conform to it? What reality would that be? ..." 06:00:56 chesseality, imo. 06:02:20 I did write a reply. My own point of view is that mathematics is the real reality. 06:06:11 `thanks reality 06:06:13 Thanks, reality. Theality. 06:06:51 fizzie: a truce has been established. I am now neutral on speech recognition 06:07:37 what 06:08:02 ok, I still hate it a little. 06:08:47 why would you give up your non-biology-related principles! 06:09:06 if you think about it speech recognition = biology. 06:09:40 Can a game be defined with sequent calculus in a symmetric way? I have been able to define the subtraction game although the rules aren't symmetric for each player; the first player has to select a rule to follow (if the proof is working from bottom to top), while the second player selects which sequent above the line will be the next state. 06:09:55 but the only similar thing between them is that you hate them! and that' snot even true any mroe! NOTHING IS REAL ELLIOTT 06:10:08 Bike. shut up. 06:10:29 also, speech recognition = humans = biology 06:11:08 No! They are related in this way, but it is different kind of things. 06:13:13 If there is a single sequent above and a single below the line, then you can define single-player games, such as sokoban. The axiom schema is positions with one player, any number of empty spaces, any number of crates-on-targets, and nothing else. 06:14:17 Therefore, any solvable game is a theorem of this system. 06:14:27 -!- Taneb has joined. 06:15:49 Can you make anything similar, or make a better two-player game with this? 06:17:21 elliott: zzo38's right here, man. it is different kind of things! 06:21:15 @messages? 06:21:15 Sorry, no messages today. 06:21:18 Yay 06:24:17 -!- sprocklem has joined. 06:28:37 I have another idea about sequent calculus. Define a "macro" to mean following many rules, in a polymorphic way (but not necessarily as polymorphic as the original rules), and put together to form a single admissible rule. Therefore, a "theorem" is really a "macro" with nothing above the line. Isn't it? 06:47:54 kmc: least and greatest fixed points are so much imo 06:48:13 you should, like, learn about them and stuff 06:48:36 That reminds me 06:49:10 I need to write a blog post/essay/talk relating Taneb-style fixed curves to control-passing-style 06:54:18 Taneb: What are those things? 06:54:44 A pair of functions f and g such that f(g(x), x) = g(x) 06:54:53 splines? 06:55:13 o no.. 06:55:24 that's more specific 07:00:09 no, it's absolutely somethin different 07:03:29 Bugger, I've made a stupid mistake 07:03:55 Okay, this has totally failed 07:04:25 Taneb: maybe you can answer my questions about fixed points instead then... 07:05:24 i like banach's fixed points. they're p. good. 07:06:26 do you like Knaster-Tarski theorem.... 07:06:31 I thought I was onto something deep 07:06:43 But I made the mistake of saying the xth root of x was 1 07:06:47 https://en.wikipedia.org/wiki/Category:Fixed-point_theorems 07:06:47 tarski's fixed points are also p. good 07:06:48 help 07:07:20 have you seen the stuff about assigning truth values to weirdass sentences based on tarski's fixed points 07:07:23 pretty cool imo 07:07:51 no but i heard about "definedness analysis and liveness analysis" or something 07:07:55 -!- Gracenotes has joined. 07:08:00 Hang on 07:08:08 It approaches 1 as x approaches infinity! 07:08:10 What does it mean to "assign truth values to weirdass sentences based on tarski's fixed points"? 07:08:11 This could be useful! 07:08:21 -!- Gracenotes has quit (Client Quit). 07:08:26 uh lemme look 07:08:44 * Bike dives into pile of pdfs 07:09:37 Bike: is that like the logic equivalent of zeta regularisation 07:10:11 No, I still can't make that assumption 07:10:40 Taneb: also numbers have, like, more than one root. 07:11:26 ugh where the hell is this paper. it was good 07:12:28 and no it's not like zeta regularization very much 07:12:42 hey Bike 07:12:56 have you informed tarski that lattice theory is a waste of time b. you should really be doing category theory instead 07:13:20 Bike: well I mean, in spirit. 07:13:34 * Bike sighs. 07:13:35 -!- Gracenotes has joined. 07:13:54 wow tarski's paper has about 2400 cites. 07:13:58 imo, fuck. 07:14:25 imo read them all 07:14:28 http://www.springerlink.com/index/H880Q5G6M9661313.pdf here, something about "categories" that cites it. ur welcome. 07:16:16 $39.95 hooray 07:16:58 ok found it http://comet.lehman.cuny.edu/fitting/bookspapers/pdf/papers/TruthFalse.pdf 07:17:45 it involves things being true and false because, like, lol. 07:18:32 also it's actually kripke's not tarski's?? so you can tell him yourself shachaf. 07:18:45 lol 07:18:58 cheers 07:19:06 hth 07:20:41 i knew taneb's thing looked familiar. it's like an IVP where f = f', which is dumb but oh well 07:21:15 or like a differential equation rather. 07:21:16 a dumb one 07:25:06 Maybe the truth behind Assassin's Creed is that a logic with the axiom "forall x. x is false" is inconsistent 07:25:24 -!- sprocklem has quit (Remote host closed the connection). 07:25:35 comp_Monoid_Elements_is_assoc : forall x y z, multiply_Monoid_Elements x (multiply_Monoid_Elements y z) = multiply_Monoid_Elements (multiply_Monoid_Elements x y) z 07:25:41 I'm thinking there might be a way of making that shorter. 07:26:31 Taneb: Well, unless "forall" and "is false" is sufficiently restrictive, then yes it probably is inconsistent. 07:27:22 What does x range over, there? 07:27:27 If its domain is empty, then that axiom is true. 07:27:37 i bet you couldn't find an x such that ¬x is true!! 07:28:00 Now, a logic with the axiom "not P" for all formulas P would definitely be inconsistent. 07:28:29 tswett, the joke is, that when this is combined with the principle of explosion, you get "Nothing is true, everything is permitted" 07:28:37 tswett: I don't think that is necessarily inconsistent either if the logic is sufficiently restrictive. 07:28:54 Taneb: hm, sounds true. 07:29:13 Here, have a picture. http://i.imgur.com/tKns3wi.jpg 07:29:29 Seen it a dozen times at least 07:29:43 still good though. 07:29:52 It isn't inconsistent unless all well-formed strings are theorems. 07:30:30 zzo38, what if the axiom itself is in its domain 07:31:21 Taneb: Well, of course it is in its own domain, but I don't think that changes what I said. 07:31:46 Because then it is trivially true (it is an axiom), but also false! 07:33:17 Taneb: you have? 07:33:22 But maybe it isn't necessary "true" or "false" but can be a theorem or nontheorem, since "false" might not necessarily be meaningful in a logic such as this. 07:33:22 Taneb: well, feast your eyes on this! http://i.imgur.com/tKns3wi.jpg 07:33:39 tswett, I've seen that at least a baker's dozen times! 07:33:54 Yay, you said the thing I was hoping you were going to say. 07:33:55 zzo38, shh it was a bad joke 07:36:56 I would like to learn how to use a sword 07:37:00 And also how to ride a unicycle 07:37:05 Perhaps not at the same time 07:45:55 All right. So, given an object in a category, its endomorphisms form a monoid. 07:46:03 This feels like a natural transformation. 07:47:13 Maybe it's just a functor. 07:47:32 From the category of categories to the category of monoids. 07:47:49 Mm, no, that would mean that it turns every category into a monoid. 07:48:04 This one, given a category, turns all of that category's objects into monoids. 07:48:29 Are you just talking about a subcategory with one object? 07:48:42 Yeah, I guess I am. 07:53:48 -!- itsy has quit (Remote host closed the connection). 07:58:55 -!- sprocklem has joined. 08:10:32 Taneb: Do you not want to learn to use a sword while riding a unicycle while blindfolded? 08:10:51 Yeah, why not 08:17:55 -!- itsy has joined. 08:18:17 It's the World Egg Throwing Championships today :-) 08:39:00 constructivism, more like destructivism 08:39:07 the joke is that constructivism is bad 08:51:47 -!- AnotherTest has joined. 08:52:23 -!- oonbotti2 has quit (Remote host closed the connection). 08:52:42 -!- oonbotti2 has joined. 08:56:40 -!- itsy has quit (Ping timeout: 256 seconds). 09:02:06 `pastelog the joke is 09:02:23 `pastelogs the joke is 09:02:43 hi kmc 09:02:49 hichaf 09:02:54 why can't i paste logs 09:02:55 http://codu.org/projects/hackbot/fshg/index.cgi/raw-file/tip/paste/paste.14280 09:03:00 because no patience 09:03:03 http://codu.org/projects/hackbot/fshg/index.cgi/raw-file/tip/paste/paste.20487 09:03:04 thackego 09:03:18 -!- epicmonkey has joined. 09:03:42 how's sf 09:05:03 good 09:05:42 did you know that fixed points are the best thing in the world 09:05:59 there was a huge party in the middle of the street in the castro 09:06:11 i heard about such things 09:06:12 -!- AnotherTest has quit (Quit: Leaving.). 09:06:38 oh 09:07:23 also a huge number of people in dolores park before that 09:07:48 nice park 09:08:36 -!- conehead has quit (Quit: Computer has gone to sleep.). 09:08:44 -!- oonbotti has joined. 09:09:08 -!- oonbotti2 has left. 09:10:49 so which this F-Fix thing 09:10:55 There's a category F-Fix(C) where an object is (X : C, f : X <-> F X) and an arrow (X, f) -> (Y, g) is an arrow h : X -> Y such that fmap h . f = g . h 09:11:06 s/which/with/ /me sighs 09:11:54 so if you have a forgetful functor : F-Fix(C) -> C does it have a left adjoint 09:12:05 by C i mean Hask btw 09:12:12 i'm a forgetful functor 09:12:19 oh i guess not in general because that would be a monad 09:12:50 kmc: me too 09:13:04 kmc: is the joke that you left adjoint unsmoked in sf 09:13:23 or maybe that's the opposite of the joke 09:13:37 -_- 09:14:00 kmc doesn't like drugz jokes 09:14:03 if we reduce kmc to just drugz all the time we'll drive him to drink 09:14:03 :'( 09:14:06 [drinkz joke] 09:14:18 thats ok i already drink all the time 09:14:36 at this particular moment it is i who have reduced myself to drugz 09:14:39 drinkz <: drugz 09:14:47 you're off the hook for that 09:14:53 how many drugz did you drugz 09:15:06 in quantity or in number of different kinds 09:15:31 yes 09:16:34 i'm drugz but only metaphorically 09:16:55 somebody told me that all things are composed of drugs, math, and cardboard in varying ratio 09:16:57 fixed points are drugz 09:17:00 fixed pointz 09:18:40 elliott: driving someone to drink is good 09:18:45 why 09:18:52 otherwise they might drink and drive 09:30:11 There's a new series of PSAs on avoiding drinking and driving going on on a local TV station, they're very cute. 09:30:34 There's a drinking bird and a drinking fish. 09:30:47 kmc: should I stop making kmc drugz jokes 09:34:16 if kmc minds all these tasteless kmc drugz jokes i'll stop making them too 09:37:34 -!- mnoqy has joined. 09:40:30 can't promise I'll stop making them but I might be able to install some kind of weekly quota 09:40:42 hi mnoqy 09:40:47 hi 09:40:59 should i refrain from bugging you about fixed points like i've been bugging everyone else 09:41:08 btw fixed points are p. great 09:41:10 hm most likely 09:41:30 hm ok 10:01:30 kmc: look how great we are re: faq 10:13:27 -!- sprocklem has quit (Remote host closed the connection). 10:38:14 -!- zzo38 has quit (Remote host closed the connection). 10:50:16 -!- MindlessDrone has joined. 11:00:16 -!- sacje has quit (Quit: sacje). 11:22:53 -!- oonbotti has quit (Disconnected by services). 11:23:32 -!- Koen_ has joined. 11:23:49 -!- Phantom_Hoover has joined. 11:24:36 -!- Koen__ has joined. 11:24:36 -!- Koen_ has quit (Read error: Connection reset by peer). 12:16:40 shachaf: What is your fixed point? 12:17:37 > let shachaf = \x -> (fix x shachaf,shachaf) in fix shachaf 12:17:38 Occurs check: cannot construct the infinite type: 12:17:38 t2 = ((t2 -> t0) -> t2... 12:17:47 > let shachaf = \x -> (shachaf x,shachaf) in fix shachaf 12:17:48 Occurs check: cannot construct the infinite type: t1 = (t1, t2)Occurs check... 12:21:33 > let shachaf = fix in fix shachaf 12:21:34 Occurs check: cannot construct the infinite type: a0 = a0 -> a0 12:21:34 Expected t... 12:21:42 > let shachaf = fix shachaf in fix shachaf 12:21:43 Occurs check: cannot construct the infinite type: a0 = a0 -> a0 12:21:47 Ok 12:37:39 -!- nooodl has joined. 12:58:47 -!- sacje has joined. 13:25:30 -!- mnoqy has quit (Ping timeout: 241 seconds). 13:25:58 -!- mnoqy has joined. 14:12:30 -!- oerjan has joined. 14:28:00 -!- intosh has joined. 14:28:38 -!- olsner has quit (Ping timeout: 268 seconds). 14:31:30 Is the sequence of the even naturals computable by a push down automaton 14:35:26 how does a push down automaton compute naturals? 14:36:03 hi oerjan 14:36:07 hi shachaf 14:36:16 any clues on fixed points 14:36:18 That is a question 14:36:42 Taneb: even a finite automaton can _recognize_ them, after all. 14:37:15 Some form of printy dealy? 14:38:12 i suspect they cannot, if printing a number means you have to look deep in the stack 14:38:29 because that obviously erases most of it 14:39:46 hm does a pumping lemma apply to output as well? 14:40:50 that'd be a pumpout lemma 14:41:05 shachaf: only that Knaster-Tarski was missing the Fixed-point theorem category. which i've now fixed. 14:41:26 (ok i guess i have learned some fixed-point theorems in my time.) 14:41:47 oerjan: plz add redirect knaster-tarski ----> Knaster–Tarski theorem 14:41:58 i just went to that page and it didn't exist 14:42:11 thx hth wwod 14:42:21 shachaf: um surely you'd get a direct suggestion. i think that's overdoing it. 14:42:36 uh 14:42:50 have you seen the redirect pages wikipedia has 14:43:48 shachaf: well it shows up if you _search_ for knaster-tarski, anyhow. 14:44:21 oerjan: anyway read http://ncatlab.org/nlab/show/fixed+point instead 14:44:36 it's p. good as nlab pages go 14:48:20 too tired 14:48:32 * oerjan thinks he may have a cold 14:50:37 hm what does the pumping lemma correspond to directly on pd automata. 14:51:26 hm i think a pd automaton with only output is sort of equivalent to a pd automaton that accepts only one input... 14:51:41 (well, if deterministic.) 14:53:02 in this case the accepted input is infinite, but i doubt that makes much of a difference? 14:55:11 -!- epicmonkey has quit (Read error: Operation timed out). 14:55:27 Taneb: i think that's equivalent to asking if the language of strings of the form "2,4,...,2n" (with your chosen output representation) is context-free. 14:56:29 i'm pretty sure the pumping lemma disallows that. 14:57:22 in fact you don't even need to restrict it to _even_ naturals, it cannot produce the naturals themselves. 15:09:02 Now, a logic with the axiom "not P" for all formulas P would definitely be inconsistent. <-- hm is intuitionistic logic inconsistent with that? 15:10:21 if you cannot deduce P from not (not P), then it's no longer _obvious_ that you can get an inconsistency from that... 15:10:25 -!- Nisstyre-laptop has joined. 15:11:05 If a : not (not P) and b : not P, then a b : False. 15:11:39 oh right duh 15:12:14 you need to disallow False -> P somehow. 15:14:20 Disallow ex falso quodlibet? 15:14:37 yeah 15:15:24 isn't that what paraconsistent logics do, or maybe they just don't allow you to deduce false 15:15:44 I think both are options. 15:16:01 But I think it's more common for (P and not P) not to imply False. 15:16:29 -!- Nisstyre-laptop has quit (Quit: Leaving). 15:16:34 ok 15:17:24 because if you wanted to keep the intuitionistic definition of not P = P -> False, the other option would seem better 15:25:00 -!- hagb4rd has quit (Quit: reboot). 15:26:45 -!- longsight has joined. 15:31:07 holy shit my electric razor short circuited 15:37:36 -!- longsight has quit (Ping timeout: 252 seconds). 15:37:52 -!- Phantom_Hoover has quit (Ping timeout: 256 seconds). 15:45:40 -!- hagb4rd has joined. 15:54:58 -!- Phantom_Hoover has joined. 15:56:54 `addquote I would like to learn how to use a sword And also how to ride a unicycle Perhaps not at the same time 15:57:01 oh wait 15:57:04 `revert 15:57:07 Done. 15:57:11 `revert 15:57:18 * oerjan confuses himself 15:57:21 1065) I would like to learn how to use a sword And also how to ride a unicycle Perhaps not at the same time 15:57:24 Done. 15:57:34 `quote 1065 15:57:36 No output. 15:57:41 `revert 15:57:44 Done. 15:57:47