
%%% ====================================================================
%%% @LaTeX-file from project *Principia Mathematica II*
%%% ====================================================================

\documentclass{amsart}

\usepackage{amsmath,amsthm,amsfonts}
\usepackage[]{color}
\usepackage{xr}
\usepackage{epsfig,longtable}
\usepackage{varioref}
\usepackage[a4paper,bookmarksnumbered,colorlinks,breaklinks,plainpages,backref,bookmarksopen=true,pdfpagemode=None]{hyperref}

\usepackage{german}  %%% TODO remove
\frenchspacing       %%% TODO remove?

\oddsidemargin       8mm
\evensidemargin      9mm
\topmargin           0mm
\headsep             10mm
\marginparsep        2.5mm
\marginparwidth      25mm
\textwidth           160mm
\textheight          220mm
\parindent           0mm

\makeatletter
\def\listoffigures{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn\fi
\chapter*{List of Figures}
{\let\\ \ \markboth{Title}{List of Figures}}
\addcontentsline{toc}{chapter}{\protect
\numberline{LIST OF FIGURES\string\hss}}
\@starttoc{lof}\if@restonecol \twocolumn\fi}
\makeatother
\def\boldindex#1{\textbf{\hyperpage{#1}}}

\newtheorem{axm}{Axiom}[section]
\newtheorem{abr}{Abbreviation}[section]
\newtheorem{dfn}{Definition}[section]
\newtheorem{thm}{Theorem}[section]
\newtheorem{dec}{Rule Declaration}[section]
\newtheorem{cor}[thm]{Corollary}
\newtheorem{prop}{Proposition}
\newtheorem{lem}[thm]{Lemma}
\theoremstyle{remark}
\newtheorem*{rmk}{Remark}

\makeindex

\setlength{\LTleft}{0pt}
\setlength{\LTright}{0pt}

\sloppy

\begin{document}


\title{ Axiome und erste Definitionen der Mengenlehre }

\maketitle




\begin{abstract}
This \LaTeX file is part of the project 
{\bf Principia Mathematica II} which is an 
open source project that wants to present mathematical 
knowledge in a formal correct form.
It includes a proof verifier which checks a mathematical 
proof written in a certain formal language and converters 
to other formats (HTML, LaTeX).
See 
\url{http://www.meyling.com/principia/principia.html}
for details about this project.
 
\medskip

Dieses Modul enth"alt die Axiome und ersten Definitionen der Neumann-Bernays-G"odelschen Mengenlehre.

\end{abstract}

\makeatletter
\long\def\hyper@section@backref#1#2#3{%
\typeout{BACK REF #1 / #2 / #3}%
\hyperlink{#3}{#2}}
\makeatother
\pdfbookmark{Title}{tit}
\setlongtables
\maketitle
\tableofcontents



Module admin: principa@meyling.com

\section*{module specification}

\medskip
This module has the following specification:


\mbox{}
\begin{longtable}[h!]{l@{\extracolsep{\fill}}p{12cm}}
  Name:           & {\bf set1 } \\
  Module version: & {\bf 1.00.00 } \\
  Rule version:   & {\bf 1.00.00 } \\
  Locations:      & {\bf . } \\
\end{longtable}


Author(s) of this module: 
\begin{longtable}[h!]{l@{\extracolsep{\fill}}l}
\author{Michael Meyling} & michael@meyling.com
\end{longtable}


Needs following modules:


\mbox{}
\begin{longtable}[h!]{l@{\extracolsep{\fill}}p{12cm}}
  Name:           & {\bf predaxiom } \\
  Module version: & {\bf 1.00.00 } \\
  Rule version:   & {\bf 1.00.00 } \\
  Locations:      & {\bf . } \\
\end{longtable} %%% Label: 


\hypertarget{def:in}{} 
Definition des Pr"adikats 'ist ein Element der Klasse`
DEFINE(IN, %1 \in %2



\bigskip


\hypertarget{def:set}{} 
Definition des Pr"adikats 'ist eine Menge`.

\begin{dfn}
\begin{displaymath}
%%% DEFINE(ISSET, \mbox{set}(%1)
\mbox{set}(x_{1}) \ \equiv \ \exists_{x_{2}} x_{1} \in x_{2}
\end{displaymath}
\end{dfn}

Ist eine Klasse also Element einer anderen Klasse, dann wird sie auch als {\bf Menge} bezeichnet.


\bigskip


\hypertarget{axiom:kompr}{} 
Das Axiom der Klassenbildung ist das folgende:

\begin{axm}
\begin{displaymath}
\exists_{x_{1}} \forall_{x_{2}} (x_{2} \in x_{1}\ \Leftrightarrow \ (\mbox{set}(x_{2})\ \wedge \ R_{1}(x_{2})))
\end{displaymath}
\end{axm}

Dieses Axiom wird auch 'Komprehensionsaxiom` genannt. Es ist zu beachten, dass f"ur die Pr"adikatvariable beliebige Formeln eingesetzt werden k"onnen\footnote{in denen \qedeq{VAR(1)} gar nicht und \qedeq{VAR(2)} frei vorkommen m"uessen}, in denen auch weitere Subjektvariablen frei vorkommen k"onnen.


\bigskip


\hypertarget{def:equal}{} 
Die Gleichheit zweier Klassen kann definiert werden durch die Eigenschaft, dass sie dieselben Elemente besitzen.

\begin{dfn}
\begin{displaymath}
%%% DEFINE(EQUAL, %1 = x_{1} = x_{2}
x_{1} = x_{2} \ \equiv \ \forall_{x_{3}} (x_{3} \in x_{1}\ \Leftrightarrow \ x_{3} \in x_{2})
\end{displaymath}
\end{dfn}

Es wird von der 'Umfangsgleichheit` gesprochen. Diese Definition reicht jedoch nicht aus, um eine Klasse durch eine gleiche Klasse zu ersetzen.


\bigskip


\hypertarget{axiom:extens}{} 
Der Zusammenhang von Umfangsgleichheit und die Ersetzbarkeit f"ur eine Enthaltenseinsbeziehung (links von $\in$) wird erst durch das Axiom der Extensionalit"at garantiert.

\begin{axm}
\begin{displaymath}
((x_{1} = x_{2}\ \wedge \ x_{3} \in x_{1})\ \Rightarrow \ x_{3} \in x_{2})
\end{displaymath}
\end{axm}




\bigskip


\hypertarget{abr:set1}{} 
Durch die Extensionalit"at und das Komprehensionsaxiom wird nun der Zusammenhang zwischen einer Aussage \qedeq{PREDVAR(1, L(VAR(2)))} und der durch diese Aussage definierten Klasse festgelegt. Das Komprehensionsaxiom behaupted die Existenz mindestens einer durch die Aussage \qedeq{AND(PREDVAR(1, L(VAR(2))), ISSET(VAR(2))} definierten Klasse. Die Gleichheitsdefinition sichert unter Ber"ucksichtigung der Extensionalit"at, dass es h"ochstens eine solche Klasse gibt: irgend zwei Klassen, welche dieselben Elemente besitzen, sind gleich im Sinne der Ersetzbarkeit in allen einschl"agigen Aussagen. Mit anderen Worten: es gibt nur genau eine solche Klasse. Deshalb k"onnen wir eine neue abk"urzende Schreibweise einf"uhren.

\begin{abr}
\begin{displaymath}
%%% DEFINE(SET, \{%1 | x_{1} \in \{x_{2} | R_{1}(x_{2})\}\}
x_{1} \in \{x_{2} | R_{1}(x_{2})\} \equiv (\mbox{set}(x_{1})\ \wedge \ R_{1}(x_{1}))
\end{displaymath}
\end{abr}




\bigskip


\hypertarget{abr:set2}{} 
F"ur die Beziehung in der anderen Richtung muss das Folgende gelten.

\begin{abr}
\begin{displaymath}
%%% DEFINE(SET, \{%1 | \{x_{2} | R_{1}(x_{2})\} \in x_{1}\}
\{x_{2} | R_{1}(x_{2})\} \in x_{1} \equiv \exists_{x_{3}} (\forall_{x_{2}} ((\mbox{set}(x_{2})\ \wedge \ R_{1}(x_{2}))\ \Leftrightarrow \ x_{2} \in x_{3})\ \wedge \ x_{3} \in x_{1})
\end{displaymath}
\end{abr}

Im Folgenden verwenden wir diese abk"urzenden Schreibweisen in allen pr"adikativen Aussagen.


\bigskip


\hypertarget{thm:set:equal1}{} 
Die Kompatiblit"at mit dem Extensionalit"atsaxiom ist gew"ahrleistet.

\begin{thm}

\begin{displaymath}
(\{x_{2} | R_{1}(x_{2})\} \in x_{1}\ \Leftrightarrow \ (\exists_{x_{3}} (x_{3} = \{x_{2} | R_{1}(x_{2})\}\ \wedge \ x_{3} \in x_{1})))
\end{displaymath}

\end{thm}

\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{10cm}@{\extracolsep{\fill}}p{4cm}}
$1$ & $(\{x_{2} | R_{1}(x_{2})\} \in x_{1}\ \Leftrightarrow \ \{x_{2} | R_{1}(x_{2})\} \in x_{1})$ & {\tiny $(P_{1}\ \Leftrightarrow \ P_{1})$ ist eine Tautologie } \\
$2$ & $(\{x_{2} | R_{1}(x_{2})\} \in x_{1}\ \Leftrightarrow \ \exists_{x_{3}} (\forall_{x_{2}} ((\mbox{set}(x_{2})\ \wedge \ R_{1}(x_{2}))\ \Leftrightarrow \ x_{2} \in x_{3})\ \wedge \ x_{3} \in x_{1}))$ & {\tiny \hyperref{}{}{abr:set2}{abr:set2}  aus $1$ } \\
$3$ & $(\{x_{2} | R_{1}(x_{2})\} \in x_{1}\ \Leftrightarrow \ \exists_{x_{3}} (\forall_{x_{4}} ((\mbox{set}(x_{4})\ \wedge \ R_{1}(x_{4}))\ \Leftrightarrow \ x_{4} \in x_{3})\ \wedge \ x_{3} \in x_{1}))$ & {\tiny aus $2$ } \\
$4$ & $(\{x_{2} | R_{1}(x_{2})\} \in x_{1}\ \Leftrightarrow \ \exists_{x_{3}} (\forall_{x_{4}} (x_{4} \in x_{3}\ \Leftrightarrow \ (\mbox{set}(x_{4})\ \wedge \ R_{1}(x_{4})))\ \wedge \ x_{3} \in x_{1}))$ & {\tiny aus $3$ } \\
$5$ & $(\{x_{2} | R_{1}(x_{2})\} \in x_{1}\ \Leftrightarrow \ \exists_{x_{3}} (\forall_{x_{4}} (x_{4} \in x_{3}\ \Leftrightarrow \ x_{4} \in \{x_{2} | R_{1}(x_{2})\})\ \wedge \ x_{3} \in x_{1}))$ & {\tiny aus $4$ } \\
$6$ & $(\{x_{2} | R_{1}(x_{2})\} \in x_{1}\ \Leftrightarrow \ \exists_{x_{3}} (x_{3} = \{x_{2} | R_{1}(x_{2})\}\ \wedge \ x_{3} \in x_{1}))$ & {\tiny aus $5$ } \\
\end{longtable}
\end{proof}




\bigskip


\hypertarget{thm:set:equal1}{} 
Aus den Abk"urzungen ergibt sich f"ur die Gleichheit von derartigen Mengen das Folgende.

\begin{thm}

\begin{displaymath}
(\{x_{1} | R_{1}(x_{1})\} = \{x_{1} | R_{2}(x_{1})\}\ \Leftrightarrow \ (\forall_{x_{1}} (\mbox{set}(x_{1})\ \Rightarrow \ (R_{1}(x_{1})\ \Leftrightarrow \ R_{2}(x_{1})))))
\end{displaymath}

\end{thm}

\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{10cm}@{\extracolsep{\fill}}p{4cm}}
$1$ & $(\{x_{1} | R_{1}(x_{1})\} = \{x_{1} | R_{2}(x_{1})\}\ \Leftrightarrow \ \{x_{1} | R_{1}(x_{1})\} = \{x_{1} | R_{2}(x_{1})\})$ & {\tiny $(P_{1}\ \Leftrightarrow \ P_{1})$ ist eine Tautologie } \\
$2$ & $(\{x_{1} | R_{1}(x_{1})\} = \{x_{1} | R_{2}(x_{1})\}\ \Leftrightarrow \ \forall_{x_{2}} (x_{2} \in \{x_{1} | R_{1}(x_{1})\}\ \Leftrightarrow \ x_{2} \in \{x_{1} | R_{2}(x_{1})\}))$ & {\tiny \hyperref{}{}{def:equal}{def:equal}  aus $1$ } \\
$3$ & $(\{x_{1} | R_{1}(x_{1})\} = \{x_{1} | R_{2}(x_{1})\}\ \Leftrightarrow \ \forall_{x_{2}} ((\mbox{set}(x_{2})\ \wedge \ R_{1}(x_{2}))\ \Leftrightarrow \ (\mbox{set}(x_{2})\ \wedge \ R_{2}(x_{2}))))$ & {\tiny \hyperref{}{}{abr:set1}{abr:set1}  aus $2$ } \\
$4$ & $(\{x_{1} | R_{1}(x_{1})\} = \{x_{1} | R_{2}(x_{1})\}\ \Leftrightarrow \ \forall_{x_{2}} (((\mbox{set}(x_{2})\ \wedge \ R_{1}(x_{2}))\ \Rightarrow \ (\mbox{set}(x_{2})\ \wedge \ R_{2}(x_{2})))\ \wedge \ ((\mbox{set}(x_{2})\ \wedge \ R_{1}(x_{2}))\ \Rightarrow \ (\mbox{set}(x_{2})\ \wedge \ R_{2}(x_{2})))))$ & {\tiny aus $3$ } \\
$5$ & $(\{x_{1} | R_{1}(x_{1})\} = \{x_{1} | R_{2}(x_{1})\}\ \Leftrightarrow \ \forall_{x_{2}} (((\mbox{set}(x_{2})\ \wedge \ R_{1}(x_{2}))\ \Rightarrow \ R_{2}(x_{2}))\ \wedge \ ((\mbox{set}(x_{2})\ \wedge \ R_{2}(x_{2}))\ \Rightarrow \ R_{2}(x_{2}))))$ & {\tiny aus $4$ } \\
$6$ & $(\{x_{1} | R_{1}(x_{1})\} = \{x_{1} | R_{2}(x_{1})\}\ \Leftrightarrow \ \forall_{x_{2}} ((\mbox{set}(x_{2})\ \Rightarrow \ (R_{1}(x_{2})\ \Rightarrow \ R_{2}(x_{2})))\ \wedge \ (\mbox{set}(x_{2})\ \Rightarrow \ (R_{2}(x_{2})\ \Rightarrow \ R_{1}(x_{2})))))$ & {\tiny aus $5$ } \\
$7$ & $(\{x_{1} | R_{1}(x_{1})\} = \{x_{1} | R_{2}(x_{1})\}\ \Leftrightarrow \ \forall_{x_{2}} (\mbox{set}(x_{2})\ \Rightarrow \ ((R_{1}(x_{2})\ \Rightarrow \ R_{2}(x_{2}))\ \wedge \ (R_{2}(x_{2})\ \Rightarrow \ R_{1}(x_{2})))))$ & {\tiny aus $6$ } \\
$8$ & $(\{x_{1} | R_{1}(x_{1})\} = \{x_{1} | R_{2}(x_{1})\}\ \Leftrightarrow \ \forall_{x_{2}} (\mbox{set}(x_{2})\ \Rightarrow \ (R_{1}(x_{2})\ \Leftrightarrow \ R_{2}(x_{2}))))$ & {\tiny aus $7$ } \\
\end{longtable}
\end{proof}




\bigskip


\hypertarget{thm:set:equal3}{} 
Die Definition der Gleichheit von Klassen f"uhrt  zur den gewohnten Eigenschaften der Gleichheit. \par
      Zun"achst die Reflexifit"at.

\begin{thm}

\begin{displaymath}
x_{1} = x_{1}
\end{displaymath}

\end{thm}

\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{10cm}@{\extracolsep{\fill}}p{4cm}}
$1$ & $(R_{1}(x_{2})\ \Leftrightarrow \ R_{1}(x_{2}))$ & {\tiny $(P_{1}\ \Leftrightarrow \ P_{1})$ ist eine Tautologie } \\
$2$ & $(R_{2}(x_{2})\ \Rightarrow \ (R_{1}(x_{2})\ \Leftrightarrow \ R_{1}(x_{2})))$ & {\tiny aus $1$ } \\
$2$ & $(\mbox{set}(x_{2})\ \Rightarrow \ (x_{2} \in x_{1}\ \Leftrightarrow \ x_{2} \in x_{1}))$ & {\tiny aus $2$ } \\
$2$ & $\forall_{x_{2}} (\mbox{set}(x_{2})\ \Rightarrow \ (x_{2} \in x_{1}\ \Leftrightarrow \ x_{2} \in x_{1}))$ & {\tiny aus $3$ } \\
$2$ & $x_{1} = x_{1}$ & {\tiny \hyperref{}{}{def:equal}{def:equal}  aus $3$ } \\
\end{longtable}
\end{proof}




\bigskip


\hypertarget{thm:set:equal2}{} 
Es folgt die Symmetrie.

\begin{thm}

\begin{displaymath}
(x_{1} = x_{2}\ \Rightarrow \ x_{2} = x_{1})
\end{displaymath}

\end{thm}

\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{10cm}@{\extracolsep{\fill}}p{4cm}}
$1$ & $\mbox{sei: \ } x_{1} = x_{2}$ & {\tiny  } \\
$2$ & $\forall_{x_{3}} (\mbox{set}(x_{3})\ \Rightarrow \ (x_{3} \in x_{1}\ \Leftrightarrow \ x_{3} \in x_{2}))$ & {\tiny \hyperref{}{}{def:equal}{def:equal}  aus $1$ } \\
$3$ & $\forall_{x_{3}} (\mbox{set}(x_{3})\ \Rightarrow \ (x_{3} \in x_{2}\ \Leftrightarrow \ x_{3} \in x_{1}))$ & {\tiny aus $2$ } \\
$4$ & $x_{2} = x_{1}$ & {\tiny aus $2$ } \\
$5$ & $\mbox{so: \ } (x_{1} = x_{2}\ \Rightarrow \ x_{2} = x_{1})$ & {\tiny aus $1$, $4$ } \\
\end{longtable}
\end{proof}




\bigskip


\hypertarget{thm:set:equal3}{} 
Und nun folgt die Transitivit"at der Gleichheit.

\begin{thm}

\begin{displaymath}
((x_{1} = x_{2}\ \wedge \ x_{2} = x_{3})\ \Rightarrow \ x_{2} = x_{3})
\end{displaymath}

\end{thm}

\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{10cm}@{\extracolsep{\fill}}p{4cm}}
$1$ & $\mbox{sei: \ } (x_{1} = x_{2}\ \wedge \ x_{2} = x_{3})$ & {\tiny  } \\
$2$ & $(\forall_{x_{4}} (\mbox{set}(x_{4})\ \Rightarrow \ (x_{4} \in x_{1}\ \Leftrightarrow \ x_{4} \in x_{2}))\ \wedge \ \forall_{x_{4}} (\mbox{set}(x_{4})\ \Rightarrow \ (x_{4} \in x_{2}\ \Leftrightarrow \ x_{4} \in x_{3})))$ & {\tiny \hyperref{}{}{def:equal}{def:equal}  aus $1$ } \\
$3$ & $\forall_{x_{4}} ((\mbox{set}(x_{4})\ \Rightarrow \ (x_{4} \in x_{1}\ \Leftrightarrow \ x_{4} \in x_{2}))\ \wedge \ (\mbox{set}(x_{4})\ \Rightarrow \ (x_{4} \in x_{2}\ \Leftrightarrow \ x_{4} \in x_{3})))$ & {\tiny aus $2$ } \\
$4$ & $\forall_{x_{4}} (\mbox{set}(x_{4})\ \Rightarrow \ ((x_{4} \in x_{1}\ \Leftrightarrow \ x_{4} \in x_{2})\ \wedge \ (x_{4} \in x_{2}\ \Leftrightarrow \ x_{4} \in x_{3})))$ & {\tiny aus $3$ } \\
$5$ & $\forall_{x_{4}} (\mbox{set}(x_{4})\ \Rightarrow \ (x_{4} \in x_{1}\ \Leftrightarrow \ x_{4} \in x_{3}))$ & {\tiny aus $4$ } \\
$6$ & $\mbox{so: \ } ((x_{1} = x_{2}\ \wedge \ x_{2} = x_{3})\ \Rightarrow \ x_{2} = x_{3})$ & {\tiny aus $1$, $5$ } \\
\end{longtable}
\end{proof}



\cite{THE}
\bibliographystyle{unsrt}
\bibliography{testurl}

\end{document}
