% -*- TeX:EN -*- %%% ==================================================================== %%% $RCSfile: Module2Latex.java,v $ %%% $Revision: 1.28 $ %%% ==================================================================== %%% %%% Generated by class com.meyling.principia.latex.Module2Latex %%% at 2004-09-26T23:33:10+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{predaxiom_1.00.00_1.00.00.qedeq} \hyperbaseurl{predaxiom_1.00.00_1.00.00.qedeq} \makeatother \setlength{\LTleft}{0pt} \setlength{\LTright}{0pt} \setlength{\parindent}{0pt} \frenchspacing \sloppy \pagestyle{headings} \title{Axioms of Predicate Calculus} \author{Michael Meyling} \date{\tt } \begin{document} \maketitle \setlongtables {\small This document is part of the project ``Hilbert II''. To get more information about this project look at:\\ \mbox{\url{http://www.qedeq.org}}. Permission is granted to copy, distribute and/or modify this document under the terms of the GNU Free Documentation License, Version 1.2 or any later version published by the Free Software Foundation; with no Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts. See also under \url{http://www.gnu.org/copyleft/} } \section*{Abstract} This module contains the axioms of predicate calculus. The following quantification axioms and these of \href{propaxiom_1.00.00_1.00.00.html}{propositional calculus} (or \href{propaxiom_1.00.00_1.00.00.o.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 `Hilbert II' see \href{http://www.qedeq.org/}{project homepage}. \section*{Specification} This document has the following specification: \begin{longtable}[h!]{l@{\extracolsep{\fill}}p{12cm}} Name: & predaxiom \\ Version: & 1.00.00 \\ Rule version: & 1.00.00 \\ Orgin: & \url{http://www.qedeq.org/0_00_53/predaxiom_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*{Content} Axiom of Specialization: \begin{axm}[axiom5] \hypertarget{axiom5}{} \begin{displaymath} \forall x\, R(x)\ \rightarrow \ R(y)\end{displaymath} \end{axm} \begin{axm}[axiom6] \hypertarget{axiom6}{} \begin{displaymath} R(y)\ \rightarrow \ \exists x\, R(x)\end{displaymath} \end{axm} \begin{dec}[predrule1] Rename Bound Variable \hypertarget{predrule1}{} \label{predrule1} \end{dec} For an explanation see \href{http://www.qedeq.org/0_00_53/rules_1.00.00.html#renameboundvar}{rename bound variable} or \href{http://www.qedeq.org/0_00_53/rules_1.00.00.o.html#renameboundvar}{rename bound variable (o)} \bigskip \begin{dec}[predrule2] Rename Free Variable \hypertarget{predrule2}{} \label{predrule2} \end{dec} For an explanation see \href{http://www.qedeq.org/0_00_53/rules_1.00.00.html#renamefreevar}{rename free variable} or \href{http://www.qedeq.org/0_00_53/rules_1.00.00.html#renamefreevar}{rename free variable (o)} \bigskip \begin{dec}[predrule3] Particularize \hypertarget{predrule3}{} \label{predrule3} \end{dec} For an explanation see \href{http://www.qedeq.org/0_00_53/rules_1.00.00.html#replacepredicate}{rename predicate variable} or \href{http://www.qedeq.org/0_00_53/rules_1.00.00.o.html#replacepredicate}{rename predicate variable (o)} \bigskip \begin{dec}[predrule4] Particularize \hypertarget{predrule4}{} \label{predrule4} \end{dec} For an explanation see \href{http://www.qedeq.org/0_00_53/rules_1.00.00.html#particularization}{particularization} or \href{http://www.qedeq.org/0_00_53/rules_1.00.00.o.html#particularization}{particularization (o)} \bigskip \begin{dec}[predrule5] Generalize \hypertarget{predrule5}{} \label{predrule5} \end{dec} For an explanation see \href{http://www.qedeq.org/0_00_53/rules_1.00.00.html#generalization}{generalization} or \href{http://www.qedeq.org/0_00_53/rules_1.00.00.o.html#generalization}{generalization (o)} \bigskip \section{Cross Reference} This module is used by the following modules: \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}