"File page.tex
\documentclass [fleqn]{article}
\everymath{\rm}
\everydisplay{\rm}
\usepackage{latexsym}
\setlength {\overfullrule }{0mm}
%\input{lgwinclude}
\usepackage{url}
\usepackage[dvipdfm=true]{hyperref}
\usepackage{amsmath}
\usepackage{theorem}
\usepackage{amssymb}
\hypersetup{pdfpagemode=none}
\hypersetup{pdfstartpage=1}
\hypersetup{pdfstartview=FitBH}
\hypersetup{pdfpagescrop={120 80 490 730}}
\hypersetup{pdftitle=Logiweb sequent calculus}
\hypersetup{colorlinks=true}
% Save current \parindent (used by e.g. pyk display ... end display)
\newlength{\docparindent}
\setlength{\docparindent}{\parindent}
%Our extras
\newtheorem{Def}{Definition}[section]
\newtheorem{Lem}[Def]{Lemma}
\newtheorem{The}[Def]{Theorem}
\newtheorem{Cor}[Def]{Corollary}
\newtheorem{Alg}[Def]{Algorithm}
\theorembodyfont{\rmfamily} %normale bogstaver
\newtheorem{Exa}[Def]{Example}
\newtheorem{Rem}[Def]{Remark}
\newenvironment{proof}{
{\bf{\scriptsize{\uppercase{proof:}}}}\\}{
\begin{flushright}
\ensuremath{\blacksquare}
\end{flushright}}
\newcommand{\qedsubproof}{\begin{flushright}\ensuremath{\square}\end{flushright}}
\begin{document}
\title{Formal Logic}
\author{Lasse Nielsen \& Morten Ib Nielsen\\
Department of Computer Science, University of Copenhagen}
\date{\today}
\maketitle
\section{Initial remarks}
Initially we planned to show a simple result of Group Theory namely the
uniqueness of the neutral element. Our idea was to develop propositional logic
and predicate calculus first. Based on these we planned to develop the axiomatic set theory ZFC
and finally when we had sets we could define groups. Unfortunately it turned out that this was
much more cumbersome than we thought both because we are newcommers to Logiweb\texttrademark and also because core Logiweb\texttrademark
is very low level. Being newcommers to Logiweb\texttrademark we have used a lot of time
trying to find out how to use the system. This hasn't been easy due to the total absence of a hands on users manual.
Thus we wasted a lot of time early on trying to parse other peoples code from earlier years in order to understand how
to use pyk (the language used to construct proofs ect. in Logiweb\texttrademark). This was a very frustrating and non-trivial task since this years pyk syntax is different from earlier years!
A lot of emailing back and forth with Klaus Grue helped us, but progress was slow. Very late in the course we had the oportunity
to sit down with Klaus in a kind of assisted programming session, where Klaus helped us with our problems as they occured -
this was very rewarding. After that we revised our goals with respect to this project and we found that even though we were now
able to prove things in Logiweb\texttrademark our initial goal was out of range because of the assembler like nature of our predicate calculus.
Instead we decided to take the first step towards a more high level interface to our predicate calculus.
\section{Conclusion}
This Logiweb\texttrademark page is an exam project on the course \emph{202 Logik} spring 2006 at
the Department of Computer Science, University of Copenhagen. The purpose with this page is to use
Logiweb\texttrademark \emph{to publish a machine checkable proof for a theorem of our choise} - which we have done.
Since
both of us have backgrounds in mathematics and formal methods in computer science we started out having
high ambitions. As hinted we had to revise our goals along the way for several reasons. Instead of doing
a large and complicated proof we have decided to show how to use the Logiweb\texttrademark system to
\emph{define a theory} (a set of axioms), \emph{define and prove lemmas in a theory} (both using axioms
aswell as allready proved lemmas). Along the way we have explained key parts of the Logiweb\texttrademark notation.
It is our hope that this Logiweb\texttrademark page will serve as a helping hand to
future students on this course providing the \emph{getting started} manual that we have been missing so much.
We start out defining a theory called \emph{pred calc} containing one possible set of axioms and inference rules
for the predicate calculus. Since these axioms are very low level we define, inspired by Natural Deduction
(see \cite{huth}), a set of higher level (and more intuitive) proof rules wich we prove. Finally we use these
higher level rules to prove the sequent: TODO.
\section{Introduction}
This Logiweb\texttrademark page is formally correct. This means that it has been verified and found correct by the Logiweb\texttrademark proof engine.
Therefore we can say that it is correct modulo errors in the proof engine. Is the content correct then? Well yes, but only in the sense that the lemmas
we have proved are consequences of the axioms and proof rules we have introduced. There is no guarantee of soundness of our axioms and proof rules.
We have structured this document as follows. In section \ref{sec:predcalc} we define the axioms and proof rules
of predicate calculus. We conclude the section with two simple proofs namely the very (intuitively) obvious
lemma \emph{trivia} \ref{lem:trivia} and the lemma \emph{repeat} \ref{lem:repeat}. Then in section
\ref{sec:natded} we state and prove lemmas inspired by Natural Deduction. Finally in section \ref{sec:higherproof}
we use these lemmas to prove the sequent: TODO.
\section{First order predicate calculus}\label{sec:predcalc}
Based on mathworld\footnote{http://mathworld.wolfram.com/First-OrderLogic.html.} and thus on Kleene (2002) we define
first-order predicate calculus below. We note that the axioms 1 through 10 together with the inference rule
modus ponens (pcmp) constitutes the propositional calculus. Our definitions are not excately like those found on Mathworld for two reasons.
First we have made $\Rightarrow$ right associative in order to get rid of unnecessary parenthisis. This means that
" [ math metavar var f end metavar imply metavar var g end metavar imply metavar var f end metavar end math ] " really means
" [ math metavar var f end metavar imply metavar var g end metavar imply metavar var f end metavar end math ] " below. Second we had to express formulations such as \emph{in which $x$ occurs free} in
a machine checkable way.
The " [ math define statement of pred calc as all metavar var x end metavar indeed all metavar var r end metavar indeed all metavar var g end metavar indeed all metavar var f end metavar indeed quote metavar var x end metavar end quote avoid zero quote metavar var r end metavar end quote endorse quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote endorse sub zero quote metavar var g end metavar end quote is quote metavar var f end metavar end quote where quote metavar var x end metavar end quote is quote metavar var r end metavar end quote end sub endorse forall metavar var x end metavar dot metavar var f end metavar end forall imply metavar var g end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar imply metavar var g end metavar imply metavar var f end metavar land metavar var g end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar land metavar var g end metavar imply metavar var g end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar infer metavar var g end metavar infer metavar var f end metavar imply metavar var g end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar imply metavar var g end metavar imply metavar var f end metavar imply lnot metavar var g end metavar imply lnot metavar var f end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar imply metavar var g end metavar imply metavar var f end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed all metavar var x end metavar indeed quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote endorse metavar var f end metavar imply metavar var g end metavar infer exists metavar var x end metavar dot metavar var f end metavar end exists imply metavar var g end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar imply metavar var g end metavar lor metavar var f end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar infer metavar var f end metavar imply metavar var g end metavar infer metavar var g end metavar rule plus all metavar var f end metavar indeed lnot lnot metavar var f end metavar imply metavar var f end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed all metavar var h end metavar indeed metavar var f end metavar imply metavar var g end metavar imply metavar var f end metavar imply metavar var g end metavar imply metavar var h end metavar imply metavar var f end metavar imply metavar var h end metavar rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed lambda var x dot deduction zero quote metavar var a end metavar end quote conclude quote metavar var b end metavar end quote end deduction endorse metavar var a end metavar infer metavar var b end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar land metavar var g end metavar imply metavar var f end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed all metavar var h end metavar indeed metavar var f end metavar imply metavar var g end metavar imply metavar var h end metavar imply metavar var g end metavar imply metavar var f end metavar lor metavar var h end metavar imply metavar var g end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed all metavar var x end metavar indeed quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote endorse metavar var g end metavar imply metavar var f end metavar infer metavar var g end metavar imply forall metavar var x end metavar dot metavar var f end metavar end forall rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar imply metavar var f end metavar lor metavar var g end metavar rule plus all metavar var x end metavar indeed all metavar var r end metavar indeed all metavar var g end metavar indeed all metavar var f end metavar indeed quote metavar var x end metavar end quote avoid zero quote metavar var r end metavar end quote endorse quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote endorse sub zero quote metavar var g end metavar end quote is quote metavar var f end metavar end quote where quote metavar var x end metavar end quote is quote metavar var r end metavar end quote end sub endorse metavar var g end metavar imply exists metavar var x end metavar dot metavar var f end metavar end exists end define end math ] " contains the following axioms:
\begin{enumerate}
\item " [ math define statement of pc1 as pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar imply metavar var g end metavar imply metavar var f end metavar end define , define proof of pc1 as rule tactic end define end math ] "
\item " [ math define statement of pc2 as pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed all metavar var h end metavar indeed metavar var f end metavar imply metavar var g end metavar imply metavar var f end metavar imply metavar var g end metavar imply metavar var h end metavar imply metavar var f end metavar imply metavar var h end metavar end define , define proof of pc2 as rule tactic end define end math ] "
\item " [ math define statement of pc3 as pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar imply metavar var g end metavar imply metavar var f end metavar land metavar var g end metavar end define , define proof of pc3 as rule tactic end define end math ] "
\item " [ math define statement of pc4 as pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar imply metavar var f end metavar lor metavar var g end metavar end define , define proof of pc4 as rule tactic end define end math ] "
\item " [ math define statement of pc5 as pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar imply metavar var g end metavar lor metavar var f end metavar end define , define proof of pc5 as rule tactic end define end math ] "
\item " [ math define statement of pc6 as pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar land metavar var g end metavar imply metavar var f end metavar end define , define proof of pc6 as rule tactic end define end math ] "
\item " [ math define statement of pc7 as pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar land metavar var g end metavar imply metavar var g end metavar end define , define proof of pc7 as rule tactic end define end math ] "
\item " [ math define statement of pc8 as pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed all metavar var h end metavar indeed metavar var f end metavar imply metavar var g end metavar imply metavar var h end metavar imply metavar var g end metavar imply metavar var f end metavar lor metavar var h end metavar imply metavar var g end metavar end define , define proof of pc8 as rule tactic end define end math ] "
\item " [ math define statement of pc9 as pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar imply metavar var g end metavar imply metavar var f end metavar imply lnot metavar var g end metavar imply lnot metavar var f end metavar end define , define proof of pc9 as rule tactic end define end math ] "
\item " [ math define statement of pc10 as pred calc infer all metavar var f end metavar indeed lnot lnot metavar var f end metavar imply metavar var f end metavar end define , define proof of pc10 as rule tactic end define end math ] "
\item " [ math define statement of pc11 as pred calc infer all metavar var x end metavar indeed all metavar var r end metavar indeed all metavar var g end metavar indeed all metavar var f end metavar indeed quote metavar var x end metavar end quote avoid zero quote metavar var r end metavar end quote endorse quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote endorse sub zero quote metavar var g end metavar end quote is quote metavar var f end metavar end quote where quote metavar var x end metavar end quote is quote metavar var r end metavar end quote end sub endorse forall metavar var x end metavar dot metavar var f end metavar end forall imply metavar var g end metavar end define , define proof of pc11 as rule tactic end define end math ] "
\item " [ math define statement of pc12 as pred calc infer all metavar var x end metavar indeed all metavar var r end metavar indeed all metavar var g end metavar indeed all metavar var f end metavar indeed quote metavar var x end metavar end quote avoid zero quote metavar var r end metavar end quote endorse quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote endorse sub zero quote metavar var g end metavar end quote is quote metavar var f end metavar end quote where quote metavar var x end metavar end quote is quote metavar var r end metavar end quote end sub endorse metavar var g end metavar imply exists metavar var x end metavar dot metavar var f end metavar end exists end define , define proof of pc12 as rule tactic end define end math ] "
\end{enumerate}
The proof rules in the " [ math define statement of pred calc as all metavar var x end metavar indeed all metavar var r end metavar indeed all metavar var g end metavar indeed all metavar var f end metavar indeed quote metavar var x end metavar end quote avoid zero quote metavar var r end metavar end quote endorse quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote endorse sub zero quote metavar var g end metavar end quote is quote metavar var f end metavar end quote where quote metavar var x end metavar end quote is quote metavar var r end metavar end quote end sub endorse forall metavar var x end metavar dot metavar var f end metavar end forall imply metavar var g end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar imply metavar var g end metavar imply metavar var f end metavar land metavar var g end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar land metavar var g end metavar imply metavar var g end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar infer metavar var g end metavar infer metavar var f end metavar imply metavar var g end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar imply metavar var g end metavar imply metavar var f end metavar imply lnot metavar var g end metavar imply lnot metavar var f end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar imply metavar var g end metavar imply metavar var f end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed all metavar var x end metavar indeed quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote endorse metavar var f end metavar imply metavar var g end metavar infer exists metavar var x end metavar dot metavar var f end metavar end exists imply metavar var g end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar imply metavar var g end metavar lor metavar var f end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar infer metavar var f end metavar imply metavar var g end metavar infer metavar var g end metavar rule plus all metavar var f end metavar indeed lnot lnot metavar var f end metavar imply metavar var f end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed all metavar var h end metavar indeed metavar var f end metavar imply metavar var g end metavar imply metavar var f end metavar imply metavar var g end metavar imply metavar var h end metavar imply metavar var f end metavar imply metavar var h end metavar rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed lambda var x dot deduction zero quote metavar var a end metavar end quote conclude quote metavar var b end metavar end quote end deduction endorse metavar var a end metavar infer metavar var b end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar land metavar var g end metavar imply metavar var f end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed all metavar var h end metavar indeed metavar var f end metavar imply metavar var g end metavar imply metavar var h end metavar imply metavar var g end metavar imply metavar var f end metavar lor metavar var h end metavar imply metavar var g end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed all metavar var x end metavar indeed quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote endorse metavar var g end metavar imply metavar var f end metavar infer metavar var g end metavar imply forall metavar var x end metavar dot metavar var f end metavar end forall rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar imply metavar var f end metavar lor metavar var g end metavar rule plus all metavar var x end metavar indeed all metavar var r end metavar indeed all metavar var g end metavar indeed all metavar var f end metavar indeed quote metavar var x end metavar end quote avoid zero quote metavar var r end metavar end quote endorse quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote endorse sub zero quote metavar var g end metavar end quote is quote metavar var f end metavar end quote where quote metavar var x end metavar end quote is quote metavar var r end metavar end quote end sub endorse metavar var g end metavar imply exists metavar var x end metavar dot metavar var f end metavar end exists end define end math ] " are:
\begin{itemize}
\item " [ math define statement of pcmp as pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar infer metavar var f end metavar imply metavar var g end metavar infer metavar var g end metavar end define , define proof of pcmp as rule tactic end define end math ] "
\item " [ math define statement of pcia as pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed all metavar var x end metavar indeed quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote endorse metavar var g end metavar imply metavar var f end metavar infer metavar var g end metavar imply forall metavar var x end metavar dot metavar var f end metavar end forall end define , define proof of pcia as rule tactic end define end math ] "
\item " [ math define statement of pcie as pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed all metavar var x end metavar indeed quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote endorse metavar var f end metavar imply metavar var g end metavar infer exists metavar var x end metavar dot metavar var f end metavar end exists imply metavar var g end metavar end define , define proof of pcie as rule tactic end define end math ] "
\item " [ math define statement of pcdeduction as pred calc infer all metavar var a end metavar indeed all metavar var b end metavar indeed lambda var x dot deduction zero quote metavar var a end metavar end quote conclude quote metavar var b end metavar end quote end deduction endorse metavar var a end metavar infer metavar var b end metavar end define , define proof of pcdeduction as rule tactic end define end math ] "
\end{itemize}
\subsection{A conservative extension}
The rule \emph{pcdeduction} is not really a part of Predicate Calculus acording to mathworld but it is a conservative extension
in the sence than we cannot prove anything using this rule that we cannot prove without it. We include it in order to make proofs shorter
and thus easier to understand for humans. As a curiosity we cannot prove that \emph{pcdeduction} is a conservative extension formally
\footnote{In a machine checkable way.}.
\subsection{Notation}
Some of the notation used above is most likely unfamilliar. So let's spend a few paragraphs explaining it before we continue.
The meaning of the axioms and proof rules above are of course given by their definition but in order to understand the definitions
we need to explain the basic syntax (or at least the part of it we use) in Logiweb\texttrademark definitions and proofs.
\begin{itemize}
\item{\textbf{The symbol $\vdash$}} is placed between two propositions. The meaning of $A \vdash B$ is that if $A$ can be proved then so can $B$.
$\vdash$ can be used sequentially in the way that $A \vdash B \vdash C$ means if $A$ can be proved, then if $B$ can be proved, then so can $C$.
That is if $A$ and $B$ can be proved then so can $C$.
\item{\textbf{The symbol $\triangleright$}} is placed between a rule and a line number.
It is the opposite of $\vdash$ in the sence that if $R$ is a rule saying that $A \vdash B$ and $L$ is a line concluding $A$, then
$R \triangleright L$ concludes $B$.
\item{\textbf{Explanation of $\gg$}}. A line in a proof consists of the symbol $\gg$ with the use of a rule on the left, and the conclusion on the right.
The example above would give the line $R \triangleright L \gg B$.
\item{\textbf{The meaning of $\Vdash$}} is almost the same as $\vdash$. If the condition on the left evaluates to true, then the proposition on the right can be proved.
The condition on the left of a $\Vdash$ is a so called side-condition. The only side-conditions we use are expressed using substitution and $\sharp$ (explained below).
\item{\textbf{The $\triangleright\!\!\triangleright$}} symbol is used much like $\triangleright$, but it is the opposite of $\Vdash$ instead of $\vdash$, thus the line number on the right
of the symbol must conclude that the side-condition is fullfilled.
\item{\textbf{The side-condition $\left< A \equiv B \mid C := D \right>$}} is fulfilled, if the proposition $A$ where any occurrence of the meta-variable $C$ is replaced
by the proposition $D$ is exactly equal to the proposition $B$. Another way to express this using a more common notation of substitution would be $B \equiv A[D/C]$.
\item{\textbf{The side-condition $A \sharp B$}} is fulfilled if the meta-variable $A$ does not occur in the proposition $B$.
\end{itemize}
\subsection{Some small proofs}
Having explained the syntax of definitons and proofs we continue with two simple, but usefull, lemmas just to show
how it is done. Lemma \ref{lem:trivia} is proved using only axioms and proof rules while the proof of lemma \ref{lem:repeat}
uses the result of lemma \ref{lem:trivia} aswell.
\begin{Lem}\label{lem:trivia}
" [ math define statement of trivia as pred calc infer all metavar var f end metavar indeed metavar var f end metavar imply metavar var f end metavar end define end math ] "
\end{Lem}
" [ math define proof of trivia as lambda var c dot lambda var x dot proof expand quote pred calc infer all metavar var f end metavar indeed pc2 conclude metavar var f end metavar imply metavar var f end metavar imply metavar var f end metavar imply metavar var f end metavar imply metavar var f end metavar imply metavar var f end metavar imply metavar var f end metavar imply metavar var f end metavar imply metavar var f end metavar cut pc1 conclude metavar var f end metavar imply metavar var f end metavar imply metavar var f end metavar cut pcmp modus ponens metavar var f end metavar imply metavar var f end metavar imply metavar var f end metavar modus ponens metavar var f end metavar imply metavar var f end metavar imply metavar var f end metavar imply metavar var f end metavar imply metavar var f end metavar imply metavar var f end metavar imply metavar var f end metavar imply metavar var f end metavar imply metavar var f end metavar conclude metavar var f end metavar imply metavar var f end metavar imply metavar var f end metavar imply metavar var f end metavar imply metavar var f end metavar imply metavar var f end metavar cut pc1 conclude metavar var f end metavar imply metavar var f end metavar imply metavar var f end metavar imply metavar var f end metavar cut pcmp modus ponens metavar var f end metavar imply metavar var f end metavar imply metavar var f end metavar imply metavar var f end metavar modus ponens metavar var f end metavar imply metavar var f end metavar imply metavar var f end metavar imply metavar var f end metavar imply metavar var f end metavar imply metavar var f end metavar conclude metavar var f end metavar imply metavar var f end metavar end quote state proof state cache var c end expand end define end math ] "
\begin{Lem}
" [ math define statement of trivia2 as pred calc infer all metavar var f end metavar indeed metavar var f end metavar infer metavar var f end metavar end define end math ] "
\end{Lem}
" [ math define proof of trivia2 as lambda var c dot lambda var x dot proof expand quote pred calc infer all metavar var f end metavar indeed all metavar var f end metavar indeed metavar var f end metavar infer repeat modus ponens metavar var f end metavar conclude metavar var f end metavar cut pcdeduction modus ponens all metavar var f end metavar indeed metavar var f end metavar infer metavar var f end metavar conclude metavar var f end metavar infer metavar var f end metavar end quote state proof state cache var c end expand end define end math ] "
\begin{Lem}[Repetition]\label{lem:repeat}
" [ math define statement of repeat as pred calc infer all metavar var f end metavar indeed metavar var f end metavar infer metavar var f end metavar end define end math ] "
\end{Lem}
" [ math define proof of repeat as lambda var c dot lambda var x dot proof expand quote pred calc infer all metavar var f end metavar indeed metavar var f end metavar infer trivia conclude metavar var f end metavar imply metavar var f end metavar cut pcmp modus ponens metavar var f end metavar modus ponens metavar var f end metavar imply metavar var f end metavar conclude metavar var f end metavar end quote state proof state cache var c end expand end define end math ] "
\section{Natural deduction}\label{sec:natded}
The axioms and proof rules in " [ math define statement of pred calc as all metavar var x end metavar indeed all metavar var r end metavar indeed all metavar var g end metavar indeed all metavar var f end metavar indeed quote metavar var x end metavar end quote avoid zero quote metavar var r end metavar end quote endorse quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote endorse sub zero quote metavar var g end metavar end quote is quote metavar var f end metavar end quote where quote metavar var x end metavar end quote is quote metavar var r end metavar end quote end sub endorse forall metavar var x end metavar dot metavar var f end metavar end forall imply metavar var g end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar imply metavar var g end metavar imply metavar var f end metavar land metavar var g end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar land metavar var g end metavar imply metavar var g end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar infer metavar var g end metavar infer metavar var f end metavar imply metavar var g end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar imply metavar var g end metavar imply metavar var f end metavar imply lnot metavar var g end metavar imply lnot metavar var f end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar imply metavar var g end metavar imply metavar var f end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed all metavar var x end metavar indeed quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote endorse metavar var f end metavar imply metavar var g end metavar infer exists metavar var x end metavar dot metavar var f end metavar end exists imply metavar var g end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar imply metavar var g end metavar lor metavar var f end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar infer metavar var f end metavar imply metavar var g end metavar infer metavar var g end metavar rule plus all metavar var f end metavar indeed lnot lnot metavar var f end metavar imply metavar var f end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed all metavar var h end metavar indeed metavar var f end metavar imply metavar var g end metavar imply metavar var f end metavar imply metavar var g end metavar imply metavar var h end metavar imply metavar var f end metavar imply metavar var h end metavar rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed lambda var x dot deduction zero quote metavar var a end metavar end quote conclude quote metavar var b end metavar end quote end deduction endorse metavar var a end metavar infer metavar var b end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar land metavar var g end metavar imply metavar var f end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed all metavar var h end metavar indeed metavar var f end metavar imply metavar var g end metavar imply metavar var h end metavar imply metavar var g end metavar imply metavar var f end metavar lor metavar var h end metavar imply metavar var g end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed all metavar var x end metavar indeed quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote endorse metavar var g end metavar imply metavar var f end metavar infer metavar var g end metavar imply forall metavar var x end metavar dot metavar var f end metavar end forall rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar imply metavar var f end metavar lor metavar var g end metavar rule plus all metavar var x end metavar indeed all metavar var r end metavar indeed all metavar var g end metavar indeed all metavar var f end metavar indeed quote metavar var x end metavar end quote avoid zero quote metavar var r end metavar end quote endorse quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote endorse sub zero quote metavar var g end metavar end quote is quote metavar var f end metavar end quote where quote metavar var x end metavar end quote is quote metavar var r end metavar end quote end sub endorse metavar var g end metavar imply exists metavar var x end metavar dot metavar var f end metavar end exists end define end math ] " constitutes a very low level proof system.
In order to ameliorate this we introduce and prove some higher level (and more intuitive) proof rules. These proof rules
are inspired by natural deduction as defined in \cite{huth}. We conclude this section by justifying why we have replaced two
rules from \cite{huth} with a new rule.
\begin{Lem}
" [ math define statement of andintro as pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar infer metavar var g end metavar infer metavar var f end metavar land metavar var g end metavar end define end math ] "
\end{Lem}
" [ math define proof of andintro as lambda var c dot lambda var x dot proof expand quote pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar infer metavar var g end metavar infer pc3 conclude metavar var f end metavar imply metavar var g end metavar imply metavar var f end metavar land metavar var g end metavar cut pcmp modus ponens metavar var f end metavar modus ponens metavar var f end metavar imply metavar var g end metavar imply metavar var f end metavar land metavar var g end metavar conclude metavar var g end metavar imply metavar var f end metavar land metavar var g end metavar cut pcmp modus ponens metavar var g end metavar modus ponens metavar var g end metavar imply metavar var f end metavar land metavar var g end metavar conclude metavar var f end metavar land metavar var g end metavar end quote state proof state cache var c end expand end define end math ] "
\begin{Lem}
" [ math define statement of andelim1 as pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar land metavar var g end metavar infer metavar var f end metavar end define end math ] "
\end{Lem}
" [ math define proof of andelim1 as lambda var c dot lambda var x dot proof expand quote pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar land metavar var g end metavar infer pc6 conclude metavar var f end metavar land metavar var g end metavar imply metavar var f end metavar cut pcmp modus ponens metavar var f end metavar land metavar var g end metavar modus ponens metavar var f end metavar land metavar var g end metavar imply metavar var f end metavar conclude metavar var f end metavar end quote state proof state cache var c end expand end define end math ] "
\begin{Lem}
" [ math define statement of andelim2 as pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar land metavar var g end metavar infer metavar var g end metavar end define end math ] "
\end{Lem}
" [ math define proof of andelim2 as lambda var c dot lambda var x dot proof expand quote pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar land metavar var g end metavar infer pc7 conclude metavar var f end metavar land metavar var g end metavar imply metavar var g end metavar cut pcmp modus ponens metavar var f end metavar land metavar var g end metavar modus ponens metavar var f end metavar land metavar var g end metavar imply metavar var g end metavar conclude metavar var g end metavar end quote state proof state cache var c end expand end define end math ] "
\begin{Lem}
" [ math define statement of orintro1 as pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar infer metavar var f end metavar lor metavar var g end metavar end define end math ] "
\end{Lem}
" [ math define proof of orintro1 as lambda var c dot lambda var x dot proof expand quote pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar infer pc4 conclude metavar var f end metavar imply metavar var f end metavar lor metavar var g end metavar cut pcmp modus ponens metavar var f end metavar modus ponens metavar var f end metavar imply metavar var f end metavar lor metavar var g end metavar conclude metavar var f end metavar lor metavar var g end metavar end quote state proof state cache var c end expand end define end math ] "
\begin{Lem}
" [ math define statement of orintro2 as pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var g end metavar infer metavar var f end metavar lor metavar var g end metavar end define end math ] "
\end{Lem}
" [ math define proof of orintro2 as lambda var c dot lambda var x dot proof expand quote pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var g end metavar infer pc5 conclude metavar var g end metavar imply metavar var f end metavar lor metavar var g end metavar cut pcmp modus ponens metavar var g end metavar modus ponens metavar var g end metavar imply metavar var f end metavar lor metavar var g end metavar conclude metavar var f end metavar lor metavar var g end metavar end quote state proof state cache var c end expand end define end math ] "
\begin{Lem}
" [ math define statement of orelim as pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed all metavar var h end metavar indeed metavar var f end metavar lor metavar var g end metavar infer metavar var f end metavar infer metavar var h end metavar infer metavar var g end metavar infer metavar var h end metavar infer metavar var h end metavar end define end math ] "
\end{Lem}
" [ math define proof of orelim as lambda var c dot lambda var x dot proof expand quote pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed all metavar var h end metavar indeed metavar var f end metavar lor metavar var g end metavar infer metavar var f end metavar infer metavar var h end metavar infer metavar var g end metavar infer metavar var h end metavar infer pcded modus ponens metavar var f end metavar infer metavar var h end metavar conclude metavar var f end metavar imply metavar var h end metavar cut pcded modus ponens metavar var g end metavar infer metavar var h end metavar conclude metavar var g end metavar imply metavar var h end metavar cut pc8 conclude metavar var f end metavar imply metavar var h end metavar imply metavar var g end metavar imply metavar var h end metavar imply metavar var f end metavar lor metavar var g end metavar imply metavar var h end metavar cut pcmp modus ponens metavar var f end metavar imply metavar var h end metavar modus ponens metavar var f end metavar imply metavar var h end metavar imply metavar var g end metavar imply metavar var h end metavar imply metavar var f end metavar lor metavar var g end metavar imply metavar var h end metavar conclude metavar var g end metavar imply metavar var h end metavar imply metavar var f end metavar lor metavar var g end metavar imply metavar var h end metavar cut pcmp modus ponens metavar var g end metavar imply metavar var h end metavar modus ponens metavar var g end metavar imply metavar var h end metavar imply metavar var f end metavar lor metavar var g end metavar imply metavar var h end metavar conclude metavar var f end metavar lor metavar var g end metavar imply metavar var h end metavar cut pcmp modus ponens metavar var f end metavar lor metavar var g end metavar modus ponens metavar var f end metavar lor metavar var g end metavar imply metavar var h end metavar conclude metavar var h end metavar end quote state proof state cache var c end expand end define end math ] "
\begin{Lem}
" [ math define statement of notintro as pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar infer metavar var g end metavar infer metavar var f end metavar infer lnot metavar var g end metavar infer lnot metavar var f end metavar end define end math ] "
\end{Lem}
" [ math define proof of notintro as lambda var c dot lambda var x dot proof expand quote pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar infer metavar var g end metavar infer metavar var f end metavar infer lnot metavar var g end metavar infer pcded modus ponens metavar var f end metavar infer metavar var g end metavar conclude metavar var f end metavar imply metavar var g end metavar cut pcded modus ponens metavar var f end metavar infer lnot metavar var g end metavar conclude metavar var f end metavar imply lnot metavar var g end metavar cut pc9 conclude metavar var f end metavar imply metavar var g end metavar imply metavar var f end metavar imply lnot metavar var g end metavar imply lnot metavar var f end metavar cut pcmp modus ponens metavar var f end metavar imply metavar var g end metavar modus ponens metavar var f end metavar imply metavar var g end metavar imply metavar var f end metavar imply lnot metavar var g end metavar imply lnot metavar var f end metavar conclude metavar var f end metavar imply lnot metavar var g end metavar imply lnot metavar var f end metavar cut pcmp modus ponens metavar var f end metavar imply lnot metavar var g end metavar modus ponens metavar var f end metavar imply lnot metavar var g end metavar imply lnot metavar var f end metavar conclude lnot metavar var f end metavar end quote state proof state cache var c end expand end define end math ] "
\begin{Lem}
" [ math define statement of notnotelim as pred calc infer all metavar var f end metavar indeed lnot lnot metavar var f end metavar infer metavar var f end metavar end define end math ] "
\end{Lem}
" [ math define proof of notnotelim as lambda var c dot lambda var x dot proof expand quote pred calc infer all metavar var f end metavar indeed lnot lnot metavar var f end metavar infer pc10 conclude lnot lnot metavar var f end metavar imply metavar var f end metavar cut pcmp modus ponens lnot lnot metavar var f end metavar modus ponens lnot lnot metavar var f end metavar imply metavar var f end metavar conclude metavar var f end metavar end quote state proof state cache var c end expand end define end math ] "
\begin{Lem}\label{lem:forallintro}
" [ math define statement of forallintro as pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed all metavar var x end metavar indeed quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar lor lnot metavar var g end metavar end quote endorse metavar var f end metavar infer forall metavar var x end metavar dot metavar var f end metavar end forall end define end math ] "
" [ math define proof of forallintro as lambda var c dot lambda var x dot proof expand quote pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed all metavar var x end metavar indeed quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar lor lnot metavar var g end metavar end quote endorse metavar var f end metavar infer lem conclude metavar var g end metavar lor lnot metavar var g end metavar cut all metavar var g end metavar indeed all metavar var f end metavar indeed metavar var g end metavar lor lnot metavar var g end metavar infer repeat modus ponens metavar var f end metavar conclude metavar var f end metavar cut pcdeduction modus ponens all metavar var g end metavar indeed all metavar var f end metavar indeed metavar var g end metavar lor lnot metavar var g end metavar infer metavar var f end metavar conclude metavar var g end metavar lor lnot metavar var g end metavar imply metavar var f end metavar cut pcia modus probans quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar lor lnot metavar var g end metavar end quote modus ponens metavar var g end metavar lor lnot metavar var g end metavar imply metavar var f end metavar conclude metavar var g end metavar lor lnot metavar var g end metavar imply forall metavar var x end metavar dot metavar var f end metavar end forall cut pcmp modus ponens metavar var g end metavar lor lnot metavar var g end metavar modus ponens metavar var g end metavar lor lnot metavar var g end metavar imply forall metavar var x end metavar dot metavar var f end metavar end forall conclude forall metavar var x end metavar dot metavar var f end metavar end forall end quote state proof state cache var c end expand end define end math ] "
\begin{Rem}
In lemma \ref{lem:forallintro} we use the side condition " [ math quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar lor lnot metavar var g end metavar end quote end math ] ". We would like to use the
equivalent " [ math quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote end math ] " instead but we haven't been able to find a way to prove the former side condition
from the latter.
\end{Rem}
\end{Lem}
\begin{Lem}
" [ math define statement of forallelim as pred calc infer all metavar var x end metavar indeed all metavar var r end metavar indeed all metavar var g end metavar indeed all metavar var f end metavar indeed quote metavar var x end metavar end quote avoid zero quote metavar var r end metavar end quote endorse quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote endorse sub zero quote metavar var g end metavar end quote is quote metavar var f end metavar end quote where quote metavar var x end metavar end quote is quote metavar var r end metavar end quote end sub endorse forall metavar var x end metavar dot metavar var f end metavar end forall infer metavar var g end metavar end define end math ] "
\end{Lem}
" [ math define proof of forallelim as lambda var c dot lambda var x dot proof expand quote pred calc infer all metavar var x end metavar indeed all metavar var r end metavar indeed all metavar var g end metavar indeed all metavar var f end metavar indeed quote metavar var x end metavar end quote avoid zero quote metavar var r end metavar end quote endorse quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote endorse sub zero quote metavar var g end metavar end quote is quote metavar var f end metavar end quote where quote metavar var x end metavar end quote is quote metavar var r end metavar end quote end sub endorse pc11 modus probans quote metavar var x end metavar end quote avoid zero quote metavar var r end metavar end quote modus probans quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote modus probans sub zero quote metavar var g end metavar end quote is quote metavar var f end metavar end quote where quote metavar var x end metavar end quote is quote metavar var r end metavar end quote end sub conclude forall metavar var x end metavar dot metavar var f end metavar end forall imply metavar var g end metavar cut all metavar var x end metavar indeed all metavar var g end metavar indeed all metavar var f end metavar indeed forall metavar var x end metavar dot metavar var f end metavar end forall infer pcmp modus ponens forall metavar var x end metavar dot metavar var f end metavar end forall modus ponens forall metavar var x end metavar dot metavar var f end metavar end forall imply metavar var g end metavar conclude metavar var g end metavar cut pcdeduction modus ponens all metavar var x end metavar indeed all metavar var g end metavar indeed all metavar var f end metavar indeed forall metavar var x end metavar dot metavar var f end metavar end forall infer metavar var g end metavar conclude forall metavar var x end metavar dot metavar var f end metavar end forall infer metavar var g end metavar end quote state proof state cache var c end expand end define end math ] "
\begin{Lem}
" [ math define statement of existsintro as pred calc infer all metavar var x end metavar indeed all metavar var r end metavar indeed all metavar var g end metavar indeed all metavar var f end metavar indeed quote metavar var x end metavar end quote avoid zero quote metavar var r end metavar end quote endorse quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote endorse sub zero quote metavar var g end metavar end quote is quote metavar var f end metavar end quote where quote metavar var x end metavar end quote is quote metavar var r end metavar end quote end sub endorse metavar var g end metavar infer exists metavar var x end metavar dot metavar var f end metavar end exists end define end math ] "
\end{Lem}
" [ math define proof of existsintro as lambda var c dot lambda var x dot proof expand quote pred calc infer all metavar var x end metavar indeed all metavar var r end metavar indeed all metavar var g end metavar indeed all metavar var f end metavar indeed quote metavar var x end metavar end quote avoid zero quote metavar var r end metavar end quote endorse quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote endorse sub zero quote metavar var g end metavar end quote is quote metavar var f end metavar end quote where quote metavar var x end metavar end quote is quote metavar var r end metavar end quote end sub endorse pc12 modus probans quote metavar var x end metavar end quote avoid zero quote metavar var r end metavar end quote modus probans quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote modus probans sub zero quote metavar var g end metavar end quote is quote metavar var f end metavar end quote where quote metavar var x end metavar end quote is quote metavar var r end metavar end quote end sub conclude metavar var g end metavar imply exists metavar var x end metavar dot metavar var f end metavar end exists cut all metavar var x end metavar indeed all metavar var g end metavar indeed all metavar var f end metavar indeed metavar var g end metavar infer pcmp modus ponens metavar var g end metavar modus ponens metavar var g end metavar imply exists metavar var x end metavar dot metavar var f end metavar end exists conclude exists metavar var x end metavar dot metavar var f end metavar end exists cut pcdeduction modus ponens all metavar var x end metavar indeed all metavar var g end metavar indeed all metavar var f end metavar indeed metavar var g end metavar infer exists metavar var x end metavar dot metavar var f end metavar end exists conclude metavar var g end metavar infer exists metavar var x end metavar dot metavar var f end metavar end exists end quote state proof state cache var c end expand end define end math ] "
\begin{Lem}
" [ math define statement of existselim as pred calc infer all metavar var x end metavar indeed all metavar var f end metavar indeed all metavar var g end metavar indeed quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote endorse exists metavar var x end metavar dot metavar var f end metavar end exists infer metavar var f end metavar infer metavar var g end metavar infer metavar var g end metavar end define end math ] "
\end{Lem}
" [ math define proof of existselim as lambda var c dot lambda var x dot proof expand quote pred calc infer all metavar var x end metavar indeed all metavar var f end metavar indeed all metavar var g end metavar indeed quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote endorse exists metavar var x end metavar dot metavar var f end metavar end exists infer metavar var f end metavar infer metavar var g end metavar infer pcded modus ponens metavar var f end metavar infer metavar var g end metavar conclude metavar var f end metavar imply metavar var g end metavar cut pcie modus probans quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote modus ponens metavar var f end metavar imply metavar var g end metavar conclude exists metavar var x end metavar dot metavar var f end metavar end exists imply metavar var g end metavar cut pcmp modus ponens exists metavar var x end metavar dot metavar var f end metavar end exists modus ponens exists metavar var x end metavar dot metavar var f end metavar end exists imply metavar var g end metavar conclude metavar var g end metavar end quote state proof state cache var c end expand end define end math ] "
\subsection{Derived lemmas}
Below we apply the theorems above to prove some other fairly standard rules.
\begin{Lem}
" [ math define statement of mt as pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar imply metavar var g end metavar infer lnot metavar var g end metavar infer lnot metavar var f end metavar end define end math ] "
\end{Lem}
" [ math define proof of mt as lambda var c dot lambda var x dot proof expand quote pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar imply metavar var g end metavar infer lnot metavar var g end metavar infer all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar infer pcmp modus ponens metavar var f end metavar modus ponens metavar var f end metavar imply metavar var g end metavar conclude metavar var g end metavar cut pcdeduction modus ponens all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar infer metavar var g end metavar conclude metavar var f end metavar infer metavar var g end metavar cut all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar infer repeat modus ponens lnot metavar var g end metavar conclude lnot metavar var g end metavar cut pcdeduction modus ponens all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar infer lnot metavar var g end metavar conclude metavar var f end metavar infer lnot metavar var g end metavar cut notintro modus ponens metavar var f end metavar infer metavar var g end metavar modus ponens metavar var f end metavar infer lnot metavar var g end metavar conclude lnot metavar var f end metavar end quote state proof state cache var c end expand end define end math ] "
\begin{Lem}
" [ math define statement of notnotintro as pred calc infer all metavar var f end metavar indeed metavar var f end metavar infer lnot lnot metavar var f end metavar end define end math ] "
\end{Lem}
" [ math define proof of notnotintro as lambda var c dot lambda var x dot proof expand quote pred calc infer all metavar var f end metavar indeed metavar var f end metavar infer all metavar var f end metavar indeed metavar var f end metavar infer lnot metavar var f end metavar infer repeat modus ponens metavar var f end metavar conclude metavar var f end metavar cut pcdeduction modus ponens all metavar var f end metavar indeed metavar var f end metavar infer lnot metavar var f end metavar infer metavar var f end metavar conclude metavar var f end metavar imply lnot metavar var f end metavar imply metavar var f end metavar cut pcmp modus ponens metavar var f end metavar modus ponens metavar var f end metavar imply lnot metavar var f end metavar imply metavar var f end metavar conclude lnot metavar var f end metavar imply metavar var f end metavar cut trivia conclude lnot metavar var f end metavar imply lnot metavar var f end metavar cut pc9 conclude lnot metavar var f end metavar imply metavar var f end metavar imply lnot metavar var f end metavar imply lnot metavar var f end metavar imply lnot lnot metavar var f end metavar cut pcmp modus ponens lnot metavar var f end metavar imply metavar var f end metavar modus ponens lnot metavar var f end metavar imply metavar var f end metavar imply lnot metavar var f end metavar imply lnot metavar var f end metavar imply lnot lnot metavar var f end metavar conclude lnot metavar var f end metavar imply lnot metavar var f end metavar imply lnot lnot metavar var f end metavar cut pcmp modus ponens lnot metavar var f end metavar imply lnot metavar var f end metavar modus ponens lnot metavar var f end metavar imply lnot metavar var f end metavar imply lnot lnot metavar var f end metavar conclude lnot lnot metavar var f end metavar end quote state proof state cache var c end expand end define end math ] "
\begin{Lem}
" [ math define statement of pbc as pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed lnot metavar var f end metavar infer metavar var g end metavar infer lnot metavar var f end metavar infer lnot metavar var g end metavar infer metavar var f end metavar end define end math ] "
\end{Lem}
" [ math define proof of pbc as lambda var c dot lambda var x dot proof expand quote pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed lnot metavar var f end metavar infer metavar var g end metavar infer lnot metavar var f end metavar infer lnot metavar var g end metavar infer notintro modus ponens lnot metavar var f end metavar infer metavar var g end metavar modus ponens lnot metavar var f end metavar infer lnot metavar var g end metavar conclude lnot lnot metavar var f end metavar cut notnotelim modus ponens lnot lnot metavar var f end metavar conclude metavar var f end metavar end quote state proof state cache var c end expand end define end math ] "
\subsection{Law of the Excluded Middle}
In this section we prove the \emph{Law of the Excluded Middle}.
\begin{The}\label{the:lem}
" [ math define statement of lem as pred calc infer all metavar var f end metavar indeed metavar var f end metavar lor lnot metavar var f end metavar end define end math ] "
\end{The}
" [ math define proof of lem as lambda var c dot lambda var x dot proof expand quote pred calc infer all metavar var f end metavar indeed all metavar var f end metavar indeed lnot metavar var f end metavar lor lnot metavar var f end metavar infer all metavar var f end metavar indeed metavar var f end metavar infer orintro1 modus ponens metavar var f end metavar conclude metavar var f end metavar lor lnot metavar var f end metavar cut pcdeduction modus ponens all metavar var f end metavar indeed metavar var f end metavar infer metavar var f end metavar lor lnot metavar var f end metavar conclude metavar var f end metavar infer metavar var f end metavar lor lnot metavar var f end metavar cut all metavar var f end metavar indeed metavar var f end metavar infer repeat modus ponens lnot metavar var f end metavar lor lnot metavar var f end metavar conclude lnot metavar var f end metavar lor lnot metavar var f end metavar cut pcdeduction modus ponens all metavar var f end metavar indeed metavar var f end metavar infer lnot metavar var f end metavar lor lnot metavar var f end metavar conclude metavar var f end metavar infer lnot metavar var f end metavar lor lnot metavar var f end metavar cut notintro modus ponens metavar var f end metavar infer metavar var f end metavar lor lnot metavar var f end metavar modus ponens metavar var f end metavar infer lnot metavar var f end metavar lor lnot metavar var f end metavar conclude lnot metavar var f end metavar cut orintro2 modus ponens lnot metavar var f end metavar conclude metavar var f end metavar lor lnot metavar var f end metavar cut pcdeduction modus ponens all metavar var f end metavar indeed lnot metavar var f end metavar lor lnot metavar var f end metavar infer metavar var f end metavar lor lnot metavar var f end metavar conclude lnot metavar var f end metavar lor lnot metavar var f end metavar infer metavar var f end metavar lor lnot metavar var f end metavar cut all metavar var f end metavar indeed lnot metavar var f end metavar lor lnot metavar var f end metavar infer repeat modus ponens lnot metavar var f end metavar lor lnot metavar var f end metavar conclude lnot metavar var f end metavar lor lnot metavar var f end metavar cut pcdeduction modus ponens all metavar var f end metavar indeed lnot metavar var f end metavar lor lnot metavar var f end metavar infer lnot metavar var f end metavar lor lnot metavar var f end metavar conclude lnot metavar var f end metavar lor lnot metavar var f end metavar infer lnot metavar var f end metavar lor lnot metavar var f end metavar cut notintro modus ponens lnot metavar var f end metavar lor lnot metavar var f end metavar infer metavar var f end metavar lor lnot metavar var f end metavar modus ponens lnot metavar var f end metavar lor lnot metavar var f end metavar infer lnot metavar var f end metavar lor lnot metavar var f end metavar conclude lnot lnot metavar var f end metavar lor lnot metavar var f end metavar cut notnotelim modus ponens lnot lnot metavar var f end metavar lor lnot metavar var f end metavar conclude metavar var f end metavar lor lnot metavar var f end metavar end quote state proof state cache var c end expand end define end math ] "
\subsection{A word on $\bot$}
The proof rules of natural deduction in \cite{huth} uses bottom.
Bottom represents the concept of unsoundness, that is it should be impossible to prove bottom in a sound logic.
The way to prove bottom would be to prove any absurdity that is for any proposition $A$ to prove both $A$ and not $A$. In \cite{huth}
this is captured in the proof rule $\frac{\lnot A \quad A}{\bot}$.
In \cite{huth} bottom is used in two ways. First if you under the assumption of a proposition $A$ can prove bottom then you can conclude that $A$ is false,
that is not $A$ is true. In \cite{hugh} this is captured by the proof rule $\frac{\begin{tiny}\begin{array}{c}A \\ \vdots \\ \bot\end{array}\end{tiny}}{\lnot A}$ (notelim).
This makes sense if we assume that the logical system is sound, because this means that it is free of absurdities, so if $A$ was true
it would be impossible to prove an absurdity thus $A$ must be false. Second the assumption of bottom can be used to conclude anything. In \cite{huth} this is
captured in the proof rule $\frac \bot A$ (botelim).
Since the predicate logic from Mathworld, which we have used as a basis for " [ math define statement of pred calc as all metavar var x end metavar indeed all metavar var r end metavar indeed all metavar var g end metavar indeed all metavar var f end metavar indeed quote metavar var x end metavar end quote avoid zero quote metavar var r end metavar end quote endorse quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote endorse sub zero quote metavar var g end metavar end quote is quote metavar var f end metavar end quote where quote metavar var x end metavar end quote is quote metavar var r end metavar end quote end sub endorse forall metavar var x end metavar dot metavar var f end metavar end forall imply metavar var g end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar imply metavar var g end metavar imply metavar var f end metavar land metavar var g end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar land metavar var g end metavar imply metavar var g end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar infer metavar var g end metavar infer metavar var f end metavar imply metavar var g end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar imply metavar var g end metavar imply metavar var f end metavar imply lnot metavar var g end metavar imply lnot metavar var f end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar imply metavar var g end metavar imply metavar var f end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed all metavar var x end metavar indeed quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote endorse metavar var f end metavar imply metavar var g end metavar infer exists metavar var x end metavar dot metavar var f end metavar end exists imply metavar var g end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar imply metavar var g end metavar lor metavar var f end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar infer metavar var f end metavar imply metavar var g end metavar infer metavar var g end metavar rule plus all metavar var f end metavar indeed lnot lnot metavar var f end metavar imply metavar var f end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed all metavar var h end metavar indeed metavar var f end metavar imply metavar var g end metavar imply metavar var f end metavar imply metavar var g end metavar imply metavar var h end metavar imply metavar var f end metavar imply metavar var h end metavar rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed lambda var x dot deduction zero quote metavar var a end metavar end quote conclude quote metavar var b end metavar end quote end deduction endorse metavar var a end metavar infer metavar var b end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar land metavar var g end metavar imply metavar var f end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed all metavar var h end metavar indeed metavar var f end metavar imply metavar var g end metavar imply metavar var h end metavar imply metavar var g end metavar imply metavar var f end metavar lor metavar var h end metavar imply metavar var g end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed all metavar var x end metavar indeed quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote endorse metavar var g end metavar imply metavar var f end metavar infer metavar var g end metavar imply forall metavar var x end metavar dot metavar var f end metavar end forall rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar imply metavar var f end metavar lor metavar var g end metavar rule plus all metavar var x end metavar indeed all metavar var r end metavar indeed all metavar var g end metavar indeed all metavar var f end metavar indeed quote metavar var x end metavar end quote avoid zero quote metavar var r end metavar end quote endorse quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote endorse sub zero quote metavar var g end metavar end quote is quote metavar var f end metavar end quote where quote metavar var x end metavar end quote is quote metavar var r end metavar end quote end sub endorse metavar var g end metavar imply exists metavar var x end metavar dot metavar var f end metavar end exists end define end math ] ", doesn't use or define the notion of bottom,
we cannot adopt the rules of natural deduction directly. We have chosen to solve this problem by replacing the problematic proof rules above with a new proof rule called
\emph{notintro}. This way we can avoid the use of bottom alltogether while we preserve the rest of the system.
To justify our actions we hand proof the following metatheorem:
\begin{The}
Let Nat' be the system of proof rules introduced in section \ref{sec:natded} and let Nat be the same sytem without the rule notintro but with rules notelim and botelim added.
Let $F$ be fixed and define $\bot\equiv F \land \lnot F$\footnotemark. The the following holds:
\begin{enumerate}
\item If $B$ can be proved in Nat' then B can be proved in Nat.
\item If $B$ can be proved in Nat then $B[\bot/F\land\lnot F]$ can be proved in Nat'.
\end{enumerate}
\end{The}
\footnotetext{$F$ must be fixed for all occurrences of bottom e.g. $\bot \land \bot$ must be translated to $(F \land \lnot F) \lor (F \land \lnot F)$ and can't be translated to $(F \land \lnot F) \lor (G \land \lnot G)$.}
\begin{proof}
Both claims in this metatheorem is proved by induction on the derivation of the proof on the left hand side of the implication.
To save space we only consider the interesting cases. Therefore we skil all of the lemmas the two systems have in common.
\\
\\
\textbf{Proof of 1:}\\
The rule $\frac{A \quad \lnot A}{\bot}$. \\
Given proofs of $A$ and $\lnot A$ we need to prove $F \land \lnot F$.
Using the induction hypothesis on the proofs of $A$ and $\lnot A$, we get proofs of $A'$ and $\lnot A'$ using our system of lemmas.
Now we have proofs of $A'$ and $\lnot A'$, which means that we can also prove $A'$ and $\lnot A'$ using $F$ or $\lnot F$ as assumptions.
Now we can construct the proof of $F \land \lnot F$ like this.
$$
\frac
{\frac
{\frac
{
\begin{array}{c}
\lnot F \\
\vdots \\
A'
\end{array}
\quad
\begin{array}{c}
\lnot F \\
\vdots \\
\lnot A'
\end{array}
}
{\lnot \lnot F}
}
{F}
\frac
{
\begin{array}{c}
F \\
\vdots \\
A'
\end{array}
\quad
\begin{array}{c}
F \\
\vdots \\
\lnot A'
\end{array}
}
{\lnot F}
}
{F \land \lnot F}
$$
%
The rule $\frac{\bot}{A}$. \\
Given proof of $F \land \lnot F$ we need to prove $A$.
Using the induction hypothesis on the proof of $F \land \lnot F$, which means that we can also construct proofs of $F$ and $\lnot F$ using the andelim1 and andelim2 rules. Finally we can prove $F$ and $\lnot F$ under the assumption of $\lnot A$.
Now we can construct the proof of $A$ like this.
$$
\frac
{\frac
{
\frac
{\begin{array}{c}
A' \\
\vdots \\
F \land \lnot F
\end{array}
}
{F}
\quad
\frac
{\begin{array}{c}
A' \\
\vdots \\
F \land \lnot F
\end{array}
}
{\lnot F}
}
{\lnot \lnot A'}
}
{A'}
$$
%
The rule $\frac{A \vdash \bot}{\lnot A}$.
Using the induction hypothesis on the proof of $A \vdash \bot$ we obtain a proof of $A' \vdash F \land \lnot F$.
Using the andelim1 and andelim2 lemmas, we get proofs of $A' \vdash F$ and $A' \vdash \lnot F$.
Now we can construct the proof of $\lnot A'$ like this.
$$
\frac
{
\frac
{\begin{array}{c}
A' \\
\vdots \\
F \land \lnot F
\end{array}
}
{F}
\quad
\frac
{\begin{array}{c}
A' \\
\vdots \\
F \land \lnot F
\end{array}
}
{\lnot F}
}
{\lnot A'}
$$
That concludes all the interesting rules. The other rules follow by using the induction hypothesis on the given proofs, and using the same rule to conclude the desired proposition.
\\
\\
\textbf{Proof of 2:}\\
There is only one interesting rule, and that is notintro.
Given the proofs of $A \vdash B$ and $A \vdash \lnot B$ we wish to prove $\lnot A$.
We construct the proof like this.
$$
\frac
{\frac
{\begin{array}{c}
A \\
\vdots \\
B
\end{array}
\begin{array}{c}
A \\
\vdots \\
\lnot B
\end{array}
}
{\bot}
}
{\lnot A}
$$
That concludes all the interesting rules. The other rules follow by using the induction hypothesis on the given proofs, and using the same rule to conclude the desired proposition.
% }}}
\end{proof}
\subsubsection{A practical lemma}
We saw that $\bot$ could be replaced with $A \land \lnot A$ above and that the proof rule botelim allows us to conclude anything once we have $\bot$. This gives rise to the
following very usefull lemma.
\begin{Lem}
" [ math define statement of bottomelim as pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar land lnot metavar var f end metavar infer metavar var g end metavar end define end math ] "
\end{Lem}
" [ math define proof of bottomelim as lambda var c dot lambda var x dot proof expand quote pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar land lnot metavar var f end metavar infer all metavar var f end metavar indeed all metavar var g end metavar indeed lnot metavar var g end metavar infer andelim1 modus ponens metavar var f end metavar land lnot metavar var f end metavar conclude metavar var f end metavar cut pcdeduction modus ponens all metavar var f end metavar indeed all metavar var g end metavar indeed lnot metavar var g end metavar infer metavar var f end metavar conclude lnot metavar var g end metavar infer metavar var f end metavar cut all metavar var f end metavar indeed all metavar var g end metavar indeed lnot metavar var g end metavar infer andelim2 modus ponens metavar var f end metavar land lnot metavar var f end metavar conclude lnot metavar var f end metavar cut pcdeduction modus ponens all metavar var f end metavar indeed all metavar var g end metavar indeed lnot metavar var g end metavar infer lnot metavar var f end metavar conclude lnot metavar var g end metavar infer lnot metavar var f end metavar cut notintro modus ponens lnot metavar var g end metavar infer metavar var f end metavar modus ponens lnot metavar var g end metavar infer lnot metavar var f end metavar conclude lnot lnot metavar var g end metavar cut notnotelim modus ponens lnot lnot metavar var g end metavar conclude metavar var g end metavar end quote state proof state cache var c end expand end define end math ] "
\begin{Lem}
" [ math define statement of lemnotintro as pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar imply metavar var g end metavar land lnot metavar var g end metavar infer lnot metavar var f end metavar end define end math ] "
\end{Lem}
" [ math define proof of lemnotintro as lambda var c dot lambda var x dot proof expand quote pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar imply metavar var g end metavar land lnot metavar var g end metavar infer all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar infer pcmp modus ponens metavar var f end metavar modus ponens metavar var f end metavar imply metavar var g end metavar land lnot metavar var g end metavar conclude metavar var g end metavar land lnot metavar var g end metavar cut andelim1 modus ponens metavar var g end metavar land lnot metavar var g end metavar conclude metavar var g end metavar cut pcdeduction modus ponens all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar infer metavar var g end metavar conclude metavar var f end metavar infer metavar var g end metavar cut all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar infer pcmp modus ponens metavar var f end metavar modus ponens metavar var f end metavar imply metavar var g end metavar land lnot metavar var g end metavar conclude metavar var g end metavar land lnot metavar var g end metavar cut andelim2 modus ponens metavar var g end metavar land lnot metavar var g end metavar conclude lnot metavar var g end metavar cut pcdeduction modus ponens all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar infer lnot metavar var g end metavar conclude metavar var f end metavar infer lnot metavar var g end metavar cut notintro modus ponens metavar var f end metavar infer metavar var g end metavar modus ponens metavar var f end metavar infer lnot metavar var g end metavar conclude lnot metavar var f end metavar end quote state proof state cache var c end expand end define end math ] "
TO HERE OK.
Finally we note that in first order predicate calculus metavariables used in functions $F$ and predicates $P$ are \emph{object metavariables}.
\subsection{Deduction lemma}
\begin{Lem}
" [ math define statement of pcded as pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar infer metavar var g end metavar infer metavar var f end metavar imply metavar var g end metavar end define , define proof of pcded as rule tactic end define end math ] "
\end{Lem}
\begin{Lem}
" [ math define statement of iatest as pred calc infer all metavar var g end metavar indeed all metavar var y end metavar indeed quote metavar var y end metavar end quote avoid zero quote metavar var g end metavar end quote endorse metavar var g end metavar imply forall metavar var y end metavar dot metavar var y end metavar imply metavar var g end metavar end forall end define end math ] "
\end{Lem}
" [ math define proof of iatest as lambda var c dot lambda var x dot proof expand quote pred calc infer all metavar var g end metavar indeed all metavar var y end metavar indeed quote metavar var y end metavar end quote avoid zero quote metavar var g end metavar end quote endorse pc1 conclude metavar var g end metavar imply metavar var y end metavar imply metavar var g end metavar cut pcia modus probans quote metavar var y end metavar end quote avoid zero quote metavar var g end metavar end quote modus ponens metavar var g end metavar imply metavar var y end metavar imply metavar var g end metavar conclude metavar var g end metavar imply forall metavar var y end metavar dot metavar var y end metavar imply metavar var g end metavar end forall end quote state proof state cache var c end expand end define end math ] "
\section{A nontrivial sequent}\label{sec:higherproof}
\begin{Lem}
" [ math define statement of nontriv0 as pred calc infer all metavar var p end metavar indeed all metavar var q end metavar indeed metavar var p end metavar imply metavar var q end metavar imply metavar var q end metavar infer metavar var q end metavar imply metavar var p end metavar infer metavar var p end metavar imply metavar var q end metavar infer metavar var p end metavar end define end math ] "
\end{Lem}
" [ math define proof of nontriv0 as lambda var c dot lambda var x dot proof expand quote pred calc infer all metavar var p end metavar indeed all metavar var q end metavar indeed metavar var p end metavar imply metavar var q end metavar imply metavar var q end metavar infer metavar var q end metavar imply metavar var p end metavar infer metavar var p end metavar imply metavar var q end metavar infer pcmp modus ponens metavar var p end metavar imply metavar var q end metavar modus ponens metavar var p end metavar imply metavar var q end metavar imply metavar var q end metavar conclude metavar var q end metavar cut pcmp modus ponens metavar var q end metavar modus ponens metavar var q end metavar imply metavar var p end metavar conclude metavar var p end metavar end quote state proof state cache var c end expand end define end math ] "
\begin{Lem}
" [ math define statement of nontriv1 as pred calc infer all metavar var p end metavar indeed all metavar var q end metavar indeed metavar var p end metavar infer lnot metavar var p end metavar infer metavar var q end metavar end define end math ] "
\end{Lem}
" [ math define proof of nontriv1 as lambda var c dot lambda var x dot proof expand quote pred calc infer all metavar var p end metavar indeed all metavar var q end metavar indeed metavar var p end metavar infer lnot metavar var p end metavar infer andintro modus ponens metavar var p end metavar modus ponens lnot metavar var p end metavar conclude metavar var p end metavar land lnot metavar var p end metavar cut bottomelim modus ponens metavar var p end metavar land lnot metavar var p end metavar conclude metavar var q end metavar end quote state proof state cache var c end expand end define end math ] "
\begin{Lem}
" [ math define statement of nontriv2 as pred calc infer all metavar var p end metavar indeed all metavar var q end metavar indeed lnot metavar var p end metavar imply metavar var q end metavar infer lnot metavar var p end metavar infer metavar var p end metavar imply metavar var q end metavar land lnot metavar var p end metavar imply metavar var q end metavar end define end math ] "
\end{Lem}
" [ math define proof of nontriv2 as lambda var c dot lambda var x dot proof expand quote pred calc infer all metavar var p end metavar indeed all metavar var q end metavar indeed lnot metavar var p end metavar imply metavar var q end metavar infer lnot metavar var p end metavar infer all metavar var p end metavar indeed all metavar var q end metavar indeed metavar var p end metavar infer nontriv1 modus ponens metavar var p end metavar modus ponens lnot metavar var p end metavar conclude metavar var q end metavar cut pcdeduction modus ponens all metavar var p end metavar indeed all metavar var q end metavar indeed metavar var p end metavar infer metavar var q end metavar conclude metavar var p end metavar imply metavar var q end metavar cut andintro modus ponens metavar var p end metavar imply metavar var q end metavar modus ponens lnot metavar var p end metavar imply metavar var q end metavar conclude metavar var p end metavar imply metavar var q end metavar land lnot metavar var p end metavar imply metavar var q end metavar end quote state proof state cache var c end expand end define end math ] "
\begin{Lem}
" [ math define statement of nontriv3 as pred calc infer all metavar var p end metavar indeed all metavar var q end metavar indeed lnot metavar var p end metavar imply metavar var q end metavar infer metavar var p end metavar end define end math ] "
\end{Lem}
" [ math define proof of nontriv3 as lambda var c dot lambda var x dot proof expand quote pred calc infer all metavar var p end metavar indeed all metavar var q end metavar indeed lnot metavar var p end metavar imply metavar var q end metavar infer all metavar var p end metavar indeed all metavar var q end metavar indeed lnot metavar var p end metavar infer nontriv2 modus ponens lnot metavar var p end metavar imply metavar var q end metavar modus ponens lnot metavar var p end metavar conclude metavar var p end metavar imply metavar var q end metavar land lnot metavar var p end metavar imply metavar var q end metavar cut pcdeduction modus ponens all metavar var p end metavar indeed all metavar var q end metavar indeed lnot metavar var p end metavar infer metavar var p end metavar imply metavar var q end metavar land lnot metavar var p end metavar imply metavar var q end metavar conclude lnot metavar var p end metavar imply metavar var p end metavar imply metavar var q end metavar land lnot metavar var p end metavar imply metavar var q end metavar cut lemnotintro modus ponens lnot metavar var p end metavar imply metavar var p end metavar imply metavar var q end metavar land lnot metavar var p end metavar imply metavar var q end metavar conclude lnot lnot metavar var p end metavar cut notnotelim modus ponens lnot lnot metavar var p end metavar conclude metavar var p end metavar end quote state proof state cache var c end expand end define end math ] "
\begin{Lem}
" [ math define statement of nontriv4 as pred calc infer all metavar var p end metavar indeed all metavar var q end metavar indeed metavar var p end metavar imply metavar var q end metavar imply metavar var q end metavar infer metavar var q end metavar imply metavar var p end metavar infer metavar var p end metavar end define end math ] "
\end{Lem}
" [ math define proof of nontriv4 as lambda var c dot lambda var x dot proof expand quote pred calc infer all metavar var p end metavar indeed all metavar var q end metavar indeed metavar var p end metavar imply metavar var q end metavar imply metavar var q end metavar infer metavar var q end metavar imply metavar var p end metavar infer all metavar var p end metavar indeed all metavar var q end metavar indeed metavar var p end metavar imply metavar var q end metavar infer nontriv0 modus ponens metavar var p end metavar imply metavar var q end metavar imply metavar var q end metavar modus ponens metavar var q end metavar imply metavar var p end metavar modus ponens metavar var p end metavar imply metavar var q end metavar conclude metavar var p end metavar cut pcdeduction modus ponens all metavar var p end metavar indeed all metavar var q end metavar indeed metavar var p end metavar imply metavar var q end metavar infer metavar var p end metavar conclude metavar var q end metavar imply metavar var q end metavar infer metavar var p end metavar cut all metavar var p end metavar indeed all metavar var q end metavar indeed lnot metavar var p end metavar imply metavar var q end metavar infer nontriv3 modus ponens lnot metavar var p end metavar imply metavar var q end metavar conclude metavar var p end metavar cut pcdeduction modus ponens all metavar var p end metavar indeed all metavar var q end metavar indeed lnot metavar var p end metavar imply metavar var q end metavar infer metavar var p end metavar conclude lnot metavar var p end metavar imply metavar var q end metavar infer metavar var p end metavar cut orelim modus ponens metavar var q end metavar imply metavar var q end metavar infer metavar var p end metavar modus ponens lnot metavar var p end metavar imply metavar var q end metavar infer metavar var p end metavar conclude metavar var p end metavar end quote state proof state cache var c end expand end define end math ] "
\begin{appendix}
\section{Pyk definitions}
\begin{flushleft}
" [ math define pyk of ell aa as text "ell aa" end text end define linebreak define pyk of ell ab as text "ell ab" end text end define linebreak define pyk of ell ac as text "ell ac" end text end define linebreak define pyk of ell ad as text "ell ad" end text end define linebreak define pyk of ell ae as text "ell ae" end text end define linebreak define pyk of ell af as text "ell af" end text end define linebreak define pyk of ell ag as text "ell ag" end text end define linebreak define pyk of ell ah as text "ell ah" end text end define linebreak define pyk of ell ai as text "ell ai" end text end define linebreak define pyk of ell aj as text "ell aj" end text end define linebreak define pyk of ell ak as text "ell ak" end text end define linebreak define pyk of ell al as text "ell al" end text end define linebreak define pyk of ell am as text "ell am" end text end define linebreak define pyk of ell an as text "ell an" end text end define linebreak define pyk of ell ao as text "ell ao" end text end define linebreak define pyk of ell ap as text "ell ap" end text end define linebreak define pyk of ell aq as text "ell aq" end text end define linebreak define pyk of ell ar as text "ell ar" end text end define linebreak define pyk of ell as as text "ell as" end text end define linebreak define pyk of pred calc as text "pred calc" end text end define linebreak define pyk of pc1 as text "pc1" end text end define linebreak define pyk of pc2 as text "pc2" end text end define linebreak define pyk of pc3 as text "pc3" end text end define linebreak define pyk of pc4 as text "pc4" end text end define linebreak define pyk of pc5 as text "pc5" end text end define linebreak define pyk of pc6 as text "pc6" end text end define linebreak define pyk of pc7 as text "pc7" end text end define linebreak define pyk of pc8 as text "pc8" end text end define linebreak define pyk of pc9 as text "pc9" end text end define linebreak define pyk of pc10 as text "pc10" end text end define linebreak define pyk of pc11 as text "pc11" end text end define linebreak define pyk of pc12 as text "pc12" end text end define linebreak define pyk of pcmp as text "pcmp" end text end define linebreak define pyk of pcunsound as text "pcunsound" end text end define linebreak define pyk of pcded as text "pcded" end text end define linebreak define pyk of pcia as text "pcia" end text end define linebreak define pyk of pcie as text "pcie" end text end define linebreak define pyk of pcdeduction as text "pcdeduction" end text end define linebreak define pyk of trivia as text "trivia" end text end define linebreak define pyk of trivia2 as text "trivia2" end text end define linebreak define pyk of iatest as text "iatest" end text end define linebreak define pyk of andintro as text "andintro" end text end define linebreak define pyk of andelim1 as text "andelim1" end text end define linebreak define pyk of andelim2 as text "andelim2" end text end define linebreak define pyk of orintro1 as text "orintro1" end text end define linebreak define pyk of orintro2 as text "orintro2" end text end define linebreak define pyk of orelim as text "orelim" end text end define linebreak define pyk of notintro as text "notintro" end text end define linebreak define pyk of notnotintro as text "notnotintro" end text end define linebreak define pyk of notnotelim as text "notnotelim" end text end define linebreak define pyk of mt as text "mt" end text end define linebreak define pyk of pbc as text "pbc" end text end define linebreak define pyk of repeat as text "repeat" end text end define linebreak define pyk of lem as text "lem" end text end define linebreak define pyk of forallintro as text "forallintro" end text end define linebreak define pyk of forallelim as text "forallelim" end text end define linebreak define pyk of existsintro as text "existsintro" end text end define linebreak define pyk of existselim as text "existselim" end text end define linebreak define pyk of bottomelim as text "bottomelim" end text end define linebreak define pyk of lemnotintro as text "lemnotintro" end text end define linebreak define pyk of nontriv0 as text "nontriv0" end text end define linebreak define pyk of nontriv1 as text "nontriv1" end text end define linebreak define pyk of nontriv2 as text "nontriv2" end text end define linebreak define pyk of nontriv3 as text "nontriv3" end text end define linebreak define pyk of nontriv4 as text "nontriv4" end text end define linebreak define pyk of nontriv5 as text "nontriv5" end text end define linebreak define pyk of nontriv6 as text "nontriv6" end text end define linebreak define pyk of x setequiv x as text ""! setequiv "!" end text end define linebreak define pyk of x setequals x as text ""! setequals "!" end text end define linebreak define pyk of lnot x as text "lnot "!" end text end define linebreak define pyk of x land x as text ""! land "!" end text end define linebreak define pyk of x lor x as text ""! lor "!" end text end define linebreak define pyk of forall x dot x end forall as text "forall "! dot "! end forall" end text end define linebreak define pyk of exists x dot x end exists as text "exists "! dot "! end exists" end text end define linebreak define pyk of x setin x as text ""! setin "!" end text end define linebreak define pyk of problemtwo as text "problemtwo" end text end define linebreak unicode end of text end math ] "
\end{flushleft}
\section{Tex definitions}
\begin{itemize}
\item " [ math define tex of lnot var x as text "\neg #1." end text end define end math ] "
\item " [ math define tex of var x land var y as text "#1. \wedge #2." end text end define end math ] "
\item " [ math define tex of var x lor var y as text "#1. \vee #2." end text end define end math ] "
\item " [ math define tex of var x imply var y as text "#1. \Rightarrow #2." end text end define end math ] "
\item " [ math define tex of forall var y dot var b end forall as text "\forall #1. . \left(#2.\right)" end text end define end math ] "
\item " [ math define tex of exists var y dot var b end exists as text "\exists #1. . \left(#2.\right)" end text end define end math ] "
\item " [ math define tex of var y setin var b as text "#1. \in #2." end text end define end math ] "
\item " [ math define tex of var y setequiv var b as text "#1. \equiv #2." end text end define end math ] "
\item " [ math define tex of var y setequals var b as text "#1. = #2." end text end define end math ] "
\end{itemize}
\section{Extra proof line numbers}
" [ math define tex of ell aa as text "
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi " end text end define end math ] "
" [ math define tex of ell ab as text "
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi " end text end define end math ] "
" [ math define tex of ell ac as text "
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi " end text end define end math ] "
" [ math define tex of ell ad as text "
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi " end text end define end math ] "
" [ math define tex of ell ae as text "
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi " end text end define end math ] "
" [ math define tex of ell af as text "
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi " end text end define end math ] "
" [ math define tex of ell ag as text "
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi " end text end define end math ] "
" [ math define tex of ell ah as text "
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi " end text end define end math ] "
" [ math define tex of ell ai as text "
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi " end text end define end math ] "
" [ math define tex of ell aj as text "
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi " end text end define end math ] "
" [ math define tex of ell ak as text "
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi " end text end define end math ] "
" [ math define tex of ell al as text "
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi " end text end define end math ] "
" [ math define tex of ell am as text "
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi " end text end define end math ] "
" [ math define tex of ell an as text "
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi " end text end define end math ] "
" [ math define tex of ell ao as text "
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi " end text end define end math ] "
" [ math define tex of ell ap as text "
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi " end text end define end math ] "
" [ math define tex of ell aq as text "
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi " end text end define end math ] "
" [ math define tex of ell ar as text "
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi " end text end define end math ] "
" [ math define tex of ell as as text "
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi " end text end define end math ] "
\section{Priority table}
" [ flush left math define priority of problemtwo as preassociative priority problemtwo equal priority base equal priority bracket x end bracket equal priority big bracket x end bracket equal priority math x end math equal priority flush left x end left equal priority var x equal priority var y equal priority var z equal priority proclaim x as x end proclaim equal priority define x of x as x end define equal priority pyk equal priority tex equal priority tex name equal priority priority equal priority x equal priority true equal priority if x then x else x end if equal priority introduce x of x as x end introduce equal priority value equal priority claim equal priority bottom equal priority function f of x end function equal priority identity x end identity equal priority false equal priority untagged zero equal priority untagged one equal priority untagged two equal priority untagged three equal priority untagged four equal priority untagged five equal priority untagged six equal priority untagged seven equal priority untagged eight equal priority untagged nine equal priority zero equal priority one equal priority two equal priority three equal priority four equal priority five equal priority six equal priority seven equal priority eight equal priority nine equal priority var a equal priority var b equal priority var c equal priority var d equal priority var e equal priority var f equal priority var g equal priority var h equal priority var i equal priority var j equal priority var k equal priority var l equal priority var m equal priority var n equal priority var o equal priority var p equal priority var q equal priority var r equal priority var s equal priority var t equal priority var u equal priority var v equal priority var w equal priority tagged parenthesis x end tagged equal priority tagged if x then x else x end if equal priority array x is x end array equal priority left equal priority center equal priority right equal priority empty equal priority substitute x set x to x end substitute equal priority map tag x end tag equal priority raw map untag x end untag equal priority map untag x end untag equal priority normalizing untag x end untag equal priority apply x to x end apply equal priority apply one x to x end apply equal priority identifier x end identifier equal priority identifier one x plus id x end identifier equal priority array plus x and x end plus equal priority array remove x array x level x end remove equal priority array put x value x array x level x end put equal priority array add x value x index x value x level x end add equal priority bit x of x end bit equal priority bit one x of x end bit equal priority example rack equal priority vector hook equal priority bibliography hook equal priority dictionary hook equal priority body hook equal priority codex hook equal priority expansion hook equal priority code hook equal priority cache hook equal priority diagnose hook equal priority pyk aspect equal priority tex aspect equal priority texname aspect equal priority value aspect equal priority message aspect equal priority macro aspect equal priority definition aspect equal priority unpack aspect equal priority claim aspect equal priority priority aspect equal priority lambda identifier equal priority apply identifier equal priority true identifier equal priority if identifier equal priority quote identifier equal priority proclaim identifier equal priority define identifier equal priority introduce identifier equal priority hide identifier equal priority pre identifier equal priority post identifier equal priority eval x stack x cache x end eval equal priority eval two x ref x id x stack x cache x end eval equal priority eval three x function x stack x cache x end eval equal priority eval four x arguments x stack x cache x end eval equal priority lookup x stack x default x end lookup equal priority abstract x term x stack x cache x end abstract equal priority quote x end quote equal priority expand x state x cache x end expand equal priority expand two x definition x state x cache x end expand equal priority expand list x state x cache x end expand equal priority macro equal priority macro state equal priority zip x with x end zip equal priority assoc one x address x index x end assoc equal priority protect x end protect equal priority self equal priority macro define x as x end define equal priority value define x as x end define equal priority intro define x as x end define equal priority pyk define x as x end define equal priority tex define x as x end define equal priority tex name define x as x end define equal priority priority table x end table equal priority macro define one equal priority macro define two x end define equal priority macro define three x end define equal priority macro define four x state x cache x definition x end define equal priority state expand x state x cache x end expand equal priority quote expand x term x stack x end expand equal priority quote expand two x term x stack x end expand equal priority quote expand three x term x stack x value x end expand equal priority quote expand star x term x stack x end expand equal priority parenthesis x end parenthesis equal priority big parenthesis x end parenthesis equal priority display x end display equal priority statement x end statement equal priority spying test x end test equal priority false spying test x end test equal priority aspect x subcodex x end aspect equal priority aspect x term x cache x end aspect equal priority tuple x end tuple equal priority tuple one x end tuple equal priority tuple two x end tuple equal priority let two x apply x end let equal priority let one x apply x end let equal priority claim define x as x end define equal priority checker equal priority check x cache x end check equal priority check two x cache x def x end check equal priority check three x cache x def x end check equal priority check list x cache x end check equal priority check list two x cache x value x end check equal priority test x end test equal priority false test x end test equal priority raw test x end test equal priority message equal priority message define x as x end define equal priority the statement aspect equal priority statement equal priority statement define x as x end define equal priority example axiom equal priority example scheme equal priority example rule equal priority absurdity equal priority contraexample equal priority example theory primed equal priority example lemma equal priority metavar x end metavar equal priority meta a equal priority meta b equal priority meta c equal priority meta d equal priority meta e equal priority meta f equal priority meta g equal priority meta h equal priority meta i equal priority meta j equal priority meta k equal priority meta l equal priority meta m equal priority meta n equal priority meta o equal priority meta p equal priority meta q equal priority meta r equal priority meta s equal priority meta t equal priority meta u equal priority meta v equal priority meta w equal priority meta x equal priority meta y equal priority meta z equal priority sub x set x to x end sub equal priority sub star x set x to x end sub equal priority the empty set equal priority example remainder equal priority make visible x end visible equal priority intro x index x pyk x tex x end intro equal priority intro x pyk x tex x end intro equal priority error x term x end error equal priority error two x term x end error equal priority proof x term x cache x end proof equal priority proof two x term x end proof equal priority sequent eval x term x end eval equal priority seqeval init x term x end eval equal priority seqeval modus x term x end eval equal priority seqeval modus one x term x sequent x end eval equal priority seqeval verify x term x end eval equal priority seqeval verify one x term x sequent x end eval equal priority sequent eval plus x term x end eval equal priority seqeval plus one x term x sequent x end eval equal priority seqeval minus x term x end eval equal priority seqeval minus one x term x sequent x end eval equal priority seqeval deref x term x end eval equal priority seqeval deref one x term x sequent x end eval equal priority seqeval deref two x term x sequent x def x end eval equal priority seqeval at x term x end eval equal priority seqeval at one x term x sequent x end eval equal priority seqeval infer x term x end eval equal priority seqeval infer one x term x premise x sequent x end eval equal priority seqeval endorse x term x end eval equal priority seqeval endorse one x term x side x sequent x end eval equal priority seqeval est x term x end eval equal priority seqeval est one x term x name x sequent x end eval equal priority seqeval est two x term x name x sequent x def x end eval equal priority seqeval all x term x end eval equal priority seqeval all one x term x variable x sequent x end eval equal priority seqeval cut x term x end eval equal priority seqeval cut one x term x forerunner x end eval equal priority seqeval cut two x term x forerunner x sequent x end eval equal priority computably true x end true equal priority claims x cache x ref x end claims equal priority claims two x cache x ref x end claims equal priority the proof aspect equal priority proof equal priority lemma x says x end lemma equal priority proof of x reads x end proof equal priority in theory x lemma x says x end lemma equal priority in theory x antilemma x says x end antilemma equal priority in theory x rule x says x end rule equal priority in theory x antirule x says x end antirule equal priority verifier equal priority verify one x end verify equal priority verify two x proofs x end verify equal priority verify three x ref x sequents x diagnose x end verify equal priority verify four x premises x end verify equal priority verify five x ref x array x sequents x end verify equal priority verify six x ref x list x sequents x end verify equal priority verify seven x ref x id x sequents x end verify equal priority cut x and x end cut equal priority head x end head equal priority tail x end tail equal priority rule one x theory x end rule equal priority rule x subcodex x end rule equal priority rule tactic equal priority plus x and x end plus equal priority theory x end theory equal priority theory two x cache x end theory equal priority theory three x name x end theory equal priority theory four x name x sum x end theory equal priority example axiom lemma primed equal priority example scheme lemma primed equal priority example rule lemma primed equal priority contraexample lemma primed equal priority example axiom lemma equal priority example scheme lemma equal priority example rule lemma equal priority contraexample lemma equal priority example theory equal priority ragged right equal priority ragged right expansion equal priority parameter term x stack x seed x end parameter equal priority parameter term star x stack x seed x end parameter equal priority instantiate x with x end instantiate equal priority instantiate star x with x end instantiate equal priority occur x in x substitution x end occur equal priority occur star x in x substitution x end occur equal priority unify x with x substitution x end unify equal priority unify star x with x substitution x end unify equal priority unify two x with x substitution x end unify equal priority ell a equal priority ell b equal priority ell c equal priority ell d equal priority ell e equal priority ell f equal priority ell g equal priority ell h equal priority ell i equal priority ell j equal priority ell k equal priority ell l equal priority ell m equal priority ell n equal priority ell o equal priority ell p equal priority ell q equal priority ell r equal priority ell s equal priority ell t equal priority ell u equal priority ell v equal priority ell w equal priority ell x equal priority ell y equal priority ell z equal priority ell big a equal priority ell big b equal priority ell big c equal priority ell big d equal priority ell big e equal priority ell big f equal priority ell big g equal priority ell big h equal priority ell big i equal priority ell big j equal priority ell big k equal priority ell big l equal priority ell big m equal priority ell big n equal priority ell big o equal priority ell big p equal priority ell big q equal priority ell big r equal priority ell big s equal priority ell big t equal priority ell big u equal priority ell big v equal priority ell big w equal priority ell big x equal priority ell big y equal priority ell big z equal priority ell dummy equal priority sequent reflexivity equal priority tactic reflexivity equal priority sequent commutativity equal priority tactic commutativity equal priority the tactic aspect equal priority tactic equal priority tactic define x as x end define equal priority proof expand x state x cache x end expand equal priority proof expand list x state x cache x end expand equal priority proof state equal priority conclude one x cache x end conclude equal priority conclude two x proves x cache x end conclude equal priority conclude three x proves x lemma x substitution x end conclude equal priority conclude four x lemma x end conclude equal priority ell aa equal priority ell ab equal priority ell ac equal priority ell ad equal priority ell ae equal priority ell af equal priority ell ag equal priority ell ah equal priority ell ai equal priority ell aj equal priority ell ak equal priority ell al equal priority ell am equal priority ell an equal priority ell ao equal priority ell ap equal priority ell aq equal priority ell ar equal priority ell as equal priority check equal priority general macro define x as x end define equal priority make root visible x end visible equal priority sequent example axiom equal priority sequent example rule equal priority sequent example contradiction equal priority sequent example theory equal priority sequent example lemma equal priority set x end set equal priority object var x end var equal priority object a equal priority object b equal priority object c equal priority object d equal priority object e equal priority object f equal priority object g equal priority object h equal priority object i equal priority object j equal priority object k equal priority object l equal priority object m equal priority object n equal priority object o equal priority object p equal priority object q equal priority object r equal priority object s equal priority object t equal priority object u equal priority object v equal priority object w equal priority object x equal priority object y equal priority object z equal priority sub x is x where x is x end sub equal priority sub zero x is x where x is x end sub equal priority sub one x is x where x is x end sub equal priority sub star x is x where x is x end sub equal priority deduction x conclude x end deduction equal priority deduction zero x conclude x end deduction equal priority deduction one x conclude x condition x end deduction equal priority deduction two x conclude x condition x end deduction equal priority deduction three x conclude x condition x bound x end deduction equal priority deduction four x conclude x condition x bound x end deduction equal priority deduction four star x conclude x condition x bound x end deduction equal priority deduction five x condition x bound x end deduction equal priority deduction six x conclude x exception x bound x end deduction equal priority deduction six star x conclude x exception x bound x end deduction equal priority deduction seven x end deduction equal priority deduction eight x bound x end deduction equal priority deduction eight star x bound x end deduction equal priority system s equal priority double negation equal priority rule mp equal priority rule gen equal priority deduction equal priority axiom s one equal priority axiom s two equal priority axiom s three equal priority axiom s four equal priority axiom s five equal priority axiom s six equal priority axiom s seven equal priority axiom s eight equal priority axiom s nine equal priority repetition equal priority lemma a one equal priority lemma a two equal priority lemma a four equal priority lemma a five equal priority prop three two a equal priority prop three two b equal priority prop three two c equal priority prop three two d equal priority prop three two e one equal priority prop three two e two equal priority prop three two e equal priority prop three two f one equal priority prop three two f two equal priority prop three two f equal priority prop three two g one equal priority prop three two g two equal priority prop three two g equal priority prop three two h one equal priority prop three two h two equal priority prop three two h equal priority block one x state x cache x end block equal priority block two x end block equal priority pred calc equal priority pc1 equal priority pc2 equal priority pc3 equal priority pc4 equal priority pc5 equal priority pc6 equal priority pc7 equal priority pc8 equal priority pc9 equal priority pc10 equal priority pc11 equal priority pc12 equal priority pcmp equal priority pcunsound equal priority pcded equal priority pcia equal priority pcie equal priority pcdeduction equal priority trivia equal priority trivia2 equal priority iatest equal priority andintro equal priority andelim1 equal priority andelim2 equal priority orintro1 equal priority orintro2 equal priority orelim equal priority notintro equal priority notnotintro equal priority notnotelim equal priority mt equal priority pbc equal priority repeat equal priority lem equal priority forallintro equal priority forallelim equal priority existsintro equal priority existselim equal priority bottomelim equal priority lemnotintro equal priority nontriv0 equal priority nontriv1 equal priority nontriv2 equal priority nontriv3 equal priority nontriv4 equal priority nontriv5 equal priority nontriv6 end priority greater than preassociative priority x sub x end sub equal priority x intro x index x pyk x tex x end intro equal priority x intro x pyk x tex x end intro equal priority x intro x index x pyk x tex x name x end intro equal priority x intro x pyk x tex x name x end intro equal priority x prime equal priority x assoc x end assoc equal priority x set x to x end set equal priority x set multi x to x end set equal priority x bit nil equal priority x bit one equal priority binary equal priority x color x end color equal priority x color star x end color equal priority x raw head equal priority x raw tail equal priority x cardinal untag equal priority x head equal priority x tail equal priority x is singular equal priority x is cardinal equal priority x is data equal priority x is atomic equal priority x cardinal retract equal priority x tagged retract equal priority x boolean retract equal priority x ref equal priority x id equal priority x debug equal priority x root equal priority x zeroth equal priority x first equal priority x second equal priority x third equal priority x fourth equal priority x fifth equal priority x sixth equal priority x seventh equal priority x eighth equal priority x ninth equal priority x is error equal priority x is metavar equal priority x is metaclosed equal priority x is metaclosed star equal priority x hide end priority greater than preassociative priority unicode start of text x end unicode text equal priority unicode end of text equal priority text x end text equal priority text x plus x equal priority text x plus indent x equal priority unicode newline x equal priority unicode space x equal priority unicode exclamation mark x equal priority unicode quotation mark x equal priority unicode number sign x equal priority unicode dollar sign x equal priority unicode percent x equal priority unicode ampersand x equal priority unicode apostrophe x equal priority unicode left parenthesis x equal priority unicode right parenthesis x equal priority unicode asterisk x equal priority unicode plus sign x equal priority unicode comma x equal priority unicode hyphen x equal priority unicode period x equal priority unicode slash x equal priority unicode zero x equal priority unicode one x equal priority unicode two x equal priority unicode three x equal priority unicode four x equal priority unicode five x equal priority unicode six x equal priority unicode seven x equal priority unicode eight x equal priority unicode nine x equal priority unicode colon x equal priority unicode semicolon x equal priority unicode less than x equal priority unicode equal sign x equal priority unicode greater than x equal priority unicode question mark x equal priority unicode commercial at x equal priority unicode capital a x equal priority unicode capital b x equal priority unicode capital c x equal priority unicode capital d x equal priority unicode capital e x equal priority unicode capital f x equal priority unicode capital g x equal priority unicode capital h x equal priority unicode capital i x equal priority unicode capital j x equal priority unicode capital k x equal priority unicode capital l x equal priority unicode capital m x equal priority unicode capital n x equal priority unicode capital o x equal priority unicode capital p x equal priority unicode capital q x equal priority unicode capital r x equal priority unicode capital s x equal priority unicode capital t x equal priority unicode capital u x equal priority unicode capital v x equal priority unicode capital w x equal priority unicode capital x x equal priority unicode capital y x equal priority unicode capital z x equal priority unicode left bracket x equal priority unicode backslash x equal priority unicode right bracket x equal priority unicode circumflex x equal priority unicode underscore x equal priority unicode grave accent x equal priority unicode small a x equal priority unicode small b x equal priority unicode small c x equal priority unicode small d x equal priority unicode small e x equal priority unicode small f x equal priority unicode small g x equal priority unicode small h x equal priority unicode small i x equal priority unicode small j x equal priority unicode small k x equal priority unicode small l x equal priority unicode small m x equal priority unicode small n x equal priority unicode small o x equal priority unicode small p x equal priority unicode small q x equal priority unicode small r x equal priority unicode small s x equal priority unicode small t x equal priority unicode small u x equal priority unicode small v x equal priority unicode small w x equal priority unicode small x x equal priority unicode small y x equal priority unicode small z x equal priority unicode left brace x equal priority unicode vertical line x equal priority unicode right brace x equal priority unicode tilde x equal priority preassociative x greater than x equal priority postassociative x greater than x equal priority priority x equal x equal priority priority x end priority equal priority newline x equal priority macro newline x equal priority macro indent x end priority greater than preassociative priority x apply x equal priority x tagged apply x end priority greater than preassociative priority x suc end priority greater than preassociative priority x apply x equal priority x tagged apply x end priority greater than preassociative priority x times x equal priority x times zero x end priority greater than preassociative priority x plus x equal priority x plus zero x equal priority x plus one x equal priority x minus x equal priority x minus zero x equal priority x minus one x end priority greater than preassociative priority x term plus x end plus equal priority x term union x equal priority x term minus x end minus end priority greater than postassociative priority x raw pair x equal priority x eager pair x equal priority x tagged pair x equal priority x untagged double x equal priority x pair x equal priority x double x end priority greater than postassociative priority x comma x end priority greater than preassociative priority x boolean equal x equal priority x data equal x equal priority x cardinal equal x equal priority x peano equal x equal priority x tagged equal x equal priority x math equal x equal priority x reduce to x equal priority x term equal x equal priority x term list equal x equal priority x term root equal x equal priority x term in x equal priority x term subset x equal priority x term set equal x equal priority x sequent equal x equal priority x free in x equal priority x free in star x equal priority x free for x in x equal priority x free for star x in x equal priority x claim in x equal priority x less x equal priority x less zero x equal priority x less one x equal priority x equal x equal priority x unequal x equal priority x is object var equal priority x avoid zero x equal priority x avoid one x equal priority x avoid star x equal priority x setequiv x equal priority x setequals x end priority greater than preassociative priority not x equal priority lnot x end priority greater than preassociative priority x and x equal priority x macro and x equal priority x simple and x equal priority x claim and x equal priority x land x end priority greater than preassociative priority x or x equal priority x parallel x equal priority x macro or x equal priority x lor x end priority greater than preassociative priority exist x indeed x equal priority for all x indeed x equal priority for all objects x indeed x equal priority forall x dot x end forall equal priority exists x dot x end exists end priority greater than postassociative priority x macro imply x equal priority x imply x equal priority x if and only if x end priority greater than postassociative priority x guard x equal priority x spy x equal priority x tagged guard x end priority greater than preassociative priority x select x else x end select end priority greater than preassociative priority lambda x dot x equal priority tagged lambda x dot x equal priority tagging x equal priority open if x then x else x equal priority let x be x in x equal priority let x abbreviate x in x end priority greater than preassociative priority x avoid x end priority greater than preassociative priority x init equal priority x modus equal priority x verify equal priority x curry plus equal priority x curry minus equal priority x dereference end priority greater than preassociative priority x at x equal priority x modus ponens x equal priority x modus probans x equal priority x conclude x equal priority x object modus ponens x end priority greater than postassociative priority x infer x equal priority x endorse x equal priority x id est x end priority greater than preassociative priority all x indeed x equal priority for all terms x indeed x end priority greater than postassociative priority x rule plus x end priority greater than postassociative priority x cut x end priority greater than preassociative priority x proves x end priority greater than preassociative priority x proof of x reads x equal priority line x because x indeed x end line x equal priority because x indeed x qed equal priority line x premise x end line x equal priority line x side condition x end line x equal priority arbitrary x end line x equal priority locally define x as x end line x equal priority block x line x end block x equal priority because x indeed x end line equal priority any term x end line x end priority greater than postassociative priority x alternative x end priority greater than postassociative priority x , x equal priority x [ x ] x end priority greater than preassociative priority x tab x equal priority evaluates to end priority greater than preassociative priority x row x equal priority x linebreak x equal priority x safe row x end priority greater than preassociative priority x setin x end priority greater than unicode end of text end define end math end left ] "
\begin{thebibliography}{99}
%\addcontentsline{toc}{section}{\bibname}
\bibitem[LiCS]{huth} Logic in Computer Science - Modelling and Reasoning about Systems, Second Edition - 2004.\\
\emph{By Michael Huth \& Mark Ryan}\\
ISBN: 0-521-54310-X
\end{thebibliography}
\end{appendix}
\end{document}
End of file
latex page
latex page
dvipdfm page"
The pyk compiler, version 0.grue.20060417+ by Klaus Grue,