%%% ====================================================================
%%% @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.02.00.qedeq}
\hyperbaseurl{predtheo2_1.00.00_1.02.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.02.00 \\
Orgin: & \url{http://www.meyling.com/principia/0_00_51/predtheo2_1.00.00_1.02.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.02.00 \\
Orgin: & \url{prophilbert3_1.00.00_1.02.00.qedeq}  \\
pdf: & \url{prophilbert3_1.00.00_1.02.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$ & $(\exists x(R(x))\ \Rightarrow \  \forall x(R(x)))$
  & {\tiny \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{rule11}{HS} with \hyperref[predtheo1:1]{$1$} and \hyperref[predtheo1:2]{$2$}
} \\
\\ & & & \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$ & $(\neg \forall x(R(x))\ \Rightarrow \  \neg R(y))$
  & {\tiny \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{rule10}{apply} \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb7}{hilb7} in \hyperref[predtheo3:1]{$1$}
} \\
\label{predtheo3:3}
  $3$ & $(\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:2]{$2$}} \\
\label{predtheo3:4}
  $4$ & $(\neg \exists y(\neg R(y))\ \Rightarrow \  \neg \neg \forall x(R(x)))$
  & {\tiny \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{rule10}{apply} \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb7}{hilb7} in \hyperref[predtheo3:3]{$3$}
} \\
\label{predtheo3:5}
  $5$ & $(\neg \exists y(\neg R(y))\ \Rightarrow \  \forall x(R(x)))$
  & {\tiny \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{rule30}{elementary equivalence} in \hyperref[predtheo3:4]{$4$} at \hyperref[predtheo3:1]{$1$} of \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb6}{hilb6}  with \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb6}{hilb6} 
} \\
\label{predtheo3:6}
  $6$ & $(\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:5]{$5$} 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 y(R(y))\ \Rightarrow \  R(u))$
  & {\tiny \hyperref{subst_1.00.00_1.01.00.pdf}{}{rule8}{Substitute Variables} in \hyperref[predtheo4:1]{$1$}
} \\
\label{predtheo4:3}
  $3$ & $(\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:2]{$2$}
} \\
\label{predtheo4:4}
  $4$ & $(\exists v(R(v))\ \Rightarrow \  R(z))$
  & {\tiny \hyperref{subst_1.00.00_1.01.00.pdf}{}{rule8}{Substitute Variables} in \hyperref[predtheo4:1]{$1$}
} \\
\label{predtheo4:5}
  $5$ & $(\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:4]{$4$}
} \\
\label{predtheo4:6}
  $6$ & $(\exists x(\exists y(R(x, y)))\ \Rightarrow \  \exists y(R(z, y)))$
  & {\tiny \hyperref{subst_1.00.00_1.01.00.pdf}{}{rule8}{Substitute Variables} in \hyperref[predtheo4:5]{$5$}
} \\
\label{predtheo4:7}
  $7$ & $(\exists x(\exists y(R(x, y)))\ \Rightarrow \  R(z, u))$
  & {\tiny \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{rule11}{HS} with \hyperref[predtheo4:6]{$6$} and \hyperref[predtheo4:3]{$3$}
} \\
\label{predtheo4:8}
  $8$ & $(\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:7]{$7$}} \\
\label{predtheo4:9}
  $9$ & $(\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:8]{$8$}} \\
\label{predtheo4:10}
  $10$ & $(\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:9]{$9$} at occurence $1$
} \\
\label{predtheo4:11}
  $11$ & $(\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:10]{$10$} 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 y(R(y))\ \Rightarrow \  R(u))$
  & {\tiny \hyperref{subst_1.00.00_1.01.00.pdf}{}{rule8}{Substitute Variables} in \hyperref[predtheo5:1]{$1$}
} \\
\label{predtheo5:3}
  $3$ & $(\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:2]{$2$}
} \\
\label{predtheo5:4}
  $4$ & $(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:5}
  $5$ & $(R(x)\ \Rightarrow \  \forall z(R(z)))$
  & {\tiny \hyperref{subst_1.00.00_1.01.00.pdf}{}{rule8}{Substitute Variables} in \hyperref[predtheo5:4]{$4$}
} \\
\label{predtheo5:6}
  $6$ & $(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:5]{$5$}
} \\
\label{predtheo5:7}
  $7$ & $(\exists y(R(x, y))\ \Rightarrow \  \forall z(R(z, u)))$
  & {\tiny \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{rule11}{HS} with \hyperref[predtheo5:3]{$3$} and \hyperref[predtheo5:6]{$6$}
} \\
\label{predtheo5:8}
  $8$ & $(\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:7]{$7$}} \\
\label{predtheo5:9}
  $9$ & $(\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:8]{$8$}} \\
\label{predtheo5:10}
  $10$ & $(\forall x(\exists y(R(x, y)))\ \Rightarrow \  \exists y(\forall x(R(x, y))))$
  & {\tiny \hyperref{subst_1.00.00_1.01.00.pdf}{}{rule8}{Substitute Variables} in \hyperref[predtheo5:9]{$9$}
} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}

\section*{}

\end{document}