% -*- 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{predtheo1_1.00.00_1.00.00.qedeq} \hyperbaseurl{predtheo1_1.00.00_1.00.00.qedeq} \makeatother \setlength{\LTleft}{0pt} \setlength{\LTright}{0pt} \setlength{\parindent}{0pt} \frenchspacing \sloppy \pagestyle{headings} \title{First theorems 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 includes first proofs of predicate calculus theorems. \section*{Specification} This document has the following specification: \begin{longtable}[h!]{l@{\extracolsep{\fill}}p{12cm}} Name: & predtheo1 \\ Version: & 1.00.00 \\ Rule version: & 1.00.00 \\ Orgin: & \url{http://www.qedeq.org/0_00_53/predtheo1_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: & propaxiom \\ Version: & 1.00.00 \\ Rule version: & 1.00.00 \\ Orgin: & \url{propaxiom_1.00.00_1.00.00.qedeq} \\ pdf: & \url{propaxiom_1.00.00_1.00.00.pdf} \\ 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} \\ \end{longtable} \section*{Content} First we prove a simple implication: \begin{thm}[theo1] \hypertarget{theo1}{} \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{theo1: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{theo1: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[theo1:1]{$1$} } \\ \label{theo1: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[theo1:2]{$2$} at occurence $1$ } \\ \label{theo1: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{theo1: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[theo1:4]{$4$} } \\ \label{theo1: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[theo1:5]{$5$} } \\ \label{theo1: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[theo1:3]{$3$}, \hyperref[theo1:6]{$6$}} \\ \label{theo1: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[theo1:7]{$7$} at occurence $1$ } \\ \label{theo1: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[theo1:8]{$8$}} \\ \label{theo1: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[theo1:9]{$9$} at occurence $1$ } \\ & & \qedhere \end{longtable} \end{proof} \end{document}