next up previous contents
: TARSKI.miz : mizarと集合論 : 目次   目次

TARSKIの公理系

このテキストは,集合論を題材に,mizarを使った, 数学定理の記述が,実際にどのようになされているか を説明します。

mizarでは,その数学記述言語によって書かれたテキストをarticleと称します。 mizarシステムやそれで使われる数学記述言語の文法については, 中村八束教授著のmizar講義録第3版

http://markun.cs.shinshu-u.ac.jp/kiso/projects2/proofchecker/mizar/Mizar-J/Miz-tit.htm

に説明されています。 また,PC用のmizarシステムのダウンロード,WEB上で使用できる mizarシステムは

http://markun.cs.shinshu-u.ac.jp/kiso/projects2/proofchecker/mizar/index-j.html
にあります。

このテキストでは,mizarで記述された数学定理のデータベースである ライブラリ中の集合論についての,基礎的なarticle

\begin{displaymath}
TARSKI.miz,XBOOLl0.miz,XBOOLl1.miz
\end{displaymath}

について説明します。





Yasunari SHIDAMA