MODULE (
  HEADER (
    SPEC (
      NAME ("set1"),
      VERSION ("1.00.00"),
      VERSION ("1.00.00"),
      LOCATIONS (
        LOCATION ("http://www.qedeq.org/0_00_53")
      )
    ),
    HEADLINE ("Axiome und erste Definitionen der Mengenlehre"),
    DESCRIPTION (
      "Dieses Modul enth""alt die Axiome und ersten Definitionen der Neumann-Bernays-G""odelschen Mengenlehre."
    ),
    EMAIL ("module@qedeq.org"),
    AUTHORS (
      AUTHOR ("Michael Meyling",EMAIL ("mime@qedeq.org"))
    )
  ),
  IMPORTS (
    IMPORT (
      SPEC (
        NAME ("predaxiom"),
        VERSION ("1.00.00"),
        VERSION ("1.00.00"),
        LOCATIONS (
          LOCATION ("."),
          LOCATION ("http://www.qedeq.org/0_00_53")
        )
      )
    )
  ),
  PARAGRAPHS (
    PARAGRAPH (
      LABEL ("def:in"),
      "Definition des Pr""adikats 'ist ein Element der Klasse`",
      DEFINE (
        "IN",
        "%1 \in %2"
      )
    ),
    PARAGRAPH (
      LABEL ("def:set"),
      "Definition des Pr""adikats 'ist eine Menge`.",
      DEFINITION (
        DEFINE (
          "ISSET",
          "\mbox{set}(%1)"
        ),
        ISSET(VAR(1)),
        EXISTS(VAR(2), IN(VAR(1), VAR(2)))
      ),
      "Ist eine Klasse also Element einer anderen Klasse, dann wird sie auch als {\bf Menge} bezeichnet."
      
    ),
    PARAGRAPH (
      LABEL ("axiom:kompr"),
      "Das Axiom der Klassenbildung ist das folgende:",
      AXIOM (
        EXISTS(VAR(1), FORALL( VAR(2), EQUI(IN(VAR(2), VAR(1)), AND(ISSET(VAR(2)), PREDVAR(1, L(VAR(2)))))))
      ),
      "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."
    ),
    PARAGRAPH (
      LABEL ("def:equal"),      
      "Die Gleichheit zweier Klassen kann definiert werden durch die Eigenschaft, dass sie dieselben Elemente besitzen.",
      DEFINITION (
        DEFINE (
          "EQUAL",
          "%1 = %2"
        ),
        EQUAL(VAR(1), VAR(2)),
        FORALL(VAR(3), EQUI(IN(VAR(3), VAR(1)), IN(VAR(3), VAR(2))))
      ),
      "Es wird von der 'Umfangsgleichheit` gesprochen. Diese Definition reicht jedoch nicht aus, um eine Klasse durch eine gleiche Klasse zu ersetzen."
    ),
    PARAGRAPH (
      LABEL ("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.",
      AXIOM (
        IMPL (
          AND (
            EQUAL (VAR(1), VAR(2)),
            IN (VAR(3), VAR(1))
          ),
          IN (VAR(3), VAR(2))
        )
      )
    ),
    PARAGRAPH (
      LABEL ("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.",
      ABBREVIATION (
        DEFINE (
          "SET",
          "\{%1 | %2\}"
        ),
        IN(VAR(1), SET(VAR(2), PREDVAR(1, L(VAR(2))))),
        AND(ISSET(VAR(1)), PREDVAR(1, L(VAR(1))))
      )
    ),
    PARAGRAPH (
      LABEL ("abr:set2"),
            "F""ur die Beziehung in der anderen Richtung muss das Folgende gelten.",
      ABBREVIATION (
        DEFINE (
          "SET",
          "\{%1 | %2\}"
        ),
        IN(SET(VAR(2), PREDVAR(1, L(VAR(2)))), VAR(1)),
        EXISTS (
          VAR(3), 
          AND (
            FORALL (
              VAR(2), 
              EQUI (
                AND (
                  ISSET(VAR(2)), 
                  PREDVAR(1, L(VAR(2)))
                ), 
                IN(VAR(2), VAR(3))
              )
            ),
            IN(VAR(3), VAR(1)) 
          )
        )
      ),
      "Im Folgenden verwenden wir diese abk""urzenden Schreibweisen in allen pr""adikativen Aussagen."
    ),
    PARAGRAPH (
      LABEL ("thm:set:equal1"),
      "Die Kompatiblit""at mit dem Extensionalit""atsaxiom ist gew""ahrleistet.",
      PROPOSITION (
        SENTENCE (
          EQUI(
            IN(SET(VAR(2), PREDVAR(1, L(VAR(2)))), VAR(1)),
            EQUI(
              EXISTS (
                VAR(3),
                AND (
                  EQUAL (
                    VAR(3),
                    SET(VAR(2), PREDVAR(1, L(VAR(2))))
                  ),
                  IN (VAR(3), VAR(1))
                )
              )
            )
          )
        ),
        PROOF (
          LINE (
            1,
            EQUI(
              IN(SET(VAR(2), PREDVAR(1, L(VAR(2)))), VAR(1)),
              IN(SET(VAR(2), PREDVAR(1, L(VAR(2)))), VAR(1))
            ),
            TAUT(EQUI(PROP(1), PROP(1)))
          ),
          LINE (
            2,
            EQUI(
              IN(SET(VAR(2), PREDVAR(1, L(VAR(2)))), VAR(1)),
              EXISTS (
                VAR(3), 
                AND (
                  FORALL (
                    VAR(2), 
                    EQUI (
                      AND (
                        ISSET(VAR(2)), 
                        PREDVAR(1, L(VAR(2)))
                      ), 
                      IN(VAR(2), VAR(3))
                    )
                  ),
                  IN(VAR(3), VAR(1))
                )
              )
            ),
            LINK ("abr:set2"),
            LREF (1)
          ),
          LINE (
            3,
            EQUI (
              IN(SET(VAR(2), PREDVAR(1, L(VAR(2)))), VAR(1)),
              EXISTS (
                VAR(3),
                AND (
                  FORALL (
                    VAR(4),
                    EQUI (
                      AND (
                        ISSET(VAR(4)),
                        PREDVAR(1, L(VAR(4)))
                      ),
                      IN(VAR(4), VAR(3))
                    )
                  ),
                  IN (VAR(3), VAR(1))
                )
              )
            ),
            LREF (2)
          ),
          LINE (
            4,
            EQUI (
              IN(SET(VAR(2), PREDVAR(1, L(VAR(2)))), VAR(1)),
              EXISTS (
                VAR(3),
                AND (
                  FORALL (
                    VAR(4),
                    EQUI (
                      IN(VAR(4), VAR(3)),
                      AND (
                        ISSET(VAR(4)),
                        PREDVAR(1, L(VAR(4)))
                      )
                    )
                  ),
                  IN (VAR(3), VAR(1))
                )
              )
            ),
            LREF (3)
          ),
          LINE (
            5,
            EQUI (
              IN(SET(VAR(2), PREDVAR(1, L(VAR(2)))), VAR(1)),
              EXISTS (
                VAR(3),
                AND (
                  FORALL (
                    VAR(4),
                    EQUI (
                      IN(VAR(4), VAR(3)),
                      IN(VAR(4), SET(VAR(2), PREDVAR(1, L(VAR(2)))))
                    )
                  ),
                  IN (VAR(3), VAR(1))
                )
              )
            ),
            LREF (4)
          ),
          LINE (
            6,
            EQUI(
              IN(SET(VAR(2), PREDVAR(1, L(VAR(2)))), VAR(1)),
              EXISTS (
                VAR(3),
                AND (
                  EQUAL (
                    VAR(3),
                    SET(VAR(2), PREDVAR(1, L(VAR(2))))
                  ),
                  IN (VAR(3), VAR(1))
                )
              )
            ),
            LREF (5)
          )
        )
      )
    ),
    PARAGRAPH (
      LABEL ("thm:set:equal1"),
      "Aus den Abk""urzungen ergibt sich f""ur die Gleichheit von derartigen Mengen das Folgende.",
      PROPOSITION (
        SENTENCE (
          EQUI(
            EQUAL(
              SET(VAR(1), PREDVAR(1, L(VAR(1)))), 
              SET(VAR(1), PREDVAR(2, L(VAR(1))))
            ),
            EQUI(
              FORALL (VAR(1), 
                IMPL (
                  ISSET(VAR(1)),
                  EQUI (
                    PREDVAR(1, L(VAR(1))),
                    PREDVAR(2, L(VAR(1)))
                  )
                )
              )
            )
          )
        ),
        PROOF (
          LINE (
            1,
            EQUI(
              EQUAL(
                SET(VAR(1), PREDVAR(1, L(VAR(1)))), 
                SET(VAR(1), PREDVAR(2, L(VAR(1))))
              ),
              EQUAL(
                SET(VAR(1), PREDVAR(1, L(VAR(1)))), 
                SET(VAR(1), PREDVAR(2, L(VAR(1))))
              )
            ),
            TAUT(EQUI(PROP(1), PROP(1)))
          ),
          LINE (
            2,
            EQUI(
              EQUAL(
                SET(VAR(1), PREDVAR(1, L(VAR(1)))), 
                SET(VAR(1), PREDVAR(2, L(VAR(1))))
              ),
              FORALL(
                VAR(2), 
                EQUI (
                  IN(VAR(2), SET(VAR(1), PREDVAR(1, L(VAR(1))))), 
                  IN(VAR(2), SET(VAR(1), PREDVAR(2, L(VAR(1)))))
                )
              )
            ),
            LINK("def:equal"),
            LREF(1)
          ),
          LINE (
            3,
            EQUI(
              EQUAL(
                SET(VAR(1), PREDVAR(1, L(VAR(1)))), 
                SET(VAR(1), PREDVAR(2, L(VAR(1))))
              ),
              FORALL(
                VAR(2), 
                EQUI (
                  AND(ISSET(VAR(2)), PREDVAR(1, L(VAR(2)))),
                  AND(ISSET(VAR(2)), PREDVAR(2, L(VAR(2))))
                )
              )
            ),
            LINK("abr:set1"),
            LREF(2)
          ),
          LINE (
            4,
            EQUI(
              EQUAL(
                SET(VAR(1), PREDVAR(1, L(VAR(1)))), 
                SET(VAR(1), PREDVAR(2, L(VAR(1))))
              ),
              FORALL(
                VAR(2),
                AND ( 
                  IMPL (
                    AND(ISSET(VAR(2)), PREDVAR(1, L(VAR(2)))),
                    AND(ISSET(VAR(2)), PREDVAR(2, L(VAR(2))))
                  ),
                  IMPL (
                    AND(ISSET(VAR(2)), PREDVAR(1, L(VAR(2)))),
                    AND(ISSET(VAR(2)), PREDVAR(2, L(VAR(2))))
                  )
                )
              )
            ),
            LREF(3)
          ),
          LINE (
            5,
            EQUI(
              EQUAL(
                SET(VAR(1), PREDVAR(1, L(VAR(1)))), 
                SET(VAR(1), PREDVAR(2, L(VAR(1))))
              ),
              FORALL(
                VAR(2),
                AND ( 
                  IMPL (
                    AND(ISSET(VAR(2)), PREDVAR(1, L(VAR(2)))),
                    PREDVAR(2, L(VAR(2)))
                  ),
                  IMPL (
                    AND(ISSET(VAR(2)), PREDVAR(2, L(VAR(2)))),
                    PREDVAR(2, L(VAR(2)))
                  )
                )
              )
            ),
            LREF(4)
          ),
          LINE (
            6,
            EQUI(
              EQUAL(
                SET(VAR(1), PREDVAR(1, L(VAR(1)))), 
                SET(VAR(1), PREDVAR(2, L(VAR(1))))
              ),
              FORALL(
                VAR(2),
                AND ( 
                  IMPL (
                    ISSET(VAR(2)), 
                    IMPL (
                      PREDVAR(1, L(VAR(2))),
                      PREDVAR(2, L(VAR(2)))
                    )
                  ),
                  IMPL (
                    ISSET(VAR(2)), 
                    IMPL (
                      PREDVAR(2, L(VAR(2))),
                      PREDVAR(1, L(VAR(2)))
                    )
                  )
                )
              )
            ),
            LREF(5)
          ),
          LINE (
            7,
            EQUI(
              EQUAL(
                SET(VAR(1), PREDVAR(1, L(VAR(1)))), 
                SET(VAR(1), PREDVAR(2, L(VAR(1))))
              ),
              FORALL(
                VAR(2),
                IMPL ( 
                  ISSET(VAR(2)),
                  AND (
                    IMPL (
                      PREDVAR(1, L(VAR(2))),
                      PREDVAR(2, L(VAR(2)))
                    ),
                    IMPL (
                      PREDVAR(2, L(VAR(2))),
                      PREDVAR(1, L(VAR(2)))
                    )
                  )
                )
              )
            ),
            LREF(6)
          ),
          LINE (
            8,
            EQUI(
              EQUAL(
                SET(VAR(1), PREDVAR(1, L(VAR(1)))), 
                SET(VAR(1), PREDVAR(2, L(VAR(1))))
              ),
              FORALL(
                VAR(2),
                IMPL ( 
                  ISSET(VAR(2)),
                  EQUI (
                    PREDVAR(1, L(VAR(2))),
                    PREDVAR(2, L(VAR(2)))
                  )
                )
              )
            ),
            LREF(7)
          )
        )
      )
    ),
    PARAGRAPH (
      LABEL ("thm:set:equal3"),
      "Die Definition der Gleichheit von Klassen f""uhrt  zur den gewohnten Eigenschaften der Gleichheit. \par
      Zun""achst die Reflexifit""at.",
      PROPOSITION (
        SENTENCE (
          EQUAL( VAR(1), VAR(1))
        ),
        PROOF (
          LINE (
            1,
            EQUI (
              PREDVAR(1, L(VAR(2))),
              PREDVAR(1, L(VAR(2)))
            ),
            TAUT(EQUI(PROP(1), PROP(1)))
          ),
          LINE (
            2,
            IMPL (
              PREDVAR( 2, L(VAR(2))),
              EQUI (
                PREDVAR(1, L(VAR(2))),
                PREDVAR(1, L(VAR(2)))
              )
            ),
            LREF(1)
          ),
          LINE (
            2,
            IMPL (
              ISSET(VAR(2)),
              EQUI (
                IN(VAR(2), VAR(1)),
                IN(VAR(2), VAR(1))
              )
            ),
            LREF(2)
          ),
          LINE (
            2,
            FORALL(
              VAR(2),
              IMPL (
                ISSET(VAR(2)),
                EQUI (
                  IN(VAR(2), VAR(1)),
                  IN(VAR(2), VAR(1))
                )
              )
            ),
            LREF(3)
          ),
          LINE (
            2,
            EQUAL( VAR(1), VAR(1)),
            LINK("def:equal"),
            LREF(3)
          )
        )
      )
    ),
    PARAGRAPH (
      LABEL ("thm:set:equal2"),
      "Es folgt die Symmetrie.",
      PROPOSITION (
        SENTENCE (
          IMPL (
            EQUAL (VAR(1), VAR(2)),
            EQUAL (VAR(2), VAR(1))
          )
        ),
        PROOF (
          LINE (
            1,
            LET(EQUAL (VAR(1), VAR(2)))
          ),
          LINE (
            2,
            FORALL(
              VAR(3),
              IMPL (
                ISSET(VAR(3)),
                EQUI (
                  IN(VAR(3), VAR(1)),
                  IN(VAR(3), VAR(2))
                )
              )
            ),
            LINK("def:equal"),
            LREF(1)
          ),
          LINE (
            3,
            FORALL(
              VAR(3),
              IMPL (
                ISSET(VAR(3)),
                EQUI (
                  IN(VAR(3), VAR(2)),
                  IN(VAR(3), VAR(1))
                )
              )
            ),
            LREF(2)
          ),
          LINE (
            4,
            EQUAL (VAR(2), VAR(1)),
            LREF(2)
          ),
          LINE (
            5,
            TEL(
              IMPL (
                EQUAL (VAR(1), VAR(2)),
                EQUAL (VAR(2), VAR(1))
              )
            ),
            LREF(1, 4)
          )
        )
      )
    ),
    PARAGRAPH (
      LABEL ("thm:set:equal3"),
      "Und nun folgt die Transitivit""at der Gleichheit.",
      PROPOSITION (
        SENTENCE (
          IMPL (
            AND (
              EQUAL( VAR(1), VAR(2)),
              EQUAL( VAR(2), VAR(3))
            ),
            EQUAL( VAR(2), VAR(3))
          )
        ),
        PROOF (
          LINE (
            1,
            LET (
              AND (
                EQUAL( VAR(1), VAR(2)),
                EQUAL( VAR(2), VAR(3))
              )
            )
          ),
          LINE (
            2,
            AND (
              FORALL(
                VAR(4),
                IMPL (
                  ISSET(VAR(4)),
                  EQUI (
                    IN(VAR(4), VAR(1)),
                    IN(VAR(4), VAR(2))
                  )
                )
              ),
              FORALL(
                VAR(4),
                IMPL (
                  ISSET(VAR(4)),
                  EQUI (
                    IN(VAR(4), VAR(2)),
                    IN(VAR(4), VAR(3))
                  )
                )
              )
            ),
            LINK("def:equal"),
            LREF(1)
          ),
          LINE (
            3,
            FORALL(
              VAR(4),
              AND (
                IMPL (
                  ISSET(VAR(4)),
                  EQUI (
                    IN(VAR(4), VAR(1)),
                    IN(VAR(4), VAR(2))
                  )
                ),
                IMPL (
                  ISSET(VAR(4)),
                  EQUI (
                    IN(VAR(4), VAR(2)),
                    IN(VAR(4), VAR(3))
                  )
                )
              )
            ),
            LREF(2)
          ),
          LINE (
            4,
            FORALL(
              VAR(4),
              IMPL (
                ISSET(VAR(4)),
                AND (
                  EQUI (
                    IN(VAR(4), VAR(1)),
                    IN(VAR(4), VAR(2))
                  ),
                  EQUI (
                    IN(VAR(4), VAR(2)),
                    IN(VAR(4), VAR(3))
                  )
                )
              )
            ),
            LREF(3)
          ),
          LINE (
            5,
            FORALL(
              VAR(4),
              IMPL (
                ISSET(VAR(4)),
                EQUI (
                  IN(VAR(4), VAR(1)),
                  IN(VAR(4), VAR(3))
                )
              )
            ),
            LREF(4)
          ),
          LINE (
            6,
            TEL (
              IMPL (
                AND (
                  EQUAL( VAR(1), VAR(2)),
                  EQUAL( VAR(2), VAR(3))
                ),
                EQUAL( VAR(2), VAR(3))
              )
            ),
            LREF(1, 5)
          )
        )
      )
    )
  )
)