% -*- 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 <module@qedeq.org>}


\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}
