Newest at the top
| 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" >:) |
| 2025-01-18 00:10:37 +0100 | <EvanR> | I'll have to look that up and hope it's not ridiculously trivial lol |
| 2025-01-18 00:10:24 +0100 | <EvanR> | Herbrand |
| 2025-01-18 00:09:59 +0100 | <EvanR> | when you're dealing with raw data, no IO |
| 2025-01-18 00:09:51 +0100 | <monochrom> | In particular if you think that you are using merely syntax trees for your argument, then you are choosing the Herbrand model, therefore it's a model, therefore it's also a semantics! There is no escape from arguing semantics |
| 2025-01-18 00:09:43 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 264 seconds) |
| 2025-01-18 00:09:35 +0100 | <EvanR> | which happens in haskell sometimes |
| 2025-01-18 00:09:22 +0100 | <EvanR> | and never really refer to any meaning |
| 2025-01-18 00:09:12 +0100 | <EvanR> | or the logic of how you put the sentences together |
| 2025-01-18 00:08:56 +0100 | <EvanR> | because you're really talking about the syntax |
| 2025-01-18 00:08:49 +0100 | <EvanR> | sometimes something can be said about any possible semantics |
| 2025-01-18 00:08:12 +0100 | <monochrom> | I think both are necessarily semantic. But then that's a tautology. You need to choose a semantic (aka model again) before you can argue anything. |
| 2025-01-18 00:05:55 +0100 | <monochrom> | You can choose a different level of abstraction (aka model) you get a different conclusion. This is supposed to be normal. |
| 2025-01-18 00:05:34 +0100 | <EvanR> | uncountable is necessarily semantic |
| 2025-01-18 00:05:15 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) |
| 2025-01-18 00:05:13 +0100 | <EvanR> | monochrom, yes that's what I was getting at |
| 2025-01-18 00:04:59 +0100 | <EvanR> | also there's a difference between computable real and algorithmic real |
| 2025-01-18 00:04:43 +0100 | <monochrom> | And it is also related to the deal with real numbers, set theory, everything. There are countable models of ZFC, and yet there are also uncountable sets. |
| 2025-01-18 00:04:42 +0100 | <geekosaur> | hence are countable |
| 2025-01-18 00:04:38 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 00:04:37 +0100 | <geekosaur> | yes |
| 2025-01-18 00:04:26 +0100 | <haskellbridge> | <thirdofmay18081814goya> geekosaur: the computable reals are embeddable in the naturals! |
| 2025-01-18 00:04:12 +0100 | <EvanR> | is "x" there a metavariable or literally x |
| 2025-01-18 00:04:06 +0100 | <geekosaur> | there are countably many values of IEEE float or double, though. you're limited to some form of "computable reals" on any physical computer |
| 2025-01-18 00:03:19 +0100 | <haskellbridge> | <thirdofmay18081814goya> well if a theory is a set of axioms and derivable sentences, then we should admit such a language (the one having the judgment 'x is a value of type Real Number') |
| 2025-01-18 00:03:02 +0100 | <EvanR> | usually you need a language for that |
| 2025-01-18 00:02:56 +0100 | <EvanR> | as far as real numbers go it's a pretty nutty way to specify one xD |
| 2025-01-18 00:02:47 +0100 | <monochrom> | We know of at least two theories (aka models) of programming, and they disagree on countability as well as other things. The moral is that you choose a theory to suit a purpose, not for Platonic "absolute" "truth". |
| 2025-01-18 00:02:29 +0100 | paul_j | (~user@8.190.187.81.in-addr.arpa) (Quit: Asta la vista) |
| 2025-01-18 00:02:23 +0100 | <EvanR> | jumping to another level of abstraction, beyond the syntax |
| 2025-01-18 00:02:04 +0100 | <EvanR> | that's mixing concepts |
| 2025-01-18 00:01:38 +0100 | <haskellbridge> | <thirdofmay18081814goya> right, e.g. a language with the judgment 'x is a value of type Real Number' does not have countably many statements I think |
| 2025-01-18 00:01:18 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 244 seconds) |
| 2025-01-18 00:00:52 +0100 | <EvanR> | haskell being an example of one |
| 2025-01-18 00:00:45 +0100 | <monochrom> | "I thank GHC for suggesting this newtype." |
| 2025-01-18 00:00:41 +0100 | <EvanR> | formal languages come with grammar rules which limit you to a countable number of sentences |
| 2025-01-18 00:00:19 +0100 | <monochrom> | And on second thought, I am not even sure I can take credit. My purpose was to make a newtype to allow the like of (\x -> x x), and the error message literally inspires that definition! |
| 2025-01-18 00:00:01 +0100 | <EvanR> | countable and constructible is certainly not the same thing |
| 2025-01-17 23:59:57 +0100 | <haskellbridge> | <thirdofmay18081814goya> I am not convinced there are countably many statements in any mathematical theory |
| 2025-01-17 23:59:36 +0100 | <EvanR> | which doesn't stop people believing in uncountability |