%%% ====================================================================
%%% @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{predaxiom_1.00.00_1.00.00.qedeq}
\hyperbaseurl{predaxiom_1.00.00_1.00.00.qedeq}
\makeatother

\setlength{\LTleft}{0pt}
\setlength{\LTright}{0pt}

\sloppy

\begin{document}

\title{Axioms of Predicate Calculus}
\author{Michael Meyling}
\email{principa@meyling.com}
\date{2002-07-27T20:56:02}

\begin{abstract}
This module contains the axioms of predicate calculus. The following quantification axioms and these of \href{propaxiom_1.00.00_1.00.00.html}{propositional calculus} (together with some rules) allow the deduction of all theorems of predicate calculus. To learn about possible conclusions click through the following `.. used by..' list. \par This file is part of the project `Principia Mathematica II' see \href{http://www.meyling.com/principia/principia.html}{project homepage}.
\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: & predaxiom \\
Version: & 1.00.00 \\
Rule version: & 1.00.00 \\
Orgin: & \url{http://www.meyling.com/principia/0_00_51/predaxiom_1.00.00_1.00.00.qedeq} \\
\end{longtable}


\medskip
Is used by the following modules:

\mbox{}
\begin{longtable}[h!]{l@{\extracolsep{\fill}}p{12cm}}
Name: & predtheo1 \\
Version: & 1.00.00 \\
Rule version: & 1.00.00 \\
Orgin: & \url{predtheo1_1.00.00_1.00.00.qedeq}  \\
pdf: & \url{predtheo1_1.00.00_1.00.00.pdf}  \\
Name: & predtheo2 \\
Version: & 1.00.00 \\
Rule version: & 1.00.00 \\
Orgin: & \url{predtheo2_1.00.00_1.00.00.qedeq}  \\
pdf: & \url{predtheo2_1.00.00_1.00.00.pdf}  \\
Name: & predtheo2 \\
Version: & 1.00.00 \\
Rule version: & 1.02.00 \\
Orgin: & \url{predtheo2_1.00.00_1.02.00.qedeq}  \\
pdf: & \url{predtheo2_1.00.00_1.02.00.pdf}  \\
\end{longtable}



Axiom of Specialization:




\begin{axm}
\hypertarget{axiom5}{}
\begin{displaymath}
(\exists x(R(x))\ \Rightarrow \  R(y))\end{displaymath}
\end{axm}



\begin{axm}
\hypertarget{axiom6}{}
\begin{displaymath}
(R(y)\ \Rightarrow \  \forall x(R(x)))\end{displaymath}
\end{axm}



\begin{dec}
Rename Bound Variable
\hypertarget{predrule1}{}
\label{predrule1}
\end{dec}



For an explanation see \href{rules_1.00.00.html#renameboundvariable}{rename bound variable}



\bigskip




\begin{dec}
Rename Free Variable
\hypertarget{predrule2}{}
\label{predrule2}
\end{dec}



For an explanation see \href{rules_1.00.00.html#renamefreevariable}{rename free variable}



\bigskip




\begin{dec}
Particularize
\hypertarget{predrule3}{}
\label{predrule3}
\end{dec}



For an explanation see \href{rules_1.00.00.html#replacepredicate}{rename predicate variable}



\bigskip




\begin{dec}
Particularize
\hypertarget{predrule4}{}
\label{predrule4}
\end{dec}



For an explanation see \href{rules_1.00.00.html#particularization}{particularization}



\bigskip




\begin{dec}
Generalize
\hypertarget{predrule5}{}
\label{predrule5}
\end{dec}



For an explanation see \href{rules_1.00.00.html#generalization}{generalization}



\bigskip


\section*{}
This module used by the following modules:

\mbox{}
\begin{longtable}[h!]{l@{\extracolsep{\fill}}p{12cm}}
Name: & predtheo1 \\
Version: & 1.00.00 \\
Rule version: & 1.00.00 \\
Orgin: & \url{predtheo1_1.00.00_1.00.00.qedeq}  \\
pdf: & \url{predtheo1_1.00.00_1.00.00.pdf}  \\
Name: & predtheo2 \\
Version: & 1.00.00 \\
Rule version: & 1.00.00 \\
Orgin: & \url{predtheo2_1.00.00_1.00.00.qedeq}  \\
pdf: & \url{predtheo2_1.00.00_1.00.00.pdf}  \\
Name: & predtheo2 \\
Version: & 1.00.00 \\
Rule version: & 1.02.00 \\
Orgin: & \url{predtheo2_1.00.00_1.02.00.qedeq}  \\
pdf: & \url{predtheo2_1.00.00_1.02.00.pdf}  \\
\end{longtable}

\end{document}