←2017-07-23 2017-07-24 2017-07-25→ ↑2017 ↑all
00:01:13 -!- augur has joined.
00:34:07 -!- hppavilion[1] has quit (Read error: Connection reset by peer).
00:34:31 -!- hppavilion[1] has joined.
00:35:01 -!- Slereah has quit (Ping timeout: 255 seconds).
00:47:35 -!- Slereah has joined.
00:50:49 -!- Slereah__ has joined.
00:52:01 -!- Slereah has quit (Ping timeout: 248 seconds).
00:56:57 -!- Slereah has joined.
00:58:17 -!- Slereah__ has quit (Ping timeout: 260 seconds).
00:59:30 -!- Slereah__ has joined.
01:01:47 -!- Slereah has quit (Ping timeout: 260 seconds).
01:14:03 -!- Slereah has joined.
01:14:16 -!- Slereah__ has quit (Ping timeout: 260 seconds).
01:30:00 -!- xkapastel has quit (Quit: Connection closed for inactivity).
01:31:08 -!- ais523 has joined.
01:36:14 -!- Slereah__ has joined.
01:37:27 -!- Slereah has quit (Ping timeout: 240 seconds).
01:38:49 -!- Slereah has joined.
01:40:23 -!- imode has joined.
01:40:52 -!- Slereah__ has quit (Ping timeout: 260 seconds).
01:46:43 -!- Slereah__ has joined.
01:47:35 -!- Slereah has quit (Ping timeout: 240 seconds).
01:52:58 -!- doesthiswork has joined.
02:35:00 -!- tswett_ has joined.
02:35:13 -!- ais523 has quit (Remote host closed the connection).
02:36:24 -!- ais523 has joined.
02:42:28 -!- Slereah__ has quit (Ping timeout: 260 seconds).
02:50:17 -!- hppavilion[1] has quit (Ping timeout: 260 seconds).
02:54:04 -!- hppavilion[1] has joined.
03:10:07 -!- Slereah has joined.
03:14:52 -!- Slereah__ has joined.
03:16:35 -!- Slereah has quit (Ping timeout: 240 seconds).
03:19:18 -!- Slereah__ has quit (Ping timeout: 255 seconds).
03:25:49 <zzo38> We can invent the computer design that is like half between MIX and MMIX (almost), and, can be call MDIX.
03:26:43 <shachaf> zzo38: But I thought you said that MIX wasn't referring to a number.
03:26:45 <shachaf> `5 w
03:26:49 <HackEgo> 1/2:smell//Smell is a sense, which is particularly strong in old factory sites. \ the u//The U are a very mad people. \ program//A program is an image created by means of prography. \ warranty//HACKEGO COMES WITHOUT WARRANTY, EXPRESS OR IMPLIED, AND IS UNFIT FOR ANY PURPOSE, INCLUDING THE PURPOSE OF BEING UNFIT FOR ANYTHING. Its warranty has expire
03:26:52 <shachaf> `n
03:26:53 <HackEgo> 2/2:d. \ roujo//Roujo is a Java heretic leaning on ungrammatical Haskell. His claim to Canadianness is marred by an unholy portal to China. The treaties suffer, so the cocktail will be postponed. He does not understand shell quoting.
03:27:05 <zzo38> shachaf: It is referring to a number, but not a year number.
03:27:33 -!- PattuX has quit (Quit: Connection closed for inactivity).
03:27:37 <shachaf> Why would it refer to a number?
03:28:25 <zzo38> It is an average of the numbers of many other computers of the time (rounded down), apparently.
03:29:07 <shachaf> whoa, so it is.
03:38:06 -!- Slereah has joined.
03:38:55 <shachaf> zzo38: Are you going to ICFP this year?
03:40:57 -!- tswett_ has quit (Ping timeout: 240 seconds).
03:44:40 <zzo38> I do not think so. What day and where is it anyways?
03:44:55 <shachaf> I think it's in England.
03:45:03 <shachaf> Sep 3-9, Oxford
03:50:45 <zzo38> I do not expect to be in England in September
04:19:48 -!- sleffy has quit (Ping timeout: 268 seconds).
04:20:26 <zzo38> I tried loading a MMIX program with mmotype and it says "File was created Thu Jun 16 12:35:08 1881", even though I know that isn't the case. Why it says that?
04:30:39 -!- sleffy has joined.
04:37:04 -!- hppavilion[1] has quit (Ping timeout: 268 seconds).
04:37:46 -!- sleffy has quit (Ping timeout: 276 seconds).
04:54:24 -!- hppavilion[1] has joined.
05:10:01 -!- doesthiswork has quit (Quit: Leaving.).
05:12:40 -!- doesthiswork has joined.
05:26:54 <imode> book encoding is a neat hack for really tiny graphs.
05:27:57 <imode> just encode the graph as pages of planar graphs and concatenate them together.
05:29:50 -!- ^v has quit (Ping timeout: 258 seconds).
05:38:05 -!- ais523 has quit.
05:51:12 -!- sleffy has joined.
05:57:49 <zzo38> Do you have an example of that?
06:05:35 -!- sleffy has quit (Ping timeout: 240 seconds).
06:06:06 <imode> https://en.wikipedia.org/wiki/Book_embedding
06:07:56 <zzo38> OK
06:08:50 <zzo38> OK, that picture explains it
06:21:36 -!- erkin has joined.
06:46:13 -!- sleffy has joined.
07:02:08 -!- FreeFull has quit.
07:04:37 -!- sleffy has quit (Ping timeout: 260 seconds).
07:05:03 -!- sleffy has joined.
07:32:47 -!- doesthiswork has quit (Quit: Leaving.).
07:33:26 -!- sleffy has quit (Ping timeout: 268 seconds).
07:33:52 -!- sleffy has joined.
08:01:11 <zzo38> I have this way to round up to one less than a power of two in MMIX: SRU $0,in,8; ZSNZ $1,$0,255; MOR $0,#FF7F3F1F0F070301,in; OR out,$0,$1 (This assumes the input is a 16-bit number) Is there a better way?
08:01:40 -!- augur has quit (Remote host closed the connection).
08:02:43 <shachaf> Meaning, set all the bits lower than the highest set bit?
08:02:53 <zzo38> Yes
08:02:59 <zzo38> That is the same thing
08:05:28 <zzo38> (For a 8-bit number, the third instruction by itself is sufficient)
08:10:25 -!- sleffy has quit (Ping timeout: 255 seconds).
08:12:29 -!- sleffy has joined.
08:19:05 -!- augur has joined.
08:19:09 <zzo38> Do you like this?
08:20:40 -!- imode has quit (Ping timeout: 246 seconds).
08:20:41 <zzo38> There is also the way to reverse the bits of a 64-bit number in MMIX, which uses MOR twice, with the constant #0102040810204080, but once in the Y position and once in the Z position.
08:21:57 <zzo38> I think the MOR instruction of MMIX really is useful.
08:23:27 -!- augur has quit (Ping timeout: 240 seconds).
08:25:12 <shachaf> Do you like MXOR?
08:26:57 <zzo38> MXOR has less uses that I can find, but it may be good too
08:29:48 -!- AnotherTest has joined.
08:31:33 <shachaf> Obviously the one you mentioned has mor uses.
08:32:18 <zzo38> Yes
08:38:58 <HackEgo> [wiki] [[Ly]] https://esolangs.org/w/index.php?diff=52527&oldid=52520 * LyricLy * (+89)
08:39:20 -!- augur has joined.
08:40:29 <HackEgo> [wiki] [[Ly]] https://esolangs.org/w/index.php?diff=52528&oldid=52527 * LyricLy * (+58) /* ly.py */
08:41:17 -!- augur has quit (Remote host closed the connection).
08:43:54 -!- sleffy has quit (Ping timeout: 240 seconds).
08:47:05 <int-e> A single MXOR can be used to convert 8 bytes simultaneously from/to Gray code. Unfortunately, that's the most convincing use of MXOR that I have so far, disregarding the fact that in many cases, MXOR and MOR can be used interchangably, because one of the matrices is a permutation matrix. It seems that MXOR should help for some computations in GF(2^8) at least.
08:50:44 <zzo38> I did not think of Gray code, although I did realize the other thing you mention
09:34:43 -!- PattuX has joined.
10:48:29 -!- hppavilion[1] has quit (Quit: HRII'FHALMA MNAHN'K'YARNAK NGAH NILGH'RI'BTHNKNYTH).
11:34:51 -!- boily has joined.
11:38:09 <boily> @metar CYUL
11:38:09 <lambdabot> CYUL 241000Z 04011G17KT 15SM BKN055 OVC080 17/09 A2986 RMK SC6AC2 SLP114 DENSITY ALT 500FT
11:42:00 -!- augur has joined.
11:46:25 -!- augur has quit (Ping timeout: 248 seconds).
12:10:43 <boily> @metar CYUL
12:10:43 <lambdabot> CYUL 241100Z 04013KT 15SM OVC055 17/09 A2988 RMK SC8 SLP121 DENSITY ALT 500FT
12:10:59 <boily> clouder.
12:29:45 -!- boily has quit (Quit: HARMONIC CHICKEN).
13:31:58 <\oren\> https://twitter.com/Witch_chan2000/status/879189141954625539
13:37:49 -!- imode has joined.
14:00:32 -!- doesthiswork has joined.
14:30:16 -!- `^_^v has joined.
14:34:28 <Jafet> bad wikipedia articles are a gold mine of ideas
14:34:53 <Jafet> A program is how a robot decides when or how to do something.
14:35:13 <Jafet> a Program is a group of related projects managed in a coordinated manner to obtain benefits and control
14:35:40 <Jafet> the source code of a program is the design for the program that it produces
14:35:52 <Jafet> A program was a stack of layers.
14:45:38 -!- GeoDude has changed nick to GeekDude.
14:48:19 -!- tswett has quit (Quit: Leaving).
15:13:12 -!- doesthiswork has quit (Quit: Leaving.).
15:41:50 -!- heroux has quit (Ping timeout: 268 seconds).
15:42:41 -!- augur has joined.
15:43:29 -!- heroux has joined.
15:47:12 -!- augur has quit (Ping timeout: 255 seconds).
15:50:06 -!- erkin has quit (Quit: Ouch! Got SIGABRT, dying...).
15:53:08 -!- `^_^v has quit (Ping timeout: 258 seconds).
15:54:30 -!- PattuX has quit (Quit: Connection closed for inactivity).
15:57:20 -!- `^_^v has joined.
16:37:27 -!- AnotherTest has quit (Ping timeout: 260 seconds).
16:46:25 -!- viznut_ has changed nick to viznut.
17:01:18 -!- `^_^v has quit (Quit: This computer has gone to sleep).
17:07:41 -!- PattuX has joined.
17:08:48 <\oren\> Lol I have a huge office to myself right now. we got a second office recently to store more programmers in but noone wants to be the first guy on the new office
17:12:33 -!- augur has joined.
17:21:40 -!- LKoen has joined.
17:27:12 -!- FreeFull has joined.
17:44:09 -!- augur has quit (Remote host closed the connection).
17:53:37 -!- __kerbal__ has joined.
18:04:28 -!- `^_^v has joined.
18:05:05 -!- Sprocklem has quit (Ping timeout: 248 seconds).
18:12:15 <* Taneb> hello
18:13:22 -!- AnotherTest has joined.
18:13:53 <__kerbal__> hello
18:17:07 <Taneb> I've just had a few rather fun days in Italy
18:17:55 <shachaf> Haneb
18:19:21 <Taneb> Hichaf
18:19:29 <shachaf> I saw that you saw a cat.
18:19:48 <shachaf> i was all, like, whoa, dude
18:20:00 <Taneb> Yes!
18:20:04 <Taneb> That was in Venice!
18:20:40 <shachaf> I saw a good cat last night but I didn't photograph.
18:26:28 <shachaf> `5 w
18:26:34 <HackEgo> 1/1:warrigal//Warrigal is #esoteric's resident dingo. It sometimes pretends to be a human. \ yeeeeeeesh//See yeeeeeesh. \ the//the Toe of Harriness's Enclosure \ hacker//Jim Hacker is a former British prime minister. \ companion cube//There's cake inside it. Tear it apart, rip open your companion, and extract the delicious, delicious cake...
18:27:11 <shachaf> `cwlprits companion cube
18:27:18 <HackEgo> zgrëp zgrëp
18:27:21 <shachaf> `? cats
18:27:22 <HackEgo> Cats are cool, but should be illegal.
18:27:26 <shachaf> `? kitten
18:27:27 <HackEgo> kitten? ¯\(°​_o)/¯
18:30:47 <\oren\> Argh, the coffee machine is very advanced, but you still have to take the milk carafe out of the fridge and put it back each time
18:31:14 <LKoen> I've seen coffee machines that made lattes
18:31:31 <\oren\> Maybe in 2020 we'll finally have an integrated milk chiller
18:34:09 <\oren\> 식료품groceries is good music for blasting in a completely empty empty office
18:34:56 <APic> lulz
18:34:58 <APic> Good one!
18:45:29 <imode> thanks for the weird music \oren\.
18:47:24 -!- LKoen has quit (Quit: “It’s only logical. First you learn to talk, then you learn to think. Too bad it’s not the other way round.”).
18:53:11 -!- augur has joined.
18:53:22 -!- sleffy has joined.
18:54:12 -!- augur has quit (Remote host closed the connection).
18:55:21 -!- augur has joined.
19:08:20 <Jafet> `` cd wisdom; for f in ye*sh; do \? $f; done
19:08:24 <HackEgo> ​/hackenv/bin/?: line 5: cd: wisdom: Not a directory \ /hackenv/bin/?: line 5: cd: wisdom: Not a directory \ /hackenv/bin/?: line 5: cd: wisdom: Not a directory \ /hackenv/bin/?: line 5: cd: wisdom: Not a directory \ /hackenv/bin/?: line 5: cd: wisdom: Not a directory \ /hackenv/bin/?: line 5: cd: wisdom: Not a directory \ /hackenv/bin/?: line 5:
19:09:29 -!- ais523 has joined.
19:09:55 <Jafet> `` cd wisdom; for f in ye*sh; do echo -n "$f//"; cat "$f"; done
19:09:56 <HackEgo> yeeeeeeeeeesh//See yeeeeeeeeesh. \ yeeeeeeeesh//See yeeeeeeesh. \ yeeeeeeesh//See yeeeeeesh. \ yeeeeeesh//See yeeeeesh. \ yeeeeesh//See yeeeesh. \ yeeeesh//See yeeesh. \ yeeesh//See yeesh.
19:10:06 <Jafet> `? yeesh
19:10:07 <HackEgo> yeesh? ¯\(°​_o)/¯
19:10:31 <shachaf> `dowg yeesh
19:10:37 <HackEgo> No output.
19:10:40 <int-e> how useful
19:10:45 <APic> 😎
19:10:47 <shachaf> `dowg yeeesh
19:10:54 <HackEgo> 6202:2015-11-10 <tsweẗt> le/rn yeeesh/See yeesh.
19:11:12 <int-e> `dowg yeeeeeeeeeesh
19:11:18 <HackEgo> 6229:2015-11-19 <tsweẗt> le/rn yeeeeeeeeeesh/See yeeeeeeeeesh.
19:11:28 <int-e> one per day?
19:11:30 <int-e> `dowg yeeeeeeeeesh
19:11:36 <HackEgo> 10346:2017-03-04 <shachäf> forget yeeeeeeeeesh \ 6228:2015-11-19 <tsweẗt> le/rn yeeeeeeeeesh/See yeeeeeeeesh.
19:12:09 <shachaf> `? int-e
19:12:10 <HackEgo> int-e är inte svensk. Hen kommer att spränga solen. Hen står för sig själv. Hen gillar inte färger, men han gillar dissonans. Er hat ein Hipster-Spiel gekauft.
19:12:28 <shachaf> int-e is into rutabagas?
19:13:05 <Jafet> `` echo wisdom/no*dl
19:13:06 <HackEgo> wisdom/nooooodl
19:13:27 -!- augur has quit (Remote host closed the connection).
19:14:31 <int-e> shachaf: why'd you "`forget" that one but not the others?
19:15:05 <shachaf> So you'll have something to ask.
19:15:39 <shachaf> `dowg yeeeeesh
19:15:45 <HackEgo> 11080:2017-07-10 <boil̈y> revert \ 11079:2017-07-10 <boil̈y> forget yeeeeesh \ 6200:2015-11-10 <tsweẗt> le/rn yeeeeesh/See yeeeesh.
19:15:48 <int-e> `cd wisdom; echo ye*sh
19:15:49 <HackEgo> invalid command ( ͡° ͜ʖ ͡°)
19:15:53 <int-e> `` cd wisdom; echo ye*sh
19:15:54 <HackEgo> yeeeeeeeeeesh yeeeeeeeesh yeeeeeeesh yeeeeeesh yeeeeesh yeeeesh yeeesh
19:16:02 <shachaf> `doag bin/cd
19:16:09 <HackEgo> 7819:2016-05-06 <Moon_̈_> mkx bin/cd//erro "invalid command ( \xcd\xa1\xc2\xb0 \xcd\x9c\xca\x96 \xcd\xa1\xc2\xb0)" \ 7818:2016-05-06 <Moon_̈_> mkx bin/cd//erro invalid command ( \xcd\xa1\xc2\xb0 \xcd\x9c\xca\x96 \xcd\xa1\xc2\xb0) \ 7817:2016-05-06 <Moon_̈_> mkx bin/cd//echo stop trying, it doesnt work
19:16:27 <shachaf> `rm bin/cd
19:16:28 <HackEgo> No output.
19:16:35 <shachaf> cd oughtn't be a command anyway.
19:16:41 <int-e> `` rm wisdom/ye*sh
19:16:43 <HackEgo> No output.
19:16:45 <APic> kkkk
19:16:46 <APic> 😉
19:16:59 <shachaf> Except I once wrote a cd program that attaches to its parent with ptrace and changes its current directory.
19:17:24 <int-e> Oh it's part of the moon episode.
19:19:30 -!- ais523 has quit (Remote host closed the connection).
19:20:40 -!- ais523 has joined.
19:21:44 -!- __kerbal__ has quit (Ping timeout: 260 seconds).
19:24:42 -!- ais523 has quit (Remote host closed the connection).
19:25:53 -!- ais523 has joined.
19:26:15 -!- augur has joined.
20:29:46 -!- imode has quit (Ping timeout: 255 seconds).
20:43:37 <shachaf> `5 w
20:43:41 <HackEgo> 1/3:virgil//Virgil is a prayer at dawn, as well as an ancient Italian poet who led Dante to hell so they can ask the blind transgendered seer Anchises stupid politics questions concerning contemporary noble families. \ dingbat//dingbat is a famous font designer for Microsoft. \ usb3//USB3 hosts are packaged with a full independent implementation of
20:43:43 <shachaf> `n
20:43:44 <HackEgo> 2/3: the older USB/USB2, going through separate pins in the same socket. It is similar to DVI, except you need a separate passive converter stub to plug VGA monitor to DVI socket, but you don't need one to plug a USB client to an USB3 host. \ ngram model//An ngram model is just a Markov model with a sliding window state. \ associativity//Associativ
20:43:46 <shachaf> `n
20:43:47 <HackEgo> 3/3:ity means that h(th) = (ht)h, if you're flexible about it.
20:44:48 <shachaf> `5
20:44:49 <HackEgo> 1/2:255) <olsner> it is from 2002 though, I was younger then \ 763) <olsner> when everyone else was busy going "ewwww, comic sans!" I was reading the text and learned everything \ 525) <Taneb> Mayor says we need to make aluminum items <Phantom_Hoover> Taneb, PH says you need to make lava items. \ 609) <ais523> the parser would be even simpler if I
20:44:50 <shachaf> `n
20:44:51 <HackEgo> 2/2: didn't try to do type inference in it \ 127) <fungot> Sgeo: hahaah, and i love when they announced it i dare u to press alt f4 and your house ( acts 16:31 your bible)
20:45:16 <shachaf> Taneb: Don't you mean aluminium?
20:45:42 <Taneb> shachaf, Ideally, yes
21:00:38 <Jafet> this fosforic spelling dispute is sodum
21:02:00 <Jafet> apparently the element named for copernicus is copernicium
21:02:53 <shachaf> Are you sure that's not just a variant of copper?
21:03:45 <HackEgo> [wiki] [[User:Scoppini]] https://esolangs.org/w/index.php?diff=52529&oldid=44156 * Scoppini * (+14)
21:04:04 <Jafet> as surely as 1 and 1 make 2
21:04:34 <shachaf> you gotta tell me if you're a copernicus
21:04:50 <HackEgo> [wiki] [[Language list]] https://esolangs.org/w/index.php?diff=52530&oldid=52448 * Scoppini * (+14) /* S */
21:05:19 <HackEgo> [wiki] [[Language list]] https://esolangs.org/w/index.php?diff=52531&oldid=52530 * Scoppini * (+0) /* S */
21:10:53 <Jafet> there's also pernicium, named for being pernicious
21:12:59 -!- imode has joined.
21:13:46 <shachaf> Please see http://feelingmyage.co.uk/wp-content/uploads/2011/09/periodictable.gif
21:14:11 <imode> what the hell. can any of you see me?
21:14:30 <imode> or am I just typing to a dead terminal.
21:15:23 <shachaf> Or is it both?
21:15:32 <shachaf> You feel like you are being watched.
21:15:43 <imode> oh wow, okay. so this network doesn't block IRC, but it locks web browsing behind guest access.
21:15:55 <imode> time to tunnel.
21:16:36 <shachaf> I think there are easier ways to check whether you're connected to IRC, for example /msg imode test
21:16:59 <imode> shachaf: yeah, I figured. but I was so dumbstruck that I didn't think of it. :P
21:26:13 <\oren\> So I guess the main reason I even need to come to work is so I can move a jumper and push a red button now and then
21:27:32 <\oren\> er, wait not jumper. breaker?
21:27:58 <\oren\> the thingy that resets after a power problem
21:29:36 <imode> breaker.
21:29:42 <shachaf> \oren\: isn't "breaker" the name of your current build system hth
21:29:48 <\oren\> no
21:30:13 <\oren\> the component I'm working on now uses boost jam
21:32:21 <\oren\> anyway, luckily, it seems I het the right red button
21:52:06 -!- augur has quit (Remote host closed the connection).
21:58:06 -!- augur has joined.
22:12:26 <zzo38> I commonly use "PING ME" to test if IRC connection is working (the server will respond PONG if it is OK)
22:12:53 <ais523> most clients do that automatically every now and then
22:13:44 <ais523> \oren\: "circuit breaker" is the normal phrase in British English
22:14:05 <ais523> referring to a fuse-like component that works electromechanically rather than via physically catching fire, and thus is resettable rather than needing to be replaced
22:18:10 -!- imode has quit (Ping timeout: 240 seconds).
22:37:27 -!- AnotherTest has quit (Ping timeout: 240 seconds).
22:37:31 <zzo38> My own client automatically responds to the server's pings (unless you turn off that function), but does not emit its own automatically
22:38:36 -!- hppavilion[1] has joined.
22:45:43 -!- boily has joined.
22:45:46 <boily> @metar CYUL
22:45:46 <lambdabot> CYUL 242138Z 08011G16KT 5SM -RA BR FEW009 SCT014 OVC025 16/14 A2995 RMK SF1SC2SC5 SLP143 DENSITY ALT 200FT
22:50:32 -!- `^_^v has quit (Quit: This computer has gone to sleep).
23:14:18 -!- tswett has joined.
23:18:37 <tswett> I'm pondering what I might use as a "home theory" for math.
23:19:21 <tswett> A lot of mathematicians seem to "live in" ZFC. They consider the axioms of ZFC to be true statements, and they don't worry too much about their theorems not generalizing outside of ZFC.
23:20:47 <tswett> I'd call myself a bit more of a skeptic.
23:21:32 <tswett> I'll admit the axioms of extensionality, specification, pairing, union, replacement, and infinity.
23:21:40 <tswett> Power sets seem suspect.
23:21:49 <tswett> And the axiom of choice? Hahaha.
23:25:02 <tswett> I want my home theory to be something I can actually think of a model of.
23:25:25 <shachaf> Do they really?
23:25:46 <shachaf> https://arxiv.org/pdf/1212.6543.pdf suggests otherwise.
23:26:15 <tswett> It suggests that power sets *don't* seem suspect?
23:27:38 <shachaf> "Perhaps you will wake up tomorrow, check your email, and find an announcement that ZFC is inconsistent. Apparently, someone has taken the ZFC axioms, performed a long string of logical deductions, and arrived at a contradiction. The work has been checked and re-checked. There is no longer any doubt."
23:27:43 <shachaf> "How would you react? In particular, how would you feel about the implications for your own work? All your theorems would still be true under ZFC, but so too would their negations. Would you conclude that your life’s work had been destroyed?"
23:29:38 <ais523> I don't normally work in ZFC, but if I did, I'd try to identify which axiom was incorrect and see what could be proved without it
23:29:54 <ais523> the axiom of choice is a big suspect in that respect
23:30:18 <tswett> But in ZFC is inconsistent, ZF is inconsistent, too.
23:30:27 <ais523> although, I thought the axiom of choice had been proven to be independent of ZF? if so, that implies that ZFC is consistent by definition
23:30:39 <ais523> (if ZF is inconsistent, nothing is independent of it)
23:30:40 <tswett> Oh, so ZF is consistent now? :)
23:30:42 <ais523> I guess the proof could be wrong
23:31:34 <int-e> You can have the same collapse in the meta theory
23:31:45 <int-e> then ZF could be proved both consistent and inconsistent
23:31:59 <ais523> I like that
23:32:07 <ais523> OTOH it'd leave me sceptical of the proof that ZFC were inconsistent
23:32:20 <ais523> on the basis that there's no reason to conclude that that proof were "about" ZFC
23:32:22 <shachaf> british spellings are so odd sometimes
23:32:43 <ais523> US spells "sceptical" with a k, right?
23:32:51 <ais523> that looks bizarre to me
23:32:53 <shachaf> yes, sceptikal
23:33:05 <tswett> "Sceptical" is still pronounced like "skeptical", right?
23:33:20 <ais523> yes, the start is like "sceptre"
23:33:36 <ais523> (which is also spelled differently in US English, but it's the end of the word that's spelled differently, not the start)
23:33:38 <shachaf> Wait, how do you pronounce "sceptre"?
23:33:56 <ais523> skep - ter
23:33:59 <Hoolootwo> septer
23:34:10 <ais523> although come to think of it I probably pronounce it incorrectly
23:34:18 <shachaf> I always thought it was "septer", and https://encrypted.google.com/search?q=define:sceptre agrees.
23:34:24 <ais523> it'd make sence if the c were silent
23:34:41 <ais523> my written vocabulary is rather larger than my spoken vocabulary
23:34:47 <ais523> because most of my social interaction is online nowadays
23:34:56 <shachaf> I learned a lot of my English from reading.
23:35:04 <shachaf> But since then I've spoken a fair amount.
23:35:14 <tswett> So lemme figure out the... uh... what do you call a property of a category that asserts that it contains objects of a particular type?
23:35:15 <shachaf> I still have a noticeable non-native accent, though.
23:35:25 <shachaf> "has"?
23:35:31 <shachaf> "has products"
23:35:32 <tswett> Sure, a "has-property".
23:35:41 <shachaf> "gains products until end of turn"
23:35:47 <ais523> "type" here is informal-English, rather than the technical programming meaning?
23:35:49 <tswett> Lemme figure out the has-properties I'm willing to admit.
23:35:54 <tswett> ais523: yeah.
23:36:03 <tswett> So cartesian closedness is a has-property.
23:36:10 <tswett> A category is cartesian closed if it has exponentials.
23:36:19 <shachaf> "your categories have flying. your opponents' categories lose flying and cannot gain flying."
23:36:28 <ais523> tswett: we call those commutativity properties
23:36:39 <tswett> I'll take finite limits and coproducts (for $200, Alex).
23:36:46 <ais523> i.e. a property that a category obeys a certain commutative diagram
23:37:00 <ais523> some of them have distinguished objects or morphisms that are necessary to make the diagrams work
23:37:16 <shachaf> Or a certain family of commutative diagrams?
23:37:28 <shachaf> Are commutative diagrams different from equations?
23:37:28 <tswett> ais523: that sounds like it means there are commutativity properties that aren't "has-properties".
23:37:45 <tswett> Well, a commutative diagram is essentially a finite collection of equations, right?
23:37:50 <tswett> Unless it's an infinite diagram, of course.
23:37:50 <ais523> shachaf: normally they're like equations but with naturality requirements
23:38:06 <shachaf> Commutative diagrams have naturality requirements?
23:38:09 <ais523> I could explain this better if I understood it myself
23:38:11 <ais523> which I don't really
23:39:40 <tswett> I'll also take nLab's "parametrized natural numbers objects".
23:43:00 <shachaf> i,i skeptic tank
23:45:17 <ais523> shachaf: seems there /isn't/ a naturality requirement; I just looked it up
23:45:27 <ais523> so right, just equations
23:45:33 <tswett> I can, in fact, think of a model of this "theory"... I think...
23:45:40 <tswett> The objects are all primitive recursive subsets of N.
23:45:48 <tswett> And the morphisms are all primitive recursive functions.
23:45:57 -!- hppavilion[0] has joined.
23:46:20 <tswett> Where I guess a "primitive recursive subset" would have to be defined as a set whose membership function is a primitive recursive function.
23:47:36 -!- hppavilion[1] has quit (Ping timeout: 260 seconds).
23:48:40 <tswett> Except I don't know if that actually works...
23:49:51 <tswett> That category "obviously" has products, coproducts, and a PNNO. So the only question is whether or not it has pullbacks.
23:50:21 <tswett> Yeah, it totally has pullbacks.
←2017-07-23 2017-07-24 2017-07-25→ ↑2017 ↑all