b'\n_START_ARTICLE_\nTeoria dos conjuntos de Tarski-Grothendieck\n_START_PARAGRAPH_\nA teoria dos conjuntos de Tarski-Grothendieck (TG, assim denominada em refer\xc3\xaancia aos matem\xc3\xa1ticos Alfred Tarski e Alexander Grothendieck) \xc3\xa9 uma teoria dos conjuntos axiom\xc3\xa1tica. Tamb\xc3\xa9m \xc3\xa9 uma extens\xc3\xa3o n\xc3\xa3o conservativa da teoria dos conjuntos de Zermelo-Fraenkel (ZFC) e pode ser distinguida de outras teorias dos conjuntos axiom\xc3\xa1ticas por causa da inclus\xc3\xa3o do axioma de Tarski, que diz que para cada conjunto existe um universo de Grothendieck a qual pertence. O axioma de Tarski implica na exist\xc3\xaancia de cardinais inacess\xc3\xadveis, fornecendo uma ontologia mais rica do que outras teorias como a ZFC. Por exemplo, adicionar esse axioma d\xc3\xa1 suporte a teoria das categorias._NEWLINE_O sistema Mizar e Metamath usam a teoria dos conjuntos de Tarski-Grothendieck para verifica\xc3\xa7\xc3\xa3o formal de provas.\n_START_SECTION_\nImplementa\xc3\xa7\xc3\xa3o em Metamath\n_START_PARAGRAPH_\nO sistema Metamath permite l\xc3\xb3gica de alta ordem arbitr\xc3\xa1rias, mas \xc3\xa9 tipicamente usado com as defini\xc3\xa7\xc3\xb5es \xe2\x80\x9cset.mm\xe2\x80\x9d de axiomas. O axioma ax-groth adiciona o axioma de Tarski, que \xc3\xa9 definido da seguinte maneira em Metamath:_NEWLINE_\xe2\x8a\xa2 \xe2\x88\x83y(x \xe2\x88\x88 y \xe2\x88\xa7 \xe2\x88\x80z \xe2\x88\x88 y (\xe2\x88\x80w(w \xe2\x8a\x86 z \xe2\x86\x92 w \xe2\x88\x88 y) \xe2\x88\xa7 \xe2\x88\x83w \xe2\x88\x88 y \xe2\x88\x80v(v \xe2\x8a\x86 z \xe2\x86\x92 v \xe2\x88\x88 w)) \xe2\x88\xa7 \xe2\x88\x80z(z \xe2\x8a\x86 y \xe2\x86\x92 (z \xe2\x89\x88 y \xe2\x88\xa8 z \xe2\x88\x88 y)))'