Newest at the top
| 2026-01-15 22:30:26 +0100 | <monochrom> | HoTT, CoC, Agda, Lean, Haskell all have T and F in the language domain. |
| 2026-01-15 22:30:09 +0100 | <jreicher> | Except I'm not a platonist. :p |
| 2026-01-15 22:29:58 +0100 | <EvanR> | you might have spontaneously created a new platonic semantics for haskell beyond the ones we already had |
| 2026-01-15 22:29:25 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-15 22:29:17 +0100 | <jreicher> | Put another way, when the "output" of the "operator" is T or F, those values don't exist in the language domain. They are the semantic values in the metalanguage. |
| 2026-01-15 22:28:40 +0100 | <EvanR> | operator one of the most overloaded terms, in the process also overloading the term operator overloading |
| 2026-01-15 22:27:44 +0100 | <monochrom> | That too. Just look at GHC being written in GHC. |
| 2026-01-15 22:27:40 +0100 | <jreicher> | When we say a comparison "operator" is a predicate, the operator is linguistic, but the predication is metalinguistic. |
| 2026-01-15 22:27:11 +0100 | <EvanR> | it's relative right, you could have two of the same theories one standing for metatheory one for theory but they're the same language |
| 2026-01-15 22:26:42 +0100 | <monochrom> | In fact how about I use HoTT as the metalanguage for defining the language and semantics of set theory? |
| 2026-01-15 22:26:31 +0100 | <jreicher> | Exactly. And to me the original question was about the metalinguistic objects, and not the linguistic ones. |
| 2026-01-15 22:26:16 +0100 | pavonia | (~user@user/siracusa) siracusa |
| 2026-01-15 22:26:10 +0100 | <monochrom> | Traditional mathematics also needs a language and a metalanguage. |
| 2026-01-15 22:26:08 +0100 | <EvanR> | instead of using it for actual purposes xD |
| 2026-01-15 22:25:54 +0100 | <EvanR> | if you're proving things about the logic itself |
| 2026-01-15 22:25:37 +0100 | <jreicher> | Language and metalanguage. |
| 2026-01-15 22:25:28 +0100 | <jreicher> | Yes, but you then have two logics. The logic which is the object of study (proof), and the logic being used to study it (prove things about it). |
| 2026-01-15 22:25:06 +0100 | Everything | (~Everythin@172-232-54-192.ip.linodeusercontent.com) (Quit: leaving) |
| 2026-01-15 22:24:55 +0100 | <dolio> | Type theory has no need of logic. It has subsumed it. |
| 2026-01-15 22:24:53 +0100 | <EvanR> | type theory *is* logic |
| 2026-01-15 22:24:51 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) (Quit: Leaving...) |
| 2026-01-15 22:24:11 +0100 | <jreicher> | I think that mixes up language levels. Type theory itself needs to be written in logic, which means predicates are used to describe it. It will be different predicates that are objects within type theory. |
| 2026-01-15 22:23:57 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 22:23:50 +0100 | <dolio> | 'For every x with multiple related ys, pick one of the ys.' |
| 2026-01-15 22:23:14 +0100 | <monochrom> | In type theory, predicates are special cases of functions. |
| 2026-01-15 22:23:13 +0100 | <dolio> | Yeah, that assertion is equivalent to the axiom of choice. |
| 2026-01-15 22:22:33 +0100 | <dolio> | :) |
| 2026-01-15 22:22:32 +0100 | <jreicher> | monochrom: what do you mean? |
| 2026-01-15 22:22:20 +0100 | <monochrom> | dolio: To obtain a functional subrelation from a relation with an infinite co-domain, we quickly run into the axiom of choice... :) |
| 2026-01-15 22:19:37 +0100 | <monochrom> | jreicher: I am clearly siding with type theory rather than traditional mathematics. |
| 2026-01-15 22:17:26 +0100 | <jreicher> | Yes partial functions will definitely happen. But maybe we can accept those. The bigger problem is that if there are many y for a given x for which S(x,y) then a sub relation that is a function will not really resemble S in any meaningful way |
| 2026-01-15 22:16:32 +0100 | <dolio> | Otherwise you could only hope to get a partial function in general. |
| 2026-01-15 22:16:18 +0100 | <dolio> | I guess, you should be able to restrict the domain, too. |
| 2026-01-15 22:15:28 +0100 | Lears | Leary |
| 2026-01-15 22:15:09 +0100 | <dolio> | No, R is a sub-relation of S if R(x,y) implies S(x,y) forall x and y. |
| 2026-01-15 22:14:35 +0100 | Leary | (~Leary@user/Leary/x-0910699) (Ping timeout: 240 seconds) |
| 2026-01-15 22:14:14 +0100 | <jreicher> | dolio: And what do you mean by sub-relation? Does it also mean restricting the domain to a subset? |
| 2026-01-15 22:13:40 +0100 | <dolio> | It means there's a sub-relation that is a function. |
| 2026-01-15 22:13:26 +0100 | <jreicher> | int-e: I suspect you underestimate the significance of "most convenient". Mathematical definitions are language design in much the same way that programming languages are designed. So if a mathematician says something is "convenient", it means it's a good design. And mathematicians have been working on this much longer than computer scientists. |
| 2026-01-15 22:13:19 +0100 | Lears | (~Leary@user/Leary/x-0910699) Leary |
| 2026-01-15 22:12:55 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-01-15 22:12:07 +0100 | <jreicher> | dolio: I'm not sure what you mean by "contain", but I'm fairly sure the answer will be "no", regardless of what meaning you choose. |
| 2026-01-15 22:09:49 +0100 | <dolio> | Not that every relation from A to B is a function from A to B. |
| 2026-01-15 22:09:22 +0100 | <dolio> | jreicher: Also, relations are functions in that they are maps into a collection of truth values. |
| 2026-01-15 22:08:39 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 22:07:38 +0100 | <EvanR> | you can get a relation for any function also lets you avoid subtyping |
| 2026-01-15 22:06:56 +0100 | <dolio> | jreicher: But does every relation contain a function? |
| 2026-01-15 22:04:49 +0100 | <EvanR> | sometimes taking the place of |
| 2026-01-15 22:04:33 +0100 | <EvanR> | how concepts interrelate is more interesting than "what they are really" |
| 2026-01-15 22:03:49 +0100 | <EvanR> | :D |