% -*- TeX:EN -*- %%% ==================================================================== %%% $RCSfile: Module2Latex.java,v $ %%% $Revision: 1.28 $ %%% ==================================================================== %%% %%% Generated by class com.meyling.principia.latex.Module2Latex %%% at 2004-09-26T23:33:11+0200. %%% %%% Project Hilbert II - http://www.qedeq.org %%% Copyright 2001, 2002, 2003, 2004 Michael Meyling (mime@qedeq.org) %%% %%% This file is part of *Principia Mathematica II*, the prototype of %%% Hilbert 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. %%% \documentclass[a4paper]{article} \usepackage{amsmath,amsthm,amsfonts} \usepackage[]{color} \usepackage{xr} \usepackage{epsfig,longtable} \usepackage{varioref} \usepackage[bookmarksnumbered,colorlinks,breaklinks,plainpages,backref,bookmarksopen=true,pdfpagemode=None]{hyperref} \oddsidemargin 8mm \evensidemargin 9mm \topmargin 0mm \headsep 10mm \marginparsep 2.5mm \marginparwidth 25mm \textwidth 160mm \textheight 220mm \newtheorem{axm}{Axiom}[section] \newtheorem{abr}{Abbreviation}[section] \newtheorem{thm}{Theorem}[section] \newtheorem{dec}{Rule Declaration}[section] \newtheorem{cor}[thm]{Corollary} \newtheorem{prop}{Proposition} \newtheorem{lem}[thm]{Lemma} \theoremstyle{remark} \newtheorem*{rmk}{Remark} \makeindex \makeatletter \externaldocument{predtheo2_1.00.00_1.00.00.qedeq} \hyperbaseurl{predtheo2_1.00.00_1.00.00.qedeq} \makeatother \setlength{\LTleft}{0pt} \setlength{\LTright}{0pt} \setlength{\parindent}{0pt} \frenchspacing \sloppy \pagestyle{headings} \title{Some more theorems of Predicate Calculus} \author{Michael Meyling} \date{\tt } \begin{document} \maketitle \setlongtables {\small This document is part of the project ``Hilbert II''. To get more information about this project look at:\\ \mbox{\url{http://www.qedeq.org}}. 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 also under \url{http://www.gnu.org/copyleft/} } \section*{Abstract} This module includes first proofs of predicate calculus theorems. \section*{Specification} This document has the following specification: \begin{longtable}[h!]{l@{\extracolsep{\fill}}p{12cm}} Name: & predtheo2 \\ Version: & 1.00.00 \\ Rule version: & 1.00.00 \\ Orgin: & \url{http://www.qedeq.org/0_00_53/predtheo2_1.00.00_1.00.00.qedeq} \\ \end{longtable} \medskip Author of this module: \begin{longtable}[h!]{l@{\extracolsep{\fill}}l} Michael Meyling & mime@qedeq.org \\ \end{longtable} \section*{References} This document uses the results of the following documents: \begin{longtable}[h!]{l@{\extracolsep{\fill}}p{12cm}} Name: & predaxiom \\ Version: & 1.00.00 \\ Rule version: & 1.00.00 \\ Orgin: & \url{predaxiom_1.00.00_1.00.00.qedeq} \\ pdf: & \url{predaxiom_1.00.00_1.00.00.pdf} \\ Name: & prophilbert3 \\ Version: & 1.00.00 \\ Rule version: & 1.00.00 \\ Orgin: & \url{prophilbert3_1.00.00_1.00.00.qedeq} \\ pdf: & \url{prophilbert3_1.00.00_1.00.00.pdf} \\ \end{longtable} \section*{Content} A simple implication: \begin{thm}[predtheo1] \hypertarget{predtheo1}{} \begin{displaymath} \forall x\, R(x)\ \rightarrow \ \exists x\, R(x)\end{displaymath} \end{thm} \begin{proof} \mbox{}\\ \begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}} \label{predtheo1:1} $1$ & $\forall x\, R(x)\ \rightarrow \ R(y)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{axiom5}{axiom5} } \\ \label{predtheo1:2} $2$ & $R(y)\ \rightarrow \ \exists x\, R(x)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{axiom6}{axiom6} } \\ \label{predtheo1:3} $3$ & $(P\ \rightarrow \ Q)\ \rightarrow \ ((A\ \rightarrow \ P)\ \rightarrow \ (A\ \rightarrow \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert1_1.00.00_1.00.00.pdf}{}{hilb1}{hilb1} } \\ \label{predtheo1:4} $4$ & $(B\ \rightarrow \ Q)\ \rightarrow \ ((A\ \rightarrow \ B)\ \rightarrow \ (A\ \rightarrow \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $P$ by $B$ in \hyperref[predtheo1:3]{$3$} } \\ \label{predtheo1:5} $5$ & $(B\ \rightarrow \ C)\ \rightarrow \ ((A\ \rightarrow \ B)\ \rightarrow \ (A\ \rightarrow \ C))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $Q$ by $C$ in \hyperref[predtheo1:4]{$4$} } \\ \label{predtheo1:6} $6$ & $(B\ \rightarrow \ C)\ \rightarrow \ ((D\ \rightarrow \ B)\ \rightarrow \ (D\ \rightarrow \ C))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $A$ by $D$ in \hyperref[predtheo1:5]{$5$} } \\ \label{predtheo1:7} $7$ & $(R(y)\ \rightarrow \ C)\ \rightarrow \ ((D\ \rightarrow \ R(y))\ \rightarrow \ (D\ \rightarrow \ C))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $R(y)$ in \hyperref[predtheo1:6]{$6$} } \\ \label{predtheo1:8} $8$ & $(R(y)\ \rightarrow \ \exists x\, R(x))\ \rightarrow \ ((D\ \rightarrow \ R(y))\ \rightarrow \ (D\ \rightarrow \ \exists x\, R(x)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $\exists x\, R(x)$ in \hyperref[predtheo1:7]{$7$} } \\ \label{predtheo1:9} $9$ & $(R(y)\ \rightarrow \ \exists x\, R(x))\ \rightarrow \ ((\forall x\, R(x)\ \rightarrow \ R(y))\ \rightarrow \ (\forall x\, R(x)\ \rightarrow \ \exists x\, R(x)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $\forall x\, R(x)$ in \hyperref[predtheo1:8]{$8$} } \\ \label{predtheo1:10} $10$ & $(\forall x\, R(x)\ \rightarrow \ R(y))\ \rightarrow \ (\forall x\, R(x)\ \rightarrow \ \exists x\, R(x))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[predtheo1:2]{$2$}, \hyperref[predtheo1:9]{$9$}} \\ \label{predtheo1:11} $11$ & $\forall x\, R(x)\ \rightarrow \ \exists x\, R(x)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[predtheo1:1]{$1$}, \hyperref[predtheo1:10]{$10$}} \\ & & \qedhere \end{longtable} \end{proof} A well known implication: \begin{thm}[predtheo2] \hypertarget{predtheo2}{} \begin{displaymath} \exists x\, R(x)\ \rightarrow \ \neg \forall x\, \neg R(x)\end{displaymath} \end{thm} \begin{proof} \mbox{}\\ \begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}} \label{predtheo2:1} $1$ & $\forall x\, R(x)\ \rightarrow \ R(y)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{axiom5}{axiom5} } \\ \label{predtheo2:2} $2$ & $\forall x\, \neg R(x)\ \rightarrow \ \neg R(y)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule3}{replace} $R(@S_{1})$ by $\neg R(@S_{1})$ in \hyperref[predtheo2:1]{$1$} } \\ \label{predtheo2:3} $3$ & $\neg \forall x\, \neg R(x)\ \vee \ \neg R(y)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule5}{use abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{impl}{impl} in \hyperref[predtheo2:2]{$2$} at occurence $1$ } \\ \label{predtheo2:4} $4$ & $(P\ \vee \ Q)\ \rightarrow \ (Q\ \vee \ P)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom3}{axiom3} } \\ \label{predtheo2:5} $5$ & $(\neg \forall x\, \neg R(x)\ \vee \ Q)\ \rightarrow \ (Q\ \vee \ \neg \forall x\, \neg R(x))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $P$ by $\neg \forall x\, \neg R(x)$ in \hyperref[predtheo2:4]{$4$} } \\ \label{predtheo2:6} $6$ & $(\neg \forall x\, \neg R(x)\ \vee \ \neg R(y))\ \rightarrow \ (\neg R(y)\ \vee \ \neg \forall x\, \neg R(x))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $Q$ by $\neg R(y)$ in \hyperref[predtheo2:5]{$5$} } \\ \label{predtheo2:7} $7$ & $\neg R(y)\ \vee \ \neg \forall x\, \neg R(x)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[predtheo2:3]{$3$}, \hyperref[predtheo2:6]{$6$}} \\ \label{predtheo2:8} $8$ & $R(y)\ \rightarrow \ \neg \forall x\, \neg R(x)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{impl}{impl} in \hyperref[predtheo2:7]{$7$} at occurence $1$ } \\ \label{predtheo2:9} $9$ & $\exists y\, R(y)\ \rightarrow \ \neg \forall x\, \neg R(x)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule4}{Particularize} by $y$ in \hyperref[predtheo2:8]{$8$}} \\ \label{predtheo2:10} $10$ & $\exists x\, R(x)\ \rightarrow \ \neg \forall x\, \neg R(x)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule1}{rename} $y$ into $x$ in \hyperref[predtheo2:9]{$9$} at occurence $1$ } \\ & & \qedhere \end{longtable} \end{proof} The reverse is also true: \begin{thm}[predtheo3] \hypertarget{predtheo3}{} \begin{displaymath} \neg \forall x\, \neg R(x)\ \rightarrow \ \exists x\, R(x)\end{displaymath} \end{thm} \begin{proof} \mbox{}\\ \begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}} \label{predtheo3:1} $1$ & $R(y)\ \rightarrow \ \exists x\, R(x)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{axiom6}{axiom6} } \\ \label{predtheo3:2} $2$ & $(P\ \rightarrow \ Q)\ \rightarrow \ (\neg Q\ \rightarrow \ \neg P)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert1_1.00.00_1.00.00.pdf}{}{hilb7}{hilb7} } \\ \label{predtheo3:3} $3$ & $(A\ \rightarrow \ Q)\ \rightarrow \ (\neg Q\ \rightarrow \ \neg A)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $P$ by $A$ in \hyperref[predtheo3:2]{$2$} } \\ \label{predtheo3:4} $4$ & $(A\ \rightarrow \ B)\ \rightarrow \ (\neg B\ \rightarrow \ \neg A)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $Q$ by $B$ in \hyperref[predtheo3:3]{$3$} } \\ \label{predtheo3:5} $5$ & $(R(y)\ \rightarrow \ B)\ \rightarrow \ (\neg B\ \rightarrow \ \neg R(y))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $A$ by $R(y)$ in \hyperref[predtheo3:4]{$4$} } \\ \label{predtheo3:6} $6$ & $(R(y)\ \rightarrow \ \exists x\, R(x))\ \rightarrow \ (\neg \exists x\, R(x)\ \rightarrow \ \neg R(y))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $\exists x\, R(x)$ in \hyperref[predtheo3:5]{$5$} } \\ \label{predtheo3:7} $7$ & $\neg \exists x\, R(x)\ \rightarrow \ \neg R(y)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[predtheo3:1]{$1$}, \hyperref[predtheo3:6]{$6$}} \\ \label{predtheo3:8} $8$ & $\neg \exists x\, R(x)\ \rightarrow \ \forall y\, \neg R(y)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule5}{Generalize} by $y$ in \hyperref[predtheo3:7]{$7$}} \\ \label{predtheo3:9} $9$ & $(\neg \exists x\, R(x)\ \rightarrow \ B)\ \rightarrow \ (\neg B\ \rightarrow \ \neg \neg \exists x\, R(x))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $A$ by $\neg \exists x\, R(x)$ in \hyperref[predtheo3:4]{$4$} } \\ \label{predtheo3:10} $10$ & $(\neg \exists x\, R(x)\ \rightarrow \ \forall y\, \neg R(y))\ \rightarrow \ (\neg \forall y\, \neg R(y)\ \rightarrow \ \neg \neg \exists x\, R(x))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $\forall y\, \neg R(y)$ in \hyperref[predtheo3:9]{$9$} } \\ \label{predtheo3:11} $11$ & $\neg \forall y\, \neg R(y)\ \rightarrow \ \neg \neg \exists x\, R(x)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[predtheo3:8]{$8$}, \hyperref[predtheo3:10]{$10$}} \\ \label{predtheo3:12} $12$ & $\neg \neg P\ \rightarrow \ P$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert1_1.00.00_1.00.00.pdf}{}{hilb6}{hilb6} } \\ \label{predtheo3:13} $13$ & $\neg \neg Q\ \rightarrow \ Q$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $P$ by $Q$ in \hyperref[predtheo3:12]{$12$} } \\ \label{predtheo3:14} $14$ & $\neg \neg \exists x\, R(x)\ \rightarrow \ \exists x\, R(x)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $Q$ by $\exists x\, R(x)$ in \hyperref[predtheo3:13]{$13$} } \\ \label{predtheo3:15} $15$ & $(P\ \rightarrow \ Q)\ \rightarrow \ (\neg P\ \vee \ Q)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert1_1.00.00_1.00.00.pdf}{}{defimpl1}{defimpl1} } \\ \label{predtheo3:16} $16$ & $(\neg P\ \vee \ Q)\ \rightarrow \ (P\ \rightarrow \ Q)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert1_1.00.00_1.00.00.pdf}{}{defimpl2}{defimpl2} } \\ \label{predtheo3:17} $17$ & $(P\ \rightarrow \ Q)\ \rightarrow \ ((A\ \vee \ P)\ \rightarrow \ (A\ \vee \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom4}{axiom4} } \\ \label{predtheo3:18} $18$ & $(B\ \rightarrow \ Q)\ \rightarrow \ ((A\ \vee \ B)\ \rightarrow \ (A\ \vee \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $P$ by $B$ in \hyperref[predtheo3:17]{$17$} } \\ \label{predtheo3:19} $19$ & $(B\ \rightarrow \ C)\ \rightarrow \ ((A\ \vee \ B)\ \rightarrow \ (A\ \vee \ C))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $Q$ by $C$ in \hyperref[predtheo3:18]{$18$} } \\ \label{predtheo3:20} $20$ & $(B\ \rightarrow \ C)\ \rightarrow \ ((D\ \vee \ B)\ \rightarrow \ (D\ \vee \ C))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $A$ by $D$ in \hyperref[predtheo3:19]{$19$} } \\ \label{predtheo3:21} $21$ & $(\neg \neg \exists x\, R(x)\ \rightarrow \ C)\ \rightarrow \ ((D\ \vee \ \neg \neg \exists x\, R(x))\ \rightarrow \ (D\ \vee \ C))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $\neg \neg \exists x\, R(x)$ in \hyperref[predtheo3:20]{$20$} } \\ \label{predtheo3:22} $22$ & $(\neg \neg \exists x\, R(x)\ \rightarrow \ \exists x\, R(x))\ \rightarrow \ ((D\ \vee \ \neg \neg \exists x\, R(x))\ \rightarrow \ (D\ \vee \ \exists x\, R(x)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $\exists x\, R(x)$ in \hyperref[predtheo3:21]{$21$} } \\ \label{predtheo3:23} $23$ & $(\neg \neg \exists x\, R(x)\ \rightarrow \ \exists x\, R(x))\ \rightarrow \ ((\neg \neg \forall y\, \neg R(y)\ \vee \ \neg \neg \exists x\, R(x))\ \rightarrow \ (\neg \neg \forall y\, \neg R(y)\ \vee \ \exists x\, R(x)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $\neg \neg \forall y\, \neg R(y)$ in \hyperref[predtheo3:22]{$22$} } \\ \label{predtheo3:24} $24$ & $(\neg \neg \forall y\, \neg R(y)\ \vee \ \neg \neg \exists x\, R(x))\ \rightarrow \ (\neg \neg \forall y\, \neg R(y)\ \vee \ \exists x\, R(x))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[predtheo3:14]{$14$}, \hyperref[predtheo3:23]{$23$}} \\ \label{predtheo3:25} $25$ & $(A\ \rightarrow \ Q)\ \rightarrow \ (\neg A\ \vee \ Q)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $P$ by $A$ in \hyperref[predtheo3:15]{$15$} } \\ \label{predtheo3:26} $26$ & $(A\ \rightarrow \ B)\ \rightarrow \ (\neg A\ \vee \ B)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $Q$ by $B$ in \hyperref[predtheo3:25]{$25$} } \\ \label{predtheo3:27} $27$ & $(\neg \forall y\, \neg R(y)\ \rightarrow \ B)\ \rightarrow \ (\neg \neg \forall y\, \neg R(y)\ \vee \ B)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $A$ by $\neg \forall y\, \neg R(y)$ in \hyperref[predtheo3:26]{$26$} } \\ \label{predtheo3:28} $28$ & $(\neg \forall y\, \neg R(y)\ \rightarrow \ \neg \neg \exists x\, R(x))\ \rightarrow \ (\neg \neg \forall y\, \neg R(y)\ \vee \ \neg \neg \exists x\, R(x))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $\neg \neg \exists x\, R(x)$ in \hyperref[predtheo3:27]{$27$} } \\ \label{predtheo3:29} $29$ & $(P\ \rightarrow \ Q)\ \rightarrow \ ((A\ \rightarrow \ P)\ \rightarrow \ (A\ \rightarrow \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert1_1.00.00_1.00.00.pdf}{}{hilb1}{hilb1} } \\ \label{predtheo3:30} $30$ & $(B\ \rightarrow \ Q)\ \rightarrow \ ((A\ \rightarrow \ B)\ \rightarrow \ (A\ \rightarrow \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $P$ by $B$ in \hyperref[predtheo3:29]{$29$} } \\ \label{predtheo3:31} $31$ & $(B\ \rightarrow \ C)\ \rightarrow \ ((A\ \rightarrow \ B)\ \rightarrow \ (A\ \rightarrow \ C))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $Q$ by $C$ in \hyperref[predtheo3:30]{$30$} } \\ \label{predtheo3:32} $32$ & $(B\ \rightarrow \ C)\ \rightarrow \ ((D\ \rightarrow \ B)\ \rightarrow \ (D\ \rightarrow \ C))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $A$ by $D$ in \hyperref[predtheo3:31]{$31$} } \\ \label{predtheo3:33} $33$ & $((\neg \neg \forall y\, \neg R(y)\ \vee \ \neg \neg \exists x\, R(x))\ \rightarrow \ C)\ \rightarrow \ ((D\ \rightarrow \ (\neg \neg \forall y\, \neg R(y)\ \vee \ \neg \neg \exists x\, R(x)))\ \rightarrow \ (D\ \rightarrow \ C))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $\neg \neg \forall y\, \neg R(y)\ \vee \ \neg \neg \exists x\, R(x)$ in \hyperref[predtheo3:32]{$32$} } \\ \label{predtheo3:34} $34$ & $((\neg \neg \forall y\, \neg R(y)\ \vee \ \neg \neg \exists x\, R(x))\ \rightarrow \ (\neg \neg \forall y\, \neg R(y)\ \vee \ \exists x\, R(x)))\ \rightarrow \ ((D\ \rightarrow \ (\neg \neg \forall y\, \neg R(y)\ \vee \ \neg \neg \exists x\, R(x)))\ \rightarrow \ (D\ \rightarrow \ (\neg \neg \forall y\, \neg R(y)\ \vee \ \exists x\, R(x))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $\neg \neg \forall y\, \neg R(y)\ \vee \ \exists x\, R(x)$ in \hyperref[predtheo3:33]{$33$} } \\ \label{predtheo3:35} $35$ & $((\neg \neg \forall y\, \neg R(y)\ \vee \ \neg \neg \exists x\, R(x))\ \rightarrow \ (\neg \neg \forall y\, \neg R(y)\ \vee \ \exists x\, R(x)))\ \rightarrow \ (((\neg \forall y\, \neg R(y)\ \rightarrow \ \neg \neg \exists x\, R(x))\ \rightarrow \ (\neg \neg \forall y\, \neg R(y)\ \vee \ \neg \neg \exists x\, R(x)))\ \rightarrow \ ((\neg \forall y\, \neg R(y)\ \rightarrow \ \neg \neg \exists x\, R(x))\ \rightarrow \ (\neg \neg \forall y\, \neg R(y)\ \vee \ \exists x\, R(x))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $\neg \forall y\, \neg R(y)\ \rightarrow \ \neg \neg \exists x\, R(x)$ in \hyperref[predtheo3:34]{$34$} } \\ \label{predtheo3:36} $36$ & $((\neg \forall y\, \neg R(y)\ \rightarrow \ \neg \neg \exists x\, R(x))\ \rightarrow \ (\neg \neg \forall y\, \neg R(y)\ \vee \ \neg \neg \exists x\, R(x)))\ \rightarrow \ ((\neg \forall y\, \neg R(y)\ \rightarrow \ \neg \neg \exists x\, R(x))\ \rightarrow \ (\neg \neg \forall y\, \neg R(y)\ \vee \ \exists x\, R(x)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[predtheo3:24]{$24$}, \hyperref[predtheo3:35]{$35$}} \\ \label{predtheo3:37} $37$ & $(\neg \forall y\, \neg R(y)\ \rightarrow \ \neg \neg \exists x\, R(x))\ \rightarrow \ (\neg \neg \forall y\, \neg R(y)\ \vee \ \exists x\, R(x))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[predtheo3:28]{$28$}, \hyperref[predtheo3:36]{$36$}} \\ \label{predtheo3:38} $38$ & $(\neg A\ \vee \ Q)\ \rightarrow \ (A\ \rightarrow \ Q)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $P$ by $A$ in \hyperref[predtheo3:16]{$16$} } \\ \label{predtheo3:39} $39$ & $(\neg A\ \vee \ B)\ \rightarrow \ (A\ \rightarrow \ B)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $Q$ by $B$ in \hyperref[predtheo3:38]{$38$} } \\ \label{predtheo3:40} $40$ & $(\neg \neg \forall y\, \neg R(y)\ \vee \ B)\ \rightarrow \ (\neg \forall y\, \neg R(y)\ \rightarrow \ B)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $A$ by $\neg \forall y\, \neg R(y)$ in \hyperref[predtheo3:39]{$39$} } \\ \label{predtheo3:41} $41$ & $(\neg \neg \forall y\, \neg R(y)\ \vee \ \exists x\, R(x))\ \rightarrow \ (\neg \forall y\, \neg R(y)\ \rightarrow \ \exists x\, R(x))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $\exists x\, R(x)$ in \hyperref[predtheo3:40]{$40$} } \\ \label{predtheo3:42} $42$ & $((\neg \neg \forall y\, \neg R(y)\ \vee \ \exists x\, R(x))\ \rightarrow \ C)\ \rightarrow \ ((D\ \rightarrow \ (\neg \neg \forall y\, \neg R(y)\ \vee \ \exists x\, R(x)))\ \rightarrow \ (D\ \rightarrow \ C))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $\neg \neg \forall y\, \neg R(y)\ \vee \ \exists x\, R(x)$ in \hyperref[predtheo3:32]{$32$} } \\ \label{predtheo3:43} $43$ & $((\neg \neg \forall y\, \neg R(y)\ \vee \ \exists x\, R(x))\ \rightarrow \ (\neg \forall y\, \neg R(y)\ \rightarrow \ \exists x\, R(x)))\ \rightarrow \ ((D\ \rightarrow \ (\neg \neg \forall y\, \neg R(y)\ \vee \ \exists x\, R(x)))\ \rightarrow \ (D\ \rightarrow \ (\neg \forall y\, \neg R(y)\ \rightarrow \ \exists x\, R(x))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $\neg \forall y\, \neg R(y)\ \rightarrow \ \exists x\, R(x)$ in \hyperref[predtheo3:42]{$42$} } \\ \label{predtheo3:44} $44$ & $((\neg \neg \forall y\, \neg R(y)\ \vee \ \exists x\, R(x))\ \rightarrow \ (\neg \forall y\, \neg R(y)\ \rightarrow \ \exists x\, R(x)))\ \rightarrow \ (((\neg \forall y\, \neg R(y)\ \rightarrow \ \neg \neg \exists x\, R(x))\ \rightarrow \ (\neg \neg \forall y\, \neg R(y)\ \vee \ \exists x\, R(x)))\ \rightarrow \ ((\neg \forall y\, \neg R(y)\ \rightarrow \ \neg \neg \exists x\, R(x))\ \rightarrow \ (\neg \forall y\, \neg R(y)\ \rightarrow \ \exists x\, R(x))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $\neg \forall y\, \neg R(y)\ \rightarrow \ \neg \neg \exists x\, R(x)$ in \hyperref[predtheo3:43]{$43$} } \\ \label{predtheo3:45} $45$ & $((\neg \forall y\, \neg R(y)\ \rightarrow \ \neg \neg \exists x\, R(x))\ \rightarrow \ (\neg \neg \forall y\, \neg R(y)\ \vee \ \exists x\, R(x)))\ \rightarrow \ ((\neg \forall y\, \neg R(y)\ \rightarrow \ \neg \neg \exists x\, R(x))\ \rightarrow \ (\neg \forall y\, \neg R(y)\ \rightarrow \ \exists x\, R(x)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[predtheo3:41]{$41$}, \hyperref[predtheo3:44]{$44$}} \\ \label{predtheo3:46} $46$ & $(\neg \forall y\, \neg R(y)\ \rightarrow \ \neg \neg \exists x\, R(x))\ \rightarrow \ (\neg \forall y\, \neg R(y)\ \rightarrow \ \exists x\, R(x))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[predtheo3:37]{$37$}, \hyperref[predtheo3:45]{$45$}} \\ \label{predtheo3:47} $47$ & $\neg \forall y\, \neg R(y)\ \rightarrow \ \exists x\, R(x)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[predtheo3:11]{$11$}, \hyperref[predtheo3:46]{$46$}} \\ \label{predtheo3:48} $48$ & $\neg \forall x\, \neg R(x)\ \rightarrow \ \exists x\, R(x)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule1}{rename} $y$ into $x$ in \hyperref[predtheo3:47]{$47$} at occurence $1$ } \\ & & \qedhere \end{longtable} \end{proof} Exchange of universal quantors: \begin{thm}[predtheo4] \hypertarget{predtheo4}{} \begin{displaymath} \forall x\, \forall y\, R(x, y)\ \rightarrow \ \forall y\, \forall x\, R(x, y)\end{displaymath} \end{thm} \begin{proof} \mbox{}\\ \begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}} \label{predtheo4:1} $1$ & $\forall x\, R(x)\ \rightarrow \ R(y)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{axiom5}{axiom5} } \\ \label{predtheo4:2} $2$ & $\forall x\, R(x)\ \rightarrow \ R(w)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule2}{rename} $y$ into $w$ in \hyperref[predtheo4:1]{$1$} } \\ \label{predtheo4:3} $3$ & $\forall r\, R(r)\ \rightarrow \ R(w)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule1}{rename} $x$ into $r$ in \hyperref[predtheo4:2]{$2$} at occurence $1$ } \\ \label{predtheo4:4} $4$ & $\forall r\, R(r)\ \rightarrow \ R(u)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule2}{rename} $w$ into $u$ in \hyperref[predtheo4:3]{$3$} } \\ \label{predtheo4:5} $5$ & $\forall y\, R(y)\ \rightarrow \ R(u)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule1}{rename} $r$ into $y$ in \hyperref[predtheo4:4]{$4$} at occurence $1$ } \\ \label{predtheo4:6} $6$ & $\forall y\, R(z, y)\ \rightarrow \ R(z, u)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule3}{replace} $R(@S_{1})$ by $R(z, @S_{1})$ in \hyperref[predtheo4:5]{$5$} } \\ \label{predtheo4:7} $7$ & $\forall x\, R(x)\ \rightarrow \ R(r)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule2}{rename} $y$ into $r$ in \hyperref[predtheo4:1]{$1$} } \\ \label{predtheo4:8} $8$ & $\forall s\, R(s)\ \rightarrow \ R(r)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule1}{rename} $x$ into $s$ in \hyperref[predtheo4:7]{$7$} at occurence $1$ } \\ \label{predtheo4:9} $9$ & $\forall s\, R(s)\ \rightarrow \ R(z)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule2}{rename} $r$ into $z$ in \hyperref[predtheo4:8]{$8$} } \\ \label{predtheo4:10} $10$ & $\forall v\, R(v)\ \rightarrow \ R(z)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule1}{rename} $s$ into $v$ in \hyperref[predtheo4:9]{$9$} at occurence $1$ } \\ \label{predtheo4:11} $11$ & $\forall v\, \forall w\, R(v, w)\ \rightarrow \ \forall w\, R(z, w)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule3}{replace} $R(@S_{1})$ by $\forall w\, R(@S_{1}, w)$ in \hyperref[predtheo4:10]{$10$} } \\ \label{predtheo4:12} $12$ & $\forall c\, \forall w\, R(c, w)\ \rightarrow \ \forall w\, R(z, w)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule1}{rename} $v$ into $c$ in \hyperref[predtheo4:11]{$11$} at occurence $1$ } \\ \label{predtheo4:13} $13$ & $\forall c\, \forall d\, R(c, d)\ \rightarrow \ \forall w\, R(z, w)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule1}{rename} $w$ into $d$ in \hyperref[predtheo4:12]{$12$} at occurence $1$ } \\ \label{predtheo4:14} $14$ & $\forall c\, \forall d\, R(c, d)\ \rightarrow \ \forall x_{14}\, R(z, x_{14})$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule1}{rename} $w$ into $x_{14}$ in \hyperref[predtheo4:13]{$13$} at occurence $1$ } \\ \label{predtheo4:15} $15$ & $\forall x\, \forall d\, R(x, d)\ \rightarrow \ \forall x_{14}\, R(z, x_{14})$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule1}{rename} $c$ into $x$ in \hyperref[predtheo4:14]{$14$} at occurence $1$ } \\ \label{predtheo4:16} $16$ & $\forall x\, \forall y\, R(x, y)\ \rightarrow \ \forall x_{14}\, R(z, x_{14})$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule1}{rename} $d$ into $y$ in \hyperref[predtheo4:15]{$15$} at occurence $1$ } \\ \label{predtheo4:17} $17$ & $\forall x\, \forall y\, R(x, y)\ \rightarrow \ \forall y\, R(z, y)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule1}{rename} $x_{14}$ into $y$ in \hyperref[predtheo4:16]{$16$} at occurence $1$ } \\ \label{predtheo4:18} $18$ & $(P\ \rightarrow \ Q)\ \rightarrow \ ((A\ \rightarrow \ P)\ \rightarrow \ (A\ \rightarrow \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert1_1.00.00_1.00.00.pdf}{}{hilb1}{hilb1} } \\ \label{predtheo4:19} $19$ & $(C\ \rightarrow \ Q)\ \rightarrow \ ((A\ \rightarrow \ C)\ \rightarrow \ (A\ \rightarrow \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $P$ by $C$ in \hyperref[predtheo4:18]{$18$} } \\ \label{predtheo4:20} $20$ & $(C\ \rightarrow \ D)\ \rightarrow \ ((A\ \rightarrow \ C)\ \rightarrow \ (A\ \rightarrow \ D))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $Q$ by $D$ in \hyperref[predtheo4:19]{$19$} } \\ \label{predtheo4:21} $21$ & $(C\ \rightarrow \ D)\ \rightarrow \ ((P_{7}\ \rightarrow \ C)\ \rightarrow \ (P_{7}\ \rightarrow \ D))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $A$ by $P_{7}$ in \hyperref[predtheo4:20]{$20$} } \\ \label{predtheo4:22} $22$ & $(\forall y\, R(z, y)\ \rightarrow \ D)\ \rightarrow \ ((P_{7}\ \rightarrow \ \forall y\, R(z, y))\ \rightarrow \ (P_{7}\ \rightarrow \ D))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $\forall y\, R(z, y)$ in \hyperref[predtheo4:21]{$21$} } \\ \label{predtheo4:23} $23$ & $(\forall y\, R(z, y)\ \rightarrow \ R(z, u))\ \rightarrow \ ((P_{7}\ \rightarrow \ \forall y\, R(z, y))\ \rightarrow \ (P_{7}\ \rightarrow \ R(z, u)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $R(z, u)$ in \hyperref[predtheo4:22]{$22$} } \\ \label{predtheo4:24} $24$ & $(\forall y\, R(z, y)\ \rightarrow \ R(z, u))\ \rightarrow \ ((\forall x\, \forall y\, R(x, y)\ \rightarrow \ \forall y\, R(z, y))\ \rightarrow \ (\forall x\, \forall y\, R(x, y)\ \rightarrow \ R(z, u)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $P_{7}$ by $\forall x\, \forall y\, R(x, y)$ in \hyperref[predtheo4:23]{$23$} } \\ \label{predtheo4:25} $25$ & $(\forall x\, \forall y\, R(x, y)\ \rightarrow \ \forall y\, R(z, y))\ \rightarrow \ (\forall x\, \forall y\, R(x, y)\ \rightarrow \ R(z, u))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[predtheo4:6]{$6$}, \hyperref[predtheo4:24]{$24$}} \\ \label{predtheo4:26} $26$ & $\forall x\, \forall y\, R(x, y)\ \rightarrow \ R(z, u)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[predtheo4:17]{$17$}, \hyperref[predtheo4:25]{$25$}} \\ \label{predtheo4:27} $27$ & $\forall x\, \forall y\, R(x, y)\ \rightarrow \ \forall z\, R(z, u)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule5}{Generalize} by $z$ in \hyperref[predtheo4:26]{$26$}} \\ \label{predtheo4:28} $28$ & $\forall x\, \forall y\, R(x, y)\ \rightarrow \ \forall u\, \forall z\, R(z, u)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule5}{Generalize} by $u$ in \hyperref[predtheo4:27]{$27$}} \\ \label{predtheo4:29} $29$ & $\forall x\, \forall y\, R(x, y)\ \rightarrow \ \forall y\, \forall z\, R(z, y)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule1}{rename} $u$ into $y$ in \hyperref[predtheo4:28]{$28$} at occurence $1$ } \\ \label{predtheo4:30} $30$ & $\forall x\, \forall y\, R(x, y)\ \rightarrow \ \forall y\, \forall x\, R(x, y)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule1}{rename} $z$ into $x$ in \hyperref[predtheo4:29]{$29$} at occurence $1$ } \\ & & \qedhere \end{longtable} \end{proof} Implication of changing sequence of existence and universal quantor: \begin{thm}[predtheo5] \hypertarget{predtheo5}{} \begin{displaymath} \exists x\, \forall y\, R(x, y)\ \rightarrow \ \forall y\, \exists x\, R(x, y)\end{displaymath} \end{thm} \begin{proof} \mbox{}\\ \begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}} \label{predtheo5:1} $1$ & $\forall x\, R(x)\ \rightarrow \ R(y)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{axiom5}{axiom5} } \\ \label{predtheo5:2} $2$ & $\forall x\, R(x)\ \rightarrow \ R(w)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule2}{rename} $y$ into $w$ in \hyperref[predtheo5:1]{$1$} } \\ \label{predtheo5:3} $3$ & $\forall r\, R(r)\ \rightarrow \ R(w)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule1}{rename} $x$ into $r$ in \hyperref[predtheo5:2]{$2$} at occurence $1$ } \\ \label{predtheo5:4} $4$ & $\forall r\, R(r)\ \rightarrow \ R(u)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule2}{rename} $w$ into $u$ in \hyperref[predtheo5:3]{$3$} } \\ \label{predtheo5:5} $5$ & $\forall y\, R(y)\ \rightarrow \ R(u)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule1}{rename} $r$ into $y$ in \hyperref[predtheo5:4]{$4$} at occurence $1$ } \\ \label{predtheo5:6} $6$ & $\forall y\, R(x, y)\ \rightarrow \ R(x, u)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule3}{replace} $R(@S_{1})$ by $R(x, @S_{1})$ in \hyperref[predtheo5:5]{$5$} } \\ \label{predtheo5:7} $7$ & $R(y)\ \rightarrow \ \exists x\, R(x)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{axiom6}{axiom6} } \\ \label{predtheo5:8} $8$ & $R(v)\ \rightarrow \ \exists x\, R(x)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule2}{rename} $y$ into $v$ in \hyperref[predtheo5:7]{$7$} } \\ \label{predtheo5:9} $9$ & $R(v)\ \rightarrow \ \exists w\, R(w)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule1}{rename} $x$ into $w$ in \hyperref[predtheo5:8]{$8$} at occurence $1$ } \\ \label{predtheo5:10} $10$ & $R(x)\ \rightarrow \ \exists w\, R(w)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule2}{rename} $v$ into $x$ in \hyperref[predtheo5:9]{$9$} } \\ \label{predtheo5:11} $11$ & $R(x)\ \rightarrow \ \exists z\, R(z)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule1}{rename} $w$ into $z$ in \hyperref[predtheo5:10]{$10$} at occurence $1$ } \\ \label{predtheo5:12} $12$ & $R(x, u)\ \rightarrow \ \exists z\, R(z, u)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule3}{replace} $R(@S_{1})$ by $R(@S_{1}, u)$ in \hyperref[predtheo5:11]{$11$} } \\ \label{predtheo5:13} $13$ & $(P\ \rightarrow \ Q)\ \rightarrow \ ((A\ \rightarrow \ P)\ \rightarrow \ (A\ \rightarrow \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert1_1.00.00_1.00.00.pdf}{}{hilb1}{hilb1} } \\ \label{predtheo5:14} $14$ & $(C\ \rightarrow \ Q)\ \rightarrow \ ((A\ \rightarrow \ C)\ \rightarrow \ (A\ \rightarrow \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $P$ by $C$ in \hyperref[predtheo5:13]{$13$} } \\ \label{predtheo5:15} $15$ & $(C\ \rightarrow \ D)\ \rightarrow \ ((A\ \rightarrow \ C)\ \rightarrow \ (A\ \rightarrow \ D))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $Q$ by $D$ in \hyperref[predtheo5:14]{$14$} } \\ \label{predtheo5:16} $16$ & $(C\ \rightarrow \ D)\ \rightarrow \ ((P_{7}\ \rightarrow \ C)\ \rightarrow \ (P_{7}\ \rightarrow \ D))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $A$ by $P_{7}$ in \hyperref[predtheo5:15]{$15$} } \\ \label{predtheo5:17} $17$ & $(R(x, u)\ \rightarrow \ D)\ \rightarrow \ ((P_{7}\ \rightarrow \ R(x, u))\ \rightarrow \ (P_{7}\ \rightarrow \ D))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $R(x, u)$ in \hyperref[predtheo5:16]{$16$} } \\ \label{predtheo5:18} $18$ & $(R(x, u)\ \rightarrow \ \exists z\, R(z, u))\ \rightarrow \ ((P_{7}\ \rightarrow \ R(x, u))\ \rightarrow \ (P_{7}\ \rightarrow \ \exists z\, R(z, u)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $\exists z\, R(z, u)$ in \hyperref[predtheo5:17]{$17$} } \\ \label{predtheo5:19} $19$ & $(R(x, u)\ \rightarrow \ \exists z\, R(z, u))\ \rightarrow \ ((\forall y\, R(x, y)\ \rightarrow \ R(x, u))\ \rightarrow \ (\forall y\, R(x, y)\ \rightarrow \ \exists z\, R(z, u)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $P_{7}$ by $\forall y\, R(x, y)$ in \hyperref[predtheo5:18]{$18$} } \\ \label{predtheo5:20} $20$ & $(\forall y\, R(x, y)\ \rightarrow \ R(x, u))\ \rightarrow \ (\forall y\, R(x, y)\ \rightarrow \ \exists z\, R(z, u))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[predtheo5:12]{$12$}, \hyperref[predtheo5:19]{$19$}} \\ \label{predtheo5:21} $21$ & $\forall y\, R(x, y)\ \rightarrow \ \exists z\, R(z, u)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[predtheo5:6]{$6$}, \hyperref[predtheo5:20]{$20$}} \\ \label{predtheo5:22} $22$ & $\exists x\, \forall y\, R(x, y)\ \rightarrow \ \exists z\, R(z, u)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule4}{Particularize} by $x$ in \hyperref[predtheo5:21]{$21$}} \\ \label{predtheo5:23} $23$ & $\exists x\, \forall y\, R(x, y)\ \rightarrow \ \forall u\, \exists z\, R(z, u)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule5}{Generalize} by $u$ in \hyperref[predtheo5:22]{$22$}} \\ \label{predtheo5:24} $24$ & $\exists x\, \forall y\, R(x, y)\ \rightarrow \ \forall c\, \exists z\, R(z, c)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule1}{rename} $u$ into $c$ in \hyperref[predtheo5:23]{$23$} at occurence $1$ } \\ \label{predtheo5:25} $25$ & $\exists x\, \forall y\, R(x, y)\ \rightarrow \ \forall c\, \exists d\, R(d, c)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule1}{rename} $z$ into $d$ in \hyperref[predtheo5:24]{$24$} at occurence $1$ } \\ \label{predtheo5:26} $26$ & $\exists x\, \forall y\, R(x, y)\ \rightarrow \ \forall y\, \exists d\, R(d, y)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule1}{rename} $c$ into $y$ in \hyperref[predtheo5:25]{$25$} at occurence $1$ } \\ \label{predtheo5:27} $27$ & $\exists x\, \forall y\, R(x, y)\ \rightarrow \ \forall y\, \exists x\, R(x, y)$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule1}{rename} $d$ into $x$ in \hyperref[predtheo5:26]{$26$} at occurence $1$ } \\ & & \qedhere \end{longtable} \end{proof} \end{document}