Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
| From | Mild Shock <janburse@fastmail.fm> |
|---|---|
| Newsgroups | sci.math |
| Subject | Re: Ordinals |
| Date | 2024-02-23 00:41 +0100 |
| Message-ID | <ur8m32$foln$1@solani.org> (permalink) |
| References | (5 earlier) <e0764275-04d6-462d-9ee5-fbfb983343ca@att.net> <cRSdnUA1bNQn8kj4nZ2dnZfqnPqdnZ2d@giganews.com> <-DGdncLb25xXokv4nZ2dnZfqn_qdnZ2d@giganews.com> <ur6v5g$etpf$1@solani.org> <96c85c51-cd42-4119-b389-01831dff5b0b@att.net> |
This is the school that tries to avoid
higher order logic (HOL). And then sneaks in
classes as a kind of syntactic sugar into
FOL, with this rule:
x e { y | p(y) } <=> p(x)
If you are not wearing this chastity belt, its
just some HOL juggling. Like here:
Ross Finlayson schrieb:
>
https://leanprover-community.github.io/mathlib_docs/set_theory/zfc/basic.html#Class
But I suggest to study simple types first. And
then maybe dependent types. To understand the
type theoretic capture of set theory.
See also:
Should Type Theory Replace Set Theory as
the Foundation of Mathematics?
13 February 2023 - Thorsten Altenkirch
https://link.springer.com/article/10.1007/s10516-023-09676-0
Jim Burns schrieb:
> I once had a lecturer in math who would refer to
> proper classes as "syntactic sugar",
> which I found out today is a _programming_ term.
Back to sci.math | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread
Re: Ordinals "markus...@gmail.com" <markusklyver@gmail.com> - 2024-02-20 11:35 -0800
Re: Ordinals Mild Shock <janburse@fastmail.fm> - 2024-02-20 20:54 +0100
Re: Ordinals "mitchr...@gmail.com" <mitchrae3323@gmail.com> - 2024-02-20 11:59 -0800
Re: Ordinals Ross Finlayson <ross.a.finlayson@gmail.com> - 2024-02-20 12:15 -0800
Re: Ordinals Ross Finlayson <ross.a.finlayson@gmail.com> - 2024-02-20 12:27 -0800
Re: Ordinals Jim Burns <james.g.burns@att.net> - 2024-02-20 17:02 -0500
Re: Ordinals Ross Finlayson <ross.a.finlayson@gmail.com> - 2024-02-20 19:36 -0800
Re: Ordinals Mild Shock <bursejan@gmail.com> - 2024-02-21 05:47 -0800
Re: Ordinals Mild Shock <bursejan@gmail.com> - 2024-02-21 05:50 -0800
Re: Ordinals Mild Shock <bursejan@gmail.com> - 2024-02-21 06:16 -0800
Re: Ordinals Ross Finlayson <ross.a.finlayson@gmail.com> - 2024-02-21 10:24 -0800
Re: Ordinals Mild Shock <janburse@fastmail.fm> - 2024-02-22 09:03 +0100
Re: Ordinals Mild Shock <janburse@fastmail.fm> - 2024-02-22 09:11 +0100
Re: Ordinals Ross Finlayson <ross.a.finlayson@gmail.com> - 2024-02-22 10:16 -0800
Re: Ordinals Mild Shock <janburse@fastmail.fm> - 2024-02-22 19:20 +0100
Re: Ordinals Mild Shock <janburse@fastmail.fm> - 2024-02-22 19:22 +0100
Re: Ordinals Mild Shock <janburse@fastmail.fm> - 2024-02-22 19:40 +0100
Re: Ordinals Mild Shock <janburse@fastmail.fm> - 2024-02-22 20:00 +0100
Re: Ordinals Ross Finlayson <ross.a.finlayson@gmail.com> - 2024-02-22 10:55 -0800
Re: Ordinals Mild Shock <janburse@fastmail.fm> - 2024-02-22 20:08 +0100
Re: Ordinals Mild Shock <janburse@fastmail.fm> - 2024-02-22 20:13 +0100
Re: Ordinals Ross Finlayson <ross.a.finlayson@gmail.com> - 2024-02-22 11:01 -0800
Re: Ordinals Mild Shock <janburse@fastmail.fm> - 2024-02-22 20:11 +0100
Re: Ordinals Mild Shock <janburse@fastmail.fm> - 2024-02-22 20:13 +0100
Re: Ordinals Jim Burns <james.g.burns@att.net> - 2024-02-22 14:34 -0500
Re: Ordinals Ross Finlayson <ross.a.finlayson@gmail.com> - 2024-02-22 11:39 -0800
Re: Ordinals Mild Shock <janburse@fastmail.fm> - 2024-02-23 00:41 +0100
Re: Ordinals WM <wolfgang.mueckenheim@tha.de> - 2024-02-21 08:33 +0000
Re: Ordinals Jim Burns <james.g.burns@att.net> - 2024-02-21 12:59 -0500
Re: Ordinals WM <wolfgang.mueckenheim@tha.de> - 2024-02-22 13:00 +0000
Re: Ordinals Jim Burns <james.g.burns@att.net> - 2024-02-22 11:13 -0500
Re: Ordinals WM <wolfgang.mueckenheim@tha.de> - 2024-02-23 08:47 +0000
Semanticists candy (Was: Ordinals) Mild Shock <janburse@fastmail.fm> - 2024-02-26 12:58 +0100
Re: Ordinals Jim Burns <james.g.burns@att.net> - 2024-02-27 14:25 -0500
Re: Ordinals Ross Finlayson <ross.a.finlayson@gmail.com> - 2024-02-27 11:59 -0800
Re: Ordinals WM <wolfgang.mueckenheim@tha.de> - 2024-02-27 20:05 +0000
Re: Ordinals Jim Burns <james.g.burns@att.net> - 2024-02-27 17:24 -0500
Re: Ordinals WM <wolfgang.mueckenheim@tha.de> - 2024-02-28 09:48 +0000
Re: Ordinals Jim Burns <james.g.burns@att.net> - 2024-02-28 06:52 -0500
Re: Ordinals WM <wolfgang.mueckenheim@tha.de> - 2024-02-28 17:24 +0000
Re: Ordinals Richard Damon <richard@damon-family.org> - 2024-02-28 17:07 -0500
Re: Ordinals WM <wolfgang.mueckenheim@tha.de> - 2024-02-29 08:23 +0000
Re: Ordinals Richard Damon <richard@damon-family.org> - 2024-02-29 07:35 -0500
Re: Ordinals WM <wolfgang.mueckenheim@tha.de> - 2024-02-29 19:25 +0000
Re: Ordinals "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2024-02-29 13:48 -0800
Re: Ordinals Richard Damon <richard@damon-family.org> - 2024-02-29 22:12 -0500
Re: Ordinals Ross Finlayson <ross.a.finlayson@gmail.com> - 2024-02-29 19:36 -0800
Re: Ordinals Mild Shock <janburse@fastmail.fm> - 2024-03-01 20:38 +0100
Re: Ordinals Mild Shock <janburse@fastmail.fm> - 2024-03-01 20:52 +0100
Re: Ordinals Mild Shock <janburse@fastmail.fm> - 2024-03-01 21:08 +0100
Re: Ordinals Jim Burns <james.g.burns@att.net> - 2024-03-01 15:56 -0500
Re: Ordinals Mild Shock <janburse@fastmail.fm> - 2024-03-01 22:53 +0100
Re: Ordinals Mild Shock <janburse@fastmail.fm> - 2024-03-01 23:11 +0100
Re: Ordinals Mild Shock <janburse@fastmail.fm> - 2024-03-01 23:33 +0100
Re: Ordinals Jim Burns <james.g.burns@att.net> - 2024-03-01 19:41 -0500
Re: Ordinals Ross Finlayson <ross.a.finlayson@gmail.com> - 2024-03-01 20:15 -0800
Re: Ordinals Ross Finlayson <ross.a.finlayson@gmail.com> - 2024-03-02 10:49 -0800
Re: Ordinals Mild Shock <janburse@fastmail.fm> - 2024-03-02 20:40 +0100
Re: Ordinals Ross Finlayson <ross.a.finlayson@gmail.com> - 2024-03-01 14:45 -0800
Re: Ordinals WM <wolfgang.mueckenheim@tha.de> - 2024-03-01 08:47 +0000
Re: Ordinals Richard Damon <richard@damon-family.org> - 2024-03-01 09:44 -0500
Re: Ordinals WM <wolfgang.mueckenheim@tha.de> - 2024-03-01 18:29 +0000
Re: Ordinals Richard Damon <richard@damon-family.org> - 2024-03-01 14:00 -0500
Re: Ordinals WM <wolfgang.mueckenheim@tha.de> - 2024-03-02 12:36 +0000
Re: Ordinals Richard Damon <richard@damon-family.org> - 2024-03-02 09:22 -0500
Re: Ordinals WM <wolfgang.mueckenheim@tha.de> - 2024-03-02 15:25 +0000
Re: Ordinals "mitchr...@gmail.com" <mitchrae3323@gmail.com> - 2024-02-20 17:21 -0800
RSemanticists candy (Re: Ordinals) [Addendum] Mild Shock <janburse@fastmail.fm> - 2024-02-26 13:01 +0100
csiph-web