% -*- TeX:EN -*- %%% ==================================================================== %%% @LaTeX-file qedeq_logic_language %%% Generated from http://www.qedeq.org/0_04_05/doc/project/qedeq_logic_language.xml %%% Generated at 2013-02-05 00:28:48.653 %%% ==================================================================== %%% 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{xr} \usepackage{tabularx} \usepackage[bookmarks=true,bookmarksnumbered,bookmarksopen, unicode=true,colorlinks=true,linkcolor=webgreen, pagebackref=true,pdfnewwindow=true,pdfstartview=FitH]{hyperref} \definecolor{webgreen}{rgb}{0,.5,0} \usepackage{epsfig,longtable} \usepackage{graphicx} \usepackage[all]{hypcap} \newtheorem{thm}{Theorem} \newtheorem{cor}[thm]{Corollary} \newtheorem{lem}[thm]{Lemma} \newtheorem{prop}[thm]{Proposition} \newtheorem{ax}{Axiom} \newtheorem{rul}{Rule} \theoremstyle{definition} \newtheorem{defn}{Definition} \newtheorem{idefn}[defn]{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{\textbf{Hilbert~II} \\ \vspace*{1cm} Presentation of \\ Formal Correct \\ Mathematical Knowledge \\ \vspace*{1cm} Logical Language} \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://www.qedeq.org/0_04_05/doc/project/qedeq_logic_language.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 \href{mailto:mime@qedeq.org}{mime@qedeq.org} \par The authors of this document are: Michael Meyling \href{mailto:michael@meyling.com}{michael@meyling.com} \setlength{\parskip}{0pt} \tableofcontents \setlength{\parskip}{5pt plus 2pt minus 1pt} \chapter*{Description} \label{chapter1} \hypertarget{chapter1}{} \addcontentsline{toc}{chapter}{Description} The project \textbf{Hilbert~II} includes formal correct mathematical knowledge. Here we introduce the underlying formal language for the mathematical formulas. This is done in an informal way. Important theorems (e.g.: universal decomposition, and any proofs) are left out. \par All we will do is manipulate symbols. We build lists of symbol strings and use certain simple rules to get new lists. So by starting with a few basic lists we create a whole universe of derived symbol lists. It turns out that these lists could be interpreted as a view to the incredible world of mathematics. %% end of chapter Description \chapter{Entities} \label{chapter2} \hypertarget{chapter2}{} To describe the logical language we firstly deal with a more basic notation. This notation enables us to formulate the syntax of formulas and terms later on. \section{Elements, Atoms and Lists} \label{chapter2_section1} \hypertarget{chapter2_section1}{} The basic structure we have to deal with is an element. An element is either an atom or a list. \par An atom carries textual data, atoms are just strings. \par Each list has an operator and can contain elements again. An operator is also nothing more than a simple string. A list has a size: the number of elements it contains. Their elements can be accessed by their position number. An atom has no operator, no size and no subelements in the previous sense. \section{List Notation} \label{chapter2_section2} \hypertarget{chapter2_section2}{} Lists and atoms can be written in the following manner. We write down string atoms quoted with {\tt "} and the lists as the contents of the operator string followed by {\tt (} and a comma separated list of elements and an closing {\tt )}. \section{Examples} \label{chapter2_section3} \hypertarget{chapter2_section3}{} In this syntax we can write down the following element examples. \begin{verbatim} "I am a string atom" EMPTY_LIST() THIS_LIST("contains", "three", "atoms") OPERATOR("argument 1", "argument 2") FUNCTION_A(FUNCTION_B("1", "2"), "3") \end{verbatim} In the last example we have a list that has the operator \verb#FUNCTION_A# and contains two elements. The first element is \verb#FUNCTION_B("1", "2")# which is a list too. The second element is the atom \verb#"3"#. %% end of chapter Entities \chapter{Logical Language} \label{chapter3} \hypertarget{chapter3}{} There are different basic things we have to do with. These are predicates, functions, subject variables and logical connectives. In the following all of them are named and described. \section{Logical Operator Overview} \label{chapter3_section1} \hypertarget{chapter3_section1}{} Lists are categorized according to their operators. Before we introduce the formal language in detail the used operators are briefly listed. \par \begin{tabularx}{\columnwidth}{lll} \multicolumn{2}{l@{}}{\qquad\emph{logical}} \vspace*{1mm} \\ \emph{AND} & logical conjunction operator & $\land$ \\ \emph{OR} & logical disjunction operator & $\lor$ \\ \emph{IMPL} & logical implication operator & $\rightarrow$ \\ \emph{EQUI} & logical biconditional operator & $\leftrightarrow$ \\ \emph{NOT} & logical negation operator & $\neg$ \\ \\ \multicolumn{2}{l@{}}{\qquad\emph{logical quantifiers}} \vspace*{1mm} \\ \emph{FORLL} & universal quantifier & $\forall$ \\ \emph{EXISTS} & existential quantifier & $\exists$ \\ \emph{EXISTSU} & unique existential quantifier & $\exists !$ \\ \\ \multicolumn{2}{l@{}}{\qquad\emph{variables}} \vspace*{1mm} \\ \emph{VAR} & subject variables & $x, y, z, \ldots$ \\ \emph{PREDVAR} & predicate variables & $A, B, R, \ldots$ \\ \emph{FUNVAR} & function variables & $f, g, h, \ldots$ \\ \\ \multicolumn{2}{l@{}}{\qquad\emph{constants}} \vspace*{1mm} \\ \emph{PREDCON} & predicate constants & $=, \in, \subseteq, \ldots$ \\ \emph{FUNCON } & function constants & $\emptyset, \mathfrak{P}, \ldots$ \\ \emph{CLASS} & class term & $ \{ x | \phi(x) \}$ \end{tabularx} \section{Terms and Formulas} \label{chapter3_section2} \hypertarget{chapter3_section2}{} Now we define recursivly our formal language. We call some elements \emph{subject variables}, \emph{terms} and some other \emph{formulas}. We also define the relations a subject variable \emph{is free in} and \emph{is bound in} a term or a formula. If something is not according to the formal rules errors occur. The error codes are also described. \subsection{General Error Codes } The atoms and lists that build up a formula or term are subject to restrictions. The following errors occur if an atom has no content or has content with length of $0$ or an list has no operator or one of its sub-elements does not exist. These are mainly technical error codes, only the error code 30470 shows an semantical error. \begin{tabularx}{\linewidth}{llX} 30400 & no element & an element doesn't exist - it is null \\ 30410 & no atom & an atom doesn't exist - it is null \\ 30420 & no list & a list doesn't exist - it is null \\ 30430 & no atom content & an atom has no content - it is null \\ 30440 & atom content empty & an atom has content with $0$ length \\ 30450 & no operator & a list has no operator - it is null \\ 30460 & operator empty & a list has an operator with $0$ length \\ 30470 & list expected & list element expected but not found \end{tabularx} \subsection{Subject Variable } We call an element \emph{subject variable} iff it has the operator \emph{VAR} and its list size is $1$ with an atom as its only argument. \par Each subject variable is also called a \emph{term}. Only the subject variable itself is free in itself. No subject variable is bound in a subject variable. \begin{tabularx}{\linewidth}{llX} 30710 & not exactly one argument & list has not exactly one element \\ 30730 & atom element expected & the first and only list element must be an atom \end{tabularx} \subsection{Function Term } If an element has the operator \emph{FUNVAR} or \emph{FUNCON} and its list size is greater than or equal to $1$ with an atom as its first argument and the remaining arguments are all terms then it is called a term too. \par Iff a subject variable is free in any sub-element it is also free in the new term. No other subject variables are free. Analogous for bound subject variables. \begin{tabularx}{\linewidth}{llX} 30720 & argument(s) missing & if operator is \emph{FUNCON} the list must have at least one element \\ 30730 & atom element expected & the first list element must be an atom \\ 30740 & argument(s) missing & if operator is \emph{FUNVAR} the list must have more than one element \\ 30770 & free bound mixed & found a bound subject variable that is already free in a previous list element \\ 30780 & free bound mixed & found a free subject variable that is already bound in a previous list element \\ 30690 & undefined constant & the operator is \emph{FUNCON} and this function constant has not been defined for this argument number \end{tabularx} \par Any other error for term checks may occur due to the fact that all (but the first) sub-elements must be terms too. \subsection{Predicate Formula } If an element has the operator \emph{PREDVAR} or \emph{PREDCON} and its list size is greater than or equal to $1$ with an atom as its first argument and the remaining arguments are all terms and no errors occur then it is called a \emph{formula}. \par Iff a subject variable is free in any sub-element it is also free in the new formula. No other subject variables are free. Analogous for bound subject variables. \begin{tabularx}{\linewidth}{llX} 30720 & argument(s) missing & list must have at least one element \\ 30730 & atom element expected & the first list element must be an atom \\ 30770 & free bound mixed & found a bound subject variable that is already free in a previous list element \\ 30780 & free bound mixed & found a free subject variable that is already bound in a previous list element \\ 30590 & undefined constant & the operator is \emph{PREDCON} and this predicate constant has not been defined for this argument number \end{tabularx} \par Any other error for formula checks may occur due to the fact that all (but the first) sub-elements must be terms. \subsection{Logical Connectives } If an element has the operator \emph{AND}, \emph{OR}, \emph{IMPL} or \emph{EQUI} and its list size is greater than or equal to $2$ and the remaining arguments are all formulas and no errors occur then it is called a formula too. \par Iff a subject variable is free in any sub-element it is also free in the new formula. No other subject variables are free. Analogous for bound subject variables. \begin{tabularx}{\linewidth}{llX} 30740 & argument(s) missing & list must have more than one element \\ 30760 & exactly $2$ elements expected & the operator is \emph{IMPL} and this list size is not equal to $2$ \\ 30770 & free bound mixed & found a bound subject variable that is already free in a previous list element \\ 30780 & free bound mixed & found a free subject variable that is already bound in a previous list element \end{tabularx} \par Any other error for formula checks may occur due to the fact that all sub-elements must be formulas. \subsection{Negation } If an element has the operator \emph{NOT}, its list size is exactly $1$ and its only sub-element arguments is a formula then it is called a formula too. \par Iff a subject variable is free in the sub-element it is also free in the new formula. No other subject variables are free. Analogous for bound subject variables. \begin{tabularx}{\linewidth}{llX} 30710 & exactly $1$ argument expected & list must have exactly than one element \\ \end{tabularx} \par Any other error for formula checks may occur due to the fact that the sub-element must be a formula. \subsection{Quantifiers } If an element has the operator \emph{FORALL}, \emph{EXISTS} or \emph{EXISTSU} its first sub-element is a subject variable and its second and perhaps its third sub-element is a formula then the element is called a \emph{formula} too. \par Iff a subject variable is free in the sub-element it is also free in the new formula. No other subject variables are free. Analogous for bound subject variables. \begin{tabularx}{\linewidth}{llX} 30760 & $2$ or $3$ arguments expected & list must have exactly $2$ or $3$ elements \\ 30540 & subject variable expected & first sub-element must be a subject variable \\ 30550 & already bound & subject variable already bound in second or third sub-element \\ 30770 & free bound mixed & found a bound subject variable that is already free in a previous list element \\ 30780 & free bound mixed & found a free subject variable that is already bound in a previous list element \end{tabularx} \par Any other error for formula checks may occur due to the fact that the sub-element must be a formula. \subsection{Class Term } An list element with the operator \emph{CLASS}, containing an subject variable and an formula is a term. \par Iff a subject variable is free in the formula and is not equal to the first sub-element (which is a subject variable) it is also free in the new term. No other subject variables are free. If a subject variable is bound in the formula it is bound in the new term. Also the first sub-element is bound. No other subject variables are bound. \begin{tabularx}{\linewidth}{llX} 30760 & $2$ arguments expected & the list must contain exactly two arguments \\ 30540 & subject variable expected & the first sub-element must be a subject variable \\ 30550 & already bound & the subject variable is already bound in the formula \\ 30680 & undefined class operator & the class operator is still unknown \end{tabularx} \par Any other error for formula checks may occur due to the fact that the second sub-element must be a formula. \subsection{Term } When checking an element for beeing a term the element must have the operator for a \emph{Subject Variable}, \emph{Function Term} or \emph{Class Term}. \begin{tabularx}{\linewidth}{llX} 30620 & unknown term operator & element has no operator that is known as a term operator \end{tabularx} \par Any other error for the accordant operator checks may occur. \subsection{Formula } When checking an element for beeing a formul the element must have the operator for a \emph{Predicate Formula}, \emph{Logical Connective}, \emph{Negation} or \emph{Quantifier}. \begin{tabularx}{\linewidth}{llX} 30530 & unknown logical operator & element has no known logical operator \end{tabularx} \par Any other error for the accordant operator checks may occur. %% end of chapter Logical Language \chapter{Representations} \label{chapter4} \hypertarget{chapter4}{} The representation of elements differ according to the viewpoint. Lets take the following formula for example. $$y \ = \ \{ x \ | \ \phi(x) \} \ \leftrightarrow \ \forall z\ (z \in y\ \leftrightarrow \ z \in \{ x \ | \ \phi(x) \} )$$ The predicate constant $\in$ must have been defined in previous sections. \section{List Notation} \label{chapter4_section1} \hypertarget{chapter4_section1}{} In list notation (see \ref{chapter1_section1}) the above formula looks like the following. \begin{verbatim} EQUI( PREDCON( "equal", VAR("y"), CLASS( VAR("x"), PREDVAR( "\phi", VAR("x") ) ) ), FORALL( VAR("z"), EQUI( PREDCON( "in", VAR("z"), VAR("y") ), PREDCON( "in", VAR("z"), CLASS( VAR("x"), PREDVAR( "\phi", VAR("x") ) ) ) ) ) ) \end{verbatim} \section{Java} \label{chapter4_section2} \hypertarget{chapter4_section2}{} The list notation leads directly to the following Java code. \begin{verbatim} Element el = new ElementListImpl("EQUI", new Element[] { new ElementListImpl("PREDCON", new Element[] { new AtomImpl("equal"), new ElementListImpl("VAR", new Element[] { new AtomImpl("y"), }), new ElementListImpl("CLASS", new Element[] { new ElementListImpl("VAR", new Element[] { new AtomImpl("x"), }), new ElementListImpl("PREDVAR", new Element[] { new AtomImpl("\\phi"), new ElementListImpl("VAR", new Element[] { new AtomImpl("x"), }) }) }) }), new ElementListImpl("FORALL", new Element[] { new ElementListImpl("VAR", new Element[] { new AtomImpl("z"), }), new ElementListImpl("EQUI", new Element[] { new ElementListImpl("PREDCON", new Element[] { new AtomImpl("in"), new ElementListImpl("VAR", new Element[] { new AtomImpl("z"), }), new ElementListImpl("VAR", new Element[] { new AtomImpl("y"), }) }), new ElementListImpl("PREDCON", new Element[] { new AtomImpl("in"), new ElementListImpl("VAR", new Element[] { new AtomImpl("z"), }), new ElementListImpl("CLASS", new Element[] { new ElementListImpl("VAR", new Element[] { new AtomImpl("x"), }), new ElementListImpl("PREDVAR", new Element[] { new AtomImpl("\\phi"), new ElementListImpl("VAR", new Element[] { new AtomImpl("x"), }) }) }) }) }) }) }); \end{verbatim} \section{XML} \label{chapter4_section3} \hypertarget{chapter4_section3}{} The XML representation within an QEDEQ module looks a little bit different. Here all first list atoms are represented as the attribute {\tt ref} or {\tt id}. So the above formula may look like the following. \begin{verbatim} \end{verbatim} Due to XSD restrictions for the XML document some error codes listed in Chapter~\ref{chapter2} will not occur. Instead the XML will be classified as invalid. %% end of chapter Representations \chapter{Document structure} \label{chapter5} \hypertarget{chapter5}{} In this chapter we make some remarks about the QEDEQ XML format. \section{Basic structure} \label{chapter5_section1} \hypertarget{chapter5_section1}{} The mathematical knowledge of this project is organized in so called QEDEQ modules. Such a module can be read and edited with a simple text editor. It could contain references to other QEDEQ modules which lay anywhere in the world wide web. \par A QEDEQ module is build like a mathematical text book. It's main structure looks like an \LaTeX{} book file. It contains chapters which are composed of sections and sections are composed of subsections. A subsection may be pure text or an so called \emph{node}. A node is either an axiom, definition, proposition or rule. Every node has an id and could be referenced by that. Essential formal elements of a node are formulas. \par The formal definition of an QEDEQ XML document can be found here: \url{http://www.qedeq.org/0_04_05/xml/qedeq/noNamespace/element/QEDEQ.html}. \section{References} \label{chapter5_section2} \hypertarget{chapter5_section2}{} In QEDEQ documents reference links are used very often. There exist four goals for references: modules, nodes, sub formulas and proof lines. \par If you want to address an external module you have to know its import \emph{label}. See \url{http://www.qedeq.org/0_04_05/xml/qedeq/noNamespace/element/QEDEQ.HEADER.IMPORTS.IMPORT.html}. \par A reference to a node needs the \emph{id} of that node. See \url{http://www.qedeq.org/0_04_05/xml/qedeq/noNamespace/element/NODE.html}. \par In certain cases it is also possible to reference a subformula of a proposition formula. This is only possible if the proposition formula is a conjunction (e.g. the top level logical operation is a conjunction). For each parameter a label is automatically generated. If the number of conjunction parameters is below 27 the label is simply the n'th alphabet character. If the number is greater 26 the label is written in the 26 system with alphabet characters as digits. To reference to a subformula of an external node the syntax is {\tt importLabel.nodeId/subRef}. \par You can also reference to a fromal proof line \emph{label}, see \url{http://www.qedeq.org/0_04_05/xml/qedeq/noNamespace/element/L.html}. Within the node you just need to link to the label. Outside the node context (but within the same module) the syntax is {\tt nodeId!lineLabel}. \par Here follows a reference summary. \par \begin{tabularx}{\linewidth}{ll} external module & {\tt importLabel} \\ (external) node reference & {\tt [importLabel.]nodeId} \\ (external) node sub formula ref. & {\tt [importLabel.]nodeId/subRef} \\ (external) node proof line ref. & {\tt [[importLabel].nodeId!]lineLabel} \end{tabularx} %% end of chapter Document structure \chapter{Basic Rules of Inference\index{0.01.00}} \label{chapter6} \hypertarget{chapter6}{} To get new formulas from already proven or given ones we introduce \emph{proof rules}. We can call a formula \emph{proposition} if we can write down a sequence of formulas that derive it from axioms, definitions and propositions by applying proof methods. Such a sequence is called a \emph{proof}. It is made of \emph{proof lines}. A proof line is a formula and a proof rule usage with its parameters. Each proof line has a label. The last formula of a proof must be the proposition formula itself. \par We will introduce the following proof rules. \par \begin{tabularx}{\columnwidth}{ll} \emph{Add} & add already proven formula \\ \emph{MP} & modus ponens \\ \emph{Rename} & rename bound subject variable \\ \emph{SubstFree} & substitute free subject variable by term \\ \emph{SubstFun} & substitute function variable by term \\ \emph{SubstPred} & substitute predicate variable by formula \\ \emph{Universal} & universal generalization \\ \emph{Existential} & existential generalization \end{tabularx} \par These basic rules get the rule version number $0.01.00$. The rules might get extended in higher rule versions.\footnote{For example we want to allow modus ponens also with a formula like $A \leftrightarrow B$.} \par TODO 20110612 m31: add error code description for rules \section{Addition} \label{chapter6_section1} \hypertarget{chapter6_section1}{} Addition of an axiom, definition or already proven formula. We have to reference to the location of a true formula. \par \begin{tabularx}{\columnwidth}{lll} \emph{name} & \tt{Add} & name of proof rule \\ \emph{parameter 1} & \tt{ref} & reference to axiom, definition or proposition \end{tabularx} \par See \url{http://www.qedeq.org/0_04_05/xml/qedeq/noNamespace/element/ADD.html}. \section{Modus Ponens} \label{chapter6_section2} \hypertarget{chapter6_section2}{} Modus Ponens (Conditional Elimination) \par \begin{eqnarray*} & A & \\ & A \rightarrow B& \\ \cline{2-3} & B & \end{eqnarray*} This rule states that if each of $A$ and $A \rightarrow B$ are already true formulas then $B$ is also a true formula. \par \begin{tabularx}{\columnwidth}{lll} \emph{name} & \tt{MP} & name of proof rule \\ \emph{parameter 1} & \tt{ref1} & reference to a proof line label with a formula like $A$\\ \emph{parameter 2} & \tt{ref2} & reference to a another proof line label with a formula like $A \rightarrow B$ \\ \end{tabularx} \par See \url{http://www.qedeq.org/0_04_05/xml/qedeq/noNamespace/element/MP.html}. \section{Rename bound subject variable} \label{chapter6_section3} \hypertarget{chapter6_section3}{} 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 needs to be made in one scope only. For example in this case we replace x by y at the first occurrence. \par \begin{eqnarray*} & \ldots \forall x A(x) \ldots & \\ \cline{2-3} & \ldots \forall y A(y) \ldots & \\ \end{eqnarray*} \par \begin{tabularx}{\columnwidth}{lll} \emph{name} & \tt{Rename} & name of proof rule \\ \emph{parameter 1} & \tt{ref} & reference to a proof line label \\ \emph{parameter 2} & \tt{original} & bound subject variable that should be renamed \\ \emph{parameter 3} & \tt{replacement} & new name for subject variable \\ \emph{parameter 4} & \tt{occurrence} & bound occurence where we want to replace \end{tabularx} \section{Substitute free subject variable by term.} \label{chapter6_section4} \hypertarget{chapter6_section4}{} 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. \par \begin{eqnarray*} & A(x) & \\ \cline{2-3} & A(t) & \\ \end{eqnarray*} \par \begin{tabularx}{\columnwidth}{lll} \emph{name} & \tt{SubstFree} & name of proof rule \\ \emph{parameter 1} & \tt{ref} & reference to a proof line label \\ \emph{parameter 2} & \tt{original} & free subject variable that should be replaced \\ \emph{parameter 3} & \tt{replacement} & replacement term \end{tabularx} \par See \url{http://www.qedeq.org/0_04_05/xml/qedeq/noNamespace/element/SUBST_FREE.html}. \section{Substitute predicate variable by formula} \label{chapter6_section5} \hypertarget{chapter6_section5}{} Let $\alpha$ be a true formula that contains a predicate variable $p$ of arity $n$, let $x_1$, \ldots, $x_n$ be pairwise different 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} \par \begin{eqnarray*} & A(\sigma) & \\ \cline{2-3} & A(\tau) & \\ \end{eqnarray*} \par \begin{tabularx}{\columnwidth}{lll} \emph{name} & \tt{SubstPred} & name of proof rule \\ \emph{parameter 1} & \tt{ref} & reference to a proof line label \\ \emph{parameter 2} & \tt{original} & predicate variable that should be replaced \\ \emph{parameter 3} & \tt{replacement} & replacement formula \end{tabularx} \par See \url{http://www.qedeq.org/0_04_05/xml/qedeq/noNamespace/element/SUBST_PREDVAR.html}. \section{Substitute function variable by term} \label{chapter6_section6} \hypertarget{chapter6_section6}{} Let $\alpha$ be an already proved formula that contains a function variable $\sigma$ of arity $n$, let $x_1$, \ldots, $x_n$ be pairwise different 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. Furthermore 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(t_1, \ldots, t_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} \par \begin{eqnarray*} & A(\sigma) & \\ \cline{2-3} & A(\tau) & \\ \end{eqnarray*} \par \begin{tabularx}{\columnwidth}{lll} \emph{name} & \tt{SubstFun} & name of proof rule \\ \emph{parameter 1} & \tt{ref} & reference to a proof line label \\ \emph{parameter 2} & \tt{original} & function variable that should be replaced \\ \emph{parameter 3} & \tt{replacement} & replacement term \end{tabularx} \par See \url{http://www.qedeq.org/0_04_05/xml/qedeq/noNamespace/element/SUBST_FUNVAR.html}. \section{Universal Generalization} \label{chapter6_section7} \hypertarget{chapter6_section7}{} If $\alpha \rightarrow \beta(x_1)$ is a true formula and $\alpha$ does not contain the subject variable $x_1$, then $\alpha \rightarrow (\forall x_1~(\beta(x_1)))$ is a true formula too. \par \begin{eqnarray*} & \alpha \rightarrow \beta(x_1) & \\ \cline{2-3} & \alpha \rightarrow (\forall x_1~(\beta(x_1))) & \\ \end{eqnarray*} \par \begin{tabularx}{\columnwidth}{lll} \emph{name} & \tt{Universal} & name of proof rule \\ \emph{parameter 1} & \tt{ref} & reference to a proof line label \\ \emph{parameter 2} & \tt{var} & subject variable we want to quantify with \end{tabularx} \par See \url{http://www.qedeq.org/0_04_05/xml/qedeq/noNamespace/element/UNIVERSAL.html}. \section{Existential Generalization} \label{chapter6_section8} \hypertarget{chapter6_section8}{} If $\alpha(x_1) \rightarrow \beta$ is already proved to be true and $\beta$ does not contain the subject variable $x_1$, then $(\exists x_1~\alpha(x_1)) \rightarrow \beta$ is also a true formula. \par \begin{eqnarray*} & \alpha(x_1) \rightarrow \beta & \\ \cline{2-3} & (\exists x_1~\alpha(x_1)) \rightarrow \beta & \\ \end{eqnarray*} \par \begin{tabularx}{\columnwidth}{lll} \emph{name} & \tt{Existential} & name of proof rule \\ \emph{parameter 1} & \tt{ref} & reference to a proof line label \\ \emph{parameter 2} & \tt{var} & subject variable we want to quantify with \end{tabularx} \par See \url{http://www.qedeq.org/0_04_05/xml/qedeq/noNamespace/element/EXISTENTIAL.html}. %% end of chapter Basic Rules of Inference\index{0.01.00} \chapter{Derived Rules\index{0.02.00}} \label{chapter7} \hypertarget{chapter7}{} We can use derived rules that can be completely replaced by the old rules but enable us shorter proofs. We introduce a new rule that allows us to make an assumption and derive from that hypothesis. All previous rules get also slightly modified. \par \begin{tabularx}{\columnwidth}{ll} \emph{CP} & conditional proof \\ \end{tabularx} \par These basic rules get the rule version number $0.02.00$. \section{Conditional Proof} \label{chapter7_section1} \hypertarget{chapter7_section1}{} We have the well-formed formula $\alpha$ and add it as a new proof line. We assume this formula as hypothesis. Now we modify the existing inference rules. We can add a further proof line $\beta$ if $\alpha \rightarrow \beta$ is a well-formed formula and the usage of a previous inference rule with the following restrictions justifies the addition: any substitution of a free subject variable, a predicate variable or a function variable is only allowed, if the variable doesn't occur in $\alpha$. \par This rule can be used recursive. The conjunction of all hypothesis formulas is called a \emph{condition} for the proof line we want to check. \par \begin{tabularx}{\columnwidth}{lll} \emph{name} & \tt{CP} & name of proof rule \\ \emph{parameter 1} & \tt{HYPOTHESIS} & hypothesis \\ \emph{parameter 2} & \tt{LINES} & formal proof that uses the hypothesis\\ \emph{parameter 2} & \tt{CONCLUSION} & implication with hypothesis and last proof line \end{tabularx} \par See \url{http://www.qedeq.org/0_04_05/xml/qedeq/noNamespace/element/CP.html}. %% end of chapter Derived Rules\index{0.02.00} \addcontentsline{toc}{chapter}{\indexname} \printindex \end{document}