Newest at the top
| 2025-01-18 01:38:29 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-18 01:33:57 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 01:30:36 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2025-01-18 01:24:21 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 248 seconds) |
| 2025-01-18 01:24:02 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 01:18:30 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) |
| 2025-01-18 01:16:07 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 252 seconds) |
| 2025-01-18 01:15:31 +0100 | tallcatparade | (~tallcatpa@2600:8801:9801:d600::c83b) |
| 2025-01-18 01:13:45 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-01-18 01:13:18 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-18 01:08:40 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 01:03:18 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 252 seconds) |
| 2025-01-18 00:58:55 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) |
| 2025-01-18 00:58:09 +0100 | tallcatparade | (~tallcatpa@99-171-182-203.lightspeed.sndgca.sbcglobal.net) (Ping timeout: 260 seconds) |
| 2025-01-18 00:57:47 +0100 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) Tuplanolla |
| 2025-01-18 00:57:47 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-18 00:53:18 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 00:47:48 +0100 | alecs | (~alecs@61.pool85-58-154.dynamic.orange.es) (Ping timeout: 244 seconds) |
| 2025-01-18 00:43:44 +0100 | alecs | (~alecs@61.pool85-58-154.dynamic.orange.es) alecs |
| 2025-01-18 00:42:44 +0100 | tallcatparade | (~tallcatpa@99-171-182-203.lightspeed.sndgca.sbcglobal.net) |
| 2025-01-18 00:42:24 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2025-01-18 00:40:47 +0100 | Everything | (~Everythin@195.138.86.118) (Quit: leaving) |
| 2025-01-18 00:37:55 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 00:35:53 +0100 | ss4 | (~wootehfoo@user/wootehfoot) (Quit: Leaving) |
| 2025-01-18 00:33:57 +0100 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2025-01-18 00:31:06 +0100 | igorantonow | (~igor@user/igorantonow) (Remote host closed the connection) |
| 2025-01-18 00:25:20 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 265 seconds) |
| 2025-01-18 00:24:37 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2025-01-18 00:23:51 +0100 | igorantonow | (~igor@user/igorantonow) igorantonow |
| 2025-01-18 00:23:13 +0100 | <monochrom> | haha, I haven't thought of that. |
| 2025-01-18 00:22:57 +0100 | <c_wraith> | does that also apply to pointfree debates? |
| 2025-01-18 00:21:50 +0100 | <lambdabot> | monochrom says: All pointless debates can be settled by going polymorphic. |
| 2025-01-18 00:21:50 +0100 | <monochrom> | @quote monochrom polymorphic |
| 2025-01-18 00:21:41 +0100 | <monochrom> | Oh and... |
| 2025-01-18 00:21:20 +0100 | tnt2 | tnt1 |
| 2025-01-18 00:21:20 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 272 seconds) |
| 2025-01-18 00:20:45 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-01-18 00:19:59 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 00:19:24 +0100 | <monochrom> | program : supporting libs :: true statement :: the proof system that proved it |
| 2025-01-18 00:18:48 +0100 | <monochrom> | And just around the same time in #haskell-offtopic we were talking about how programs come ship with their own C++ libs to avoid DLL hell. |
| 2025-01-18 00:17:58 +0100 | <monochrom> | You may need more than spelling out a rigorous statement. You may end up also needing to spell out exactly which proof system you chose. Like I said, choosing a different one leads to the opposite result. |
| 2025-01-18 00:16:30 +0100 | agent314 | (~quassel@37.19.210.25) agent314 |
| 2025-01-18 00:16:06 +0100 | agent314 | (~quassel@c-24-17-1-67.hsd1.wa.comcast.net) (Ping timeout: 252 seconds) |
| 2025-01-18 00:13:57 +0100 | <monochrom> | And whatever you do in model theory, you must respect that Herbrand models are here to stay, even if it may be an annoying silly oddball. |
| 2025-01-18 00:13:42 +0100 | <haskellbridge> | <thirdofmay18081814goya> i'll be back with a more rigorous statement |
| 2025-01-18 00:12:25 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-01-18 00:12:16 +0100 | <monochrom> | ... and I guess that's one way to see why there are countable models for ZFC! |
| 2025-01-18 00:11:52 +0100 | <monochrom> | So for example if you argue that programs are countable, you are just reminding us that the Herbrand model is countable. |
| 2025-01-18 00:11:08 +0100 | <monochrom> | It is fairly trivial. It's literally the set of ASTs. |
| 2025-01-18 00:10:48 +0100 | <monochrom> | "It's semantics all the way down" >:) |