%%% ==================================================================== %%% Text-file from project *Principia Mathematica II* %%% %%% Permission is granted to copy, distribute and/or modify this %%% document under the terms of the GNU Free Documentation License, %%% Version 1.2 or any later version published by the %%% Free Software Foundation; with no Invariant Sections, %%% no Front-Cover Texts, and no Back-Cover Texts. %%% See under "http://www.gnu.org/licenses/fdl.html". %%% ==================================================================== This module has the following specification: Name: set Module version: 1.00.00 Rule version: 2.00.00 Locations: http://www.qedeq.org/0_01_05/set_axiom.txt *Axioms and first definitions of axiomatic set theory* This file is part of the project `Principia Mathematica II' see This open source project wants to present mathematical knowledge in a formal correct form. Under \href{http://www.qedeq.org/}{http://www.qedeq.org/} more information about this project could be found. This file contains the axioms and first definitions of the axiomatic set theory due to Neumann-Bernays-G"odel. The following logical operator symbols are used in formulas: "-" logical negation (prefix notation with exact one argument) "&" logical conjunktion (infix notation with at least two arguments) "|" logical disjunktion (infix notation with at least two arguments) "=>" logical implication (infix notation with at least two arguments) "<=>" logical equivalence (infix notation with at least two arguments) "all" universal quantor (prefix notation with exact two arguments) "exists" existential quantor (prefix notation with exact two arguments) The subject domain are classes, class variables are written as single letters like "x", "y" etc. Defined operators for the domain: "in" set theoretic operator, solely needed predicate constant (infix notation with exact two arguments) "=" defined predicate constant (infix notation with exact two arguments) "set" defined predicate constant (prefix notation with exact one argument) Table of operator priority, sorted from highest to lowest: "set" "in", "=" "-" "&" "|" "=>", "<=>" "all", "exists" Module admin: mime@qedeq.org Author(s) of this module: Michael Meyling Needs following modules: Name: propaxiom Module version: 1.00.00 Rule version: 1.00.00 Locations: ../0_00_51/ Name: predaxiom Module version: 1.00.00 Rule version: 1.00.00 Locations: ../0_00_51/ Predicate Constant Definition x " in " y Predicate Definition "set(" x ")" :<=> exists y x in y Axiom exists x all y (y in x <=> (set(y) & Pred1(y))) Predicate Definition x "=" y :<=> all z (z in x <=> z in y) Axiom ((x = y & x in z) => y in z) Abbreviation x in "{" y "|" Pred1(y) "}" := (set(x) & Pred1(x)) Abbreviation "{" y "|" Pred1(y) "}" in x := exists z (all y ((set(y) & Pred1(y)) <=> y in z) & z in x) Abbreviation "{" x "}" := {u | u = x} Abbreviation "{" x "," y "}" := {u | (u = x | u = y)} Abbreviation x " cup " y := {z | z in x | z in y} Abbreviation x " cap " y := {z | z in x & z in y} Predicate Definition x " subset " y :<=> x cup y = y Function Definition "0" := {x | -set(x)} Function Definition "Pot(" x ")" := {y | y subset x} Axiom set(x) => set(Pot(x)) Axiom set(x) & set(y) => set(x cup y) Abbreviation "CUP(" x, Pred1(x) ")" := {y | exists x (Pred1(x) & (y in x))} Axiom set(x) => set(CUP(y, y in x)) Axiom -(x=0) => exists y ((y in x) & (y cup x = 0)) Function Definition "suc(" x ")" := {y | (y in x) | (y = x)} Abbreviation "CAP(" x, Pred1(x) ")" := {y | all x (Pred1(x) => (y in x))} Function Definition "Nat" := CAP(x, (0 in x) & all y (y in x => suc(y) in x)) Axiom set(Nat) Abbreviation "(" x "," y ")" := {{x, y}, {y}} Predicate Definition "Rel(" r ")" :<=> r subset {(x, y) | (x = x) & (y = y)} Function Definition "Dom(" f ")" := {x | exists y ((x, y) in f} Function Definition "Rng(" f ")" := {y | exists x ((x, y) in f} Predicate Definition "Fkt(" f ")" :<=> Rel(f) & all x all y all z (((x, y) in f) & ((x, z) in f) => y = z) Axiom all x (Fkt(x) & set(Dom(x)) => set(Rng(x)))