% -*- TeX:EN -*- %%% ==================================================================== %%% @LaTeX-file qedeq_logic_v1_en.tex %%% Generated at 2007-03-11 07:29:46,656 %%% ==================================================================== %%% 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. \documentclass[a4paper,german,10pt,twoside]{book} \usepackage[english]{babel} \usepackage{makeidx} \usepackage{amsmath,amsthm,amssymb} \usepackage{color} \usepackage[bookmarks,bookmarksnumbered,bookmarksopen, colorlinks,linkcolor=webgreen,pagebackref]{hyperref} \definecolor{webgreen}{rgb}{0,.5,0} \usepackage{graphicx} \usepackage{xr} \usepackage{epsfig,longtable} \usepackage{tabularx} \newtheorem{thm}{Theorem}[chapter] \newtheorem{cor}[thm]{Corollary} \newtheorem{lem}[thm]{Lemma} \newtheorem{prop}[thm]{Proposition} \newtheorem{ax}{Axiom} \newtheorem{rul}{Rule} \theoremstyle{definition} \newtheorem{defn}[thm]{Definition} \newtheorem{idefn}[thm]{Initial Definition} \theoremstyle{remark} \newtheorem{rem}[thm]{Remark} \newtheorem*{notation}{Notation} \addtolength{\textheight}{7\baselineskip} \addtolength{\topmargin}{-5\baselineskip} \setlength{\parindent}{0pt} \frenchspacing \sloppy \makeindex \title{Elements of Mathematical Logic} \author{ Michael Meyling } \begin{document} \maketitle \setlength{\parskip}{5pt plus 2pt minus 1pt} \mbox{} \vfill \par The source for this document can be found here: \par \url{http://qedeq.org/0_03_03/doc/math/qedeq_logic_v1.xml} \par Copyright by the authors. All rights reserved. \par If you have any questions, suggestions or want to add something to the list of modules that use this one, please send an email to the address \url{mailto:mime@qedeq.org} \setlength{\parskip}{0pt} \tableofcontents \setlength{\parskip}{5pt plus 2pt minus 1pt} \chapter*{Summary\index{summary}} \label{chapter0} \hypertarget{chapter0}{} \addcontentsline{toc}{chapter}{Summary\index{summary}} The project \textbf{Hilbert II} deals with the formal presentation and documentation of mathematical knowledge. For this reason \textbf{Hilbert II} provides a program suite to accomplish that tasks. The concrete documentation of mathematical basics is also a purpose of this project. For further informations about the \textbf{Hilbert II} project see under \url{http://www.qedeq.org/index_de.html}. \par This document describes the logical axoims and the rules and meta rules that are used to derive new propositions. \par The presentation is axiomatic and in a formal form. A formal calculus is given that enables us to derive all true formulas. Additional derived rules, definitions, abbreviations and syntax extensions basically correspond with the mathematical practice. \par This document is also written in a formal language, the original text is a XML file with a syntax defined by the XSD \url{http://www.qedeq.org/current/xml/qedeq.xsd}. \par This document is work in progress and is updated from time to time. Especially at the locations marked by {\glqq+++\grqq} additions or changes will take place. %% end of chapter Summary\index{summary} \chapter*{Foreword} \label{chapter1} \hypertarget{chapter1}{} \addcontentsline{toc}{chapter}{Foreword} The whole mathematical universium can be unfolded by set--theoretic means. Beside the set--theoretic axioms only logical axioms and rules are required. These elementary basics are sufficient to define the most complex mathematical structures and enable us to prove propositions for those structures. This approach can be fully formalized and can be reduced to simple manipulations of character strings. The semantical interpretation of these character strings represent the mathematical universum. \par It is more than convenient to introduce abbreviations and use further derivation rules. But these comforts could be eliminated and replaced by the basic terms at any time\footnote{At least this is theoretically possible. This transformation is not in each case practically realisable due to restrictions in time and space. For example it is not possible to write down the natural number $1,000,000,000$ completely in set notation.}. \par This project has its source in a childhood dream to undertake a formalization of mathematics. In the meantime the technical possibilities are highly developed so that a realisation seems within reach. \par Special thanks go to the professors \emph{W.~Kerby} and \emph{V.~G{\"u}nther} of the university of Hamburg for their inspiring lectures about logic and axiomatic set theory. Without these important impulses this project would not exist. \par I am deeply grateful to my wife \emph{Gesine~Dr{\"a}ger} and our son \emph{Lennart} for their support and patience. \par \vspace*{1cm} Hamburg, January, 2007 \\ \hspace*{\fill} Michael Meyling %% end of chapter Foreword \chapter*{Introduction} \label{chapter2} \hypertarget{chapter2}{} \addcontentsline{toc}{chapter}{Introduction} At the beginning we quote \emph{D. Hilbert} from the lecture {\glqq The Logical Basis of Mathematics\grqq}, September 1922\footnote{Lecture given at the Deutsche Naturforscher-Gesellschaft, September 1922.}. \par \begin{quote} { \glqq The fundamental idea of my proof theory is the following: \par All the propositions that constitute in mathematics are converted into formulas, so that mathematics proper becomes all inventory of formulas. These differ from the ordinary formulas of mathematics only in that, besides the ordinary signs, the logical signs especially {\glqq implies\grqq} ($\rightarrow$) and for {\glqq not\grqq} ($\bar{\quad}$) occur in them. Certain formulas, which serve as building blocks for the formal edifice of mathematics, are called axioms. A proof is an array that must be given as such to our perceptual intuition of it of inferences according to the schema\\ \begin{eqnarray*} & A & \\ & A \rightarrow B& \\ \cline{2-3} & B & \end{eqnarray*} where each of the premises, that is, the formulae, $A$ and $A \rightarrow B$ in the array either is an axiom or directly from an axiom by substitution, or else coincides with the end formula $B$ of an inference occurring earlier in the proof or results from it by substitution. A formula is said to be provable if it is either an axiom or the end formula of a proof.\grqq} \end{quote} \par In the 1928 published book \emph{Grundz{\"u}ge der theoretischen Logik} (Principles of Theoretical Logic) \emph{D.~Hilbert} and \emph{W.~Ackermann} formalized propositional calculus in a way that build the basis for the logical system used here. 1959 \emph{P.~S.~Novikov} specified a refined axiom and rule system for predicate calculus. \par In this text we present a first order predicate calculus with identity and functors that is the starting basis for the development of the mathematical theory. Only the results without any proofs and in short form are given in the following. %% end of chapter Introduction \chapter{Language} \label{chapter3} \hypertarget{chapter3}{} At the beginning there is logic. Logic is the analysis of methods of reasoning. It helps to derive new propositions from already given ones. Logic is universally applicable. The logical foundation of \textbf{Hilbert II} will be introduced here. The language of our calculus bases on the formalisations of \emph{D.~Hilbert}, \emph{W.~Ackermann}, \emph{P.~Bernays} and \emph{P.~S.~Novikov}. New rules can be derived from the herein presented. Only these meta rules lead to a smooth flowing logical argumentation. \section{Terms\index{term} and Formulas\index{formula}} \label{chapter3_section0} \hypertarget{chapter3_section0}{} We use the \emph{logical symbols} $L = \{$ \mbox{`$\neg$'}, \mbox{`$\vee$'}, \mbox{`$\wedge$'}, \mbox{`$\leftrightarrow$'}, \mbox{`$\rightarrow$'}, \mbox{`$\forall$'}, \mbox{`$\exists$'} $\}$, the \emph{predicate constants}\index{predicate constant}\index{constant!predicate} $C = \{c^k_i~|~i, k \in \omega\}$, the \emph{function variables}\index{function variable}\index{variable!function}\footnote{Function variables are used for a shorter notation. For example writing an identity proposition $x = y \rightarrow f(x) = f(y)$. Also this introduction prepares for the syntax extension for functional classes.} $F = \{f^k_i~|~i, k \in \omega \land k > 0\}$, the \emph{function constants}\index{function constant}\index{constant!function}\footnote{Function constants are also introduced for convenience and are used for direct defined class functions. For example to define building of the power class operator, the union and intersection operator and the successor function. All these function constants can be interpreted as abbreviations.} $H = \{h^k_i~|~i, k \in \omega\}$, the \emph{subject variables}\index{subject variable}\index{variable!subject} $V = \{v_i~|~i \in \omega\}$, as well as \emph{predicate variables}\index{predicate variable}\index{variable!predicate} $P = \{p^k_i~|~i, k \in \omega\}$.\footnote{By $\omega$ we understand the natural numbers including zero. All involved symbols are pairwise disjoint. Therefore we can conclude for example: $f^k_i = f^{k'}_{i'} \rightarrow (k = k' \land i = i')$ and $h^k_i \neq v_j$.} For the \emph{arity}\index{arity} or \emph{rank}\index{rank} of an operator we take the upper index. The set of predicate variables with zero arity is also called set of \emph{proposition variables}\index{proposition variable}\index{variable!proposition} or \emph{sentence letters}\index{sentence letters}: $A := \{p_i^0~|~i \in \omega \}$. For subject variables we write short hand certain lower letters: \mbox{$v_1 = $ `$u$'}, \mbox{$v_2 = $ `$v$'}, \mbox{$v_3 = $ `$w$'}, \mbox{$v_4 = $ `$x$'}, \mbox{$v_5 = $ `$y$'}, \mbox{$v_5 = $ `$z$'}. Furthermore we use the following short notations: for the predicate variables $p^n_1 = $ `$\phi$' und $p^n_2 = $ `$\psi$', where the appropriate arity $n$ is calculated by counting the subsequent parameters, for the proposition variables $a_1 = $ `$A$', $a_2 = $ `$B$' and $a_3 = $ `$C$', for the function variables: $f^n_1 = $ `$f$' und $f^n_2 = $ `$g$', where again the appropriate arity $n$ is calculated by counting the subsequent parameters. All binary propositional operators are written in infix notation. Parentheses surrounding groups of operands and operators are necessary to indicate the intended order in which operations are to be performed. E.~g. for the operator $\land$ with the parameters $A$ and $B$ we write $(A \land B)$. In the absence of parentheses the usual precedence rules determine the order of operations. Especially outermost parentheses are omitted. \par The operators have the order of precedence described below (starting with the highest). $$ \begin{array}{c} \neg, \forall, \exists \\ \land \\ \lor \\ \rightarrow, \leftrightarrow \\ \end{array} $$ \par The term \emph{term\index{term}} is defined recursively as follows: \begin{enumerate} \item Every subject variable is a term. \item Let $i, k \in \omega$ and let $t_1$, \ldots, $t_k$ be terms. Then $h^k_i(t_1, \ldots, t_k)$ is a term and if $k > 0$, so $f^k_i(t_1, \ldots, t_k)$ is a term too. \end{enumerate} Therefore all zero arity function constants $\{h^0_i~|~i \in \omega\}$ are terms. They are called \emph{individual constants}\index{individual constant}\index{constant!individual}.\footnote{In an analogous manner subject variables might be defined as function variables of zero arity. Because subject variables play an importent role they have their own notation.} \par We define a \emph{formula\index{formula}} and the relations \emph{free}\index{bound subject variable}\index{subject variable!free} and \emph{bound}\index{bound subject variable}\index{subject variable!bound} subject variable recursivly as follows: \begin{enumerate} \item Every proposition variable is a formula. Such formulas contain no free or bound subject variables. \item If $p^k$ is a predicate variable with arity $k$ and $c^k$ is a predicate constant with arity $k$ and $t_1, t_2, \ldots, t_k$ are terms, then $p^k(t_1, t_2, \ldots t_k)$ and $c^k(t_1, t_2, \ldots, t_k)$ are formulas. All subject variables that occur at least in one of $t_1, t_2, \ldots, t_k$ are free subject variables. Bound subject variables doesn't occur.\footnote{This second item includes the first one, which is only listed for clarity.} \item Let $\alpha, \beta$ be formulas in which no subject variables occur bound in one formula and free in the other. Then $\neg \alpha$, $(\alpha \land \beta)$, $(\alpha \lor \beta)$, $(\alpha \rightarrow \beta)$ and $(\alpha \leftrightarrow \beta)$ are also formulas. Subject variables which occur free (respectively bound) in $\alpha$ or $\beta$ stay free (respectively bound). \item If in the formula $\alpha$ the subject variable $x_1$ occurs not bound\footnote{This means that $x_1$ is free in the formula or doesn't occur at all.}, then also $\forall x_1~\alpha$ and $\exists x_1~\alpha$ are formulas. The symbol $\forall$ is called \emph{universal quantifier}\index{universal quantifier}\index{quantifier!universal} and $\exists$ as \emph{existential quantifier}\index{existential quantifier}\index{quantifier!existential}. Except for $x_1$ all free subject variables of $\alpha$ stay free. All bound subject variables are still bound and additionally $x_1$ is bound too. \end{enumerate} All formulas that are only built by usage of 1. and 3. are called formulas of the \emph{propositional calculus}\index{propositional calculus}\index{calculus!propositional}. \par For each formula $\alpha$ the following proposition holds: the set of free subject variables is disjoint with the set of bound subject variables..\footnote{ Other formalizations allow for example $\forall x_1~\alpha$ also if $x_1$ occurs already bound within $\alpha$. Also propositions like $\alpha(x) \land (\forall x_1 \beta)$ are allowed. In this formalizations free and bound are defined for a single occurrence of a variable.} \par If a formula has the form $\forall x_1 ~ \alpha$ respectively $\exists x_1 ~ \alpha$ then the formula $\alpha$ is called the \emph{scope}\index{scope}\index{quantifier!scope} of the quantifier $\forall$ respectively $\exists$. \par All formulas that are used to build up a formula by 1. to 4. are called \emph{part formulas}\index{part formula}\index{formula!part}. %% end of chapter Language \chapter{Axioms and Rules of Inference} \label{chapter4} \hypertarget{chapter4}{} We now state the system of axioms for the predicate calculus and present the rules for obtaining new formulas from them. \section{Axioms\index{axioms!of predicate calculus}\index{predicate calculus!axioms}} \label{chapter4_section0} \hypertarget{chapter4_section0}{} The logical operators of propositional calculus \mbox{`$\neg$'}, \mbox{`$\vee$'}, \mbox{`$\wedge$'}, \mbox{`$\leftrightarrow$'} und \mbox{`$\rightarrow$'} combine arbitrary \emph{propositions} to new propositions. A proposition is a statement that affirms or denies something and is either {\glqq true\grqq} or {\glqq false\grqq} (but not both).\footnote{Later on we will define the symbols $\top$ and $\bot$ as truth values.} The new ingredient of predicate calculus is quantification. \par The binary operator \mbox{`$\vee$'} (logical disjunction) combines the two propositions $\alpha$ and $\beta$ into the new proposition $\alpha \vee \beta$. It results in true if at least one of its operands is true. \par The unary operator \mbox{`$\neg$'} (logical negation) changes the truth value of a proposition $\alpha$. $\neg \alpha$ has a value of true when its operand is false and a value of false when its operand is true. \par The \emph{logical implication} (\emph{if}) the, \emph{logical conjunction} (\emph{and}) and the \emph{logical equivalence} (\emph{biconditional}) are defined as abbreviations. \footnote{Actually the symbols $\wedge, \rightarrow, \leftrightarrow$ are defined later on and are a syntax extension. But for convenience these symbols are already part of the logical language.} \par The logical implication (`if') could be defined as follows. \begin{defn}[Implication\index{definition!of implication}] \label{definition:implication} \hypertarget{definition:implication}{} $$\alpha \rightarrow \beta\ :\leftrightarrow \ \neg \alpha\ \lor \ \beta$$ \end{defn} \par The logical conjunction (`and') could be defined with de Morgan. \begin{defn}[Conjunction\index{definition!of conjunction}] \label{definition:conjunction} \hypertarget{definition:conjunction}{} $$\alpha \land \beta\ :\leftrightarrow \ \neg (\neg \alpha\ \lor \ \neg \beta)$$ \end{defn} \par The logical equivalence (`iff') is defined as usual. \begin{defn}[Equivalence\index{definition!of equivalence}] \label{definition:equivalence} \hypertarget{definition:equivalence}{} $$\alpha \land \beta\ :\leftrightarrow \ (\alpha\ \rightarrow \ \beta)\ \land \ (\beta\ \rightarrow \ \alpha)$$ \end{defn} \par Now we come to the first axiom of propositional calculus. This axiom enables us to get rid of an unnecessary disjunction. \begin{ax}[Disjunction Idempotence\index{axiom!of disjunction idempotence}] \label{axiom:disjunction_idempotence} \hypertarget{axiom:disjunction_idempotence}{} \mbox{} \begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}} \centering $(A\ \lor \ A)\ \rightarrow \ A$ \end{longtable} \end{ax} \par If a proposition is true, any alternative may be added without making it false. \begin{ax}[Axiom of Weakening\index{axiom!of weakening}] \label{axiom:disjunction_weakening} \hypertarget{axiom:disjunction_weakening}{} \mbox{} \begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}} \centering $A\ \rightarrow \ (A\ \lor \ B)$ \end{longtable} \end{ax} \par The disjunction should be commutative. \begin{ax}[Commutativity of the Disjunction\index{axiom!of weakening}] \label{axiom:disjunction_commutative} \hypertarget{axiom:disjunction_commutative}{} \mbox{} \begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}} \centering $(A\ \lor \ B)\ \rightarrow \ (B\ \lor \ A)$ \end{longtable} \end{ax} \par An disjunction could be added at both side of an implication. \begin{ax}[Disjunctive Addition\index{axiom!of disjunctive addition}] \label{axiom:disjunction_addition} \hypertarget{axiom:disjunction_addition}{} \mbox{} \begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}} \centering $(A\ \rightarrow \ B)\ \rightarrow \ ((C\ \lor \ A)\ \rightarrow \ (C\ \lor \ B))$ \end{longtable} \end{ax} \par If something is true for all $x$, it is true for any specific $y$. \begin{ax}[Universal Instantiation\index{axiom!of universal instantiation}] \label{axiom:universalInstantiation} \hypertarget{axiom:universalInstantiation}{} \mbox{} \begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}} \centering $\forall x\ \phi(x)\ \rightarrow \ \phi(y)$ \end{longtable} \end{ax} \par If a predicate holds for some particular $y$, then there is an $x$ for which the predicate holds. \begin{ax}[Existential Generalization\index{axiom!of existential generalization}] \label{axiom:existencialGeneralization} \hypertarget{axiom:existencialGeneralization}{} \mbox{} \begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}} \centering $\phi(y)\ \rightarrow \ \exists x\ \phi(x)$ \end{longtable} \end{ax} \section{Rules of Inference\index{rules!of predicate calculus}\index{rules!of inference}} \label{chapter4_section1} \hypertarget{chapter4_section1}{} The following rules of inference enable us to obtain new true formulas from the axioms that are assumed to be true. From these new formulas we derive further formulas. So we can successively extend the set of true formulas. \par \begin{rul}[Modus Ponens\index{Modus Ponens}] \label{rule:modusPonens} \hypertarget{rule:modusPonens}{} If both formulas $\alpha$ and $\alpha \rightarrow \beta$ are true, then we can conclude that $\beta$ is true as well. \end{rul} \par \begin{rul}[Replace Free Subject Variable] \label{rule:replaceFree} \hypertarget{rule:replaceFree}{} We start with a true formula. A free subject variable may be replaced by an arbitrary term, provided that the substituted term contains no subject variable that have a bound occurrence in the original formula. All occurrences of the free variable must be simultaneously replaced. \end{rul} The prohibition to use subject variables within the term that occur bound in the original formula has two reasons. First it ensures that the resulting formula is well-formed. Secondly it preserves the validity of the formula. Let us look at the following derivation. \par \begin{tabularx}{\linewidth}{rclX} $\forall x \ \exists y \ \phi(x, y)$ & $\rightarrow$ & $\exists y \ \phi(z,y)$ & with axiom~\ref{axiom:universalInstantiation} \\ $\forall x \ \exists y \ \phi(x, y)$ & $\rightarrow$ & $\exists y \ \phi(y,y)$ & forbidden replacement: $z$ in $y$, despite $y$ is already bound \\ $\forall x \ \exists y \ x \neq y$ & $\rightarrow$ & $\exists y \ \neq y$ & replace $\neq$ for $\phi$ \end{tabularx} \par This last proposition is not valid in many models. \par \begin{rul}[Rename Bound Subject Variable] \label{rule:renameBound} \hypertarget{rule:renameBound}{} We may replace a bound subject variable occurring in a formula by any other subject variable, provided that the new variable occurs not free in the original formula. If the variable to be replaced occurs in more than one scope, then the replacement need be made in one scope only. \end{rul} \par \begin{rul}[Replace Predicate Variable] \label{rule:replacePred} \hypertarget{rule:replacePred}{} Let $\alpha$ be a true formula that contains a predicate variable $p$ of arity $n$, let $x_1$, \ldots, $x_n$ be subject variables and let $\beta(x_1, \ldots, x_n)$ be a formula where $x_1$, \ldots, $x_n$ are not bound. The formula $\beta(x_1, \ldots, x_n)$ must not contain all $x_1$, \ldots, $x_n$ as free subject variables. Furthermore it can also have other subject variables either free or bound. If the following conditions are fulfilled, then a replacement of all occurrences of $p(t_1, \ldots, t_n)$ each with appropriate terms $t_1$, \ldots, $t_n$ in $\alpha$ by $\beta(t_1, \ldots, t_n)$ results in another true formula. \begin{itemize} \item the free variables of $\beta(x_1, \ldots, x_n)$ without $x_1$, \ldots, $x_n$ do not occur as bound variables in $\alpha$ \item each occurrence of $p(t_1, \ldots, t_n)$ in $\alpha$ contains no bound variable of $\beta(x_1, \ldots, x_n)$ \item the result of the substitution is a well-formed formula \end{itemize} \end{rul} See III \S 5 in \cite{hilback}. \par The prohibition to use additional subject variables within the replacement formula that occur bound in the original formula assurs that the resulting formula is well-formed. Furthermore it preserves the validity of the formla. Take a look at the following derivation. \par \begin{tabularx}{\linewidth}{rclX} $ \phi(x)$ & $\rightarrow$ & $\exists y \ \phi(y)$ & with axiom~\ref{axiom:existencialGeneralization} \\ $ (\exists y \ y = y) \land \phi(x)$ & $\rightarrow$ & $\exists y \ \phi(y)$ & \\ $ \exists y \ (y = y \land \phi(x))$ & $\rightarrow$ & $\exists y \ \phi(y)$ & \\ $ \exists y \ (y = y \land x \neq y)$ & $\rightarrow$ & $\exists y \ y \neq y$ & forbidden replacment: $\phi(x)$ by $x \neq y$, despite $y$ is already bound \\ $ \exists y \ x \neq y$ & $\rightarrow$ & $\exists y \ y \neq y$ & \end{tabularx} \par The last proposition is not valid in many models. \par Analogous to rule~\ref{rule:replacePred} we can replace function variables too. \begin{rul}[Replace Function Variable] \label{rule:replaceFunct} \hypertarget{rule:replaceFunct}{} Let $\alpha$ be an already proven formula that contains a function variable $\sigma$ of arity $n$, let $x_1$, \ldots, $x_n$ be subject variables and let $\tau(x_1, \ldots, x_n)$ be an arbitrary term where $x_1$, \ldots, $x_n$ are not bound. The term $\tau(x_1, \ldots, x_n)$ must not contain all $x_1$, \ldots, $x_n$. as free subject variables. Furhermore it can also have other subject variables either free or bound. If the following conditions are fulfilled we can obtain a new true formula by replacing each occurrence of $\sigma(t_1, \ldots, t_n)$ with appropriate terms $t_1$, \ldots, $t_n$ in $\alpha$ by $\tau(t_1, \ldots, t_n)$. \begin{itemize} \item the free variables of $\tau(x_1, \ldots, x_n)$ without $x_1$, \ldots, $x_n$ do not occur as bound variables in $\alpha$ \item each occurrence of $\sigma(x_1, \ldots, x_n)$ in $\alpha$ contains no bound variable of $\tau(x_1, \ldots, x_n)$ \item the result of the substitution is a well-formed formula \end{itemize} \end{rul} \par \begin{rul}[Universal Quantifier Introduction] \label{rule:universalIntroduction} \hypertarget{rule:universalIntroduction}{} If $\alpha \rightarrow \beta(x_1)$ is a true formula and $\alpha$ doesn't contain the subject variable $x_1$, then $\alpha \rightarrow (\forall x_1~(\beta(x_1)))$ is a true formula too. \end{rul} \par \begin{rul}[Existential Quantifier Introduction] \label{rule:existentialIntroduction} \hypertarget{rule:existentialIntroduction}{} If $\alpha(x_1) \rightarrow \beta$ is already proved to be true and $\beta$ doesn't contain the subjekt variable $x_1$, then $(\exists x_1~\alpha(x_1)) \rightarrow \beta$ is also a true formula. \end{rul} The usage and elimination of abbreviations and constants is also an inference rule. In many texts about mathematical logic these rules are not explicitly stated and this text is no exception. But in the exact QEDEQ format corresponding rules exist. %% end of chapter Axioms and Rules of Inference \chapter{Derived Propositions} \label{chapter5} \hypertarget{chapter5}{} Now we derive elementary propositions with the axioms and rules of inference of chapter~\ref{chapter4}. \section{Propositional Calculus} \label{chapter5_section0} \hypertarget{chapter5_section0}{} MISSING! OTHER: Zun{\"a}chst behandeln wir die Aussagenlogik. \begin{defn} Die Pr{\"a}dikatskonstanten $\top$ f{\"u}r \emph{true} oder \emph{wahr} und $\bot$ f{\"u}r \emph{false} oder \emph{falsch} werden wie folgt definiert: \begin{eqnarray} \top & \Leftrightarrow & A \lor \neg A \\ \bot & \Leftrightarrow & \neg \top \end{eqnarray} \end{defn} Die folgenden Formeln lassen sich beweisen. \begin{thm} \begin{eqnarray} & \top & \\ & \neg \bot & \\ A & \rightarrow & A \\ A & \leftrightarrow & A \\ A \lor B & \leftrightarrow & B \lor A \\ A \land B & \leftrightarrow & B \land A \\ A \land B & \rightarrow & A \\ (A \leftrightarrow B) & \leftrightarrow & (B \leftrightarrow A) \\ A \lor (B \lor C) & \leftrightarrow & (A \lor B) \lor C \\ A \land (B \land C) & \leftrightarrow & (A \land B) \land C \\ A & \leftrightarrow & A \lor A \\ A & \leftrightarrow & A \land A \\ A & \leftrightarrow & \neg \neg A \\ (A \rightarrow B) & \leftrightarrow & (\neg B \rightarrow \neg A) \\ (A \leftrightarrow B) & \leftrightarrow & (\neg A \leftrightarrow \neg B) \\ (A \rightarrow (B \rightarrow C)) & \leftrightarrow & (B \rightarrow (A \rightarrow C)) \\ \neg (A \lor B) & \leftrightarrow & \neg A \land \neg B \\ \neg (A \land B) & \leftrightarrow & \neg A \lor \neg B \\ A \lor (B \land C) & \leftrightarrow & (A \lor B) \land (A \lor C) \\ A \land (B \lor C) & \leftrightarrow & (A \land B) \lor (A \land C) \\ A \land \top & \leftrightarrow & A \\ A \land \bot & \leftrightarrow & \bot \\ A \lor \top & \leftrightarrow & \top \\ A \lor \bot & \leftrightarrow & A \\ A \lor \neg A & \leftrightarrow & \top \\ A \land \neg A & \leftrightarrow & \bot \\ (\top \rightarrow A) & \leftrightarrow & A \\ (\bot \rightarrow A) & \leftrightarrow & \top \\ (A \rightarrow \bot) & \leftrightarrow & \neg A \\ (A \rightarrow \top) & \leftrightarrow & \top \\ (A \leftrightarrow \top) & \leftrightarrow & A \\ (A \rightarrow B) \land (B \rightarrow C) & \rightarrow & A \rightarrow C \\ (A \leftrightarrow B) \land (B \leftrightarrow C) & \rightarrow & A \leftrightarrow C \hypertarget{andequi}{} \\ ((A \land B) \leftrightarrow (A \land C)) & \leftrightarrow & (A \rightarrow (B \leftrightarrow C)) \\ ((A \land B) \leftrightarrow (A \land \neg B)) & \leftrightarrow & \neg A \\ (A \leftrightarrow (A \land B)) & \leftrightarrow & (A \leftrightarrow B) \end{eqnarray} \end{thm} \section{Predicate Calculus} \label{chapter5_section1} \hypertarget{chapter5_section1}{} MISSING! OTHER: F{\"u}r die Pr{\"a}dikatenlogik ergeben sich die folgenden S{\"a}tze. \begin{thm}\hypertarget{elmpred}{} \begin{eqnarray} \forall x \ (\phi(x) \rightarrow \psi(x)) & \rightarrow & \forall x \ (\phi(x)) \rightarrow \forall x \ (\psi(x)) \\ \forall x \ (\phi(x) \rightarrow \psi(x)) & \rightarrow & \exists x \ (\phi(x)) \rightarrow \exists x \ (\psi(x)) \\ \exists x \ (\phi(x) \land \psi(x)) & \rightarrow & \exists x \ (\phi(x)) \land \exists x \ (\psi(x)) \\ \forall x \ (\psi(x)) \lor \forall x \ (\psi(x)) & \rightarrow & \forall x \ (\phi(x) \lor \psi(x)) \\ \exists x \ (\phi(x) \lor \psi(x))) & \leftrightarrow & \exists x \ (\phi(x)) \lor \exists x \ (\psi(x)) \\ \forall x \ (\phi(x) \land \psi(x))) & \leftrightarrow & \forall x \ (\phi(x)) \land \forall x \ (\psi(x)) \hypertarget{allandpp}{}\\ \forall x \ \forall y \ (\phi(x, y)) & \leftrightarrow & \forall y \ \forall x \ (\phi(x, y)) \\ \exists x \ \exists y \ (\phi(x, y)) & \leftrightarrow & \exists y \ \exists x \ (\phi(x, y)) \\ \forall x \ (\phi(x) \rightarrow A) & \leftrightarrow & (\forall x \ (\phi(x)) \rightarrow A) \\ \forall x \ (A \rightarrow \phi(x)) & \leftrightarrow & (A \rightarrow \forall x \ (\phi(x))) \\ \forall x \ (\phi(x) \land A) & \leftrightarrow & \forall x \ (\phi(x)) \land A \\ \forall x \ (\phi(x) \lor A) & \leftrightarrow & (\forall x \ (\phi(x)) \lor A) \\ \forall x \ (\phi(x) \leftrightarrow A) & \leftrightarrow & (\forall x \ (\phi(x)) \leftrightarrow A) \end{eqnarray} +++ erg{\"a}nzen \end{thm} \section{Derived Rules} \label{chapter5_section2} \hypertarget{chapter5_section2}{} MISSING! OTHER: Aus den logischen Grundlagen lassen sich logische S{\"a}tze und Metaregeln ableiten, die eine bequemere Argumentation erm{\"o}glichen. Erst mit diesem Regelwerk und zus{\"a}tzlichen Definitionen und Abk{\"u}rzungen wird die restliche Mathematik entwickelt. Dabei wird stets nur eine \emph{konservative}\index{konservativ} Erweiterung der bisherigen Syntax vorgenommen. D.~h. in dem erweiterten System lassen sich keine Formeln ableiten, die in der alten Syntax formuliert, aber dort nicht ableitbar sind. Im Folgenden werden solche Erweiterungen vorgestellt. \begin{rul}[Ersetzung durch logisch {\"a}quivalente Formeln] Sei die Aussage $\alpha \leftrightarrow \beta$ bereits bewiesen. Wird dann aus der Formel $\delta$ eine neue Formel $\gamma$ dadurch gewonnen, dass ein beliebiges Vorkommen von $\alpha$ durch $\beta$ ersetzt\footnote{Bei dieser Ersetzung kann es erforderlich sein, dass gebundene Variablen von $\beta$ umbenannt werden m{\"u}ssen, damit sich wieder eine Formel ergibt.} wird und besitzt $\gamma$ zumindest die freien Variablen (+++ unklar!) von $\delta$, dann gilt $\delta \leftrightarrow \gamma$. \end{rul} \begin{rul}[Allgemeine Assoziativit{\"a}t] Falls ein zweistelliger Operator das Assoziativit{\"a}tsgesetz erf{\"u}llt, so erf{\"u}llt er auch das allgemeine Assoziativit{\"a}tsgesetz. Dem Operator kann dann eine beliebige Stellenanzahl gr{\"o}{\ss}er eins zugeschrieben werden. So wird beispielsweise anstelle f{\"u}r $(a + b) + (c + d)$ einfach $a + b + c + d$ geschrieben.\footnote{Der $n$-stellig Operator wird mit einer bestimmten Klammerung definiert, jede andere Klammerreihenfolge liefert jedoch dasselbe Ergebnis.} \end{rul} \begin{rul}[Allgemeine Kommutativit{\"a}t] Falls ein Operator das allgemeine Assoziativit{\"a}tsgesetz erf{\"u}llt und kommutativ ist, so sind alle Permutationen von Parameterreihenfolgen einander gleich oder {\"a}quivalent.\footnote{Je nachdem ob es sich um einen Termoperator oder einen Formeloperator handelt.} So gilt beispielsweise $a + b + c + d = c + a + d + b$. \end{rul} \begin{defn}[Ableitbarkeit\index{Ableitbarkeit}] Eine Formel $\beta$ hei{\ss}t \emph{aus der Formel $\alpha$ ableitbar}, wenn sich $\beta$ mit Hilfe aller Regeln des Pr{\"a}dikatenkalk{\"u}ls und der um $\alpha$ vermehrten Gesamtheit aller wahren Formeln des Pr{\"a}dikatenkalk{\"u}ls herleitbar und $\alpha \rightarrow \beta$ eine Formel ist. Dabei d{\"u}rfen die beiden Quantifizierungsregeln, die Einsetzungsregel f{\"u}r Pr{\"a}dikatenvariable und die Umbenennungsregel f{\"u}r freie Subjektvariable nur auf solche Variablen angewendet werden, die in der Formel $\alpha$ nicht auftreten. \par Schreibweise: $\alpha \vdash \beta$. \end{defn} Die Ableitbarkeit einer Formel $\beta$ aus der Formel $\alpha$ ist streng zu unterscheiden von der Ableitbarkeit einer wahren Formel aus den Axiomen des Kalk{\"u}ls, denn im zweiten Fall stehen mehr Ableitungsregeln zur Verf{\"u}gung. Falls beispielsweise die Formel $A$ als Axiom aufgenommen wird, so ist die Formel $A \rightarrow B$ herleitbar. Hingegen l{\"a}{\ss}t sich aus $A$ nicht $B$ ableiten. \begin{rul}[Deduktionstheorem\index{Deduktionstheorem}] Wenn eine Formel $\beta$ aus einer Formel $\alpha$ ableitbar ist, so ist die Formel $\alpha \rightarrow \beta$ im Pr{\"a}dikatenkalk{\"u}l herleitbar. \end{rul} %% end of chapter Derived Propositions \chapter{Identy} \label{chapter6} \hypertarget{chapter6}{} MISSING! OTHER: +++ Fehlt noch \section{Identy Axioms} \label{chapter6_section0} \hypertarget{chapter6_section0}{} MISSING! OTHER: \index{Identit{\"a}t}\hypertarget{gleichheit}{} Es wird eine zweistellige Funktionskonstante festgelegt, welche in der Interpretation die Identit{\"a}t von Subjekten ausdr{\"u}cken soll. \begin{defn}[Gleichheit] $$x = y \ \Leftrightarrow \ c_1^2(x, y)$$ \end{defn} Dazu werden zwei weitere Axiome, auch \emph{Gleichheitsaxiome}\index{Gleichheit}\index{Axiome!Gleichheits-} genannt, formuliert. \begin{ax}[Reflexivit{\"a}t der Gleichheit] $$x = x$$ \end{ax} \begin{ax}[Leibnizsche Ersetzbarkeit]\index{Leibnizsche Ersetzbarkeit}\hypertarget{leibniz}{} $$x = y \rightarrow (\phi(x) \rightarrow \phi(y))$$ \end{ax} \begin{thm}[Symmetrie der Gleichheit]\index{Gleichheit!Symmetrie der} \begin{equation} x = y \leftrightarrow y = x \end{equation} \end{thm} \begin{thm}[Transitivit{\"a}t der Gleichheit]\index{Gleichheit!Transitivit{\"a}t der} \begin{equation} x = y ~ \land ~ y = z \rightarrow x = z \end{equation} \end{thm} \begin{thm} \begin{equation} x = y \rightarrow (\phi(x) \leftrightarrow \phi(y)) \end{equation} \end{thm} \begin{thm} \begin{equation} x = y \rightarrow f(x) = f(y) \end{equation} \end{thm} \section{++ TODO Quantifiers\index{Quantifiers!+++TODO}} \label{chapter6_section1} \hypertarget{chapter6_section1}{} MISSING! OTHER: Bei der folgenden Definition muss die f{\"u}r $\psi(x)$ eingesetzte Formel {\glqq erkennen lassen\grqq}, {\"u}ber welche Subjektvariable quantifiziert wird. Das ist in der Regel dar{\"u}ber zu entscheiden, welche freie Subjektvariable als erstes in der Formel vorkommt.\footnote{Beispielsweise ist in der folgenden Formel erkennbar, dass die zweite Quantifikation {\"u}ber die Subjektvariable $m$ l{\"a}uft: $\forall \ n \in \mathbb{N} \ \forall \ m \in n \ m < n $.} In der exakten Syntax des Qedeq-Formats\footnote{Siehe unter \url{http://www.qedeq.org/0_01_05/projektbeschreibung.pdf}.} ist die Subjektvariable immer angegeben. \begin{defn}[Eingeschr{\"a}nkter Allquantor]\index{Allquantor!eingeschr{\"a}nkter} $$ \forall \ \psi(x) \ (\phi(x)) \ \Leftrightarrow \ \forall \ x \ (\psi(x) \rightarrow \phi(x))$$ \end{defn} Dazu passt die folgende Definition f{\"u}r den eingeschr{\"a}nkten Existenzquantor.\footnote{Passend, da $\neg \forall \ \psi(x) \ (\phi(x)) \leftrightarrow \exists \ x \ \neg (\psi(x) \rightarrow \phi(x)) \leftrightarrow \exists \ x \ (\psi(x) \land \neg\phi(x)) \leftrightarrow \exists \ \psi(x) \ (\neg\phi(x))$.} \begin{defn}[Eingeschr{\"a}nkter Existenzquantor]\index{Existenzquantor!eingeschr{\"a}nkter} $$ \exists \ \psi(x) \ (\phi(x)) \ \Leftrightarrow \ \exists \ x \ (\psi(x) \land \phi(x))$$ \end{defn} F{\"u}r die Existenz genau eines Individuums mit einer bestimmten Eigenschaft wird nun ein gesonderter Quantor eingef{\"u}hrt. \begin{defn}[Eingeschr{\"a}nkter Existenzquantor f{\"u}r genau ein Individuum] $$ \exists! \ \psi(x) \ (\phi(x)) \ \Leftrightarrow \ \exists \ \psi(x) \ (\phi(x) \land \forall \ \psi(y) \ (\phi(y) \rightarrow x = y))$$ \end{defn} Durch die G{\"u}ltigkeit von $\exists! \ \psi(x) (\phi(x))$ kann daher eine Subjektkonstante definiert werden, wenn $\phi(x)$ und $\psi(x)$ durch Ausdr{\"u}cke ersetzt werden, die ausser $x$ keine freien Variablen, keine Pr{\"a}dikatsvariablen und keine Funktionsvariablen mehr enth{\"a}lt. \begin{rul}[Termdefinition durch Formel]\hypertarget{termdef}{} Falls die Formel $\exists! x \ \alpha(x)$ gilt, dann kann die Termsyntax durch $D(x, \alpha(x))$ erweitert werden. Die Formel $alpha(x)$ m{\"o}ge die Variable $y$ nicht enthalten und $\beta(y)$ sei eine Formel, welche die Variable $x$ nicht enth{\"a}lt. Dann wird durch $\beta(D(x, \alpha(x)))$ eine Formel definiert durch $\beta(y) \land \exists! x \ (\alpha(x) \land x = y)$. Auch in der abk{\"u}rzenden Schreibweise gilt die Subjektvariable $x$ als gebunden, die Subjektvariable $y$ ist mit den obigen Einschr{\"a}nkungen frei w{\"a}hlbar und wird in der Abk{\"u}rzung nicht weiter beachtet. Ver{\"a}nderungen von $\alpha$ in eine andere Formel $\alpha'$, die eventuell erforderlich sind, damit keine Variablenkollisionen mit Variablen aus $\beta$ entstehen, m{\"u}ssen jedoch auch in der Abk{\"u}rzung durchgef{\"u}hrt werden. Alle Termbildungsregeln werden entsprechend erweitert. Der Ausdruck ist auch ersetzbar durch $\exists! y \ (\beta(y) \land \alpha(y)$ oder durch $\beta(y) \land \alpha(y)$. \end{rul} F{\"u}r eingeschr{\"a}nkte Quantoren gelten analog zu \hyperref{elmpred} entsprechende Formeln. \\ +++ %% end of chapter Identy \begin{thebibliography}{99} \addcontentsline{toc}{chapter}{Bibliography} \bibitem{witheruss} \emph{A.N. Whitehead, B. Russell}, Principia Mathematica, Cambridge University Press, London 1910 \bibitem{bernays} \emph{P. Bernays}, Axiomatische Untersuchung des Aussagen-Kalkuls der {\glqq Principia Mathematica\grqq}, Math. Zeitschr. 25 (1926), 305-320 \bibitem{hilback} \emph{D. Hilbert, W. Ackermann}, Grundz{\"u}ge der theoretischen Logik, 2nd ed., Berlin: Springer, 1938. English version: Principles of Mathematical Logic, Chelsea, New York 1950, ed. by R.~E.~Luce. See also \url{http://www.math.uwaterloo.ca/~snburris/htdocs/scav/hilbert/hilbert.html} \bibitem{novikov} \emph{P.S. Novikov}, Elements of Mathematical Logic, Edinburgh: Oliver and Boyd, 1964. \bibitem{mendelson} \emph{E. Mendeslson}, Introduction to Mathematical Logic, 3rd. ed., Belmont, CA: Wadsworth, 1987. \bibitem{guenter} \emph{V.~G{\"u}nther}, Lecture {\glqq Mathematik und Logik\grqq}, given at the University of Hamburg, 1994/1995. \bibitem{meyling} \emph{M. Meyling}, Hilbert II, Presentation of Formal Correct Mathematical Knowledge, Basic Concept, \url{http://www.qedeq.org/current/doc/project/qedeq_basic_concept_en.pdf}. %% QEDEQ modules that use this one: \bibitem{qedeq_set_theory_v1} qedeq\_set\_theory\_v1 \end{thebibliography} \backmatter \addcontentsline{toc}{chapter}{\indexname} \printindex \end{document}