% -*- TeX:EN -*-
%%% ====================================================================
%%% $RCSfile: Module2Latex.java,v $
%%% $Revision: 1.28 $
%%% ====================================================================
%%%
%%% Generated by class com.meyling.principia.latex.Module2Latex
%%% at 2004-09-26T23:33:09+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{prophilbert1_1.00.00_1.02.00.qedeq}
\hyperbaseurl{prophilbert1_1.00.00_1.02.00.qedeq}
\makeatother

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

\setlength{\parindent}{0pt}
\frenchspacing \sloppy
\pagestyle{headings}

\title{First theorems of Propositional Calculus}
\author{Michael Meyling}
\date{\tt <module@qedeq.org>}


\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 proofs of popositional calculus theorems. The following theorems and proofs are adapted from D. Hilbert and W. Ackermann's `Grundzuege der theoretischen Logik' (Berlin 1928, Springer)


\section*{Specification}

This document has the following specification:

\begin{longtable}[h!]{l@{\extracolsep{\fill}}p{12cm}}
Name: & prophilbert1 \\
Version: & 1.00.00 \\
Rule version: & 1.02.00 \\
Orgin: & \url{http://www.qedeq.org/0_00_53/prophilbert1_1.00.00_1.02.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: & 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}  \\
\end{longtable}


\section*{Content}




Now we could declare the rule {\it Apply Axiom}.
      \par
      parameters: \par
      \begin{tabular}{ll}
      $p$ & proof line number \\
      $\langle$link$\rangle$ & axiom reference \\
      \end{tabular}
      \par
      If the proof line $n$ has the form `$p$' and an axiom {\it ref} matches the form `$(p\ \rightarrow \ q)$'  (p, q be formulas), then the string `$q$' could be added as a new proof line.
      \par
      For example: from proof line `$(r\ \vee \ s)$' we derive `$(r\ \vee \ s)$' by applying axiom 3.
      \par




\begin{dec}[rule9]
Apply Axiom
\hypertarget{rule9}{}
\label{rule9}
\end{dec}




Analogous to the preceding we declare the rule {\it Apply Sentence}.




\begin{dec}[rule10]
Apply Sentence
\hypertarget{rule10}{}
\label{rule10}
\end{dec}




First we prove a simple implication, that follows directly from the fourth axiom:




\begin{thm}[hilb1]
\hypertarget{hilb1}{}
\begin{displaymath}
(P\ \rightarrow \  Q)\ \rightarrow \  ((A\ \rightarrow \  P)\ \rightarrow \  (A\ \rightarrow \  Q))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb1:1}
  $1$ & $(P\ \rightarrow \  Q)\ \rightarrow \  ((A\ \vee \  P)\ \rightarrow \  (A\ \vee \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom4}{axiom4} } \\
\label{hilb1:2}
  $2$ & $(P\ \rightarrow \  Q)\ \rightarrow \  ((\neg A\ \vee \  P)\ \rightarrow \  (\neg A\ \vee \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $\neg A$ in \hyperref[hilb1:1]{$1$}
} \\
\label{hilb1:3}
  $3$ & $(P\ \rightarrow \  Q)\ \rightarrow \  ((A\ \rightarrow \  P)\ \rightarrow \  (\neg A\ \vee \  Q))$
  & {\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[hilb1:2]{$2$} at occurence $1$
} \\
\label{hilb1:4}
  $4$ & $(P\ \rightarrow \  Q)\ \rightarrow \  ((A\ \rightarrow \  P)\ \rightarrow \  (A\ \rightarrow \  Q))$
  & {\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[hilb1:3]{$3$} at occurence $1$
} \\
 & & \qedhere
\end{longtable}
\end{proof}


This proposition is the form for the Hypothetical Syllogism.



\bigskip




Now we could declare the rule {\it Hypothetical Syllogism}.
      \par
      parameters: \par
      \begin{tabular}{ll}
      $p$ & proof line number \\
      $m$ & proof line number \\
      \end{tabular}
      \par
      If the proof line $n$ has the form `$(p\ \rightarrow \ q)$'; and the proof line $m$ has the form `$(q\ \rightarrow \ r)$'  (p, q and r must be formulas), then the string `$(p\ \rightarrow \ s)$' could be added as a new proof line.
      \par




\begin{dec}[rule11]
Hypothetical Syllogism
\hypertarget{rule11}{}
\label{rule11}
\end{dec}


{\it References, needed for declaration:}


\hyperref{}{}{hilb1}{hilb1} 




The self implication could be derived:




\begin{thm}[hilb2]
\hypertarget{hilb2}{}
\begin{displaymath}
P\ \rightarrow \  P\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb2:1}
  $1$ & $P\ \rightarrow \  (P\ \vee \  Q)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom2}{axiom2} } \\
\label{hilb2:2}
  $2$ & $P\ \rightarrow \  (P\ \vee \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $P$ in \hyperref[hilb2:1]{$1$}
} \\
\label{hilb2:3}
  $3$ & $(P\ \vee \  P)\ \rightarrow \  P$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom1}{axiom1} } \\
\label{hilb2:4}
  $4$ & $P\ \rightarrow \  P$
  & {\tiny \hyperref{}{}{rule11}{HS} with \hyperref[hilb2:2]{$2$} and \hyperref[hilb2:3]{$3$}
} \\
 & & \qedhere
\end{longtable}
\end{proof}



One form of the classical {\bf tertium non datur}




\begin{thm}[hilb3]
\hypertarget{hilb3}{}
\begin{displaymath}
\neg P\ \vee \  P\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb3:1}
  $1$ & $P\ \rightarrow \  P$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb2}{hilb2} } \\
\label{hilb3:2}
  $2$ & $\neg P\ \vee \  P$
  & {\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[hilb3:1]{$1$} at occurence $1$
} \\
 & & \qedhere
\end{longtable}
\end{proof}



The standard form of the excluded middle:




\begin{thm}[hilb4]
\hypertarget{hilb4}{}
\begin{displaymath}
P\ \vee \  \neg P\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb4:1}
  $1$ & $\neg P\ \vee \  P$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb3}{hilb3} } \\
\label{hilb4:2}
  $2$ & $P\ \vee \  \neg P$
  & {\tiny \hyperref{}{}{rule9}{apply} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom3}{axiom3} in \hyperref[hilb4:1]{$1$}
} \\
 & & \qedhere
\end{longtable}
\end{proof}



Double negation is implicated:




\begin{thm}[hilb5]
\hypertarget{hilb5}{}
\begin{displaymath}
P\ \rightarrow \  \neg \neg P\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb5:1}
  $1$ & $P\ \vee \  \neg P$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb4}{hilb4} } \\
\label{hilb5:2}
  $2$ & $\neg P\ \vee \  \neg \neg P$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $\neg P$ in \hyperref[hilb5:1]{$1$}
} \\
\label{hilb5:3}
  $3$ & $P\ \rightarrow \  \neg \neg P$
  & {\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[hilb5:2]{$2$} at occurence $1$
} \\
 & & \qedhere
\end{longtable}
\end{proof}



The reverse is also true:




\begin{thm}[hilb6]
\hypertarget{hilb6}{}
\begin{displaymath}
\neg \neg P\ \rightarrow \  P\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb6:1}
  $1$ & $P\ \rightarrow \  \neg \neg P$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb5}{hilb5} } \\
\label{hilb6:2}
  $2$ & $\neg P\ \rightarrow \  \neg \neg \neg P$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $\neg P$ in \hyperref[hilb6:1]{$1$}
} \\
\label{hilb6:3}
  $3$ & $(P\ \vee \  \neg P)\ \rightarrow \  (P\ \vee \  \neg \neg \neg P)$
  & {\tiny \hyperref{}{}{rule9}{apply} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom4}{axiom4} in \hyperref[hilb6:2]{$2$}
} \\
\label{hilb6:4}
  $4$ & $P\ \vee \  \neg P$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb4}{hilb4} } \\
\label{hilb6:5}
  $5$ & $P\ \vee \  \neg \neg \neg P$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb6:4]{$4$}, \hyperref[hilb6:3]{$3$}} \\
\label{hilb6:6}
  $6$ & $\neg \neg \neg P\ \vee \  P$
  & {\tiny \hyperref{}{}{rule9}{apply} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom3}{axiom3} in \hyperref[hilb6:5]{$5$}
} \\
\label{hilb6:7}
  $7$ & $\neg \neg P\ \rightarrow \  P$
  & {\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[hilb6:6]{$6$} at occurence $1$
} \\
 & & \qedhere
\end{longtable}
\end{proof}



The correct reverse of an implication:




\begin{thm}[hilb7]
\hypertarget{hilb7}{}
\begin{displaymath}
(P\ \rightarrow \  Q)\ \rightarrow \  (\neg Q\ \rightarrow \  \neg P)\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb7:1}
  $1$ & $P\ \rightarrow \  \neg \neg P$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb5}{hilb5} } \\
\label{hilb7:2}
  $2$ & $Q\ \rightarrow \  \neg \neg Q$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $Q$ in \hyperref[hilb7:1]{$1$}
} \\
\label{hilb7:3}
  $3$ & $(\neg P\ \vee \  Q)\ \rightarrow \  (\neg P\ \vee \  \neg \neg Q)$
  & {\tiny \hyperref{}{}{rule9}{apply} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom4}{axiom4} in \hyperref[hilb7:2]{$2$}
} \\
\label{hilb7: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{hilb7:5}
  $5$ & $(\neg P\ \vee \  \neg \neg Q)\ \rightarrow \  (\neg \neg Q\ \vee \  \neg P)$
  & {\tiny \hyperref{subst_1.00.00_1.01.00.pdf}{}{rule8}{Substitute Variables} in \hyperref[hilb7:4]{$4$}
} \\
\label{hilb7:6}
  $6$ & $(\neg P\ \vee \  Q)\ \rightarrow \  (\neg \neg Q\ \vee \  \neg P)$
  & {\tiny \hyperref{}{}{rule11}{HS} with \hyperref[hilb7:3]{$3$} and \hyperref[hilb7:5]{$5$}
} \\
\label{hilb7:7}
  $7$ & $(P\ \rightarrow \  Q)\ \rightarrow \  (\neg \neg Q\ \vee \  \neg P)$
  & {\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[hilb7:6]{$6$} at occurence $1$
} \\
\label{hilb7:8}
  $8$ & $(P\ \rightarrow \  Q)\ \rightarrow \  (\neg Q\ \rightarrow \  \neg P)$
  & {\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[hilb7:7]{$7$} at occurence $1$
} \\
 & & \qedhere
\end{longtable}
\end{proof}



\begin{dec}[rule12]
Correct reverse of an implication
\hypertarget{rule12}{}
\label{rule12}
\end{dec}


{\it References, needed for declaration:}


\hyperref{}{}{hilb7}{hilb7} 




\begin{dec}[rule13]
Add a Conjunction on the Left
\hypertarget{rule13}{}
\label{rule13}
\end{dec}


{\it References, needed for declaration:}


\hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom4}{axiom4} 




\begin{dec}[rule14]
Add a Conjunction on the Right
\hypertarget{rule14}{}
\label{rule14}
\end{dec}


{\it References, needed for declaration:}


\hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom3}{axiom3} 
, \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom4}{axiom4} 




Definition of an Implication 1. part:




\begin{thm}[defimpl1]
\hypertarget{defimpl1}{}
\begin{displaymath}
(P\ \rightarrow \  Q)\ \rightarrow \  (\neg P\ \vee \  Q)\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{defimpl1:1}
  $1$ & $P\ \rightarrow \  P$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb2}{hilb2} } \\
\label{defimpl1:2}
  $2$ & $(P\ \rightarrow \  Q)\ \rightarrow \  (P\ \rightarrow \  Q)$
  & {\tiny \hyperref{subst_1.00.00_1.01.00.pdf}{}{rule8}{Substitute Variables} in \hyperref[defimpl1:1]{$1$}
} \\
\label{defimpl1:3}
  $3$ & $(P\ \rightarrow \  Q)\ \rightarrow \  (\neg P\ \vee \  Q)$
  & {\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[defimpl1:2]{$2$} at occurence $3$
} \\
 & & \qedhere
\end{longtable}
\end{proof}



Definition of an Implication 2. part:




\begin{thm}[defimpl2]
\hypertarget{defimpl2}{}
\begin{displaymath}
(\neg P\ \vee \  Q)\ \rightarrow \  (P\ \rightarrow \  Q)\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{defimpl2:1}
  $1$ & $P\ \rightarrow \  P$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb2}{hilb2} } \\
\label{defimpl2:2}
  $2$ & $(P\ \rightarrow \  Q)\ \rightarrow \  (P\ \rightarrow \  Q)$
  & {\tiny \hyperref{subst_1.00.00_1.01.00.pdf}{}{rule8}{Substitute Variables} in \hyperref[defimpl2:1]{$1$}
} \\
\label{defimpl2:3}
  $3$ & $(\neg P\ \vee \  Q)\ \rightarrow \  (P\ \rightarrow \  Q)$
  & {\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[defimpl2:2]{$2$} at occurence $2$
} \\
 & & \qedhere
\end{longtable}
\end{proof}



\begin{dec}[rule17]
Addition of an Implication on the Right
\hypertarget{rule17}{}
\label{rule17}
\end{dec}


{\it References, needed for declaration:}


\hyperref{}{}{defimpl1}{defimpl1} 
, \hyperref{}{}{defimpl2}{defimpl2} 




\begin{dec}[rule18]
Addition of an Implication on the Left
\hypertarget{rule18}{}
\label{rule18}
\end{dec}


{\it References, needed for declaration:}


\hyperref{}{}{defimpl1}{defimpl1} 
, \hyperref{}{}{defimpl2}{defimpl2} 




Definition of a Conjunction 1. part:




\begin{thm}[defand1]
\hypertarget{defand1}{}
\begin{displaymath}
(P\ \wedge \  Q)\ \rightarrow \  \neg (\neg P\ \vee \  \neg Q)\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{defand1:1}
  $1$ & $P\ \rightarrow \  P$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb2}{hilb2} } \\
\label{defand1:2}
  $2$ & $(P\ \wedge \  Q)\ \rightarrow \  (P\ \wedge \  Q)$
  & {\tiny \hyperref{subst_1.00.00_1.01.00.pdf}{}{rule8}{Substitute Variables} in \hyperref[defand1:1]{$1$}
} \\
\label{defand1:3}
  $3$ & $(P\ \wedge \  Q)\ \rightarrow \  \neg (\neg P\ \vee \  \neg Q)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule5}{use abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{and}{and} in \hyperref[defand1:2]{$2$} at occurence $2$
} \\
 & & \qedhere
\end{longtable}
\end{proof}



Definition of a Conjunction 2. part:




\begin{thm}[defand2]
\hypertarget{defand2}{}
\begin{displaymath}
\neg (\neg P\ \vee \  \neg Q)\ \rightarrow \  (P\ \wedge \  Q)\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{defand2:1}
  $1$ & $P\ \rightarrow \  P$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb2}{hilb2} } \\
\label{defand2:2}
  $2$ & $(P\ \wedge \  Q)\ \rightarrow \  (P\ \wedge \  Q)$
  & {\tiny \hyperref{subst_1.00.00_1.01.00.pdf}{}{rule8}{Substitute Variables} in \hyperref[defand2:1]{$1$}
} \\
\label{defand2:3}
  $3$ & $\neg (\neg P\ \vee \  \neg Q)\ \rightarrow \  (P\ \wedge \  Q)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule5}{use abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{and}{and} in \hyperref[defand2:2]{$2$} at occurence $1$
} \\
 & & \qedhere
\end{longtable}
\end{proof}



\begin{dec}[rule19]
Addition of a Conjunction on the Left
\hypertarget{rule19}{}
\label{rule19}
\end{dec}


{\it References, needed for declaration:}


\hyperref{}{}{defand1}{defand1} 
, \hyperref{}{}{defand2}{defand2} 




\begin{dec}[rule20]
Addition of a Conjunction on the Right
\hypertarget{rule20}{}
\label{rule20}
\end{dec}


{\it References, needed for declaration:}


\hyperref{}{}{defand1}{defand1} 
, \hyperref{}{}{defand2}{defand2} 




Definition of an Equivalence 1. part:




\begin{thm}[defequi1]
\hypertarget{defequi1}{}
\begin{displaymath}
(P\ \leftrightarrow \  Q)\ \rightarrow \  ((P\ \rightarrow \  Q)\ \wedge \  (Q\ \rightarrow \  P))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{defequi1:1}
  $1$ & $P\ \rightarrow \  P$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb2}{hilb2} } \\
\label{defequi1:2}
  $2$ & $(P\ \leftrightarrow \  Q)\ \rightarrow \  (P\ \leftrightarrow \  Q)$
  & {\tiny \hyperref{subst_1.00.00_1.01.00.pdf}{}{rule8}{Substitute Variables} in \hyperref[defequi1:1]{$1$}
} \\
\label{defequi1:3}
  $3$ & $(P\ \leftrightarrow \  Q)\ \rightarrow \  ((P\ \rightarrow \  Q)\ \wedge \  (Q\ \rightarrow \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule5}{use abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{equi}{equi} in \hyperref[defequi1:2]{$2$} at occurence $2$
} \\
 & & \qedhere
\end{longtable}
\end{proof}



Definition of an Equivalence 2. part:




\begin{thm}[defequi2]
\hypertarget{defequi2}{}
\begin{displaymath}
((P\ \rightarrow \  Q)\ \wedge \  (Q\ \rightarrow \  P))\ \rightarrow \  (P\ \leftrightarrow \  Q)\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{defequi2:1}
  $1$ & $P\ \rightarrow \  P$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb2}{hilb2} } \\
\label{defequi2:2}
  $2$ & $(P\ \leftrightarrow \  Q)\ \rightarrow \  (P\ \leftrightarrow \  Q)$
  & {\tiny \hyperref{subst_1.00.00_1.01.00.pdf}{}{rule8}{Substitute Variables} in \hyperref[defequi2:1]{$1$}
} \\
\label{defequi2:3}
  $3$ & $((P\ \rightarrow \  Q)\ \wedge \  (Q\ \rightarrow \  P))\ \rightarrow \  (P\ \leftrightarrow \  Q)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule5}{use abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{equi}{equi} in \hyperref[defequi2:2]{$2$} at occurence $1$
} \\
 & & \qedhere
\end{longtable}
\end{proof}



\begin{dec}[rule21]
Addition of an Equivalence on the Left
\hypertarget{rule21}{}
\label{rule21}
\end{dec}


{\it References, needed for declaration:}


\hyperref{}{}{defequi1}{defequi1} 
, \hyperref{}{}{defequi2}{defequi2} 




\begin{dec}[rule22]
Addition of an Equivalence on the Right
\hypertarget{rule22}{}
\label{rule22}
\end{dec}


{\it References, needed for declaration:}


\hyperref{}{}{defequi1}{defequi1} 
, \hyperref{}{}{defequi2}{defequi2} 




\begin{dec}[rule30]
Elementary equivalence of two formulas
\hypertarget{rule30}{}
\label{rule30}
\end{dec}




A simular formulation for the second axiom:




\begin{thm}[hilb8]
\hypertarget{hilb8}{}
\begin{displaymath}
P\ \rightarrow \  (Q\ \vee \  P)\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb8:1}
  $1$ & $P\ \rightarrow \  (P\ \vee \  Q)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom2}{axiom2} } \\
\label{hilb8:2}
  $2$ & $(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{hilb8:3}
  $3$ & $P\ \rightarrow \  (Q\ \vee \  P)$
  & {\tiny \hyperref{}{}{rule11}{HS} with \hyperref[hilb8:1]{$1$} and \hyperref[hilb8:2]{$2$}
} \\
 & & \qedhere
\end{longtable}
\end{proof}



A technical lemma (equal to the third axiom):




\begin{thm}[hilb9]
\hypertarget{hilb9}{}
\begin{displaymath}
(P\ \vee \  Q)\ \rightarrow \  (Q\ \vee \  P)\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb9:1}
  $1$ & $(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} } \\
 & & \qedhere
\end{longtable}
\end{proof}



And another technical lemma (simular to the third axiom):




\begin{thm}[hilb10]
\hypertarget{hilb10}{}
\begin{displaymath}
(Q\ \vee \  P)\ \rightarrow \  (P\ \vee \  Q)\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb10:1}
  $1$ & $(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{hilb10:2}
  $2$ & $(Q\ \vee \  P)\ \rightarrow \  (P\ \vee \  Q)$
  & {\tiny \hyperref{subst_1.00.00_1.01.00.pdf}{}{rule8}{Substitute Variables} in \hyperref[hilb10:1]{$1$}
} \\
 & & \qedhere
\end{longtable}
\end{proof}



A technical lemma (equal to the first axiom):




\begin{thm}[hilb11]
\hypertarget{hilb11}{}
\begin{displaymath}
(P\ \vee \  P)\ \rightarrow \  P\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb11:1}
  $1$ & $(P\ \vee \  P)\ \rightarrow \  P$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom1}{axiom1} } \\
 & & \qedhere
\end{longtable}
\end{proof}



A simple propositon that follows directly from the second axiom:




\begin{thm}[hilb12]
\hypertarget{hilb12}{}
\begin{displaymath}
P\ \rightarrow \  (P\ \vee \  P)\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb12:1}
  $1$ & $P\ \rightarrow \  (P\ \vee \  Q)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom2}{axiom2} } \\
\label{hilb12:2}
  $2$ & $P\ \rightarrow \  (P\ \vee \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $P$ in \hyperref[hilb12:1]{$1$}
} \\
 & & \qedhere
\end{longtable}
\end{proof}



This is a pre form for the associative law:




\begin{thm}[hilb13]
\hypertarget{hilb13}{}
\begin{displaymath}
(P\ \vee \  (Q\ \vee \  A))\ \rightarrow \  (Q\ \vee \  (P\ \vee \  A))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb13:1}
  $1$ & $P\ \rightarrow \  (Q\ \vee \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb8}{hilb8} } \\
\label{hilb13:2}
  $2$ & $A\ \rightarrow \  (P\ \vee \  A)$
  & {\tiny \hyperref{subst_1.00.00_1.01.00.pdf}{}{rule8}{Substitute Variables} in \hyperref[hilb13:1]{$1$}
} \\
\label{hilb13:3}
  $3$ & $(Q\ \vee \  A)\ \rightarrow \  (Q\ \vee \  (P\ \vee \  A))$
  & {\tiny \hyperref{}{}{rule9}{apply} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom4}{axiom4} in \hyperref[hilb13:2]{$2$}
} \\
\label{hilb13:4}
  $4$ & $(P\ \vee \  (Q\ \vee \  A))\ \rightarrow \  (P\ \vee \  (Q\ \vee \  (P\ \vee \  A)))$
  & {\tiny \hyperref{}{}{rule9}{apply} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom4}{axiom4} in \hyperref[hilb13:3]{$3$}
} \\
\label{hilb13:5}
  $5$ & $(P\ \vee \  (Q\ \vee \  A))\ \rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)$
  & {\tiny \hyperref{}{}{rule30}{elementary equivalence} in \hyperref[hilb13:4]{$4$} at \hyperref[hilb13:3]{$3$} of \hyperref{}{}{hilb9}{hilb9}  with \hyperref{}{}{hilb9}{hilb9} 
} \\
\label{hilb13:6}
  $6$ & $(P\ \vee \  A)\ \rightarrow \  (Q\ \vee \  (P\ \vee \  A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $P\ \vee \  A$ in \hyperref[hilb13:1]{$1$}
} \\
\label{hilb13:7}
  $7$ & $P\ \rightarrow \  (P\ \vee \  Q)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom2}{axiom2} } \\
\label{hilb13:8}
  $8$ & $P\ \rightarrow \  (P\ \vee \  A)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $A$ in \hyperref[hilb13:7]{$7$}
} \\
\label{hilb13:9}
  $9$ & $P\ \rightarrow \  (Q\ \vee \  (P\ \vee \  A))$
  & {\tiny \hyperref{}{}{rule11}{HS} with \hyperref[hilb13:8]{$8$} and \hyperref[hilb13:6]{$6$}
} \\
\label{hilb13:10}
  $10$ & $((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A)))$
  & {\tiny \hyperref{}{}{rule9}{apply} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom4}{axiom4} in \hyperref[hilb13:9]{$9$}
} \\
\label{hilb13:11}
  $11$ & $((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \rightarrow \  (Q\ \vee \  (P\ \vee \  A))$
  & {\tiny \hyperref{}{}{rule30}{elementary equivalence} in \hyperref[hilb13:10]{$10$} at \hyperref[hilb13:1]{$1$} of \hyperref{}{}{hilb11}{hilb11}  with \hyperref{}{}{hilb11}{hilb11} 
} \\
\label{hilb13:12}
  $12$ & $(P\ \vee \  (Q\ \vee \  A))\ \rightarrow \  (Q\ \vee \  (P\ \vee \  A))$
  & {\tiny \hyperref{}{}{rule11}{HS} with \hyperref[hilb13:5]{$5$} and \hyperref[hilb13:11]{$11$}
} \\
 & & \qedhere
\end{longtable}
\end{proof}



The associative law for the disjunction (first direction):




\begin{thm}[hilb14]
\hypertarget{hilb14}{}
\begin{displaymath}
(P\ \vee \  (Q\ \vee \  A))\ \rightarrow \  ((P\ \vee \  Q)\ \vee \  A)\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb14:1}
  $1$ & $P\ \rightarrow \  P$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb2}{hilb2} } \\
\label{hilb14:2}
  $2$ & $(P\ \vee \  (Q\ \vee \  A))\ \rightarrow \  (P\ \vee \  (Q\ \vee \  A))$
  & {\tiny \hyperref{subst_1.00.00_1.01.00.pdf}{}{rule8}{Substitute Variables} in \hyperref[hilb14:1]{$1$}
} \\
\label{hilb14:3}
  $3$ & $(P\ \vee \  (Q\ \vee \  A))\ \rightarrow \  (P\ \vee \  (A\ \vee \  Q))$
  & {\tiny \hyperref{}{}{rule30}{elementary equivalence} in \hyperref[hilb14:2]{$2$} at \hyperref[hilb14:4]{$4$} of \hyperref{}{}{hilb9}{hilb9}  with \hyperref{}{}{hilb9}{hilb9} 
} \\
\label{hilb14:4}
  $4$ & $(P\ \vee \  (Q\ \vee \  A))\ \rightarrow \  (Q\ \vee \  (P\ \vee \  A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb13}{hilb13} } \\
\label{hilb14:5}
  $5$ & $(P\ \vee \  (A\ \vee \  Q))\ \rightarrow \  (A\ \vee \  (P\ \vee \  Q))$
  & {\tiny \hyperref{subst_1.00.00_1.01.00.pdf}{}{rule8}{Substitute Variables} in \hyperref[hilb14:4]{$4$}
} \\
\label{hilb14:6}
  $6$ & $(P\ \vee \  (Q\ \vee \  A))\ \rightarrow \  (A\ \vee \  (P\ \vee \  Q))$
  & {\tiny \hyperref{}{}{rule11}{HS} with \hyperref[hilb14:3]{$3$} and \hyperref[hilb14:5]{$5$}
} \\
\label{hilb14:7}
  $7$ & $(P\ \vee \  (Q\ \vee \  A))\ \rightarrow \  ((P\ \vee \  Q)\ \vee \  A)$
  & {\tiny \hyperref{}{}{rule30}{elementary equivalence} in \hyperref[hilb14:6]{$6$} at \hyperref[hilb14:3]{$3$} of \hyperref{}{}{hilb9}{hilb9}  with \hyperref{}{}{hilb9}{hilb9} 
} \\
 & & \qedhere
\end{longtable}
\end{proof}



The associative law for the disjunction (second direction):




\begin{thm}[hilb15]
\hypertarget{hilb15}{}
\begin{displaymath}
((P\ \vee \  Q)\ \vee \  A)\ \rightarrow \  (P\ \vee \  (Q\ \vee \  A))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb15:1}
  $1$ & $(P\ \vee \  (Q\ \vee \  A))\ \rightarrow \  ((P\ \vee \  Q)\ \vee \  A)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb14}{hilb14} } \\
\label{hilb15:2}
  $2$ & $(A\ \vee \  (Q\ \vee \  P))\ \rightarrow \  ((A\ \vee \  Q)\ \vee \  P)$
  & {\tiny \hyperref{subst_1.00.00_1.01.00.pdf}{}{rule8}{Substitute Variables} in \hyperref[hilb15:1]{$1$}
} \\
\label{hilb15:3}
  $3$ & $((Q\ \vee \  P)\ \vee \  A)\ \rightarrow \  ((A\ \vee \  Q)\ \vee \  P)$
  & {\tiny \hyperref{}{}{rule30}{elementary equivalence} in \hyperref[hilb15:2]{$2$} at \hyperref[hilb15:1]{$1$} of \hyperref{}{}{hilb9}{hilb9}  with \hyperref{}{}{hilb9}{hilb9} 
} \\
\label{hilb15:4}
  $4$ & $((P\ \vee \  Q)\ \vee \  A)\ \rightarrow \  ((A\ \vee \  Q)\ \vee \  P)$
  & {\tiny \hyperref{}{}{rule30}{elementary equivalence} in \hyperref[hilb15:3]{$3$} at \hyperref[hilb15:2]{$2$} of \hyperref{}{}{hilb9}{hilb9}  with \hyperref{}{}{hilb9}{hilb9} 
} \\
\label{hilb15:5}
  $5$ & $((P\ \vee \  Q)\ \vee \  A)\ \rightarrow \  (P\ \vee \  (A\ \vee \  Q))$
  & {\tiny \hyperref{}{}{rule30}{elementary equivalence} in \hyperref[hilb15:4]{$4$} at \hyperref[hilb15:3]{$3$} of \hyperref{}{}{hilb9}{hilb9}  with \hyperref{}{}{hilb9}{hilb9} 
} \\
\label{hilb15:6}
  $6$ & $((P\ \vee \  Q)\ \vee \  A)\ \rightarrow \  (P\ \vee \  (Q\ \vee \  A))$
  & {\tiny \hyperref{}{}{rule30}{elementary equivalence} in \hyperref[hilb15:5]{$5$} at \hyperref[hilb15:4]{$4$} of \hyperref{}{}{hilb9}{hilb9}  with \hyperref{}{}{hilb9}{hilb9} 
} \\
 & & \qedhere
\end{longtable}
\end{proof}



Another consequence from hilb13 is the exchange of preconditions:




\begin{thm}[hilb16]
\hypertarget{hilb16}{}
\begin{displaymath}
(P\ \rightarrow \  (Q\ \rightarrow \  A))\ \rightarrow \  (Q\ \rightarrow \  (P\ \rightarrow \  A))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb16:1}
  $1$ & $(P\ \vee \  (Q\ \vee \  A))\ \rightarrow \  (Q\ \vee \  (P\ \vee \  A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb13}{hilb13} } \\
\label{hilb16:2}
  $2$ & $(\neg P\ \vee \  (\neg Q\ \vee \  A))\ \rightarrow \  (\neg Q\ \vee \  (\neg P\ \vee \  A))$
  & {\tiny \hyperref{subst_1.00.00_1.01.00.pdf}{}{rule8}{Substitute Variables} in \hyperref[hilb16:1]{$1$}
} \\
\label{hilb16:3}
  $3$ & $(P\ \rightarrow \  (\neg Q\ \vee \  A))\ \rightarrow \  (\neg Q\ \vee \  (\neg P\ \vee \  A))$
  & {\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[hilb16:2]{$2$} at occurence $1$
} \\
\label{hilb16:4}
  $4$ & $(P\ \rightarrow \  (Q\ \rightarrow \  A))\ \rightarrow \  (\neg Q\ \vee \  (\neg P\ \vee \  A))$
  & {\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[hilb16:3]{$3$} at occurence $1$
} \\
\label{hilb16:5}
  $5$ & $(P\ \rightarrow \  (Q\ \rightarrow \  A))\ \rightarrow \  (Q\ \rightarrow \  (\neg P\ \vee \  A))$
  & {\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[hilb16:4]{$4$} at occurence $1$
} \\
\label{hilb16:6}
  $6$ & $(P\ \rightarrow \  (Q\ \rightarrow \  A))\ \rightarrow \  (Q\ \rightarrow \  (P\ \rightarrow \  A))$
  & {\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[hilb16:5]{$5$} at occurence $1$
} \\
 & & \qedhere
\end{longtable}
\end{proof}



An analogus form for \hyperref[hilb16]{hilb16}:




\begin{thm}[hilb17]
\hypertarget{hilb17}{}
\begin{displaymath}
(Q\ \rightarrow \  (P\ \rightarrow \  A))\ \rightarrow \  (P\ \rightarrow \  (Q\ \rightarrow \  A))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb17:1}
  $1$ & $(P\ \rightarrow \  (Q\ \rightarrow \  A))\ \rightarrow \  (Q\ \rightarrow \  (P\ \rightarrow \  A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb16}{hilb16} } \\
\label{hilb17:2}
  $2$ & $(Q\ \rightarrow \  (P\ \rightarrow \  A))\ \rightarrow \  (P\ \rightarrow \  (Q\ \rightarrow \  A))$
  & {\tiny \hyperref{subst_1.00.00_1.01.00.pdf}{}{rule8}{Substitute Variables} in \hyperref[hilb17:1]{$1$}
} \\
 & & \qedhere
\end{longtable}
\end{proof}


\section{Cross Reference}

This module is used by the following modules:

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


\end{document}