"File page.tex
\documentclass [fleqn]{article}
\everymath{\rm}
\everydisplay{\rm}
\usepackage{latexsym}
\setlength {\overfullrule }{0mm}
\input{lgwinclude}
\usepackage{url}
\usepackage[dvipdfm=true]{hyperref}
\hypersetup{pdfpagemode=none}
\hypersetup{pdfstartpage=1}
\hypersetup{pdfstartview=FitBH}
\hypersetup{pdfpagescrop={120 80 490 680}}
\hypersetup{pdftitle=Logiweb sequent calculus}
\hypersetup{colorlinks=true}
% Save current \parindent (used by e.g. pyk display ... end display)
\newlength{\docparindent}
\setlength{\docparindent}{\parindent}
\newcommand{\liberalUrlBreak}[1]{{%
\mathcode`\/="!202F%
\mathcode`\0="!2030%
\mathcode`\1="!2031%
\mathcode`\2="!2032%
\mathcode`\3="!2033%
\mathcode`\4="!2034%
\mathcode`\5="!2035%
\mathcode`\6="!2036%
\mathcode`\7="!2037%
\mathcode`\8="!2038%
\mathcode`\9="!2039%
\mathcode`\:="!203A%
\mathcode`\A="!2041%
\mathcode`\B="!2042%
\mathcode`\C="!2043%
\mathcode`\D="!2044%
\mathcode`\E="!2045%
\mathcode`\F="!2046%
%\thinmuskip=0mu%
\medmuskip=0mu plus 2mu minus 0mu%
%\thickmuskip=0mu%
%\def\thinspace{\kern 0em}%
$#1$}}
\begin {document}
\title {The Logiweb sequent calculus}
\author {Klaus Grue\thanks{Department of Computer Science, University of Copenhagen (DIKU)}}
\date {\today}
\maketitle
\tableofcontents
" [ ragged right expansion ] "
\begin{abstract}
The `Logiweb sequent calculus' is suited for terse, human readable formulation of axioms, inference rules, theories, lemmas, and proofs. It supports different styles of theories like equational theories and FOL based theories. It permits to express arbitrary side conditions in the `Logiweb programming language'. As an example of use, the calculus allows to express the deduction rule as an inference rule which makes it easy to get started using a theory. The calculus has operations for `dereferencing' and `referencing' which allow to convert e.g.\ the name of a lemma into the contents of the lemma and vice versa. The calculus interacts smoothly with fully automatic tactics as well as proofs in which part of the work is done by a human author and part is done by proof tactics.
\end{abstract}
\section{Introduction}\label{sec:Introduction}
Logiweb \cite{grue04,grue05,base} is a system for electronic publication of logic. It allows authors different places in the world to define theories, state and prove lemmas, and to publish {\em Logiweb pages} that contain the results. The present paper is an example of a Logiweb page, and the present paper is correct in the sense that it has been verified by Logiweb.
Core Logiweb allows users to program proof systems in the {\em Logiweb programming language} and to publish the proof system. Users who use the same proof system and the same axiomatic theory may benefit from the results of each other in that a proof written by one author may make references across the internet to lemmas proved by another author. Cross theory cooperation (e.g.\ use of ZFC results in NBG) could be more cumbersome and cross proof system cooperation even more so, depending on the theories and systems involved.
The present paper introduces {\em Logiweb sequent calculus} which allows users to express arbitrary axiomatic theories on the same footing. That calculus supports arbitrary styles of logic (e.g.\ FOL or equational) equally well. The calculus is machine friendly in that proofs are easy to generate, verify, store, and transmit and it is general so that users of Logiweb are not tempted to make a proof system each. User friendliness in the sense that theories, lemmas, and proofs should be easy to read and write is taken care of by Logiwebs rendering and Turing complete macro expansion facilities combined with the support for proof tactics in the implementation of the calculus in \cite{base}.
The present paper gives an overview. Details are in a web appendix \cite{appendix}.
\section{Logiweb sequent calculus}
Let " [ math meta v end math ] " and " [ math meta t end math ] " denote the syntax classes of metavariables and object terms, respectively. The format " [ math meta s end math ] " of Logiweb statements is " [ math meta s [ "::=" ] meta v alternative meta t alternative meta s infer meta s alternative meta t endorse meta s alternative for all terms meta v indeed meta s alternative absurdity alternative meta s rule plus meta s end math ] ". As an example of use, consider the following:
\[ " [ array left , center , left , left is "Let" tab sequent example axiom tab "denote" tab for all terms meta a indeed meta a plus zero equal meta a , "." safe row "Let" tab sequent example rule tab "denote" tab for all terms meta a comma meta b comma meta c indeed meta a equal meta b infer meta a equal meta c infer meta b equal meta c , "." safe row "Let" tab sequent example contradiction tab "denote" tab zero equal one infer absurdity , "." safe row "Let" tab sequent example theory tab "denote" tab sequent example rule rule plus sequent example contradiction rule plus sequent example axiom , "." safe row "Let" tab sequent example lemma tab "denote" tab sequent example theory infer for all terms meta a indeed meta a equal meta a , "." end array ] " \]
\noindent The construct " [ math for all terms meta x indeed meta a end math ] " states that " [ math meta a end math ] " is provable for all object terms " [ math meta x end math ] ". Hence, " [ math sequent example axiom end math ] " above is an axiom scheme which says that " [ math meta a plus zero equal meta a end math ] " for all object terms " [ math meta a end math ] ".
The construct " [ math meta a infer meta b end math ] " states that if " [ math meta a end math ] " is provable then " [ math meta b end math ] " is provable. " [ math meta a infer meta b end math ] " is right associative and has higher priority than " [ math for all terms meta x indeed meta a end math ] ", so " [ math sequent example rule end math ] " above means " [ math for all terms meta a indeed for all terms meta b indeed for all terms meta c indeed parenthesis meta a equal meta b infer parenthesis meta a equal meta c infer meta b equal meta c end parenthesis end parenthesis end math ] ". Hence, " [ math sequent example rule end math ] " is the inference rule which states that " [ math meta a equal meta b end math ] " and " [ math meta a equal meta c end math ] " infer " [ math meta b equal meta c end math ] ". The macro that expands " [ math for all terms meta a comma meta b comma meta c indeed meta d end math ] " into " [ math for all terms meta a indeed for all terms meta b indeed for all terms meta c indeed meta d end math ] " is defined in \cite{appendix}.
The construct " [ math absurdity end math ] " denotes absurdity, i.e. meta-falsehood (we reserve " [ math false end math ] " and " [ math bottom end math ] " to denote falsehood and infinite looping, respectively, at the object level). Hence, " [ math sequent example contradiction end math ] " above states that " [ math zero equal one end math ] " is an absurdity.
The construct " [ math meta a rule plus meta b end math ] " states that both " [ math meta a end math ] " and " [ math meta b end math ] " are provable. Hence, " [ math sequent example theory end math ] " above is the axiomatic theory which comprises the axiom scheme " [ math sequent example axiom end math ] ", the inference rule " [ math sequent example rule end math ] ", and the statement that " [ math zero equal one end math ] " is an absurdity.
The lemma " [ math sequent example lemma end math ] " above says that " [ math meta a equal meta a end math ] " is provable in the theory " [ math sequent example theory end math ] ".
The construct " [ math meta a endorse meta b end math ] " states that if computation of " [ math meta a end math ] " yields " [ math true end math ] " then " [ math meta b end math ] " is provable. " [ math meta a end math ] " must be expressed in the Logiweb programming language (c.f.\ \cite{base}). " [ math true end math ] " denotes truth in the Logiweb programming language. If " [ math meta a endorse meta b end math ] " then we shall say that " [ math meta a end math ] " {\em endorses} " [ math meta b end math ] ". The endorsement operator allows to express side conditions as we shall see later.
A {\em Logiweb sequent} is a triple " [ math tuple var p comma var s comma var c end tuple end math ] " where " [ math var c end math ] " is a Logiweb statement and " [ math var p end math ] " and " [ math var s end math ] " are finite sets of Logiweb statements. The sequent " [ math tuple set var p sub one end sub comma "\ldots" comma var p sub var m end sub end set comma set var s sub one end sub comma "\ldots" comma var s sub var n end sub end set comma var c end tuple end math ] " represents " [ math var p sub one end sub infer "\ldots" infer var p sub var m end sub infer var s sub one end sub endorse "\ldots" endorse var s sub var n end sub endorse var c end math ] ". The operations of Logiweb sequent calculus are:
\[" [ array right , left , left , left is var a init tab evaluates to tab tuple the empty set comma the empty set comma var a infer var a end tuple safe row var a infer tuple var p comma var s comma var c end tuple tab evaluates to tab tuple var p term minus var a end minus comma var s comma var a infer var c end tuple safe row var a endorse tuple var p comma var s comma var c end tuple tab evaluates to tab tuple var p comma var s term minus var a end minus comma var a endorse var c end tuple safe row for all terms var x indeed tuple var p comma var s comma var c end tuple tab evaluates to tab tuple var p comma var s comma for all terms var x indeed var c end tuple , "\footnotemark" safe row tuple var p comma var s comma var a infer var c end tuple modus tab evaluates to tab tuple var p term plus var a end plus comma var s comma var c end tuple safe row tuple var p comma var s comma var a endorse var c end tuple modus tab evaluates to tab tuple var p comma var s term plus var a end plus comma var c end tuple safe row tuple var p comma var s comma for all terms var x indeed var c end tuple at var a tab evaluates to tab tuple var p comma var s comma substitute var c set var x to var a end substitute end tuple , "\footnotemark" safe row tuple var p comma var s comma var a endorse var b end tuple verify tab evaluates to tab tuple var p comma var s comma var b end tuple , "\footnotemark" safe row tuple var p comma var s comma var a infer var b infer var c end tuple curry plus tab evaluates to tab tuple var p comma var s comma parenthesis var a rule plus var b end parenthesis infer var c end tuple safe row tuple var p comma var s comma parenthesis var a rule plus var b end parenthesis infer var c end tuple curry minus tab evaluates to tab tuple var p comma var s comma var a infer var b infer var c end tuple safe row tuple var p comma var s comma var n end tuple dereference tab evaluates to tab tuple var p comma var s comma var c end tuple , "\footnotemark" safe row tuple var p comma var s comma var c end tuple id est var n tab evaluates to tab tuple var p comma var s comma var n end tuple , "\addtocounter{footnote}{-1}\footnotemark" safe row tuple var p sub one end sub comma var s sub one end sub comma var c sub one end sub end tuple cut tuple var p sub two end sub comma var s sub two end sub comma var c sub two end sub end tuple tab evaluates to tab tuple var p sub one end sub term union parenthesis var p sub two end sub term minus var c sub one end sub end minus end parenthesis comma var s sub one end sub term union var s sub two end sub comma var c sub two end sub end tuple end array ] "\]%
%
\footnotetext[1]{if " [ math var x end math ] " is not free in any member of " [ math var p end math ] " or " [ math var s end math ] "}%
%
\footnotetext[2]{if " [ math var a end math ] " is free for " [ math var x end math ] " in " [ math var c end math ] "}%
%
\footnotetext[3]{if computation of " [ math var a end math ] " yields " [ math true end math ] " in the Logiweb programming language}%
%
\footnotetext[4]{if " [ math var n end math ] " is defined to denote " [ math var c end math ] "}
\noindent Evaluation of a sequent operation gives a sequent or an exception. Exceptional cases are omitted above. Now let " [ math sequent example axiom prime end math ] " denote " [ math sequent example theory infer for all terms meta a indeed meta a plus zero equal meta a end math ] ". We have
\[ " [ array left , left , left is sequent example theory infer parenthesis sequent example theory init modus dereference cut parenthesis sequent example rule rule plus sequent example contradiction infer sequent example lemma init end parenthesis curry plus end parenthesis dereference id est sequent example axiom prime tab evaluates to safe row sequent example theory infer parenthesis tuple the empty set comma the empty set comma sequent example theory infer sequent example theory end tuple modus dereference cut parenthesis sequent example rule rule plus sequent example contradiction infer tuple the empty set comma the empty set comma sequent example axiom infer sequent example axiom end tuple end parenthesis curry plus end parenthesis dereference id est sequent example axiom prime tab evaluates to safe row sequent example theory infer parenthesis tuple set sequent example theory end set comma the empty set comma sequent example theory end tuple dereference cut tuple the empty set comma the empty set comma sequent example rule rule plus sequent example contradiction infer sequent example axiom infer sequent example axiom end tuple curry plus end parenthesis dereference id est sequent example axiom prime tab evaluates to safe row sequent example theory infer parenthesis tuple set sequent example theory end set comma the empty set comma sequent example rule rule plus sequent example contradiction rule plus sequent example axiom end tuple cut tuple the empty set comma the empty set comma sequent example rule rule plus sequent example contradiction rule plus sequent example axiom infer sequent example axiom end tuple end parenthesis dereference id est sequent example axiom prime tab evaluates to safe row sequent example theory infer parenthesis tuple set sequent example theory end set comma the empty set comma sequent example rule rule plus sequent example contradiction rule plus sequent example axiom end tuple cut tuple set sequent example rule rule plus sequent example contradiction rule plus sequent example axiom end set comma the empty set comma sequent example axiom end tuple end parenthesis dereference id est sequent example axiom prime tab evaluates to safe row sequent example theory infer tuple set sequent example theory end set comma the empty set comma sequent example lemma end tuple dereference id est sequent example axiom prime , evaluates to , sequent example theory infer tuple set sequent example theory end set comma the empty set comma for all terms meta a indeed meta a plus zero equal meta a end tuple id est sequent example axiom prime tab evaluates to safe row tuple the empty set comma the empty set comma sequent example theory infer for all terms meta a indeed meta a plus zero equal meta a end tuple id est sequent example axiom prime , evaluates to , tuple the empty set comma the empty set comma sequent example axiom prime end tuple end array ] " \]
\noindent which proves " [ math sequent example axiom prime end math ] ".
The syntax of {\em Logiweb sequent terms} reads " [ math meta q [ "::=" ] meta s init alternative meta s infer meta q alternative meta s endorse meta q alternative for all terms meta v indeed meta q alternative meta q modus alternative meta q at meta s alternative meta q verify alternative meta q curry plus alternative meta q curry minus alternative meta q id est meta s alternative meta q dereference alternative meta q cut meta q end math ] ". A sequent term " [ math var q end math ] " is said to {\em prove} the statement " [ math var c end math ] " if " [ math var q end math ] " evaluates to " [ math tuple the empty set comma the empty set comma var c end tuple end math ] " (\cite{base} allows " [ math var q end math ] " to evaluate to " [ math tuple var p comma the empty set comma var c end tuple end math ] " provided all elements of " [ math var p end math ] " are names of previously proved lemmas).
\section{Object theories}\label{section:ObjectTheories}
Logiweb sequent calculus is like assembly language: general and machine friendly, but it needs syntactic sugar. The user friendliness of the combined system of Logiweb, Logiweb sequent calculus, and syntactic sugar has been tested during a course in logic in which ten students wrote Logiweb pages that proved " [ math object x plus object y equal object y plus object x end math ] " from the raw axioms of Mendelsons system " [ math system s end math ] " (Peano arithmetic) \cite{mendelson}. It was found that the students could prove commutativity, get the proof verified, and write a report on that in less than three weeks, starting with little experience in Logiweb, mechanical proof checking, and logic in general. For links to the reports, consult \url{http://yoa.dk/}.
While proving " [ math object x plus object y equal object y plus object x end math ] " from the raw axioms may be a good student exercise, it was found that the deduction theorem and parallel instantiation of object variables was badly needed. Versions of theorems that used inference " [ math unicode end of text infer unicode end of text end math ] " and meta variables were easier to use than theorems using implication " [ math unicode end of text imply unicode end of text end math ] " and object variables, but the axiom of induction forced implication and object variables upon the students. Instantiation of object variables is cumbersome because axiom A4 in \cite{mendelson} only allows to instantiate one variable at a time whereas the students needed parallel instantiation, e.g.\ when swapping two object variables. And hypothetical reasoning either required manual unfolding of the deduction theorem or programming of a proof tactic that could cost a lot of CPU-time for large developments.
An {\em inference rule of deduction} would eliminate these problems. If, however, " [ math for all object x comma object y indeed parenthesis object x equal object y imply object y equal object x end parenthesis end math ] " is an object statement and " [ math for all terms meta a comma meta b indeed meta a equal meta b infer meta b equal meta a end math ] " is a meta statement, then the deduction rule is a meta meta statement. We do not want to introduce a meta meta level above the Logiweb sequent calculus just to express deduction so we shall express deduction using the side condition machinery of the sequent calculus.
\subsection{Peano arithmetic}
A modified version of Mendelsons system " [ math system s end math ] " (Peano arithmetic) \cite{mendelson} may be formulated thus:
\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}
\item \makebox[0.45\textwidth][l]{" [ math theory system s end theory end math ] "}" [ math in theory system s rule rule mp says for all terms meta a comma meta b indeed meta a imply meta b infer meta a infer meta b end rule end math ] "
\item \makebox[0.45\textwidth][l]{" [ math in theory system s rule rule gen says for all terms meta x comma meta a indeed meta a infer for all meta x indeed meta a end rule end math ] "}" [ math in theory system s rule deduction says for all terms meta a comma meta b indeed deduction meta a conclude meta b end deduction endorse meta a infer meta b end rule end math ] "
\item \makebox[0.45\textwidth][l]{}" [ math in theory system s rule axiom s two says for all terms meta a comma meta b indeed meta a equal meta b infer meta a suc equal meta b suc end rule end math ] "
\item \makebox[0.45\textwidth][l]{" [ math in theory system s rule axiom s three says for all terms meta a indeed not zero equal meta a suc end rule end math ] "}" [ math in theory system s rule axiom s four says for all terms meta a comma meta b indeed meta a suc equal meta b suc infer meta a equal meta b end rule end math ] "
\item \makebox[0.45\textwidth][l]{" [ math in theory system s rule axiom s five says for all terms meta a indeed meta a plus zero equal meta a end rule end math ] "}" [ math in theory system s rule axiom s six says for all terms meta a comma meta b indeed meta a plus meta b suc equal parenthesis meta a plus meta b end parenthesis suc end rule end math ] "
\item \makebox[0.45\textwidth][l]{" [ math in theory system s rule axiom s seven says for all terms meta a indeed meta a times zero equal zero end rule end math ] "}" [ math in theory system s rule axiom s eight says for all terms meta a comma meta b indeed meta a times parenthesis meta b suc end parenthesis equal parenthesis meta a times meta b end parenthesis plus meta a end rule end math ] "
\item " [ math in theory system s rule double negation says for all terms meta a indeed for all terms meta b indeed not meta b imply not meta a infer not meta b imply meta a infer meta b end rule end math ] "
\item " [ math in theory system s rule axiom s one says for all terms meta a comma meta b comma meta c indeed meta a equal meta b infer meta a equal meta c infer meta b equal meta c end rule end math ] "
\item " [ math in theory system s rule axiom s nine says for all terms meta x comma meta a comma meta b comma meta c indeed sub meta b is meta a where meta x is zero end sub endorse sub meta c is meta a where meta x is meta x suc end sub endorse meta b infer meta a imply meta c infer meta a end rule end math ] "\footnote{" [ math sub meta a is meta b where meta x is meta c end sub end math ] " says `the object term " [ math meta b end math ] " where the object variable " [ math meta x end math ] " is replaced by the object term " [ math meta c end math ] " is alpha equivalent to the object term " [ math meta a end math ] ", c.f.\ \cite{appendix}}
\end{list}
\noindent As defined in \cite{base}, " [ math in theory system s rule axiom s five says for all terms meta a indeed meta a plus zero equal meta a end rule end math ] " macro expands into a lemma and a proof where the lemma says " [ math system s infer for all terms meta a indeed meta a plus zero equal meta a end math ] " and the proof is a proof of that lemma. " [ math theory system s end theory end math ] " macro expands into a definition which defines " [ math system s end math ] " as the conjunction of " [ math for all terms meta a indeed meta a plus zero equal meta a end math ] " and all the other rules attributed to " [ math system s end math ] ". The " [ math theory meta x end theory end math ] " macro is somewhat complex since it has to scan the entire page to find all rules related to the theory being defined. The benefit of collecting rules from the entire page is that it gives authors the freedom to introduce axioms one by one.
The deduction rule " [ math deduction end math ] " is such that e.g.\ " [ math for all terms meta a comma meta b indeed meta a equal meta b infer meta b equal meta a end math ] " allows to conclude " [ math meta a equal meta b imply meta b equal meta a end math ] " and " [ math object x plus object y equal object y plus object x end math ] " allows to conclude " [ math meta a plus meta b equal meta b plus meta a end math ] " so " [ math deduction end math ] " implements both deduction and parallel instantiation. All complexity is hidden in the side condition which is defined in \cite{appendix}.
Having the deduction rule, axioms A1, A2, A4, and A5 in \cite{mendelson} become superfluous. For proofs of those axioms based on deduction, see \cite{appendix}.
As an example of a development, \cite{appendix} proves the following lemmas from \cite{mendelson} in system " [ math system s end math ] ":
\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}
\item " [ math in theory system s lemma prop three two a says for all terms meta a indeed meta a equal meta a end lemma end math ] "
\item " [ math in theory system s lemma prop three two b says for all terms meta a comma meta b indeed meta a equal meta b infer meta b equal meta a end lemma end math ] "
\item " [ math in theory system s lemma prop three two c says for all terms meta a comma meta b comma meta c indeed meta a equal meta b infer meta b equal meta c infer meta a equal meta c end lemma end math ] "
\item " [ math in theory system s lemma prop three two d says for all terms meta a comma meta b comma meta c indeed meta a equal meta c infer meta b equal meta c infer meta a equal meta b end lemma end math ] "
\item " [ math in theory system s lemma prop three two e says for all terms meta a comma meta b comma meta c indeed meta a equal meta b infer meta a plus meta c equal meta b plus meta c end lemma end math ] "
\item " [ math in theory system s lemma prop three two f says for all terms meta a indeed meta a equal zero plus meta a end lemma end math ] "
\item " [ math in theory system s lemma prop three two g says for all terms meta a comma meta b indeed meta a suc plus meta b equal parenthesis meta a plus meta b end parenthesis suc end lemma end math ] "
\item " [ math in theory system s lemma prop three two h says for all terms meta a comma meta b indeed meta a plus meta b equal meta b plus meta a end lemma end math ] "
\end{list}
\noindent In the present paper we merely show the proof of an auxiliary lemma which proves the induction step of " [ math prop three two f end math ] ":
\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}
\item " [ math in theory system s lemma prop three two f two says for all terms meta a indeed meta a equal zero plus meta a imply meta a suc equal zero plus meta a suc end lemma end math ] "
\item " [ math system s proof of prop three two f two reads any term meta a end line block any term macro indent meta a end line line ell a premise macro indent meta a equal zero plus meta a end line line ell b because axiom s two modus ponens ell a indeed macro indent meta a suc equal parenthesis zero plus meta a end parenthesis suc end line line ell c because axiom s six indeed macro indent zero plus meta a suc equal parenthesis zero plus meta a end parenthesis suc end line because prop three two d modus ponens ell b modus ponens ell c indeed macro indent meta a suc equal zero plus meta a suc end line line ell d end block because deduction modus ponens ell d indeed meta a equal zero plus meta a imply meta a suc equal zero plus meta a suc qed end math ] "
\end{list}
\noindent As defined in \cite{base}, " [ math make visible any term meta a end line meta b end visible end math ] " macro expands into " [ math for all terms meta a indeed meta b end math ] ". " [ math make root visible line "L05" because axiom s two modus ponens "L04" indeed meta a suc equal parenthesis zero plus meta a end parenthesis suc end line meta b end visible end math ] " macro expands into a local macro definition and a call to a proof tactic. The local macro definition defines " [ math "L05" end math ] " as shorthand for " [ math meta a suc equal parenthesis zero plus meta a end parenthesis suc end math ] " and the proof tactic expands the line into " [ math axiom s two init modus dereference modus at meta a at parenthesis zero plus meta a end parenthesis cut meta b end math ] " using unification. For more details see \cite{appendix}.
\section{Conclusion and further work}
Logiweb sequent calculus with examples from traditional Peano arithmetic has been presented. For further examples, click `Map Theory' at http://yoa.dk/. Map theory is an equational theory. In that theory, all definitions present on a lemmas home page become axioms according to an `axiom of definition' which is expressible by a side condition in the Logiweb sequent calculus.
The traditional deduction theorem requires that no application of Gen is made to variables free in the premise. The side condition of the deduction rule above is quite different. Proving the consistency of the deduction rule is work of the future but is expected to be straightforward since, in the standard model, a statement holds for all natural numbers if and only if it holds for all terms.
%------------------------------------------------------------------------------
\bibliographystyle{alpha}
\bibliography{./page}
%------------------------------------------------------------------------------
\everymath{}
\everydisplay{}
\end{document}
End of file
File page.bib
@incollection{bruijn80,
author = {Nicolaas Govert de Bruijn},
title = {A Survey of the Project {AUTOMATH}},
editor = {J.P. Seldin and J. R. Hindley},
booktitle = {To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus
and Formalism},
publisher = {Academic Press},
year = {1980},
pages = {579--606}}
@book {church41,
author = {A. Church},
title = {The Calculi of Lambda-Conversion},
publisher = {Princeton University Press},
year = {1941}}
@book {constable86,
author = {Robert L. Constable and S. Allen and H. Bromly and
W. Cleaveland and J. Cremer and R. Harper and D. Howe and
T. Knoblock and N. Mendler and P. Panangaden and J. Sasaki and
S. Smith},
title = {Implementing Mathematics with the Nuprl Proof Development
System},
publisher = {Prentice-Hall},
address = {Englewood Cliffs, New Jersey},
year = {1986}}
@inproceedings{dobbertin96,
author = {Hans Dobbertin and Antoon Bosselaers and Bart Preneel},
title = {{RIPEMD}-160: A Strengthened Version of {RIPEMD}},
booktitle = {Fast Software Encryption},
pages = {71-82},
year = {1996},
note = {\url{http://citeseer.nj.nec.com/dobbertin96ripemd.html}}}
@article {godel31,
author = {K. G{\"!o}del},
title = {{\"!U}ber for\-mal un\-ent\-scheid\-ba\-re
{S\"!at}\-ze der {Prin}\-ci\-pia
{Mathe}\-ma\-ti\-ca und ver\-wand\-ter
{Sys}\-teme {I}},
journal = {Mo\-nats\-hef\-te f{\"!u}r {Mathe}\-ma\-tik und {Phy}\-sik},
year = {19\-31},
volume = {12},
number = {{XXXVIII}},
pages = {173-198}}
@book {gordon79,
author = {M. J. Gordon, A. J. Milner, C. P. Wadsworth},
title = {Edinburgh {LCF}, A mechanised logic of computation},
publisher = {Springer-Verlag},
year = {1979},
volume = {78},
series = {Lecture Notes in Computer Science}}
@article {grue92,
author = {K. Grue},
title = {Map Theory},
journal = TCS,
year = {1992},
volume = {102},
number = {1},
pages = {1--133},
month = {jul}}
@book {MathComp,
author = {Klaus Grue},
year = {2001},
title = {Mathematics and Computation},
publisher = {DIKU},
address = {Universitetsparken 1, DK-2100 Copenhagen},
volume = {1--3},
edition = {7},
keywords = {Logic}}
@misc {MathML,
author = {Robert Miner and Jeff Schaeffer},
title = {A Gentle Introduction to {MathML}},
TYPE = {Tutorial},
note = {\url
{http://www.dessci.com/en/support/tutorials/mathml/default.htm}},
year = {2001}}
@techreport{grue02b,
author = {K. Grue},
year = {2002},
title = {Map Theory with Classical Maps},
institution
= {DIKU},
note = {\url{http://www.diku.dk/publikationer/tekniske.rapporter/2002/}},
number = {02/21}}
@inproceedings{grue04,
author = {K. Grue},
title = {Logiweb},
editor = {Fairouz Kamareddine},
booktitle = {Mathematical Knowledge Management Symposium 2003},
publisher = {Elsevier},
series = {Electronic Notes in Theoretical Computer Science},
volume = {93},
year = {2004},
pages = {70--101}}
@InProceedings{grue05,
author = {K. Grue},
year = {2005},
title = {The implementation of Logiweb},
booktitle = {Empirically Successful Classical Automated Reasoning
(ESCAR)},
editor = {Bernd Fischer and Stephan Schulz and Geoff Sutcliffe},
keywords = {Automated Reasoning, Electronic Publishing}}
@techreport{base,
author = {K. Grue},
year = {2006},
title = {A Logiweb base page},
institution={Logiweb},
note = {{\small \url{\lgwBaseUrl}}}}
@techreport{appendix,
author = {K. Grue},
year = {2006},
title = {Logiweb sequent calculus, appendix},
institution={Logiweb},
note = {{\small \url{\lgwCheckUrl body/tex/appendix.pdf}}}}
@misc {kohlhase03,
author = {Michael Kohlhase},
title = {{OMDoc}: An Open Markup Format for Mathematical Documents
(Version 1.1)},
type = {Open Specification},
note = {\url{http://www.mathweb.org/omdoc.ps}},
year = {2003}}
@article {mccarthy60,
author = {J. McCarthy},
title = {Recursive functions of symbolic expressions and their
computation by machine},
journal = {Communications of the ACM},
year = {1960},
pages = {184--195}}
@book {mendelson,
author = {E. Mendelson},
title = {Introduction to Mathematical Logic},
publisher = {Wadsworth and Brooks},
year = {1987},
edition = {3.}}
@manual {matuszewski93,
title = {An Outline of PC Mizar},
author = {Micha{\l} Muzalewski},
editor = {Roman Matuszewski},
year = {1993},
address = {Brussels},
organization
= {Foundation of Logic, Mathematics and Informatics,
Mizar User Group},
file = {/home/mostynm/papers/mizarmanual.ps.gz}}
@techreport {paulson98a,
author = {Lawrence C. Paulson},
title = {Introduction to {Isabelle}},
institution
= {University of Cambridge, Computer Laboratory},
year = {1998}}
@techreport {paulson98b,
author = {Lawrence C. Paulson},
title = {The {Isabelle} Reference Manual},
institution
= {University of Cambridge, Computer Laboratory},
year = {1998}}
@phdthesis {skalberg02,
author = {Sebastian C. Skalberg},
title = {An Interactive Proof System for Map Theory},
school = {University of Copenhagen},
year = {2002},
month = {oct},
note = {\url{http://www.mangust.dk/skalberg/phd/}},
postscript= {\url{http://www.mangust.dk/skalberg/phd/skalberg-phd.ps}}}
@Book {steele,
author = {Guy L. Steele},
title = {Common Lisp---The Language},
publisher = {Digital Press},
year = {1990},
edition = {2.}}
@book {TeXbook,
author = {D. Knuth},
title = {The TeXbook},
publisher = {Addison Wesley},
year = {1983}}
@inproceedings{trybulec85a,
author = {Andrzej Trybulec and Howard Blair},
title = {Computer Assisted Reasoning with {MIZAR}},
pages = {26--28},
booktitle = {Proceedings of the 9th International Joint Conference on
Artificial Intelligence},
editor = {Aravind Joshi},
month = {aug},
year = {1985},
address = {Los Angeles, CA},
publisher = {Morgan Kaufmann},
note = {\url{http://www.mizar.org/}}}
@book {vallee03,
author = {Thierry Vall\'{e}e},
title = {``{Map Theory}'' et Antifondation},
series = {Electronic Notes in Theoretical Computer Science},
volume = {79},
publisher = {Elsevier},
year = {2003},
pages = {1-258}}
End of file
latex page
bibtex page
latex page
latex page
dvipdfm page
File appendix.tex
\documentclass [fleqn]{article}
\everymath{\rm}
\usepackage{latexsym}
\setlength {\overfullrule }{0mm}
\input{lgwinclude}
\usepackage{url}
\usepackage[dvipdfm=true]{hyperref}
\hypersetup{pdfpagemode=none}
\hypersetup{pdfstartpage=1}
\hypersetup{pdfstartview=FitBH}
\hypersetup{pdfpagescrop={120 130 490 730}}
\hypersetup{pdftitle=Logiweb sequent calculus - Appendix}
\hypersetup{colorlinks=true}
\begin {document}
\title {Logiweb sequent calculus, Appendix}
\author {Klaus Grue}
\date {\today}
\maketitle
\tableofcontents
\section{Introduction}
The present appendix is part of the {\em Logiweb page} available at
\begin{raggedright}
\begin{sloppypar}
\noindent \url{\lgwCheckUrl body/tex/page.pdf}.
\end{sloppypar}
\end{raggedright}
The hex number which contains a RIPEMD-160 \cite{dobbertin96} hash key and a time stamp identifies the present paper uniquely on Logiweb. The part before the hex number is the address of a {\em Logiweb relay} which redirects the users browser to the paper. That part can be replaced by the address of any Logiweb relay. The part after the hex number indicates the address of the body of the paper relative to the official, binary representation (2/ is shorthand for ../../).
Actually, the present page is rendered as three pdf files present at \href{\lgwCheckUrl body/tex/page.pdf}{2\linebreak [0]/\linebreak [0]body\linebreak [0]/\linebreak [0]tex\linebreak [0]/\linebreak [0]page.pdf}, \href{\lgwCheckUrl body/tex/appendix.pdf}{2\linebreak [0]/\linebreak [0]body\linebreak [0]/\linebreak [0]tex\linebreak [0]/\linebreak [0]appendix.pdf}, and \href{\lgwCheckUrl body/tex/chores.pdf}{2\linebreak [0]/\linebreak [0]body\linebreak [0]/\linebreak [0]tex\linebreak [0]/\linebreak [0]chores.pdf} where appendix.pdf is the present appendix. Many proofs and definitions are deferred to the present appendix to spare the reader of the main paper in the page.pdf file. The chores.pdf file defines how to render each construct in \TeX. A good place to start browsing is \href{\lgwCheckUrl index.html}{2\linebreak [0]/\linebreak [0]index.html}.
Each Logiweb page has a Logiweb bibliography which lists previously published pages which the present page relies on. The present Logiweb page references the \href{\lgwBaseUrl index.html}{base} page at
\begin{raggedright}
\begin{sloppypar}
\noindent \url{\lgwBaseUrl body/tex/page.pdf}.
\end{sloppypar}
\end{raggedright}
\noindent which defines the proof system used to verify the present page (c.f. \href{\lgwCheckUrl bibliography/tex/page.pdf}{2\linebreak [0]/\linebreak [0]bibliography\linebreak [0]/\linebreak [0]tex\linebreak [0]/\linebreak [0]page.pdf}).
As mentioned in the main paper, the user friendliness of the Logiweb sequent calculus is achieved by using the Turing complete macro expansion facility of Logiweb. To see the proofs present in the main paper after macro expansion, consult \href{\lgwCheckUrl expansion/tex/page.pdf}{2\linebreak [0]/\linebreak [0]expansion\linebreak [0]/\linebreak [0]tex\linebreak [0]/\linebreak [0]page.pdf}. To see the proofs of the present appendix after macro expansion, consult \href{\lgwCheckUrl expansion/tex/appendix.pdf}{2\linebreak [0]/\linebreak [0]expansion\linebreak [0]/\linebreak [0]tex\linebreak [0]/\linebreak [0]appendix.pdf}.
\section{Notation}
\subsection{Hiding construct}
" [ math proclaim var x hide as text "hide" end text end proclaim end math ] " proclaims " [ math var x hide end math ] " to denote hiding. We introduce it here to have a visible hiding construct instead of the invisible `unicode start of text' operator normally used for hiding, c.f.\ the \href{\lgwBaseUrl index.html}{base} page. The use of hiding in " [ math macro define var x as var y end define hide end math ] " later in this appendix is play for the gallery since the " [ math var x end math ] " is introduced on the \href{\lgwBaseUrl index.html}{base} page and since macro definitions only have effect when they occur on the home page of the construct being macro defined.
\subsection{Metaquantification}\label{section:Metaquantification}
The following macro definition makes e.g.\ " [ math for all terms meta a comma meta b comma meta c indeed meta d end math ] " expand into " [ math all meta a indeed all meta b indeed all meta c indeed meta d end math ] ". Note that " [ math all var x indeed var y end math ] " is meta quantification as defined on the \href{\lgwBaseUrl index.html}{base} page which, unfortunately, is rendered exactly like object quantification in the present document. Such notational clashes are unavoidable in mathematics in general but becomes extremely visible in a system like Logiweb where referenced papers are only a click away. To avoid confusion between the two, identically looking quantifiers, we only use the meta quantifier from the base page in the macro definition below and otherwise use " [ math for all var x indeed var y end math ] " to denote object quantification. The " [ math protect var x end protect end math ] " operator used in the definition protects against macro expansion. The left hand side of the macro definition is protected against macro expansion as is the `recursive' call of the macro that occurs in the right hand side.
\vspace{1ex}
\noindent " [ math define macro of protect for all terms var x indeed var y end protect as lambda var t dot lambda var s dot lambda var c dot state expand macro newline open if not var t first term root equal quote var x comma var y end quote then macro newline quote expand var t term quote all var x indeed var y end quote stack tuple quote var x end quote pair var t first comma quote var y end quote pair var t second end tuple end expand else macro newline quote expand var t term quote all var x indeed protect for all terms var y indeed var z end protect end quote stack tuple quote var x end quote pair var t first first comma quote var y end quote pair var t first second comma quote var z end quote pair var t second end tuple end expand state var s cache var c end expand end define end math ] "
\vspace{1ex}
\noindent The definition above is a general macro definition as opposed to more restricted macro definitions like " [ math macro define any term var i end line var p as for all terms var i indeed var p end define end math ] " which just define a left hand side to expand into a right hand side. The " [ math macro define var x as var y end define hide end math ] " construct itself is defined by a general macro definition and happens to expand into a general macro definition, so the " [ math macro define var x as var y end define hide end math ] " construct is just syntactic sugar.
A general macro definition assigns a `macro' aspect to the principal operator of the right hand side. The definition ignores the parameters of the principal operator. Instead, the right hand side of the general macro definition must take three arguments, " [ math var t end math ] ", " [ math var s end math ] ", and " [ math var c end math ] ". When a macro aspect is invoked, it is applied to the term " [ math var t end math ] " to be expanded, a `macro state' " [ math var s end math ] ", and a `Logiweb cache' " [ math var c end math ] ".
The macro state should itself be a function of three parameters " [ math var t end math ] ", " [ math var s end math ] ", and " [ math var c end math ] " and it is the function to be invoked when continuing the macro expansion. A macro like the macro protection macro " [ math protect var x end protect end math ] " protects its argument " [ math var x end math ] " against macro expansion by returning it instead of calling " [ math var s end math ] " on it. The construct above calls the general macro expansion invokation function " [ math state expand var t state var s cache var c end expand end math ] " which simply applies " [ math var s end math ] " to " [ math var t end math ] ", " [ math var s end math ] ", and " [ math var c end math ] ". So the definition above does something to " [ math var t end math ] " and then continues macro expansion.
The Logiweb cache " [ math var c end math ] " is the cache of the home page of " [ math var t end math ] ", i.e.\ the page on which " [ math var t end math ] " occurs. The cache contains, among other, all definitions present on the home page and all pages transitively referenced by the home page. It also contains other things like compiled versions of all value defined constructs. This is badly needed for efficiency reasons because macro expansion is done not by the Logiweb computing engine itself but by a self-interpretter which is run by the Logiweb engine and simulates the Logiweb engine. This self-interpretter, which resides inside the macro state " [ math var s end math ] ", fetches compiled versions of constructs from the cache " [ math var c end math ] " for efficiency reasons.
The term " [ math var t end math ] " has the structure described in Section \ref{section:LogiwebTerms}. " [ math var t second end math ] " is the second subtree of " [ math var t end math ] " and " [ math var t first second end math ] " is the second subtree of the first subtree of " [ math var t end math ] ". " [ math var t term root equal var t prime end math ] " is true when " [ math var t end math ] " and " [ math var t prime end math ] " have the same principal operator.
The " [ math quote expand var t term var p stack var a end expand end math ] " construct expands the pattern " [ math var p end math ] " according to the association list " [ math var a end math ] ". Some day, when the author has some spare time, a new version of " [ math quote expand var t term var p stack var a end expand end math ] " will be implemented in which the association list is replaced by a facility like the `comma' in Lisp backquotes.
The construct " [ math quote expand var t term var p stack var a end expand end math ] " not only expands the pattern " [ math var p end math ] " according to the association list " [ math var a end math ] ", it also extracts the `debugging information' of the principal operator of " [ math var t end math ] " and installs that debugging information in all operators that come from the pattern " [ math var p end math ] ". The debugging information indicates the exact location of the construct before macro expansion.
The " [ math quote var t end quote end math ] " construct evaluates to the Logiweb representation of the term " [ math var t end math ] ".
\subsection{The `Arbitrary' proof constructor}
The `Arbitrary' proof constructor defined on the \href{\lgwBaseUrl index.html}{base} page does not take advantage of the meta quantification macro above. For that reason we introduce a new construct for introducing arbitrary meta variables:
" [ math macro define any term var i end line var p as for all terms var i indeed var p end define end math ] "
Actually, the definition above was used as an example of a simple macro in Section \ref{section:Metaquantification}. When the same aspect of the same construct is defined more than once (e.g.\ the macro aspect of " [ math make visible any term var i end line var p end visible end math ] "), only the first definition has effect. But the Logiweb compiler prints a warning if the same aspect of the same construct have definitions that contradict each other. The repeated definition of " [ math make visible any term var i end line var p end visible end math ] " above gives no warnings since the two definitions have identical right hand sides.
\subsection{Macro indentation}
The following construct increases the left margin. Should be used in inline math mode only. Should be replaced by automatic indentation inside blocks as soon as possible.
" [ math macro define macro indent var x as var x end define end math ] "
\subsection{Protected macro expansion}
The following construct is a general macro definition construct which both protects its left hand side against macro expansion and renders its left hand side using the tex name aspect. To see the definitions of the tex and tex name aspects of " [ math make visible general macro define var x as var y end define end visible hide end math ] " consult the \href{\lgwCheckUrl body/tex/chores.pdf}{chores} part of the present Logiweb page.
" [ math macro define general macro define var x as var y end define as define macro of protect var x end protect as var y end define end define end math ] "
\subsection{Object quantification}
The following is a repetion of Section \ref{section:Metaquantification} but concerns object quantification. It allows to write " [ math for all var x comma var y comma var z indeed var u end math ] " for " [ math for all var x indeed for all var y indeed for all var z indeed var u end math ] ".
\vspace{1ex}
\noindent " [ math define macro of protect for all var x indeed var y end protect as lambda var t dot lambda var s dot lambda var c dot state expand macro newline open if not var t first term root equal quote var x comma var y end quote then macro newline quote expand var t term quote for all objects var x indeed var y end quote stack tuple quote var x end quote pair var t first comma quote var y end quote pair var t second end tuple end expand else macro newline quote expand var t term quote for all objects var x indeed protect for all var y indeed var z end protect end quote stack tuple quote var x end quote pair var t first first comma quote var y end quote pair var t first second comma quote var z end quote pair var t second end tuple end expand state var s cache var c end expand end define end math ] "
\subsection{Proof constructs}
The " [ math make visible block var b line var l end block var p end visible end math ] " construct puts a parenthesis around the block " [ math var b end math ] " and places a cut operator between " [ math var b end math ] " and " [ math var p end math ] ". The construct is complicated by the line number " [ math var l end math ] " which should be macro defined locally to denote the conclusion of the block " [ math var b end math ] ". This is non-trivial since the conclusion is the last line prefixed by all premises, side-conditions, and meta-quantifiers introduced in earlier lines.
\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}
\item " [ math general macro define block var b line var l end block var p as lambda var t dot lambda var s dot lambda var c dot block one var t state var s cache var c end block end define end math ] "
\item " [ math value define block one var t state var s cache var c end block as var t tagged guard var s tagged guard var c tagged guard macro newline let var b be state expand var t first state var s cache var c end expand in macro newline let var x be block two var b end block in macro newline let var q be quote expand var t term quote protect let var l abbreviate var x in var p end protect end quote stack tuple quote var l end quote pair var t second comma quote var p end quote pair var t third comma quote var x end quote pair var x end tuple end expand in macro newline let var q be state expand var q state var s cache var c end expand in macro newline quote expand var t term quote var b cut var q end quote stack tuple quote var b end quote pair var b comma quote var q end quote pair var q end tuple end expand end define end math ] "
\item " [ math value define block two var b end block as macro newline open if var b term root equal quote var x infer var y end quote then quote expand var b term quote var x infer var y end quote stack tuple quote var x end quote pair var b first comma quote var y end quote pair block two var b second end block end tuple end expand else macro newline open if var b term root equal quote var x endorse var y end quote then quote expand var b term quote var x endorse var y end quote stack tuple quote var x end quote pair var b first comma quote var y end quote pair block two var b second end block end tuple end expand else macro newline open if var b term root equal quote for all terms var x indeed var y end quote then quote expand var b term quote for all terms var x indeed var y end quote stack tuple quote var x end quote pair var b first comma quote var y end quote pair block two var b second end block end tuple end expand else macro newline open if var b term root equal quote var x cut var y end quote then block two var b second end block else macro newline open if var b term root equal quote var x conclude var y end quote then var b second else absurdity end define end math ] "
\item " [ math macro define because var a indeed var i end line as parenthesis var a conclude var i end parenthesis end define end math ] "
\end{list}
\subsection{Modus ponens at the object level}
We shall apply modus ponens to two arguments so often that this idiom deserves its own macro:
" [ math macro define var x object modus ponens var y as rule mp modus ponens var x modus ponens var y end define end math ] "
\section{Side conditions}
\subsection{Logiweb terms}\label{section:LogiwebTerms}
Metavariables, object terms, statements, and sequent terms are all implemented as Logiweb terms which essentially have the following syntax:
\newcommand{\literal}[1]{\mbox{``#1''}}
\[\begin{array}{lll}
pdigit & ::= & \literal{1} \mathrel{|} \literal{2} \mathrel{|} \literal{3} \mathrel{|} \literal{4} \mathrel{|} \literal{5} \mathrel{|} \literal{6} \mathrel{|} \literal{7} \mathrel{|} \literal{8} \mathrel{|} \literal{9} \\
digit & ::= & \literal{0} \mathrel{|} pdigit \\
positive & ::= & pdigit \mathrel{|} positive \ digit \\
cardinal & ::= & \literal{0} \mathrel{|} positive \\
reference & ::= & cardinal \\
identifier & ::= & cardinal \\
symbol & ::= & \literal{(} \ reference \literal{\mbox {\tt \char32 }} \ identifier \ \literal{)} \\
arglist & ::= & \literal{)} \mathrel{|} \literal{\mbox {\tt \char32 }} \ term \ arglist \\
term & ::= & \literal{(} \ symbol \ arglist \\
\end{array}\]
\noindent The only thing omitted from the syntax is a third element of symbols which contains debugging information. For details on debugging information, consult the \href{\lgwBaseUrl index.html}{base} page.
Each Logiweb page introduces one or more new constructs. As an example, the present page introduces the binary operation " [ math var x imply var y end math ] ".
Each Logiweb page has a unique reference, and each construct introduced by a page has an identifier which is unique within the page. Hence, reference and identifier together determine a construct uniquely.
\subsection{Deduction}
\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}
\item " [ math macro define deduction var p conclude var c end deduction as lambda var x dot deduction zero quote var p end quote conclude quote var c end quote end deduction end define end math ] " \newline True if the premise " [ math var p end math ] " implies the conclusion " [ math var c end math ] " according to the deduction rule. The construct quotes its arguments and pass them on to " [ math deduction zero var p conclude var c end deduction end math ] ". The quoting and the " [ math lambda var x dot "\cdots" end math ] " makes " [ math deduction var p conclude var c end deduction end math ] " suited as a side condition. The present side condition ignores " [ math var x end math ] ". But when a side condition is invoked, it is applied to the cache of the home page of the side condition (the page on which the side condition occurs). That way the side condition gets access to all definitions present on the home page and all pages transitively referenced by the home page. As an example, that has allowed to define an `axiom of definition' in another theory on another Logiweb page in which all value definitions automatically become axiom schemes.
\item " [ math value define deduction zero var p conclude var c end deduction as var c tagged guard deduction eight var p bound true end deduction macro and deduction one deduction seven var p end deduction conclude var c condition true end deduction end define end math ] " \newline True if the premise " [ math var p end math ] " implies the conclusion " [ math var c end math ] " according to the deduction rule. The function checks the premise for meta-closedness, strips meta-quantifiers from " [ math var p end math ] " and then calls " [ math deduction one var p conclude var c condition var s end deduction end math ] " with an empty list " [ math var s end math ] " of side conditions. The " [ math var x tagged guard var y end math ] " construct evaluates and discards " [ math var x end math ] " and then returns " [ math var y end math ] ". It is included to ensure strictness of " [ math deduction zero var p conclude var c end deduction end math ] " which in turn increases the efficiency. Some day the present author will define a `strict value definition' operator so that users don't have to add " [ math var x tagged guard var y end math ] " operators manually. The " [ math var x tagged guard var y end math ] " construct takes zero CPU-time when used in functions that are `fit' for optimization. See the \href{\lgwBaseUrl index.html}{base} page for details on `fitness' analysis.
\item " [ math value define deduction one var p conclude var c condition var s end deduction as open if var c term root equal quote var x endorse var y end quote then deduction one var p conclude var c second condition var c first pair var s end deduction else deduction two var p conclude var c condition var s end deduction end define end math ] " \newline Move side conditions from the conclusion " [ math var c end math ] " to the list " [ math var s end math ] ". " [ math var x term root equal var y end math ] " is true if the terms " [ math var x end math ] " and " [ math var y end math ] " have the same root (i.e.\ the same principal operator) so " [ math var c term root equal quote var x endorse var y end quote end math ] " is true if the principal operator of " [ math var c end math ] " is an endorsement. " [ math var c first end math ] " and " [ math var c second end math ] " are the first and second argument, respectively, of the endorsement.
\item " [ math value define deduction two var p conclude var c condition var s end deduction as var s tagged guard var p term root equal quote var x infer var y end quote and var c term root equal quote var x imply var y end quote select deduction three var p first conclude var c first condition var s bound true end deduction and deduction two var p second conclude var c second condition var s end deduction else deduction four var p conclude var c condition var s bound deduction six var p conclude var c exception true bound true end deduction end deduction end select end define end math ] " \newline This function is true if the premise " [ math var p end math ] " is equal to the conclusion " [ math var c end math ] " except that inferences are replaced by implications. " [ math open if var x then var y else var z end math ] " and " [ math var x select var y else var z end select end math ] " express the same conditional construct. Choosing between the two is a purely stylistic choice.
\item " [ math value define deduction three var p conclude var c condition var s bound var b end deduction as open if not var c term root equal quote for all var x indeed var y end quote then deduction four var p conclude var c condition var s bound var b end deduction else macro newline open if var p term root equal quote for all var x indeed var y end quote and var p first term equal var c first then deduction four var p conclude var c condition var s bound var b end deduction else macro newline deduction three var p conclude var c second condition var s bound parenthesis var c first pair var c first end parenthesis pair var b end deduction end define end math ] " \newline " [ math deduction three var p conclude var c condition var s bound var b end deduction end math ] " moves quantified variables from the premise " [ math var p end math ] " to the association list " [ math var b end math ] " of `bindings'. Each quantified variable " [ math var x end math ] " is added to " [ math var b end math ] " as the pair " [ math var x pair var x end math ] " indicating the " [ math var x end math ] " should be replaced by " [ math var x end math ] " (which is a way of saying that the variable cannot be instantiated). Moving of bound variables stops when there are no more bound variables to move or when the premise and conclusion happen to quantify the same variable. In both cases we have reached a point where premise and conclusion should be identical except for instantaition of variables. " [ math var x term equal var y end math ] " is true if the terms " [ math var x end math ] " and " [ math var y end math ] " are identical. Logiweb terms contain debugging information which indicates the precise location each operator before macro expansion. " [ math var x term equal var y end math ] " ignores this debugging information when it tests two terms for identity.
\item " [ math value define deduction four var p conclude var c condition var s bound var b end deduction as var s tagged guard var b tagged guard macro newline open if var p term root equal quote object x end quote then lookup var p stack var b default true end lookup term equal var c else macro newline open if not var p term root equal var c then false else macro newline open if var p term root equal quote for all var x indeed var y end quote then var p first term equal var c first and deduction four var p second conclude var c second condition var s bound parenthesis var p first pair var p first end parenthesis pair var b end deduction else macro newline open if not var p term root equal quote meta x end quote then deduction four star var p tail conclude var c tail condition var s bound var b end deduction else macro newline var p first term equal var c first and deduction five var p condition var s bound var b end deduction end define end math ] " \newline Test that the premise " [ math var p end math ] " is identical to the conclusion " [ math var c end math ] " except for instantiation of object variables as specified by the association list " [ math var b end math ] ". A term is an object variable if the root of the term is the `object variable operator'. For that reason, one can test whether or not a variable is an object variable by comparing its root to the root of an arbitrary object variable. For each meta variable, check that there are side conditions which ensure that the meta variables denote terms whose free object variables do not get caught in the context. Meta variables are recognized the same way as object variables. The object variable " [ math object x end math ] " and the meta variable " [ math meta x end math ] " macro expand into " [ math object var var x end var end math ] " and " [ math metavar var x end metavar end math ] ", respectively, adding the object and meta variable operator, respectively, to the term " [ math var x end math ] ". The term " [ math var x end math ] " is neither an object nor a meta variable. " [ math var x end math ] " is a Logiweb programming language variable because no Logiweb definition assigns a value to it.
\item " [ math value define deduction four star var p conclude var c condition var s bound var b end deduction as var c tagged guard var s tagged guard var b tagged guard open if var p then true else deduction four var p head conclude var c head condition var s bound var b end deduction and deduction four star var p tail conclude var c tail condition var s bound var b end deduction end define end math ] " \newline Elementwise application of " [ math deduction four var p conclude var c condition var s bound var b end deduction end math ] ". " [ math var x head end math ] " and " [ math var x tail end math ] " denote the head and tail, respectively, of the pair " [ math var x end math ] ". Terms are represented as lists comprising the principal operator followed by arguments just like Lisp S-expressions. The principal operator in turn is a list whose first two elements are cardinals that identify the operator followed by debugging information.
\item " [ math value define deduction five var p condition var s bound var b end deduction as var p tagged guard var s tagged guard open if var b then true else macro newline tuple quote var x avoid var y end quote head comma tuple quote quote x end quote end quote head comma var b head head end tuple comma tuple quote quote var x end quote end quote head comma var p end tuple end tuple term in var s and deduction five var p condition var s bound var b tail end deduction end define end math ] " \newline For each variable that is bound in the context according to the association list " [ math var b end math ] ", check that the list " [ math var s end math ] " of side conditions ensures that the meta variables " [ math var p end math ] " denotes a term whose free variables do not get caught in the context. " [ math var x term in var y end math ] " is true if the term " [ math var x end math ] " belongs to the list " [ math var y end math ] " of terms.
\item " [ math value define deduction six var p conclude var c exception var e bound var b end deduction as var p tagged guard var c tagged guard var b tagged guard var e tagged guard macro newline open if var p term root equal quote object x end quote then var p term in var e select var b else parenthesis var p pair var c end parenthesis pair var b end select else macro newline open if not var p term root equal var c then true else macro newline open if var p term root equal quote meta a end quote then var b else macro newline open if var p term root equal quote for all var x indeed var y end quote then deduction six var p second conclude var c second exception var c first pair var e bound var b end deduction else macro newline deduction six star var p tail conclude var c tail exception var e bound var b end deduction end define end math ] "
\item " [ math value define deduction six star var p conclude var c exception var e bound var b end deduction as var p tagged guard var c tagged guard var b tagged guard var e tagged guard open if var p then var b else deduction six star var p tail conclude var c tail exception var e bound deduction six var p head conclude var c head exception var e bound var b end deduction end deduction end define end math ] " \newline Elementwise application of " [ math deduction six var p conclude var c exception var e bound var b end deduction end math ] ".
\item " [ math value define deduction seven var p end deduction as var p term root equal quote for all terms var x indeed var y end quote select deduction seven var p second end deduction else var p end select end define end math ] " \newline Removal of all metaquantifiers.
\item " [ math value define deduction eight var p bound var b end deduction as macro newline open if var p term root equal quote for all terms var x indeed var y end quote then deduction eight var p second bound var p first pair var b end deduction else macro newline open if var p term root equal quote meta a end quote then var p term in var b else deduction eight star var p tail bound var b end deduction end define end math ] " \newline True if all free meta variables of " [ math var p end math ] " occur in the list " [ math var b end math ] " of meta variables.
\item " [ math value define deduction eight star var p bound var b end deduction as var b tagged guard open if var p then true else deduction eight var p head bound var b end deduction macro and deduction eight star var p tail bound var b end deduction end define end math ] " \newline Elementwise application of " [ math deduction eight var p bound var b end deduction end math ] ".
\end{list}
\subsection{Avoidance}
\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}
\item " [ math value define var x is object var as var x term root equal quote object var var x end var end quote end define end math ] "
\item " [ math macro define var x avoid var y as quote var x end quote avoid zero quote var y end quote end define end math ] "
\item " [ math value define var x avoid zero var y as lambda var c dot var x is object var and var y is metaclosed and var x avoid one var y end define end math ] "
\item " [ math value define var x avoid one var y as open if var y is object var then not var x term equal var y else newline open if not var y term root equal quote for all var x indeed var y end quote then parenthesis var x avoid star var y tail end parenthesis else newline open if var x term equal var y first then true else parenthesis var x avoid one var y second end parenthesis end define end math ] "
\item " [ math value define var x avoid star var y as var x tagged guard tagged if var y then true else parenthesis var x avoid one var y head end parenthesis macro and parenthesis var x avoid star var y tail end parenthesis end if end define end math ] "
\end{list}
\subsection{Substition}
\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}
\item " [ math macro define sub var a is var b where var x is var t end sub as sub zero quote var a end quote is quote var b end quote where quote var x end quote is quote var t end quote end sub end define end math ] "
\item " [ math value define sub zero var a is var b where var x is var t end sub as lambda var c dot var x is object var and sub one var a is var b where var x is var t end sub end define end math ] "
\item " [ math value define sub one var a is var b where var x is var t end sub as var a tagged guard var x tagged guard var t tagged guard newline open if var b term root equal quote for all var u indeed var v end quote macro and var b first term equal var x then var a term equal var b else newline open if var b is object var and var b term equal var x then var a term equal var t else newline var a term root equal var b macro and sub star var a tail is var b tail where var x is var t end sub end define end math ] "
\item " [ math value define sub star var a is var b where var x is var t end sub as var b tagged guard var x tagged guard var t tagged guard tagged if var a then true else sub one var a head is var b head where var x is var t end sub macro and sub star var a tail is var b tail where var x is var t end sub end if end define end math ] "
\end{list}
\section{Proofs}
\subsection{Proofs of FOL axioms using the inference of deduction}
We now prove axiom schemes A1 and A2 from \cite{mendelson}. Furthermore, we prove two, particular instances of A4 and A5 in a way that generalizes to arbitrary instances of those axiom schemes.
Furthermore, we prove a " [ math repetition end math ] " lemma which says " [ math for all terms meta a indeed meta a infer meta a end math ] " by a `hand made proof', i.e.\ by giving a proof metatactic explicitly which generates the sequent proof.
A page is verified by a top level verifier. The top level verifier of the present page is defined on the \href{\lgwBaseUrl index.html}{base} page. That verifier invokes, among other, a proof verifier. The proof verifier invokes each proof (where each proof is supposed to be a proof metatactic). When it does so, it applies the proof metatactic to a Logiweb cache " [ math var c end math ] " and a pair " [ math var n pair var l end math ] ". The cache " [ math var c end math ] " is the Logiweb cache of the home page of the proof, i.e.\ a structure which contains all definitions present on the home page plus all transitively referenced Logiweb pages. " [ math var n end math ] " is the identifier of the lemma (a cardinal which identifies the lemma uniquely within the home page) plus the contents of the lemma. The proof metatactic given below for proving " [ math repetition end math ] " ignores both arguments and just constructs a sequent term that proves " [ math for all terms meta a indeed meta a infer meta a end math ] ". All other proofs in the present paper macro expand into proofs that are proved by a metatactic which scans the proof for object tactics and invokes those object tactics. The only object tactic used is named $\gg$ and does unification.
\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}}
\item " [ math in theory system s lemma repetition says for all terms meta a indeed meta a infer meta a end lemma end math ] "
\item " [ math in theory system s lemma lemma a one says for all terms meta a comma meta b indeed meta a imply meta b imply meta a end lemma end math ] "
\item " [ math in theory system s lemma lemma a two says for all terms meta a comma meta b comma meta c indeed parenthesis meta a imply meta b imply meta c end parenthesis imply parenthesis meta a imply meta b end parenthesis imply meta a imply meta c end lemma end math ] "
\item " [ math in theory system s lemma lemma a four says for all object x comma object y indeed object x plus object y equal object y plus object x imply two plus three equal three plus two end lemma end math ] "
\item " [ math in theory system s lemma lemma a five says for all object x indeed parenthesis two plus three equal five imply two plus three plus object x equal five plus object x end parenthesis imply two plus three equal five imply for all object x indeed two plus three plus object x equal five plus object x end lemma end math ] "
\end{list}
\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}
\item " [ math proof of repetition reads lambda var c dot lambda var x dot quote system s infer for all terms meta a indeed meta a init end quote end proof end math ] "
\item " [ math system s proof of lemma a one reads any term meta a comma meta b end line block any term macro indent meta a comma meta b end line line ell a premise macro indent meta a end line line ell b premise macro indent meta b end line because repetition modus ponens ell a indeed macro indent meta a end line line ell c end block because deduction modus ponens ell c indeed meta a imply meta b imply meta a qed end math ] "
\item " [ math system s proof of lemma a two reads any term meta a comma meta b comma meta c end line block any term macro indent meta a comma meta b comma meta c end line line ell a premise macro indent meta a imply meta b imply meta c end line line ell b premise macro indent meta a imply meta b end line line ell c premise macro indent meta a end line line ell d because ell b object modus ponens ell c indeed macro indent meta b end line line ell f because ell a object modus ponens ell c indeed macro indent meta b imply meta c end line because ell f object modus ponens ell d indeed macro indent meta c end line line ell e end block because deduction modus ponens ell e indeed parenthesis meta a imply meta b imply meta c end parenthesis imply parenthesis meta a imply meta b end parenthesis imply meta a imply meta c qed end math ] "
\item " [ math system s proof of lemma a four reads block line ell a premise macro indent object x plus object y equal object y plus object x end line because repetition modus ponens ell a indeed macro indent object x plus object y equal object y plus object x end line line ell b end block because deduction modus ponens ell b indeed for all object x indeed for all object y indeed object x plus object y equal object y plus object x imply two plus three equal three plus two qed end math ] "
\item " [ math system s proof of lemma a five reads block line ell a premise macro indent two plus three equal five imply two plus three plus object x equal five plus object x end line line ell b premise macro indent two plus three equal five end line line ell c because ell a object modus ponens ell b indeed macro indent two plus three plus object x equal five plus object x end line because rule gen modus ponens ell c indeed macro indent for all object x indeed two plus three plus object x equal five plus object x end line line ell d end block because deduction modus ponens ell d indeed for all object x indeed parenthesis two plus three equal five imply two plus three plus object x equal five plus object x end parenthesis imply two plus three equal five imply for all object x indeed two plus three plus object x equal five plus object x qed end math ] "
\end{list}
\subsection{A proof of " [ math var x plus var y equal var y plus var x end math ] "}
\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}
\item " [ math in theory system s lemma prop three two a says for all terms meta a indeed meta a equal meta a end lemma end math ] "
\item " [ math in theory system s lemma prop three two b says for all terms meta a comma meta b indeed meta a equal meta b infer meta b equal meta a end lemma end math ] "
\item " [ math in theory system s lemma prop three two c says for all terms meta a comma meta b comma meta c indeed meta a equal meta b infer meta b equal meta c infer meta a equal meta c end lemma end math ] "
\item " [ math in theory system s lemma prop three two d says for all terms meta a comma meta b comma meta c indeed meta a equal meta c infer meta b equal meta c infer meta a equal meta b end lemma end math ] "
\item " [ math in theory system s lemma prop three two e says for all terms meta a comma meta b comma meta c indeed meta a equal meta b infer meta a plus meta c equal meta b plus meta c end lemma end math ] "
\item " [ math in theory system s lemma prop three two f says for all terms meta a indeed meta a equal zero plus meta a end lemma end math ] "
\item " [ math in theory system s lemma prop three two g says for all terms meta a comma meta b indeed meta a suc plus meta b equal parenthesis meta a plus meta b end parenthesis suc end lemma end math ] "
\item " [ math in theory system s lemma prop three two h says for all terms meta a comma meta b indeed meta a plus meta b equal meta b plus meta a end lemma end math ] "
\end{list}
\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}
\item " [ math system s proof of prop three two a reads any term meta a end line line ell a because axiom s five indeed meta a plus zero equal meta a end line because axiom s one modus ponens ell a modus ponens ell a indeed meta a equal meta a qed end math ] "
\item " [ math system s proof of prop three two b reads any term meta a comma meta b end line line ell a premise meta a equal meta b end line line ell b because prop three two a indeed meta a equal meta a end line because axiom s one modus ponens ell a modus ponens ell b indeed meta b equal meta a qed end math ] "
\item " [ math system s proof of prop three two c reads any term meta a comma meta b comma meta c end line line ell a premise meta a equal meta b end line line ell b premise meta b equal meta c end line line ell c because prop three two b modus ponens ell a indeed meta b equal meta a end line because axiom s one modus ponens ell c modus ponens ell b indeed meta a equal meta c qed end math ] "
\item " [ math system s proof of prop three two d reads any term meta a comma meta b comma meta c end line line ell a premise meta a equal meta c end line line ell b premise meta b equal meta c end line line ell c because prop three two b modus ponens ell b indeed meta c equal meta b end line because prop three two c modus ponens ell a modus ponens ell c indeed meta a equal meta b qed end math ] "
\item " [ math in theory system s lemma prop three two e one says for all terms meta a comma meta b indeed meta a equal meta b imply meta a plus zero equal meta b plus zero end lemma end math ] "
\item " [ math system s proof of prop three two e one reads any term meta a comma meta b end line block any term macro indent meta a comma meta b end line line ell a premise macro indent meta a equal meta b end line line ell b because axiom s five indeed macro indent meta a plus zero equal meta a end line line ell c because prop three two c modus ponens ell b modus ponens ell a indeed macro indent meta a plus zero equal meta b end line line ell d because axiom s five indeed macro indent meta b plus zero equal meta b end line because prop three two d modus ponens ell c modus ponens ell d indeed macro indent meta a plus zero equal meta b plus zero end line line ell e end block because deduction modus ponens ell e indeed meta a equal meta b imply meta a plus zero equal meta b plus zero qed end math ] "
\item " [ math in theory system s lemma prop three two e two says for all terms meta a comma meta b comma meta c indeed parenthesis meta a equal meta b imply meta a plus meta c equal meta b plus meta c end parenthesis imply parenthesis meta a equal meta b imply meta a plus meta c suc equal meta b plus meta c suc end parenthesis end lemma end math ] "
\item " [ math system s proof of prop three two e two reads any term meta a comma meta b comma meta c end line block any term macro indent meta a comma meta b comma meta c end line line ell a premise macro indent meta a equal meta b imply meta a plus meta c equal meta b plus meta c end line line ell b premise macro indent meta a equal meta b end line line ell c because ell a object modus ponens ell b indeed macro indent meta a plus meta c equal meta b plus meta c end line line ell d because axiom s two modus ponens ell c indeed macro indent parenthesis meta a plus meta c end parenthesis suc equal parenthesis meta b plus meta c end parenthesis suc end line line ell e because axiom s six indeed macro indent meta a plus meta c suc equal parenthesis meta a plus meta c end parenthesis suc end line line ell f because prop three two c modus ponens ell e modus ponens ell d indeed macro indent meta a plus meta c suc equal parenthesis meta b plus meta c end parenthesis suc end line line ell g because axiom s six indeed macro indent meta b plus meta c suc equal parenthesis meta b plus meta c end parenthesis suc end line because prop three two d modus ponens ell f modus ponens ell g indeed macro indent meta a plus meta c suc equal meta b plus meta c suc end line line ell h end block because deduction modus ponens ell h indeed parenthesis meta a equal meta b imply meta a plus meta c equal meta b plus meta c end parenthesis imply meta a equal meta b imply meta a plus meta c suc equal meta b plus meta c suc qed end math ] "
\item " [ math system s proof of prop three two e reads any term meta a comma meta b comma meta c end line line ell d premise meta a equal meta b end line block line ell a because prop three two e one indeed macro indent object x equal object y imply object x plus zero equal object y plus zero end line line ell b because prop three two e two indeed macro indent parenthesis object x equal object y imply object x plus object z equal object y plus object z end parenthesis imply parenthesis object x equal object y imply object x plus object z suc equal object y plus object z suc end parenthesis end line because axiom s nine at object z modus ponens ell a modus ponens ell b indeed macro indent object x equal object y imply object x plus object z equal object y plus object z end line line ell c end block line ell e because deduction modus ponens ell c indeed meta a equal meta b imply meta a plus meta c equal meta b plus meta c end line because ell e object modus ponens ell d indeed meta a plus meta c equal meta b plus meta c qed end math ] "
\item " [ math in theory system s lemma prop three two f one says zero equal zero plus zero end lemma end math ] "
\item " [ math system s proof of prop three two f one reads line ell a because axiom s five indeed zero plus zero equal zero end line because prop three two b modus ponens ell a indeed zero equal zero plus zero qed end math ] "
\item " [ math in theory system s lemma prop three two f two says for all terms meta a indeed meta a equal zero plus meta a imply meta a suc equal zero plus meta a suc end lemma end math ] "
\item " [ math system s proof of prop three two f two reads any term meta a end line block any term macro indent meta a end line line ell a premise macro indent meta a equal zero plus meta a end line line ell b because axiom s two modus ponens ell a indeed macro indent meta a suc equal parenthesis zero plus meta a end parenthesis suc end line line ell c because axiom s six indeed macro indent zero plus meta a suc equal parenthesis zero plus meta a end parenthesis suc end line because prop three two d modus ponens ell b modus ponens ell c indeed macro indent meta a suc equal zero plus meta a suc end line line ell d end block because deduction modus ponens ell d indeed meta a equal zero plus meta a imply meta a suc equal zero plus meta a suc qed end math ] "
\item " [ math system s proof of prop three two f reads any term meta a end line block line ell a because prop three two f one indeed macro indent zero equal zero plus zero end line line ell b because prop three two f two indeed macro indent object x equal zero plus object x imply object x suc equal zero plus object x suc end line because axiom s nine at object x modus ponens ell a modus ponens ell b indeed macro indent object x equal zero plus object x end line line ell c end block because deduction modus ponens ell c indeed meta a equal zero plus meta a qed end math ] "
\item " [ math in theory system s lemma prop three two g one says for all terms meta a indeed meta a suc plus zero equal parenthesis meta a plus zero end parenthesis suc end lemma end math ] "
\item " [ math system s proof of prop three two g one reads any term meta a end line line ell a because axiom s five indeed meta a suc plus zero equal meta a suc end line line ell b because axiom s five indeed meta a plus zero equal meta a end line line ell c because axiom s two modus ponens ell b indeed parenthesis meta a plus zero end parenthesis suc equal meta a suc end line because prop three two d modus ponens ell a modus ponens ell c indeed meta a suc plus zero equal parenthesis meta a plus zero end parenthesis suc qed end math ] "
\item " [ math in theory system s lemma prop three two g two says for all terms meta a comma meta b indeed meta a suc plus meta b equal parenthesis meta a plus meta b end parenthesis suc imply meta a suc plus meta b suc equal parenthesis meta a plus meta b suc end parenthesis suc end lemma end math ] "
\item " [ math system s proof of prop three two g two reads any term meta a comma meta b end line block any term macro indent meta a comma meta b end line line ell a premise macro indent meta a suc plus meta b equal parenthesis meta a plus meta b end parenthesis suc end line line ell b because axiom s two modus ponens ell a indeed macro indent parenthesis meta a suc plus meta b end parenthesis suc equal parenthesis meta a plus meta b end parenthesis suc suc end line line ell c because axiom s six indeed macro indent meta a suc plus meta b suc equal parenthesis meta a suc plus meta b end parenthesis suc end line line ell d because prop three two c modus ponens ell c modus ponens ell b indeed macro indent meta a suc plus meta b suc equal parenthesis meta a plus meta b end parenthesis suc suc end line line ell e because axiom s six indeed macro indent meta a plus meta b suc equal parenthesis meta a plus meta b end parenthesis suc end line line ell f because axiom s two modus ponens ell e indeed macro indent parenthesis meta a plus meta b suc end parenthesis suc equal parenthesis meta a plus meta b end parenthesis suc suc end line because prop three two d modus ponens ell d modus ponens ell f indeed macro indent meta a suc plus meta b suc equal parenthesis meta a plus meta b suc end parenthesis suc end line line ell g end block because deduction modus ponens ell g indeed meta a suc plus meta b equal parenthesis meta a plus meta b end parenthesis suc imply meta a suc plus meta b suc equal parenthesis meta a plus meta b suc end parenthesis suc qed end math ] "
\item " [ math system s proof of prop three two g reads any term meta a comma meta b end line block line ell a because prop three two g one indeed macro indent object x suc plus zero equal parenthesis object x plus zero end parenthesis suc end line line ell b because prop three two g two indeed macro indent object x suc plus object y equal parenthesis object x plus object y end parenthesis suc imply object x suc plus object y suc equal parenthesis object x plus object y suc end parenthesis suc end line because axiom s nine at object y modus ponens ell a modus ponens ell b indeed macro indent object x suc plus object y equal parenthesis object x plus object y end parenthesis suc end line line ell e end block because deduction modus ponens ell e indeed meta a suc plus meta b equal parenthesis meta a plus meta b end parenthesis suc qed end math ] "
\item " [ math in theory system s lemma prop three two h one says for all terms meta a indeed meta a plus zero equal zero plus meta a end lemma end math ] "
\item " [ math system s proof of prop three two h one reads any term meta a end line line ell a because axiom s five indeed meta a plus zero equal meta a end line line ell b because prop three two f indeed meta a equal zero plus meta a end line because prop three two c modus ponens ell a modus ponens ell b indeed meta a plus zero equal zero plus meta a qed end math ] "
\item " [ math in theory system s lemma prop three two h two says for all terms meta a comma meta b indeed meta a plus meta b equal meta b plus meta a imply meta a plus meta b suc equal meta b suc plus meta a end lemma end math ] "
\item " [ math system s proof of prop three two h two reads any term meta a comma meta b end line block any term macro indent meta a comma meta b end line line ell a premise macro indent meta a plus meta b equal meta b plus meta a end line line ell b because axiom s two modus ponens ell a indeed macro indent parenthesis meta a plus meta b end parenthesis suc equal parenthesis meta b plus meta a end parenthesis suc end line line ell c because axiom s six indeed macro indent meta a plus meta b suc equal parenthesis meta a plus meta b end parenthesis suc end line line ell d because prop three two c modus ponens ell c modus ponens ell b indeed macro indent meta a plus meta b suc equal parenthesis meta b plus meta a end parenthesis suc end line line ell e because prop three two g indeed macro indent meta b suc plus meta a equal parenthesis meta b plus meta a end parenthesis suc end line because prop three two d modus ponens ell d modus ponens ell e indeed macro indent meta a plus meta b suc equal meta b suc plus meta a end line line ell f end block because deduction modus ponens ell f indeed meta a plus meta b equal meta b plus meta a imply meta a plus meta b suc equal meta b suc plus meta a qed end math ] "
\item " [ math system s proof of prop three two h reads any term meta a comma meta b end line block line ell a because prop three two h one indeed macro indent object x plus zero equal zero plus object x end line line ell b because prop three two h two indeed macro indent object x plus object y equal object y plus object x imply object x plus object y suc equal object y suc plus object x end line because axiom s nine at object y modus ponens ell a modus ponens ell b indeed macro indent object x plus object y equal object y plus object x end line line ell c end block because deduction modus ponens ell c indeed meta a plus meta b equal meta b plus meta a qed end math ] "
\end{list}
%------------------------------------------------------------------------------
\bibliographystyle{alpha}
\bibliography{./page}
%------------------------------------------------------------------------------
\everymath{}
\everydisplay{}
\end{document}
End of file
latex appendix
bibtex appendix
latex appendix
latex appendix
dvipdfm appendix
File chores.tex
\documentclass [fleqn]{article}
\everymath{\rm}
\usepackage{latexsym}
\setlength {\overfullrule }{0mm}
\input{lgwinclude}
\usepackage{url}
\usepackage[dvipdfm=true]{hyperref}
\hypersetup{pdfpagemode=none}
\hypersetup{pdfstartpage=1}
\hypersetup{pdfstartview=FitBH}
\hypersetup{pdfpagescrop={120 130 490 730}}
\hypersetup{pdftitle=Logiweb sequent calculus - Chores}
\hypersetup{colorlinks=true}
\begin {document}
\title {Logiweb sequent calculus, Chores}
\author {Klaus Grue}
\date {\today}
\maketitle
\tableofcontents
\section{Test cases}
\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}
\item " [ math test parenthesis object x avoid object y equal object z imply for all object x indeed object x equal object y end parenthesis apply check end test end math ] "
\item " [ math false test parenthesis object x avoid object x equal object z imply for all object x indeed object x equal object y end parenthesis apply check end test end math ] "
\item " [ math false test parenthesis object x avoid object y equal object x imply for all object x indeed object x equal object y end parenthesis apply check end test end math ] "
\item " [ math false test parenthesis object x avoid object y equal object z imply for all object y indeed object x equal object y end parenthesis apply check end test end math ] "
\item " [ math test sub object a is object a where object b is object c end sub apply check end test end math ] "
\item " [ math false test sub object b is object a where object b is object c end sub apply check end test end math ] "
\item " [ math false test sub object c is object a where object b is object c end sub apply check end test end math ] "
\item " [ math false test sub object a is object b where object b is object c end sub apply check end test end math ] "
\item " [ math false test sub object b is object b where object b is object c end sub apply check end test end math ] "
\item " [ math test sub object c is object b where object b is object c end sub apply check end test end math ] "
\item " [ math test sub for all object a indeed object a equal object b is for all object a indeed object a equal object b where object a is object c end sub apply check end test end math ] "
\item " [ math test sub for all object a indeed object a equal object c is for all object a indeed object a equal object b where object b is object c end sub apply check end test end math ] "
\item " [ math test sub for all object a indeed object a equal zero plus object a imply object c times object d equal zero plus object c times object d is for all object a indeed object a equal zero plus object a imply object b equal zero plus object b where object b is object c times object d end sub apply check end test end math ] "
\item " [ math test sub for all object a indeed object a equal zero plus object a imply object b equal zero plus object b is for all object a indeed object a equal zero plus object a imply object b equal zero plus object b where object a is object c end sub apply check end test end math ] "
\item " [ math test deduction zero conclude zero end deduction apply check end test end math ] "
\item " [ math false test deduction zero conclude one end deduction apply check end test end math ] "
\item " [ math test deduction eight quote for all terms meta a indeed meta a end quote bound true end deduction end test end math ] "
\item " [ math test deduction seven quote for all terms meta a indeed meta a end quote end deduction term equal quote meta a end quote end test end math ] "
\item " [ math test deduction for all terms meta a indeed meta a conclude meta a end deduction apply check end test end math ] "
\item " [ math false test deduction meta a conclude meta b end deduction apply check end test end math ] "
\item " [ math false test deduction for all terms meta a indeed meta a conclude meta b end deduction apply check end test end math ] "
\item " [ math test deduction for all terms meta a comma meta b indeed meta a infer meta b conclude meta a imply meta b end deduction apply check end test end math ] "
\item " [ math false test deduction for all terms meta a comma meta b indeed meta a infer meta b conclude meta a imply meta a end deduction apply check end test end math ] "
\item " [ math false test deduction for all terms meta a comma meta b indeed meta a infer meta b conclude meta b imply meta b end deduction apply check end test end math ] "
\item " [ math false test deduction for all terms meta a comma meta b indeed meta a infer meta b conclude zero end deduction apply check end test end math ] "
\item " [ math false test deduction zero conclude meta a imply meta a end deduction apply check end test end math ] "
\item " [ math test deduction for all terms meta a comma meta b comma meta c indeed meta a infer meta b infer meta c conclude meta a imply meta b imply meta c end deduction apply check end test end math ] "
\item " [ math false test deduction for all terms meta a comma meta b indeed meta a infer meta b infer meta a conclude meta a imply meta b imply meta c end deduction apply check end test end math ] "
\item " [ math false test deduction for all terms meta a comma meta b comma meta c indeed parenthesis meta a infer meta b end parenthesis infer meta c conclude parenthesis meta a imply meta b end parenthesis imply meta c end deduction apply check end test end math ] "
\item " [ math false test deduction zero conclude object x end deduction apply check end test end math ] "
\item " [ math test deduction object x conclude zero end deduction apply check end test end math ] "
\item " [ math test deduction object x conclude object x end deduction apply check end test end math ] "
\item " [ math false test deduction for all object x indeed object x conclude object x end deduction apply check end test end math ] "
\item " [ math test deduction object x conclude for all object y indeed object z end deduction apply check end test end math ] "
\item " [ math test deduction for all object x indeed object x conclude for all object x indeed object x end deduction apply check end test end math ] "
\item " [ math test deduction zero infer zero conclude zero imply zero end deduction apply check end test end math ] "
\item " [ math false test deduction object x infer zero conclude zero imply zero end deduction apply check end test end math ] "
\item " [ math test deduction zero infer object x conclude zero imply zero end deduction apply check end test end math ] "
\item " [ math false test deduction object x infer object x conclude zero imply zero end deduction apply check end test end math ] "
\item " [ math test deduction zero infer zero conclude for all object x indeed zero imply zero end deduction apply check end test end math ] "
\item " [ math test deduction object x infer zero conclude for all object x indeed object x imply zero end deduction apply check end test end math ] "
\item " [ math test deduction zero infer object x conclude for all object x indeed zero imply object x end deduction apply check end test end math ] "
\item " [ math test deduction object x infer object x conclude for all object x indeed object x imply object x end deduction apply check end test end math ] "
\item " [ math false test deduction zero infer zero conclude zero imply for all object x indeed zero end deduction apply check end test end math ] "
\item " [ math false test deduction object x infer zero conclude zero imply for all object x indeed zero end deduction apply check end test end math ] "
\item " [ math test deduction zero infer object x conclude zero imply for all object y indeed object z end deduction apply check end test end math ] "
\item " [ math false test deduction object x infer object x conclude zero imply for all object x indeed object x end deduction apply check end test end math ] "
\item " [ math false test deduction zero infer zero conclude for all object x indeed zero imply for all object x indeed zero end deduction apply check end test end math ] "
\item " [ math false test deduction object x infer zero conclude for all object x indeed object x imply for all object x indeed zero end deduction apply check end test end math ] "
\item " [ math test deduction zero infer object x conclude for all object x indeed zero imply two end deduction apply check end test end math ] "
\item " [ math test deduction object x infer object x conclude for all object x indeed object x imply three end deduction apply check end test end math ] "
\item " [ math test deduction object x plus object y equal object y plus object x conclude two plus three equal three plus two end deduction apply check end test end math ] "
\item " [ math false test deduction object x plus object y equal object y plus object x conclude two plus three equal two plus three end deduction apply check end test end math ] "
\item " [ math false test deduction object x plus object y equal object y plus object x conclude two plus three equal two plus two end deduction apply check end test end math ] "
\item " [ math false test deduction object x plus object y equal object y plus object x conclude two plus three equal three plus three end deduction apply check end test end math ] "
\end{list}
\section{Pyk definitions}
\begin{flushleft}
" [ math protect define pyk of general macro define x as x end define as text "general macro define "! as "! end define" end text end define linebreak define pyk of make root visible x end visible as text "make root visible "! end visible" end text end define linebreak define pyk of sequent example axiom as text "sequent example axiom" end text end define linebreak define pyk of sequent example rule as text "sequent example rule" end text end define linebreak define pyk of sequent example contradiction as text "sequent example contradiction" end text end define linebreak define pyk of sequent example theory as text "sequent example theory" end text end define linebreak define pyk of sequent example lemma as text "sequent example lemma" end text end define linebreak define pyk of set x end set as text "set "! end set" end text end define linebreak define pyk of object var x end var as text "object var "! end var" end text end define linebreak define pyk of object a as text "object a" end text end define linebreak define pyk of object b as text "object b" end text end define linebreak define pyk of object c as text "object c" end text end define linebreak define pyk of object d as text "object d" end text end define linebreak define pyk of object e as text "object e" end text end define linebreak define pyk of object f as text "object f" end text end define linebreak define pyk of object g as text "object g" end text end define linebreak define pyk of object h as text "object h" end text end define linebreak define pyk of object i as text "object i" end text end define linebreak define pyk of object j as text "object j" end text end define linebreak define pyk of object k as text "object k" end text end define linebreak define pyk of object l as text "object l" end text end define linebreak define pyk of object m as text "object m" end text end define linebreak define pyk of object n as text "object n" end text end define linebreak define pyk of object o as text "object o" end text end define linebreak define pyk of object p as text "object p" end text end define linebreak define pyk of object q as text "object q" end text end define linebreak define pyk of object r as text "object r" end text end define linebreak define pyk of object s as text "object s" end text end define linebreak define pyk of object t as text "object t" end text end define linebreak define pyk of object u as text "object u" end text end define linebreak define pyk of object v as text "object v" end text end define linebreak define pyk of object w as text "object w" end text end define linebreak define pyk of object x as text "object x" end text end define linebreak define pyk of object y as text "object y" end text end define linebreak define pyk of object z as text "object z" end text end define linebreak define pyk of sub x is x where x is x end sub as text "sub "! is "! where "! is "! end sub" end text end define linebreak define pyk of sub zero x is x where x is x end sub as text "sub zero "! is "! where "! is "! end sub" end text end define linebreak define pyk of sub one x is x where x is x end sub as text "sub one "! is "! where "! is "! end sub" end text end define linebreak define pyk of sub star x is x where x is x end sub as text "sub star "! is "! where "! is "! end sub" end text end define linebreak define pyk of deduction x conclude x end deduction as text "deduction "! conclude "! end deduction" end text end define linebreak define pyk of deduction zero x conclude x end deduction as text "deduction zero "! conclude "! end deduction" end text end define linebreak define pyk of deduction one x conclude x condition x end deduction as text "deduction one "! conclude "! condition "! end deduction" end text end define linebreak define pyk of deduction two x conclude x condition x end deduction as text "deduction two "! conclude "! condition "! end deduction" end text end define linebreak define pyk of deduction three x conclude x condition x bound x end deduction as text "deduction three "! conclude "! condition "! bound "! end deduction" end text end define linebreak define pyk of deduction four x conclude x condition x bound x end deduction as text "deduction four "! conclude "! condition "! bound "! end deduction" end text end define linebreak define pyk of deduction four star x conclude x condition x bound x end deduction as text "deduction four star "! conclude "! condition "! bound "! end deduction" end text end define linebreak define pyk of deduction five x condition x bound x end deduction as text "deduction five "! condition "! bound "! end deduction" end text end define linebreak define pyk of deduction six x conclude x exception x bound x end deduction as text "deduction six "! conclude "! exception "! bound "! end deduction" end text end define linebreak define pyk of deduction six star x conclude x exception x bound x end deduction as text "deduction six star "! conclude "! exception "! bound "! end deduction" end text end define linebreak define pyk of deduction seven x end deduction as text "deduction seven "! end deduction" end text end define linebreak define pyk of deduction eight x bound x end deduction as text "deduction eight "! bound "! end deduction" end text end define linebreak define pyk of deduction eight star x bound x end deduction as text "deduction eight star "! bound "! end deduction" end text end define linebreak define pyk of system s as text "system s" end text end define linebreak define pyk of double negation as text "double negation" end text end define linebreak define pyk of rule mp as text "rule mp" end text end define linebreak define pyk of rule gen as text "rule gen" end text end define linebreak define pyk of deduction as text "deduction" end text end define linebreak define pyk of axiom s one as text "axiom s one" end text end define linebreak define pyk of axiom s two as text "axiom s two" end text end define linebreak define pyk of axiom s three as text "axiom s three" end text end define linebreak define pyk of axiom s four as text "axiom s four" end text end define linebreak define pyk of axiom s five as text "axiom s five" end text end define linebreak define pyk of axiom s six as text "axiom s six" end text end define linebreak define pyk of axiom s seven as text "axiom s seven" end text end define linebreak define pyk of axiom s eight as text "axiom s eight" end text end define linebreak define pyk of axiom s nine as text "axiom s nine" end text end define linebreak define pyk of repetition as text "repetition" end text end define linebreak define pyk of lemma a one as text "lemma a one" end text end define linebreak define pyk of lemma a two as text "lemma a two" end text end define linebreak define pyk of lemma a four as text "lemma a four" end text end define linebreak define pyk of lemma a five as text "lemma a five" end text end define linebreak define pyk of prop three two a as text "prop three two a" end text end define linebreak define pyk of prop three two b as text "prop three two b" end text end define linebreak define pyk of prop three two c as text "prop three two c" end text end define linebreak define pyk of prop three two d as text "prop three two d" end text end define linebreak define pyk of prop three two e one as text "prop three two e one" end text end define linebreak define pyk of prop three two e two as text "prop three two e two" end text end define linebreak define pyk of prop three two e as text "prop three two e" end text end define linebreak define pyk of prop three two f one as text "prop three two f one" end text end define linebreak define pyk of prop three two f two as text "prop three two f two" end text end define linebreak define pyk of prop three two f as text "prop three two f" end text end define linebreak define pyk of prop three two g one as text "prop three two g one" end text end define linebreak define pyk of prop three two g two as text "prop three two g two" end text end define linebreak define pyk of prop three two g as text "prop three two g" end text end define linebreak define pyk of prop three two h one as text "prop three two h one" end text end define linebreak define pyk of prop three two h two as text "prop three two h two" end text end define linebreak define pyk of prop three two h as text "prop three two h" end text end define linebreak define pyk of block one x state x cache x end block as text "block one "! state "! cache "! end block" end text end define linebreak define pyk of block two x end block as text "block two "! end block" end text end define linebreak define pyk of x hide as text ""! hide" end text end define linebreak define pyk of macro indent x as text "macro indent "!" end text end define linebreak define pyk of x suc as text ""! suc" end text end define linebreak define pyk of x equal x as text ""! equal "!" end text end define linebreak define pyk of x unequal x as text ""! unequal "!" end text end define linebreak define pyk of x is object var as text ""! is object var" end text end define linebreak define pyk of x avoid zero x as text ""! avoid zero "!" end text end define linebreak define pyk of x avoid one x as text ""! avoid one "!" end text end define linebreak define pyk of x avoid star x as text ""! avoid star "!" end text end define linebreak define pyk of exist x indeed x as text "exist "! indeed "!" end text end define linebreak define pyk of for all x indeed x as text "for all "! indeed "!" end text end define linebreak define pyk of for all objects x indeed x as text "for all objects "! indeed "!" end text end define linebreak define pyk of x imply x as text ""! imply "!" end text end define linebreak define pyk of x if and only if x as text ""! if and only if "!" end text end define linebreak define pyk of x avoid x as text ""! avoid "!" end text end define linebreak define pyk of x object modus ponens x as text ""! object modus ponens "!" end text end define linebreak define pyk of for all terms x indeed x as text "for all terms "! indeed "!" end text end define linebreak define pyk of block x line x end block x as text "block "! line "! end block "!" end text end define linebreak define pyk of because x indeed x end line as text "because "! indeed "! end line" end text end define linebreak define pyk of any term x end line x as text "any term "! end line "!" end text end define linebreak define pyk of x alternative x as text ""! alternative "!" end text end define linebreak define pyk of evaluates to as text "evaluates to" end text end define linebreak define pyk of x safe row x as text ""! safe row "!" end text end define linebreak define pyk of check as text "check" end text end define linebreak unicode end of text end protect end math ] "
\end{flushleft}
\section{\TeX\ definitions}
\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}
\item " [ math tex define general macro define var x as var y end define as "
[#1/tex name/tex.
\stackrel {\circ}{=}#2.
]" end define end math ] "
\item " [ math tex define make root visible var x end visible as "#1/tex name/tex." end define end math ] "
\item " [ math tex name define make root visible var x end visible as "
RootVisible(#1.
)" end define end math ] "
\item " [ math tex define var x hide as "#1.
{}^{hide}" end define end math ] "
\item " [ math tex define var x suc as "#1.
{}'" end define end math ] "
\item " [ math tex define var x equal var y as "#1.
= #2." end define end math ] "
\item " [ math tex define var x unequal var y as "#1.
\neq #2." end define end math ] "
\item " [ math tex define var x imply var y as "#1.
\Rightarrow #2." end define end math ] "
\item " [ math tex define var x if and only if var y as "#1.
\Leftrightarrow #2." end define end math ] "
\item " [ math tex define var x alternative var y as "#1.
\mathrel{|} #2." end define end math ] "
\item " [ math tex define exist var x indeed var y as "
\exists #1.
\colon #2." end define end math ] "
\item " [ math tex define for all var x indeed var y as "
\forall #1.
\colon #2." end define end math ] "
\item " [ math tex define for all objects var x indeed var y as "
\forall_{obj} #1.
\colon #2." end define end math ] "
\item " [ math tex define for all terms var x indeed var y as "
\Pi #1.
\colon #2." end define end math ] "
\item " [ math tex define any term var i end line var p as "
\newline \makebox [0.1\textwidth ][l]{$
\if \relax \csname lgwprooflinep\endcsname L_? \else
\global \advance \lgwproofline by 1
L\ifnum \lgwproofline <10 0\fi \number \lgwproofline
\fi
$:}\makebox [0.4\textwidth ][l]{$Arbitrary{}\gg{}$}\quad
\parbox [t]{0.4\textwidth }{$#1.
$\hfill \makebox [0mm][l]{\quad ;}}#2." end define end math ] "
\item " [ math tex name define any term var i end line var p as "
Arbitrary \gg #1.
;#2." end define end math ] "
\item " [ math tex define var x safe row var y as "#1.
\\{}#2." end define end math ] "
\item " [ math tex name define var x safe row var y as "#1.
\backslash \backslash #2." end define end math ] "
\item " [ math tex define sequent example axiom as "
A" end define end math ] "
\item " [ math tex define sequent example rule as "
R" end define end math ] "
\item " [ math tex define sequent example contradiction as "
C" end define end math ] "
\item " [ math tex define sequent example theory as "
T" end define end math ] "
\item " [ math tex define sequent example lemma as "
L" end define end math ] "
\item " [ math tex define set var x end set as "
\{#1.
\}" end define end math ] "
\item " [ math tex define system s as "
S" end define end math ] "
\item " [ math tex define double negation as "
Neg" end define end math ] "
\item " [ math tex define axiom s one as "
S1" end define end math ] "
\item " [ math tex define axiom s two as "
S2" end define end math ] "
\item " [ math tex define axiom s three as "
S3" end define end math ] "
\item " [ math tex define axiom s four as "
S4" end define end math ] "
\item " [ math tex define axiom s five as "
S5" end define end math ] "
\item " [ math tex define axiom s six as "
S6" end define end math ] "
\item " [ math tex define axiom s seven as "
S7" end define end math ] "
\item " [ math tex define axiom s eight as "
S8" end define end math ] "
\item " [ math tex define axiom s nine as "
S9" end define end math ] "
\item " [ math tex define rule mp as "
MP" end define end math ] "
\item " [ math tex define rule gen as "
Gen" end define end math ] "
\item " [ math tex define deduction as "
Ded" end define end math ] "
\item " [ math tex define repetition as "
Repetition" end define end math ] "
\item " [ math tex define lemma a one as "
A1'" end define end math ] "
\item " [ math tex define lemma a two as "
A2'" end define end math ] "
\item " [ math tex define lemma a four as "
A4'" end define end math ] "
\item " [ math tex define lemma a five as "
A5'" end define end math ] "
\item " [ math tex define var x is object var as "#1.
{}^{var}" end define end math ] "
\item " [ math tex define var x avoid var y as "#1.
\#.#2." end define end math ] "
\item " [ math tex define var x avoid zero var y as "#1.
\#.^0#2." end define end math ] "
\item " [ math tex define var x avoid one var y as "#1.
\#.^1#2." end define end math ] "
\item " [ math tex define var x avoid star var y as "#1.
\#.^*#2." end define end math ] "
\item " [ math tex define sub var x is var y where var z is var u end sub as "
\langle #1.
{\equiv} #2.
| #3.
{:=} #4.
\rangle " end define end math ] "
\item " [ math tex define sub zero var x is var y where var z is var u end sub as "
\langle #1.
{\equiv}^0 #2.
| #3.
{:=} #4.
\rangle " end define end math ] "
\item " [ math tex define sub one var x is var y where var z is var u end sub as "
\langle #1.
{\equiv}^1 #2.
| #3.
{:=} #4.
\rangle " end define end math ] "
\item " [ math tex define sub star var x is var y where var z is var u end sub as "
\langle #1.
{\equiv}^* #2.
| #3.
{:=} #4.
\rangle " end define end math ] "
\item " [ math tex define deduction var x conclude var y end deduction as "
Ded(#1.
,#2.
)" end define end math ] "
\item " [ math tex define deduction zero var x conclude var y end deduction as "
Ded_0(#1.
,#2.
)" end define end math ] "
\item " [ math tex define deduction one var x conclude var y condition var z end deduction as "
Ded_1(#1.
,#2.
,#3.
)" end define end math ] "
\item " [ math tex define deduction two var x conclude var y condition var z end deduction as "
Ded_2(#1.
,#2.
,#3.
)" end define end math ] "
\item " [ math tex define deduction three var x conclude var y condition var z bound var u end deduction as "
Ded_3(#1.
,#2.
,#3.
,#4.
)" end define end math ] "
\item " [ math tex define deduction four var x conclude var y condition var z bound var u end deduction as "
Ded_4(#1.
,#2.
,#3.
,#4.
)" end define end math ] "
\item " [ math tex define deduction four star var x conclude var y condition var z bound var u end deduction as "
Ded_4^*(#1.
,#2.
,#3.
,#4.
)" end define end math ] "
\item " [ math tex define deduction five var x condition var y bound var z end deduction as "
Ded_5(#1.
,#2.
,#3.
)" end define end math ] "
\item " [ math tex define deduction six var p conclude var c exception var e bound var b end deduction as "
Ded_6(#1.
,#2.
,#3.
,#4.
)" end define end math ] "
\item " [ math tex define deduction six star var p conclude var c exception var e bound var b end deduction as "
Ded_6^*(#1.
,#2.
,#3.
,#4.
)" end define end math ] "
\item " [ math tex define deduction seven var p end deduction as "
Ded_7(#1.
)" end define end math ] "
\item " [ math tex define deduction eight var p bound var b end deduction as "
Ded_8(#1.
,#2.
)" end define end math ] "
\item " [ math tex define deduction eight star var p bound var b end deduction as "
Ded_8^*(#1.
,#2.
)" end define end math ] "
\item " [ math tex define block var b line var l end block var p as "
\newline \makebox [0.1\textwidth]{}%
\parbox [b]{0.4\textwidth }{\raggedright
\setlength {\parindent }{-0.1\textwidth }%
\makebox [0.1\textwidth ][l]{$
\if \relax \csname lgwprooflinep\endcsname L_? \else
\global \advance \lgwproofline by 1
L\ifnum \lgwproofline <10 0\fi \number \lgwproofline
\fi
$:}$Block {}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{$Begin
$\hfill \makebox [0mm][l]{\quad ;}}#1.
\newline \makebox [0.1\textwidth]{}%
\parbox [b]{0.4\textwidth }{\raggedright
\setlength {\parindent }{-0.1\textwidth }%
\makebox [0.1\textwidth ][l]{$#2.
$:}$Block {}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{$End
$\hfill \makebox [0mm][l]{\quad ;}}#3." end define end math ] "
\item " [ math tex name define block var b line var l end block var p as "
Begin \, #1.
; #2.
: End ; #3." end define end math ] "
\item " [ math tex define because var a indeed var i end line as "
\newline \makebox [0.1\textwidth]{}%
\parbox [b]{0.4\textwidth }{\raggedright
\setlength {\parindent }{-0.1\textwidth }%
\makebox [0.1\textwidth ][l]{$
\if \relax \csname lgwprooflinep\endcsname L_? \else
\global \advance \lgwproofline by 1
L\ifnum \lgwproofline <10 0\fi \number \lgwproofline
\fi
$:}$#1.
{}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{$#2.
$\hfill \makebox [0mm][l]{\quad ;}}" end define end math ] "
" [ math tex name define because var a indeed var i end line as "
Last\ block\ line \, #1.
\gg #2.
\,;" end define end math ] "
\item " [ math tex define var x object modus ponens var y as "#1.
\unrhd #2." end define end math ] "
\item " [ math tex define prop three two a as "
Prop\ 3.2a" end define end math ] "
\item " [ math tex define prop three two b as "
Prop\ 3.2b" end define end math ] "
\item " [ math tex define prop three two c as "
Prop\ 3.2c" end define end math ] "
\item " [ math tex define prop three two d as "
Prop\ 3.2d" end define end math ] "
\item " [ math tex define prop three two e one as "
Prop\ 3.2e_1" end define end math ] "
\item " [ math tex define prop three two e two as "
Prop\ 3.2e_2" end define end math ] "
\item " [ math tex define prop three two e as "
Prop\ 3.2e" end define end math ] "
\item " [ math tex define prop three two f one as "
Prop\ 3.2f_1" end define end math ] "
\item " [ math tex define prop three two f two as "
Prop\ 3.2f_2" end define end math ] "
\item " [ math tex define prop three two f as "
Prop\ 3.2f" end define end math ] "
\item " [ math tex define prop three two g one as "
Prop\ 3.2g_1" end define end math ] "
\item " [ math tex define prop three two g two as "
Prop\ 3.2g_2" end define end math ] "
\item " [ math tex define prop three two g as "
Prop\ 3.2g" end define end math ] "
\item " [ math tex define prop three two h one as "
Prop\ 3.2h_1" end define end math ] "
\item " [ math tex define prop three two h two as "
Prop\ 3.2h_2" end define end math ] "
\item " [ math tex define prop three two h as "
Prop\ 3.2h" end define end math ] "
\item " [ math tex define macro indent var x as "
$%
\leftskip=1em%
$#1." end define end math ] "
\item " [ math tex name define macro indent var x as "
MacroIndent(#1.
)" end define end math ] "
\item " [ math tex define block one var t state var s cache var c end block as "
Block_1(#1.
,#2.
,#3.
)" end define end math ] "
\item " [ math tex define block two var b end block as "
Block_2(#1.
)" end define end math ] "
\item " [ math tex define evaluates to as "
\rightarrow " end define end math ] "
\end{list}
\subsection{Variables}
" [ math tex define object var var x end var as "\overline{#1.}" end define end math ] "
" [ math macro define object a as object var var a end var end define end math ] "
" [ math macro define object b as object var var b end var end define end math ] "
" [ math macro define object c as object var var c end var end define end math ] "
" [ math macro define object d as object var var d end var end define end math ] "
" [ math macro define object e as object var var e end var end define end math ] "
" [ math macro define object f as object var var f end var end define end math ] "
" [ math macro define object g as object var var g end var end define end math ] "
" [ math macro define object h as object var var h end var end define end math ] "
" [ math macro define object i as object var var i end var end define end math ] "
" [ math macro define object j as object var var j end var end define end math ] "
" [ math macro define object k as object var var k end var end define end math ] "
" [ math macro define object l as object var var l end var end define end math ] "
" [ math macro define object m as object var var m end var end define end math ] "
" [ math macro define object n as object var var n end var end define end math ] "
" [ math macro define object o as object var var o end var end define end math ] "
" [ math macro define object p as object var var p end var end define end math ] "
" [ math macro define object q as object var var q end var end define end math ] "
" [ math macro define object r as object var var r end var end define end math ] "
" [ math macro define object s as object var var s end var end define end math ] "
" [ math macro define object t as object var var t end var end define end math ] "
" [ math macro define object u as object var var u end var end define end math ] "
" [ math macro define object v as object var var v end var end define end math ] "
" [ math macro define object w as object var var w end var end define end math ] "
" [ math macro define object x as object var var x end var end define end math ] "
" [ math macro define object y as object var var y end var end define end math ] "
" [ math macro define object z as object var var z end var end define end math ] "
" [ math tex define object a as "
\mathit{a}" end define end math ] "
" [ math tex define object b as "
\mathit{b}" end define end math ] "
" [ math tex define object c as "
\mathit{c}" end define end math ] "
" [ math tex define object d as "
\mathit{d}" end define end math ] "
" [ math tex define object e as "
\mathit{e}" end define end math ] "
" [ math tex define object f as "
\mathit{f}" end define end math ] "
" [ math tex define object g as "
\mathit{g}" end define end math ] "
" [ math tex define object h as "
\mathit{h}" end define end math ] "
" [ math tex define object i as "
\mathit{i}" end define end math ] "
" [ math tex define object j as "
\mathit{j}" end define end math ] "
" [ math tex define object k as "
\mathit{k}" end define end math ] "
" [ math tex define object l as "
\mathit{l}" end define end math ] "
" [ math tex define object m as "
\mathit{m}" end define end math ] "
" [ math tex define object n as "
\mathit{n}" end define end math ] "
" [ math tex define object o as "
\mathit{o}" end define end math ] "
" [ math tex define object p as "
\mathit{p}" end define end math ] "
" [ math tex define object q as "
\mathit{q}" end define end math ] "
" [ math tex define object r as "
\mathit{r}" end define end math ] "
" [ math tex define object s as "
\mathit{s}" end define end math ] "
" [ math tex define object t as "
\mathit{t}" end define end math ] "
" [ math tex define object u as "
\mathit{u}" end define end math ] "
" [ math tex define object v as "
\mathit{v}" end define end math ] "
" [ math tex define object w as "
\mathit{w}" end define end math ] "
" [ math tex define object x as "
\mathit{x}" end define end math ] "
" [ math tex define object y as "
\mathit{y}" end define end math ] "
" [ math tex define object z as "
\mathit{z}" end define end math ] "
\section{Priority table}
" [ flush left math priority table preassociative priority check 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 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 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 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 end priority greater than preassociative priority not 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 end priority greater than preassociative priority x or x equal priority x parallel x equal priority x macro or 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 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 unicode end of text end table end math end left ] "
\end{document}
End of file
latex chores
latex chores
dvipdfm chores"
The pyk compiler, version 0.grue.20060417+ by Klaus Grue,