Talk:Tarski–Grothendieck set theory

Questions

Is TG simply ZF minus Infinity, augmented by Tarski's axiom? Does that axiom also ensure the existence of infinite sets? What is known about the metamathematics of Tarski's axiom? Why is Grothendieck's name associated with TG? Has anyone written on TG outside of the Journal of Formalized Mathematics?132.181.160.42 03:38, 10 August 2006 (UTC)[reply]

ad existence of infinite sets: yes, for any ordinal, Tarski's axiom gives you a limit ordinal containing it (http://mmlquery.mizar.org/mml/current/ordinal1.html#T51); the smallest containing the empty set is omega (http://mmlquery.mizar.org/mml/current/ordinal1.html#D12) JosefUrban 19:00, 8 June 2007 (UTC)[reply]

ad usage by Grothendieck: http://modular.fas.harvard.edu/sga/sga/4-1/4-1t_185.html;

and as for "sloppiness", I do not know how to measure this, but provided that this is used by two top-level mathematicians of 20. century, I'd be a bit cautious with such words (and if used at all, I'd certainly try to justify them) JosefUrban 19:09, 8 June 2007 (UTC)[reply]

I can't read Mizar, and I don't see how Tarski's axiom implies the axiom of infinity. It looks to me that V_ω, which is a Grothendieck universe, is a model of these axioms, since all of its subsets are either hereditarily finite or have cardinality ω. — Charles Stewart (talk) 12:26, 24 June 2009 (UTC)[reply]

Tarski's axiom basically says that every set is a member of a set which is a Grothendieck universe. V_ω is not a model of this axiom, because no nonempty element of V_ω is a Grothendieck universe. More generally, every nonempty Grothendieck universe is infinite, which is why Tarski's axiom implies the axiom of infinity. — Emil J. 12:42, 24 June 2009 (UTC)[reply]

Ah, yes, of course, how silly of me. Thanks. So ZF+Tarski's axiom has the same theory as ZFC+the inaccessible cardinal axiom. — Charles Stewart (talk) 13:24, 24 June 2009 (UTC)[reply]

The link to Grothendieck universe includes the union axiom in the definition. Maybe that follows from the cardinality condition, but the only path I see involves Konig's theorem (and it's half a page rather than a one-liner). I think this requires more explanation. The union condition is critical to inaccessibility. — Preceding unsigned comment added by 65.56.106.198 (talk) 21:22, 24 July 2024 (UTC)[reply]

Implies axiom of choice?

"Tarski's axiom implies the Axiom of Choice"

why/how?does anyone have a proof of this?

16:25, 28 March 2007 (UTC)

yes, a verified one: http://mizar.uwb.edu.pl/JFM/Vol1/wellord2.html (or in full detail: http://mmlquery.mizar.org/mml/current/wellord2.html#T26, http://mmlquery.mizar.org/mml/current/wellord2.html#T28). JosefUrban 18:15, 8 June 2007 (UTC)[reply]

Sketch of Proof: Let alpha be the set of ordinal numbers in a Grothendieck universe W. Then alpha is an ordinal number, but alpha is not an element of itself, so alpha is not an element of W. Thus #alpha = #W, so W admits a well ordering. 65.56.106.198 (talk) 21:14, 24 July 2024 (UTC)[reply]

Unclear comment about definitions

"Any standard exposition of ZFC (e.g., Suppes 1960) reveals that given the four axioms above, all of the Definitional Axiom is redundant except for the existence of power sets and union sets, for which there are explicit ZFC axioms."

This isn't clear to me. How would a definitional axiom (e.g., the definition of a singleton) be "redundant"? I've deleted this passage from the article. — Preceding unsigned comment added by Jessealama (talk • contribs) 17:32, 7 June 2011 (UTC)[reply]

Needs a rewrite

This whole article needs an update, if not a rewrite. It is a mathematics article and should not reference software systems like Mizar or Metamath, and certainly shouldn't depend on them. This is particularly true because TG Set Theory is tied in with inaccessible cardinals and Mizar does not implement these properly (see https://cs.nyu.edu/pipermail/fom/2008-March/012783.html ).

The explanation of the axioms is not very illuminating. There is minimal if any cross referencing to other axiomatic set theories. There is not even a link to Grothendieck Universe.

Considering TG Set Theory is the set theory of choice for Category Theory and other theories that require operations with classes this article should be much more comprehensive. See for example the article on Morse-Kelley Set Theory as an example.

I am happy to update this article, but need to learn the protocols and how to do this? Not even sure I should be putting this comment here. — Preceding unsigned comment added by Mkortink (talk • contribs) 22:33, 23 November 2017 (UTC)[reply]

Gave description of the axiom in ordinary language

Someone off wiki asked me if the axiom was correct, and what the significance of the y was. So I added an explanation in ordinary language, hopefully will help others understand Tarski's axiom:

"There y looks much lika a "universal set" for x - it not only has as members the powerset of x, and all subsets of x, it also has the powerset of that powerset and so on - its members are closed under the operations of taking powerset or taking a subset. It's like a "universal set" except that of course it is not a member of itself and is not a set of all sets. And then any such y is itself a member of a larger "almost universal set" and so on. It's one of the strong cardinality axioms guaranteeing vastly more sets than you normally assume to exist."

Robert Walker (talk) 15:09, 20 March 2018 (UTC)[reply]