>(1R)-=A       /Symbols allowed.  > is highest priority and groups right.
pred, func, const   /Parameter categories allowed.  (Could allow sent too?)
mp    /First rule is mp (modus ponens).
P     /It says that from P
P>Q   /and P->Q
:Q    /you can infer Q.
ti                           /Everything else in the file is an axiom.  The next
:gen(p>(q>p))                /three axioms are tautologies from which all other
id                           /tautologies can be derived by modus ponens.  They
:gen((p>q>r)>(p>q)>(p>r))    /are not really needed since I have also included
con                          /the axiom...
:gen((-p>-q)>(-p>q)>p)
taut                         /Tautology.  This can be used to justify any gene-
:gen(taut)                   /ralization of a tautology (e.g. Ax(P(x)->P(x))).
ui                           /Universal instantiation.  "p[x|a]" means p with
:gen(Axp>p[x|a])             /all free x's replaced with some term a.
ud
:gen(Ax(P>Q)>(AxP>AxQ))
vg
:gen(P[x*]>AxP)              /P[x*] means x must not occur free in P.
ref
:gen(x=x)
sub
:gen(x=y>P>P[x?y,A])         /P[x?y,A] means P, perhaps with SOME free x's replaced by y.  Also P must be atomic.