Elektrine lite

← Feed

@mc@mathstodon.xyz

Post #2375039

2026-05-07 06:56 UTC

are people reinventing synthetic mathematics from first principles? https://arxiv.org/abs/2605.03868 Mumford and Friedman propose a 'practical' foundation of set theory with countable dependent choice, restricted power sets, and the existence of reals as an axiom. feels very arithmetic universe coded...

Replies (5)

  • @mabeltree@mathstodon.xyz 2026-05-07 07:42

    @mc@mathstodon.xyz To me, the introduction very much reads like https://xkcd.com/927/

    Open ##2667999

  • @JacquesC2@types.pl 2026-05-07 12:10

    @mc@mathstodon.xyz Amusingly, also re-inventing what IMPS, the theorem prover that few have even heard of, did 30 years ago.

    Open ##2668000

  • @mc@mathstodon.xyz Not that it doesn't go both ways, but it's funny how a set theory person trying to give a foundation for mathematics basically ignores computing? No mention of work on types, explicit mathematics, computability at all (there is a cite that doesn't appear to be referenced?). 2nd order arithmetic gets a nod at least (so transitively reverse maths). Maybe it's good work, I can't judge it on its own merits, but I'd be sceptical of anyone who wants to give "an antidote to godel"

    Open ##2668008

  • @cdrichards@mathstodon.xyz 2026-05-07 17:01

    @mc@mathstodon.xyz hm, no references to Lawvere’s ETCS (1964) or its recent presentation by Leinster in Rethinking Set Theory (2014) https://arxiv.org/abs/1212.6543 A educated hobbyist’s opinion: the problem with set theory as traditionally presented is not that it’s too powerful, although it may be that, too; it’s that for most mathematics other than set theory itself, it demands awkward, low-level encodings.

    Open ##2668009

  • @5ht@mathstodon.xyz 2026-05-08 06:37

    @mc@mathstodon.xyz This is not synthetic. This is non-computable axioms :-)

    Open ##2668012