% -*- 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{propaxiom_1.00.00_1.00.00.qedeq} \hyperbaseurl{propaxiom_1.00.00_1.00.00.qedeq} \makeatother \setlength{\LTleft}{0pt} \setlength{\LTright}{0pt} \setlength{\parindent}{0pt} \frenchspacing \sloppy \pagestyle{headings} \title{Axioms of Propositional 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 the axioms of propositional calculus. These axioms (together with some rules) allow the deduction of all theorems of propositional 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: & propaxiom \\ Version: & 1.00.00 \\ Rule version: & 1.00.00 \\ Orgin: & \url{http://www.qedeq.org/0_00_53/propaxiom_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} We only need the logical disjunction (`or') and the negation (`not'). The other operands will be defined by them. (It would be possible to use only one operator: `sheffer's or' or `sheffer's and'.) At first we note an abbreviation that defines the implication: \begin{abr}[impl] \hypertarget{impl}{} \begin{displaymath} @F_{0}\ \rightarrow \ @F_{1} \equiv \neg @F_{0}\ \vee \ @F_{1}\end{displaymath} \end{abr} This means that we could transform a part formula that matches the pattern on the left side into the right side and we could transform a part formula that matches the pattern on the right side into the formula on the left side. \bigskip The logical conjunction (`and') could be defined with de Morgan: \begin{abr}[and] \hypertarget{and}{} \begin{displaymath} @F_{0}\ \wedge \ @F_{1} \equiv \neg (\neg @F_{0}\ \vee \ \neg @F_{1})\end{displaymath} \end{abr} This is still an abbreviation. \bigskip The logical equivalence is defined as usual: \begin{abr}[equi] \hypertarget{equi}{} \begin{displaymath} @F_{1}\ \leftrightarrow \ @F_{2} \equiv (@F_{1}\ \rightarrow \ @F_{2})\ \wedge \ (@F_{2}\ \rightarrow \ @F_{1})\end{displaymath} \end{abr} Now we come to the first axiom of propositional calculus. This axiom enables us to get rid of an unnecessary disjunction: \begin{axm}[axiom1] \hypertarget{axiom1}{} \begin{displaymath} (P\ \vee \ P)\ \rightarrow \ P\end{displaymath} \end{axm} This expresses the `idempotence' of the disjunction. \bigskip Axiom of weakening: \begin{axm}[axiom2] \hypertarget{axiom2}{} \begin{displaymath} P\ \rightarrow \ (P\ \vee \ Q)\end{displaymath} \end{axm} If a proposition is true, any alternative may be added without making it false. \bigskip The commutativity of the disjunction is expressed with the third axiom: \begin{axm}[axiom3] \hypertarget{axiom3}{} \begin{displaymath} (P\ \vee \ Q)\ \rightarrow \ (Q\ \vee \ P)\end{displaymath} \end{axm} The last axiom is: \begin{axm}[axiom4] \hypertarget{axiom4}{} \begin{displaymath} (P\ \rightarrow \ Q)\ \rightarrow \ ((A\ \vee \ P)\ \rightarrow \ (A\ \vee \ Q))\end{displaymath} \end{axm} \begin{dec}[rule1] modus ponens \hypertarget{rule1}{} \label{rule1} \end{dec} For an explanation see \href{http://www.qedeq.org/0_00_53/rules_1.00.00.html#modusponens}{modus ponens} or \href{http://www.qedeq.org/0_00_53/rules_1.00.00.o.html#modusponens}{modus ponens (o)} \bigskip \begin{dec}[rule2] add axiom \hypertarget{rule2}{} \label{rule2} \end{dec} For an explanation see \href{http://www.qedeq.org/0_00_53/rules_1.00.00.html#addaxiom}{add axiom} or \href{http://www.qedeq.org/0_00_53/rules_1.00.00.o.html#addaxiom}{add axiom (o)} \bigskip \begin{dec}[rule3] add sentence \hypertarget{rule3}{} \label{rule3} \end{dec} For an explanation see \href{http://www.qedeq.org/0_00_53/rules_1.00.00.html#addproposition}{add proposition} or \href{http://www.qedeq.org/0_00_53/rules_1.00.00.o.html#addproposition}{add proposition (o)} \bigskip \begin{dec}[rule4] replace proposition variable \hypertarget{rule4}{} \label{rule4} \end{dec} For an explanation see \href{http://www.qedeq.org/0_00_53/rules_1.00.00.html#replaceprop}{replace proposition Variable} or \href{http://www.qedeq.org/0_00_53/rules_1.00.00.o.html#replaceprop}{replace proposition variable (o)} \bigskip \begin{dec}[rule5] use abbreviation \hypertarget{rule5}{} \label{rule5} \end{dec} For an explanation see \href{http://www.qedeq.org/0_00_53/rules_1.00.00.html#useabbreviation}{use abbreviation} or \href{http://www.qedeq.org/0_00_53/rules_1.00.00.o.html#useabbreviation}{use abbreviation (o)} \bigskip \begin{dec}[rule6] reverse abbreviation \hypertarget{rule6}{} \label{rule6} \end{dec} For an explanation see \href{http://www.qedeq.org/0_00_53/rules_1.00.00.html#reverseabbreviation}{reverse abbreviation} or \href{http://www.qedeq.org/0_00_53/rules_1.00.00.o.html#reverseabbreviation}{reverse abbreviation (o)} \bigskip \section{Cross Reference} This module is used by the following modules: \begin{longtable}[h!]{l@{\extracolsep{\fill}}p{12cm}} Name: & proptheo1 \\ Version: & 1.00.00 \\ Rule version: & 1.00.00 \\ Orgin: & \url{proptheo1_1.00.00_1.00.00.qedeq} \\ pdf: & \url{proptheo1_1.00.00_1.00.00.pdf} \\ Name: & proptheo2 \\ Version: & 1.00.00 \\ Rule version: & 1.00.00 \\ Orgin: & \url{proptheo2_1.00.00_1.00.00.qedeq} \\ pdf: & \url{proptheo2_1.00.00_1.00.00.pdf} \\ 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: & prophilbert1 \\ Version: & 1.00.00 \\ Rule version: & 1.00.00 \\ Orgin: & \url{prophilbert1_1.00.00_1.00.00.qedeq} \\ pdf: & \url{prophilbert1_1.00.00_1.00.00.pdf} \\ Name: & subst \\ Version: & 1.00.00 \\ Rule version: & 1.01.00 \\ Orgin: & \url{subst_1.00.00_1.01.00.qedeq} \\ pdf: & \url{subst_1.00.00_1.01.00.pdf} \\ Name: & prophilbert1 \\ Version: & 1.00.00 \\ Rule version: & 1.02.00 \\ Orgin: & \url{prophilbert1_1.00.00_1.02.00.qedeq} \\ pdf: & \url{prophilbert1_1.00.00_1.02.00.pdf} \\ \end{longtable} \end{document}