%%% ==================================================================== %%% @LaTeX-file generated by com.meyling.principia.latex.Module2Latex %%% ==================================================================== \documentclass{amsart} \usepackage{amsmath,amsthm,amsfonts} \usepackage[]{color} \usepackage{xr} \usepackage{epsfig,longtable} \usepackage{varioref} \usepackage[a4paper,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 \makeatletter \def\listoffigures{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn\fi \chapter*{List of Figures} {\let\\ \ \markboth{Title}{List of Figures}} \addcontentsline{toc}{chapter}{\protect \numberline{LIST OF FIGURES\string\hss}} \@starttoc{lof}\if@restonecol \twocolumn\fi} \makeatother \def\boldindex#1{\textbf{\hyperpage{#1}}} \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} \sloppy \begin{document} \title{Some more theorems of Predicate Calculus} \author{Michael Meyling} \email{principa@meyling.com} \date{2002-07-27T21:00:49} \begin{abstract} This module includes first proofs of predicate calculus theorems. \end{abstract} \makeatletter \long\def\hyper@section@backref#1#2#3{% \typeout{BACK REF #1 / #2 / #3}% \hyperlink{#3}{#2}} \makeatother \pdfbookmark{Title}{tit} \setlongtables \maketitle \tableofcontents \section*{module specification} Author of this module: \begin{longtable}[h!]{l@{\extracolsep{\fill}}l} Michael Meyling & michael@meyling.com \\ \end{longtable} \medskip This module has the following specification: \mbox{} \begin{longtable}[h!]{l@{\extracolsep{\fill}}p{12cm}} Name: & predtheo2 \\ Version: & 1.00.00 \\ Rule version: & 1.00.00 \\ Orgin: & \url{http://www.meyling.com/principia/0_00_51/predtheo2_1.00.00_1.00.00.qedeq} \\ \end{longtable} \medskip The following modules were used: \mbox{} \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} A simple implication: \begin{thm} \hypertarget{predtheo1}{} \begin{displaymath} (\exists x(R(x))\ \Rightarrow \ \forall 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$ & $(\exists 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 \ \forall 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 \ \forall x(R(x)))\ \Rightarrow \ ((D\ \Rightarrow \ R(y))\ \Rightarrow \ (D\ \Rightarrow \ \forall x(R(x)))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $\forall x(R(x))$ in \hyperref[predtheo1:7]{$7$} } \\ \label{predtheo1:9} $9$ & $((R(y)\ \Rightarrow \ \forall x(R(x)))\ \Rightarrow \ ((\exists x(R(x))\ \Rightarrow \ R(y))\ \Rightarrow \ (\exists x(R(x))\ \Rightarrow \ \forall x(R(x)))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $\exists x(R(x))$ in \hyperref[predtheo1:8]{$8$} } \\ \label{predtheo1:10} $10$ & $((\exists x(R(x))\ \Rightarrow \ R(y))\ \Rightarrow \ (\exists x(R(x))\ \Rightarrow \ \forall 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$ & $(\exists x(R(x))\ \Rightarrow \ \forall x(R(x)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[predtheo1:1]{$1$}, \hyperref[predtheo1:10]{$10$}} \\ \\ & & & \mbox{\qedhere} \end{longtable} \end{proof} A well known implication: \begin{thm} \hypertarget{predtheo2}{} \begin{displaymath} (\forall x(R(x))\ \Rightarrow \ \neg \exists 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$ & $(\exists 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$ & $(\exists 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 \exists 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 \exists x(\neg R(x))\ \vee \ Q)\ \Rightarrow \ (Q\ \vee \ \neg \exists x(\neg R(x))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $P$ by $\neg \exists x(\neg R(x))$ in \hyperref[predtheo2:4]{$4$} } \\ \label{predtheo2:6} $6$ & $((\neg \exists x(\neg R(x))\ \vee \ \neg R(y))\ \Rightarrow \ (\neg R(y)\ \vee \ \neg \exists 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 \exists 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 \exists 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$ & $(\forall y(R(y))\ \Rightarrow \ \neg \exists 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$ & $(\forall x(R(x))\ \Rightarrow \ \neg \exists 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$ } \\ \\ & & & \mbox{\qedhere} \end{longtable} \end{proof} The reverse is also true: \begin{thm} \hypertarget{predtheo3}{} \begin{displaymath} (\neg \exists x(\neg R(x))\ \Rightarrow \ \forall 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 \ \forall 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 \ \forall x(R(x)))\ \Rightarrow \ (\neg \forall x(R(x))\ \Rightarrow \ \neg R(y)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $\forall x(R(x))$ in \hyperref[predtheo3:5]{$5$} } \\ \label{predtheo3:7} $7$ & $(\neg \forall 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 \forall x(R(x))\ \Rightarrow \ \exists 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 \forall x(R(x))\ \Rightarrow \ B)\ \Rightarrow \ (\neg B\ \Rightarrow \ \neg \neg \forall x(R(x))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $A$ by $\neg \forall x(R(x))$ in \hyperref[predtheo3:4]{$4$} } \\ \label{predtheo3:10} $10$ & $((\neg \forall x(R(x))\ \Rightarrow \ \exists y(\neg R(y)))\ \Rightarrow \ (\neg \exists y(\neg R(y))\ \Rightarrow \ \neg \neg \forall x(R(x))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $\exists y(\neg R(y))$ in \hyperref[predtheo3:9]{$9$} } \\ \label{predtheo3:11} $11$ & $(\neg \exists y(\neg R(y))\ \Rightarrow \ \neg \neg \forall 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 \forall x(R(x))\ \Rightarrow \ \forall x(R(x)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $Q$ by $\forall 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 \forall x(R(x))\ \Rightarrow \ C)\ \Rightarrow \ ((D\ \vee \ \neg \neg \forall x(R(x)))\ \Rightarrow \ (D\ \vee \ C)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $\neg \neg \forall x(R(x))$ in \hyperref[predtheo3:20]{$20$} } \\ \label{predtheo3:22} $22$ & $((\neg \neg \forall x(R(x))\ \Rightarrow \ \forall x(R(x)))\ \Rightarrow \ ((D\ \vee \ \neg \neg \forall x(R(x)))\ \Rightarrow \ (D\ \vee \ \forall x(R(x)))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $\forall x(R(x))$ in \hyperref[predtheo3:21]{$21$} } \\ \label{predtheo3:23} $23$ & $((\neg \neg \forall x(R(x))\ \Rightarrow \ \forall x(R(x)))\ \Rightarrow \ ((\neg \neg \exists y(\neg R(y))\ \vee \ \neg \neg \forall x(R(x)))\ \Rightarrow \ (\neg \neg \exists y(\neg R(y))\ \vee \ \forall x(R(x)))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $\neg \neg \exists y(\neg R(y))$ in \hyperref[predtheo3:22]{$22$} } \\ \label{predtheo3:24} $24$ & $((\neg \neg \exists y(\neg R(y))\ \vee \ \neg \neg \forall x(R(x)))\ \Rightarrow \ (\neg \neg \exists y(\neg R(y))\ \vee \ \forall 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 \exists y(\neg R(y))\ \Rightarrow \ B)\ \Rightarrow \ (\neg \neg \exists y(\neg R(y))\ \vee \ B))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $A$ by $\neg \exists y(\neg R(y))$ in \hyperref[predtheo3:26]{$26$} } \\ \label{predtheo3:28} $28$ & $((\neg \exists y(\neg R(y))\ \Rightarrow \ \neg \neg \forall x(R(x)))\ \Rightarrow \ (\neg \neg \exists y(\neg R(y))\ \vee \ \neg \neg \forall x(R(x))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $\neg \neg \forall 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 \exists y(\neg R(y))\ \vee \ \neg \neg \forall x(R(x)))\ \Rightarrow \ C)\ \Rightarrow \ ((D\ \Rightarrow \ (\neg \neg \exists y(\neg R(y))\ \vee \ \neg \neg \forall x(R(x))))\ \Rightarrow \ (D\ \Rightarrow \ C)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $(\neg \neg \exists y(\neg R(y))\ \vee \ \neg \neg \forall x(R(x)))$ in \hyperref[predtheo3:32]{$32$} } \\ \label{predtheo3:34} $34$ & $(((\neg \neg \exists y(\neg R(y))\ \vee \ \neg \neg \forall x(R(x)))\ \Rightarrow \ (\neg \neg \exists y(\neg R(y))\ \vee \ \forall x(R(x))))\ \Rightarrow \ ((D\ \Rightarrow \ (\neg \neg \exists y(\neg R(y))\ \vee \ \neg \neg \forall x(R(x))))\ \Rightarrow \ (D\ \Rightarrow \ (\neg \neg \exists y(\neg R(y))\ \vee \ \forall x(R(x))))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $(\neg \neg \exists y(\neg R(y))\ \vee \ \forall x(R(x)))$ in \hyperref[predtheo3:33]{$33$} } \\ \label{predtheo3:35} $35$ & $(((\neg \neg \exists y(\neg R(y))\ \vee \ \neg \neg \forall x(R(x)))\ \Rightarrow \ (\neg \neg \exists y(\neg R(y))\ \vee \ \forall x(R(x))))\ \Rightarrow \ (((\neg \exists y(\neg R(y))\ \Rightarrow \ \neg \neg \forall x(R(x)))\ \Rightarrow \ (\neg \neg \exists y(\neg R(y))\ \vee \ \neg \neg \forall x(R(x))))\ \Rightarrow \ ((\neg \exists y(\neg R(y))\ \Rightarrow \ \neg \neg \forall x(R(x)))\ \Rightarrow \ (\neg \neg \exists y(\neg R(y))\ \vee \ \forall x(R(x))))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $(\neg \exists y(\neg R(y))\ \Rightarrow \ \neg \neg \forall x(R(x)))$ in \hyperref[predtheo3:34]{$34$} } \\ \label{predtheo3:36} $36$ & $(((\neg \exists y(\neg R(y))\ \Rightarrow \ \neg \neg \forall x(R(x)))\ \Rightarrow \ (\neg \neg \exists y(\neg R(y))\ \vee \ \neg \neg \forall x(R(x))))\ \Rightarrow \ ((\neg \exists y(\neg R(y))\ \Rightarrow \ \neg \neg \forall x(R(x)))\ \Rightarrow \ (\neg \neg \exists y(\neg R(y))\ \vee \ \forall 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 \exists y(\neg R(y))\ \Rightarrow \ \neg \neg \forall x(R(x)))\ \Rightarrow \ (\neg \neg \exists y(\neg R(y))\ \vee \ \forall 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 \exists y(\neg R(y))\ \vee \ B)\ \Rightarrow \ (\neg \exists y(\neg R(y))\ \Rightarrow \ B))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $A$ by $\neg \exists y(\neg R(y))$ in \hyperref[predtheo3:39]{$39$} } \\ \label{predtheo3:41} $41$ & $((\neg \neg \exists y(\neg R(y))\ \vee \ \forall x(R(x)))\ \Rightarrow \ (\neg \exists y(\neg R(y))\ \Rightarrow \ \forall x(R(x))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $\forall x(R(x))$ in \hyperref[predtheo3:40]{$40$} } \\ \label{predtheo3:42} $42$ & $(((\neg \neg \exists y(\neg R(y))\ \vee \ \forall x(R(x)))\ \Rightarrow \ C)\ \Rightarrow \ ((D\ \Rightarrow \ (\neg \neg \exists y(\neg R(y))\ \vee \ \forall x(R(x))))\ \Rightarrow \ (D\ \Rightarrow \ C)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $(\neg \neg \exists y(\neg R(y))\ \vee \ \forall x(R(x)))$ in \hyperref[predtheo3:32]{$32$} } \\ \label{predtheo3:43} $43$ & $(((\neg \neg \exists y(\neg R(y))\ \vee \ \forall x(R(x)))\ \Rightarrow \ (\neg \exists y(\neg R(y))\ \Rightarrow \ \forall x(R(x))))\ \Rightarrow \ ((D\ \Rightarrow \ (\neg \neg \exists y(\neg R(y))\ \vee \ \forall x(R(x))))\ \Rightarrow \ (D\ \Rightarrow \ (\neg \exists y(\neg R(y))\ \Rightarrow \ \forall x(R(x))))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $(\neg \exists y(\neg R(y))\ \Rightarrow \ \forall x(R(x)))$ in \hyperref[predtheo3:42]{$42$} } \\ \label{predtheo3:44} $44$ & $(((\neg \neg \exists y(\neg R(y))\ \vee \ \forall x(R(x)))\ \Rightarrow \ (\neg \exists y(\neg R(y))\ \Rightarrow \ \forall x(R(x))))\ \Rightarrow \ (((\neg \exists y(\neg R(y))\ \Rightarrow \ \neg \neg \forall x(R(x)))\ \Rightarrow \ (\neg \neg \exists y(\neg R(y))\ \vee \ \forall x(R(x))))\ \Rightarrow \ ((\neg \exists y(\neg R(y))\ \Rightarrow \ \neg \neg \forall x(R(x)))\ \Rightarrow \ (\neg \exists y(\neg R(y))\ \Rightarrow \ \forall x(R(x))))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $(\neg \exists y(\neg R(y))\ \Rightarrow \ \neg \neg \forall x(R(x)))$ in \hyperref[predtheo3:43]{$43$} } \\ \label{predtheo3:45} $45$ & $(((\neg \exists y(\neg R(y))\ \Rightarrow \ \neg \neg \forall x(R(x)))\ \Rightarrow \ (\neg \neg \exists y(\neg R(y))\ \vee \ \forall x(R(x))))\ \Rightarrow \ ((\neg \exists y(\neg R(y))\ \Rightarrow \ \neg \neg \forall x(R(x)))\ \Rightarrow \ (\neg \exists y(\neg R(y))\ \Rightarrow \ \forall 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 \exists y(\neg R(y))\ \Rightarrow \ \neg \neg \forall x(R(x)))\ \Rightarrow \ (\neg \exists y(\neg R(y))\ \Rightarrow \ \forall 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 \exists y(\neg R(y))\ \Rightarrow \ \forall 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 \exists x(\neg R(x))\ \Rightarrow \ \forall 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$ } \\ \\ & & & \mbox{\qedhere} \end{longtable} \end{proof} Exchange of universal quantors: \begin{thm} \hypertarget{predtheo4}{} \begin{displaymath} (\exists x(\exists y(R(x, y)))\ \Rightarrow \ \exists 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{predtheo4:1} $1$ & $(\exists 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$ & $(\exists 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$ & $(\exists 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$ & $(\exists 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$ & $(\exists 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$ & $(\exists 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$ & $(\exists 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$ & $(\exists 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$ & $(\exists 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$ & $(\exists 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$ & $(\exists v(\exists w(R(v, w)))\ \Rightarrow \ \exists w(R(z, w)))$ & {\tiny \hyperref{predaxiom_1.00.00_1.00.00.pdf}{}{predrule3}{replace} $R(@S_{1})$ by $\exists w(R(@S_{1}, w))$ in \hyperref[predtheo4:10]{$10$} } \\ \label{predtheo4:12} $12$ & $(\exists c(\exists w(R(c, w)))\ \Rightarrow \ \exists 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$ & $(\exists c(\exists d(R(c, d)))\ \Rightarrow \ \exists 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$ & $(\exists c(\exists d(R(c, d)))\ \Rightarrow \ \exists 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$ & $(\exists x(\exists d(R(x, d)))\ \Rightarrow \ \exists 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$ & $(\exists x(\exists y(R(x, y)))\ \Rightarrow \ \exists 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$ & $(\exists x(\exists y(R(x, y)))\ \Rightarrow \ \exists 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$ & $((\exists y(R(z, y))\ \Rightarrow \ D)\ \Rightarrow \ ((P_{7}\ \Rightarrow \ \exists y(R(z, y)))\ \Rightarrow \ (P_{7}\ \Rightarrow \ D)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $\exists y(R(z, y))$ in \hyperref[predtheo4:21]{$21$} } \\ \label{predtheo4:23} $23$ & $((\exists y(R(z, y))\ \Rightarrow \ R(z, u))\ \Rightarrow \ ((P_{7}\ \Rightarrow \ \exists 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$ & $((\exists y(R(z, y))\ \Rightarrow \ R(z, u))\ \Rightarrow \ ((\exists x(\exists y(R(x, y)))\ \Rightarrow \ \exists y(R(z, y)))\ \Rightarrow \ (\exists x(\exists y(R(x, y)))\ \Rightarrow \ R(z, u))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $P_{7}$ by $\exists x(\exists y(R(x, y)))$ in \hyperref[predtheo4:23]{$23$} } \\ \label{predtheo4:25} $25$ & $((\exists x(\exists y(R(x, y)))\ \Rightarrow \ \exists y(R(z, y)))\ \Rightarrow \ (\exists x(\exists 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$ & $(\exists x(\exists 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$ & $(\exists x(\exists y(R(x, y)))\ \Rightarrow \ \exists 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$ & $(\exists x(\exists y(R(x, y)))\ \Rightarrow \ \exists u(\exists 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$ & $(\exists x(\exists y(R(x, y)))\ \Rightarrow \ \exists y(\exists 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$ & $(\exists x(\exists y(R(x, y)))\ \Rightarrow \ \exists y(\exists 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$ } \\ \\ & & & \mbox{\qedhere} \end{longtable} \end{proof} Implication of changing seqence of existence and universal quantor: \begin{thm} \hypertarget{predtheo5}{} \begin{displaymath} (\forall x(\exists y(R(x, y)))\ \Rightarrow \ \exists 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{predtheo5:1} $1$ & $(\exists 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$ & $(\exists 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$ & $(\exists 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$ & $(\exists 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$ & $(\exists 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$ & $(\exists 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 \ \forall 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 \ \forall 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 \ \forall 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 \ \forall 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 \ \forall 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 \ \forall 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 \ \forall z(R(z, u)))\ \Rightarrow \ ((P_{7}\ \Rightarrow \ R(x, u))\ \Rightarrow \ (P_{7}\ \Rightarrow \ \forall z(R(z, u)))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $\forall z(R(z, u))$ in \hyperref[predtheo5:17]{$17$} } \\ \label{predtheo5:19} $19$ & $((R(x, u)\ \Rightarrow \ \forall z(R(z, u)))\ \Rightarrow \ ((\exists y(R(x, y))\ \Rightarrow \ R(x, u))\ \Rightarrow \ (\exists y(R(x, y))\ \Rightarrow \ \forall z(R(z, u)))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $P_{7}$ by $\exists y(R(x, y))$ in \hyperref[predtheo5:18]{$18$} } \\ \label{predtheo5:20} $20$ & $((\exists y(R(x, y))\ \Rightarrow \ R(x, u))\ \Rightarrow \ (\exists y(R(x, y))\ \Rightarrow \ \forall 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$ & $(\exists y(R(x, y))\ \Rightarrow \ \forall 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$ & $(\forall x(\exists y(R(x, y)))\ \Rightarrow \ \forall 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$ & $(\forall x(\exists y(R(x, y)))\ \Rightarrow \ \exists u(\forall 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$ & $(\forall x(\exists y(R(x, y)))\ \Rightarrow \ \exists c(\forall 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$ & $(\forall x(\exists y(R(x, y)))\ \Rightarrow \ \exists c(\forall 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$ & $(\forall x(\exists y(R(x, y)))\ \Rightarrow \ \exists y(\forall 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$ & $(\forall x(\exists y(R(x, y)))\ \Rightarrow \ \exists y(\forall 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$ } \\ \\ & & & \mbox{\qedhere} \end{longtable} \end{proof} \section*{} \end{document}