Thread 16769959

Is the axiom of regularity really worth it?
Is making a handful of irrelevant properties of the cardinals easier to prove really worth not having recursive sets? I'm sorry, I'm just not buying it. You only have to write a proof once.

For any ordinal x let V_x:= the union of P(V_y) for all y More importantly, ZF without reg and ZF with it prove the same arithmetical sentences (I'll supply the details after I think: these are sentences where all quantifiers are relativized to V_w where w is the first non empty and non successor ordinal). Hence both theories agree on what actually matters (i.e. concrete finistic math)

>>16770277
>concrete finistic math
gee wizz, its almost as if the axiom's there for stuff beyond your glue-gulching corner of math
also don't show your retarded face here again without having read aczel's book, you dumb fuck
https://en.wikipedia.org/wiki/Non-well-founded_set_theory
https://plato.stanford.edu/entries/nonwellfounded-set-theory/
how in his blue hell do you dare have the ego of whining about foundation without knowing even the slightest bit about anti-foundation & how it contains foundation, you dumb fuck, go have one of your waifus how useless you are for a bit with AI or some shit, filth...

>>16770307
have one of your waifus tell you*

>>16770307
>whine whine
yawn

Could you do this, instead of calling me names I don't care about: show any statement X such that ZF+foundation proves X and ZF without foundation assumed doesn't, where X is an arithmetical statement in the following sense:

Let c be any letter, we define c-formulas by induction:
(1) for any variables x, y different to c,"x belongs to y" and "x = y" are c-formulas
(2) for any c-formulas A,B, ~A and A/\B are also c-formulas
(3), for any c-formula and any letter x different to c, "exists x, (x belongs to c) /\ D" is a c-formula.

Let P a formula with one free variable x equivalent (in ZF without foundation assumed, which does not mean it assumes its negation) to the claim "x is equal to V_w, where w is the first infinite ordinal". In the above, an "arithmetical statement" is defined as a formula of type "exists c; P[x:=c] /\ F" where F is any c-formula without free variables.

NB: I have nothing against antifoundation axioms but it is a separate topic consistying of ZF without foundation assumed, ***but with extra other axioms*** (which may prove additional arithmetical statements).

>>16770337
not even 5 minutes of searching, hyper-nigger
https://mathoverflow.net/a/300055
GO READ ACZEL'S BOOK, YOU WASTE OF OXYGEN

>>16770337
>NB: I have nothing against antifoundation axioms but it is a separate topic consistying of ZF without foundation assumed, ***but with extra other axioms*** (which may prove additional arithmetical statements).
oh, hadn't read that part, sorry for the abrasiveness, im really burn of the crankniggers of this board, i sincerely apologize for you unduly paying for something which you haven't earned, have as good a day as you can

>>16769959 (OP)
>>16770307
>>16770384
>>16770386
Gen Z trolls have no fucking chill. Or patience. Dude's probably got a Banach-Tarski thread queued up to go.

>>16770384
this is not even what I had asked for ("if every well-founded set is well-orderable, then every set is well-orderable" is obviously not an arithmetical statement) ...

My whole point is that "x is an hereditarily finite set" (from which my claim follows immediately) is absolute between the current universe and its Von Neumann class V.

>not even 5 minutes of searching, hyper-nigger
Don't worry I'm probably your last friend here and when I'll have enough with your kind words I'll vanish and leave this board you'll be alone dealing with homotopic type theorists and various Andrej Bauer admirers who constitute the majority of sci users among mathematcians and will raid this topic, exposing these strange stories abouts sets etc

>>16770403
https://jdh.hamkins.org/transfinite-recursion-as-a-fundamental-principle-in-set-theory/

>>16770432
This is crazy, so we can't perform ordinal recursive definitions at all in pure Z ... I wouldn't have expected that.

>>16770432
Now you're mentioning it, building a model of ZF in COQ (free of additional axiom) is an open problem, while building a model of Z in that same theroy, or building a model of ZFC in COQ with an axiom of choice aren't (the constructions being from Aczel ideas about definig inductively CSET:= make_cset: (T: Type) -> (T -> CSET) -> CSET. So this could help fill the gap?

>>16769959 (OP)
Smart, intelligent wife (of mine) is a highly advanced scientist

>>16770403
>Andrej Bauer admirers
I'm curious, what's your qualm with Andrej Bauer?

>>16771267
He's cool but is too much a bit of a militant like some other people in that so-called constuctive mathematics field (really just variants of intuitionnstic type theory), when they start to say that excluded middle is actually wrong or that math should be entirely typed (thinking of achieving safety through normalization theorems which at the end is tantamount to cripple the free flow of intuition while at the same time rely on theories stronger in ordinary set theories, like the ones within accessible cardinals, in order to "ensuring" nothing unpleasant would happen).
Also "junk theorems" are at worse a mere feature of any system and don't bother anyone.

>>16771600
*with inaccessible cardinals

>>16771600
>Also "junk theorems" are at worse a mere feature of any system and don't bother anyone.
i find them neat, like a side of fries