Checking Proofs in the Metamathematics of First Order Logic

CHECKING PROOFS IN THE METAMATHEMATICS OF FIRST ORDER LOGIC

Mario Aiello

lstituto di Scienze dell'Informazione, Universita di Pisa, Corso Italia 40, 56100 Pisa Italy

and Richard Weyhrauch

A.T. Lab., Computer Science Department, Stanford University,

Stanford, California 94305 U.S.A.

Abstract

First order Llteoril's not only can ht· used in prov­ ing properti,·s of programs, but have <Jlso rcle­ vance in representation theory. The desire to rep­ resent first order theories in a computer in a feasible way requires the facility to discuss meta mathematical notions. Using metamathematics will - eventually allow to construct systems which can form<Jlly discuss how they reason. In thi s paper we present twu different first order axiomatiza­ tions of the metamathematics of the logic which FOI. (First Ordc·r Logic proof checker) checks and show sevt·ral proofs using each one. The difference betwl'en the axiomatizations is that one defines the metamathematics in a raany sorted logi c and the otlwr docs not. Proofs arc then compared and used to discuss the adequacy of sorae FOL features.

Section I Introduction

This p;qwr n·prl'sents a first attelilpt at axi­ umatizing thL· lllt·t;unatlll'matics of a first order · 1 ' .· ~ - =--~· ,.:!:.! :: ~ :_: :: !.J':_; I 1 :·: :; t·o· ~··:'"00!: ·: !tF ·:L-Pr f.'1')t (First Ordc·r Logic). The logic lvhi~lt FOL checks is described in detail in the user maaual for this program, Weyhrauch and Thomas 1974. lt is based on a system of natural deduction described in Prawitz 1965, 1970.

Our r.tot ivat ion in axiomatizing the m.:: tamathc­ matics of FOI. was the des ire to work on an example which could lw used as a case study for projected fL·atun·s of FOLand, at the same time, had inde­ pendent interes t with respect to representing the proofs of significant mathematical results to a computer.

ThL· L'Vt·ntual ability to clearly expn·ss the· LIIL·urc·ms of mallll'malics to a computer wi 11 require Lite facility to statt· and prove thPorc·ms of na·ta­

mathematics. Thert· arl' several clear examples:

a. Axiom schemas. How exactly do wt· express that

1s <Ill ax1om schc·1ua'! Wt· nt·ed to say: "if for any fir s t ord,·r sc·ntt·nce I' with one free variable y we denoLL' hy l'(n) thL' formula obtai1wd from P by sub­ stituting n for y assuming n is free for y in P, LIIL·n t h'· sc·ntence

This res,·arc h wa s ca rried out while th·· author was visiting at the A.I. Lab., Computer Science Department, Stanford University.

1s an axiom of arithml'lit·."

h. Theorem schemas. Thl' following kind ol "theorem" is sonwt iml·s Sl't'll in Sl'l thl'ory books

It asserts the existence of some particular projec tion of n+l-tuples. In its usual formulation this­ is not a theorem of set theory at all, but a meta­ theorem which states that, for each n, the above sentence is a theorem. We do not know of any ma­ chine implementation of first order logic capable of expressing the above notion in a straightfor­

ward way.

c. Subsidiary deduction rules. Below we slww how to prove that if there is a proof of Vx y. WFF then the re is also a proof of Yy x. WFF, when· WFF i s any well formed formula. We rhose this task bp · cause it seemed simp I e (·nou;!h to do, and is a theorem which may actually he usL·d. The use of mctatheorems as rules of inference by means of a reflection principle will be discussed in a future memo by Richard Weyhrauch. Eventually we hope to check some more substantial raetamathematical theorems.

d. Interesting mathematical theorems. We pres ent two examples. The first is any theorem about finite groups. The notion of finite group cannot be defined in the usual first order language of group theory. Thus many "tlll'orems" are actually me tatheorems, unless you axiomat ize groups in set theory. The second theore1o is tlw "duality pr inc i­ ple" in projective geometry.

Finally, from the viewpoint of A.I. and rp­ pr,·sentation theory tht· ability to state and prt>vt· th,·nrems of mctamatlwmatil's can hL· vpry ht·lpful in answc·ring the qul'stinns of how W<' "reflect" on tit'· reasoning we arc doing and if a proper axiomatizat ion of the metamathematics of an FOL language to-­ getl~t·r with some sort of computationally realiza­ ble reflection principle allows us to discuss in an adequate way our reasonings.

This paper is divided into two sections. ln the first one, we present the two axiom systems and the proof of the metathL'<HL'm: "for all V;lria­ bles x,y and WL·ll formed formulas f, 00 V x y.[ 00 is a tlH?o rem also 00 Y. y x.( 00 is a theorPmu . ln thL· second section we look at proofs appl'aring in th,· appPndices in order to explore· the f,·a turPs of FOI. that need improving and thc·ir usc· in "'"'~".l ing out formal proofs.

SPction 2 The Axiom System

In this st·ct ion Wt.· prt'Sl'nl two axiomatiza­ tions of tl~t· m<'l;unatl~t·matics of first order logic. Tilt· main difft'rt'll<'<' b .. twt·c·n them is that one is lion<· in a many sort<·d r i rst order logic and th<· other~ not. Tht·Sl' .:txiom;Jt iZiil ions r~_.prt·svnt an atlt·mpl :1l t·xpcrinwtll i11g wi tl1 prool s about proJH.·r­ til's ol lonmtLts atHI d<·dul'l io11s. No ,.ffort has bt·t·n SJH'Ill on gu.:ILIIllt·t:ing that tilL' ilxioms art· in­ dependc·nt. It would not only have been uninterest­ ing but also contrary to our basic philosophy. We wish to find axioms which naturally reflect the relevant notions. At the moment this axiomatizat­ ion is far from being in its final form. Neither the extent of tht· not ions involved nor the best way of expn·ssing them is considerc·d settled.

Strings and S<'quc·ncc·s of strings have been axiomatized and USL'U to de[ inc metamathematical notions. For instance, wPll formed formulas are represented as strings of symbols which satisfy the predicatt· FOI<M defining which e<mhinat ions of constants, variabl<·s pn·uicates and functions sym­ bols represent a wf f.; u<·duc t ions are tl~t·n repre­ sented as scquenCL'S of wff 's satisfying the predi­ cate PIWOFTI<EL

2.1 The Sorts

The sorts we have d,·( incd corr,·spond to thc· basic notions of till· llll'tamathcmatics i .c·. terms, formulas, individual variahlPs, logical symbols, function symbols <'t c. and tIll' notions of the do­ mains (strings und SL·quc·nc<·s of strings) in which the axiomatization has been tlefined. FOL (sec· Wcyhrauch and Thomas I 974) ;d lows thC' dPclarat ion of variablt·s to b,· of a l'l'rtain surt. In th<· for­ mulas appearing in this paper, each variable is declared to he of soml' particular sort. For in­ stance f,fl,f2, ·.. are of sort well formed formul~ t,tl,t2 ·.. of sort terms etc. For the complete set of FOL declarations see Aiello and Weyhrauch 1974.

2.2 The Domain of RepresL·ntation of the meta­ mathcmat ics.

Thl' basic notions of thl' mPtamathematics of first order logic havt· bet·n axiomatiz"d in tt·rms of strings and sequPnces of strings. The primitive functions on them arp concatenation (c for string~ cc for sequences) and selectors (car, cdr for strings and scar, scdr for sequences). c and cc are infix operators.

2. 2.1 Formulas and t<·rms

Formulas and tt·nns are n·pres<·nt<·d hy thl' string o[ symhols .1ppParing in thPm. Terms are de­ fined recursivL'ly as strings which ei tlwr represert an individual variable or can be decomposed into n+l substrings repn·s<·nting a function symbol of arity n, followed by n terms. Tlw two predicates defining tc·rms an·:

TERMSEQ((.l, LAMillJA)

Vs. (n:RM(s) INIJVAI\(s)V jn fn. (fn=car(s)/\ n=arity(rn) 1\ TEI<MSEQ(n,cdr(s))))

Vn s. (TEI<MSEQ(n,s) ((c;tr(s)=LPARSYM)/\((len(s)g£ s)= RI'ARSYW\ :}nl. (TERM(substring(s,2,nl))/\ TEI<MSEQ(n-J,suhstring(s,nl+l,len(s)-l)))D

wh<·rc· till' function suhstring(s,l't,n) returns till· substring of s starting from its r.t-tlt <·l t·rll·nt and ending with till· n-th. l<·n(s) comput<·s till· lt·n)·,lh of sand (n p,9 s))s<·lc·cts the n- tlt <·i<·nll·nt o[ s.

Wei I formt·d formulas (wffs) are rt·presl'nt<·d as strings which t·ithl'r an· ,.],·m<·ntary· formulas (defined hy the predicat<· EI.F) or can .hl' p<trtition ed into substrings for formulas and logical con-­ nectiv,·s. Formulas are d<·fitH'd by:

• Ys.(ELF(s) (s=FALSESYM V PREili'AR(.l(s) V jn I'.(P= =car(s) 1\ n=arity(P)/\ TERMSEQ(n,cdr(s))))),

Ys.(FORM(s) - (ELF(s)V jx f.(s=(x gen f) V s= =(x ex f))V }fl f2.(s=(fl dis f2)V s=

=(fl con f2) V s=(fl imp! f2)) V jf.s=neg(f)))

gen is the infix operator that maps its arguments x and f into th<· string "(FORALLSYM c x) c f" re­ presenting the well formed formula Yx.f. The opeE_ ator ex is used for the existential quantifier. dis, con and impl are the infix operators for the disjunction, conjunction and implication of two formulas.Finally nc·g is the OJll'rator which maps a formula into its negation.

We could possibly represent wffs as structur­ ed object s (lists, trees, etc.) which contain all the informal ion about the. structure of the formula and do not require any parsing. This approach a­ mounts to axiomatizing metamathematics in terms of the abstract syntax of first order logic, in­ stead of strings of symbols. Both of thPse possi­ bilities should he explored. We have chosen thl' first alternative because:

1. It is the most traditional, i.e. uwtamatlt ematics, as it appPars in logic hooks, is usual!~ stated in terms of strings.
2. Axioms in terms of abstract syntax arc simply theorems of the theory expressed in terms of strings. Thus the two representations look sub stantially the same with respect to "high level"­ theorems.
3. Ill-forml'd formulas can be mentionc·d. This is of course impossible in an axiomatization in terms of till' abstract syntax.

The properties of wffs relevant to our theory have been defined by the predicates FR, FRN, GEB and SBT, FR(x,f) is true iff the variable x has at least one free occurrence in the wff f, while FRN(x,n,f) and GEB(x,n,f) are respectively true when the variable x occurs free or hound at the place n in the formula f. ln addition to tlwsl' predicates, som<' general izl·d st>ll·<·tor functions are defined, which evaluate the first or thl' k-th free occurn·nc<' of a variabll' in a wff, or tlw number of its free occurrences. The predicate SBT is then defined. It axiomatizes the notion of sub stitution of a tenn for any free occurrence of a­ variable in a wff.

Yx t fl f2.(SBT(x,t,fl,f2}= Ynl n2.((n2= =(numbfrecocc(x,nl,fl)*(len(t)-l))+nl) ~ ((,INDVAR(nl g~ fl) ~ (nl g~ fl)= =(n2 gl f2))/\(INDVAR(nl gl fl) - ' ((FRN(x,nl,fl)~SUBT(t,f2,n2))/\ (.,fRN(x,nl,fl) ~ lNVART(nl,fl,n2,f2)))) )))

• \It f:J n2. (SUIIT(t ,f2,n2) \lx2 k. ( (k gl l) ~ x2 -' ~HN(x2,n2-(len(t)-k),f2)))),
• \In fl nl f2. (lNV/\RT(n,fl,nl,f2) ((GEB(nl g9 f2, nl,f2) GEJI(n g9, fl,n,fl))/\(FRN(nl g9. f2,nl,f2) :: FRN(n g~ fl,n,fl))/\(nl g£ f2)=(o g9 fl)))

In the previous definition, nl is ;my posi­ tion in tht· s lrin~_; fl and n2 is the cnrresponding position in fi'. Till· auxi I iary predic:ltt· ~;111:'1' states that the variald,·s appearing in till· tern! substitutt.'d for ;1 frl't' lH:currl·Uc..:t· uf (!It' ·Jat·i:thl L· x an' still ln·e . INV/\RT dt·f ines whil'i· ;n·ol><'rlit·s of fl are st iII Lru<> for f2. lf til<> L<·nn t is a variable, then SBT reduces to SBV:

\lxl x2 fl f2. (SBV(>.l,xl,fl,f2):\ln. ((;INOVAR( n gl fl)~(n gl fl)=(n gl f2)A(INOVAR(n g l fl)~ ((~'RN(xt,n, [J))-'I'RN(x2,n,f2))/\(,I'RN(xl,n,fl)-' INV/\RV(n,fl,12))))}),

\In fl f2 . (1NV/\RV(n,fl,f:n ~ ((�EJI(n g V [2,n,f2} -GEB ~n gl fl,n,fi))/\(I'RN(n gV f2,n,f2} FHN(n gl fl, n,fl))A(n gl f2)=(n g l fl))).

The proof of the equivalence of SBT and SBV when t is a variable is very simple. It is based on the fact that n2 coincides with nl when the term t has length I (sec Aiello and Weyhrauch 1974). The function sbt (sbv) evaluates to the string rL'pn·senting Lh<· n·sult of substituting a tt·rm (var iahl e) for <'Vt·ry fret· occurren"c of a variablL' in a givt·n wfr. sbt and sbv are dcfitwd fromtllC' pn·dicatt·s SilT and SBV as follows:

\lx t fl f2.(SIIT(x,t,fl,f2) sbt(x,t,fl)=f2)

\lxl x2 fl f2. (SBV(xl,x2,fl,f2) ·-sbv(xl,x2,fl)=f2)

The problem of finding the best way of defi­ ning functions in FOL is crucial: in the axiom system given in this paper a uniform way has not been followed. In defining the substitution we are interest e d in properties of the functi ons sbt and sbv and in drawing conclusions from the fact that a substitution has ht·en made. It is thus useful to have a predicate which defines the relation between formulas before and after a substitution instead of inferring it from the definition of the functions (stated for example as a system of equa t ions, as in Kleene 1952). One of the motivations of thl' prcsc>nt cxperim·cnt was to explore> differ­ ent ways of dl'fining functions. Wt· do not yet have '"lOugh examples of proofs to make a clear state­ ment about this mattt·r.

2.2.2 Hult·s ol inft·rt·nct·, dt·ductiuns and the notion of provability

The rules of inference with one premise, are expressl'd by means of a binary predicate> whose arguments arc two sequences of wffs (sq, pf} which satisfy PHOOI'TREL

The prc>dicatt· is true iff pf is tht· scdr of sq and the> first cl~nc>nt of sq i s a wff nbtainL'd by apply in!\ that particular dC'duct ion rult· to the first wff of pf. Tht· rules with mort· anlt'Cl'dt·nts an· de· f i lll'd t n a s i m i I a r way.

l>l'rivat ions art· rl·cur s lvt·ly dl'f inl·d as Sl~­ qut·ncc>s of wffs which t·ither an· a sing l e> wff or arc obtained from unt· or morl' derivations by ap­ plying on<· of tht· deduction rules. Thl' rc>cursion is impli cit ly statL'd by saying that thc>rc exist ohjt·cts uf sort I'IWOFTREE which satisfy one of tre pn·Ji catt·s dl'f in ing Lh·· rulc>s of inft·n·ncC'. These>

!:it·qucnct·s repn.·st·nt lht· I inl·ar i za l io11 ,,1 .: 1 dl'duc­ t ion-trcl' and are dl'f itwd :~s follows:

\/sq. (PROOFTREE(sq) (FOHM(sq}V ;}pf. (01\ I (sq ,pf}V ANDE( sq, pf )VFALSEE( sq, pf) VCJOT I ( sq, p( }V NOTE(sq,pf)VIMPLI(sq,pf} )V jpf x t. (GENI(sq ,pf, x,t}VGENE(sq,pf,x,t)VEXI( sq ,pf,x,t))V jpfl pf2.(ANDI(sq,pfl,pf2)V F/\LSf.T(sq,pfl,pf2}V IMPLE(sq,pfl,pf2))V jpfl pf 2 x i x2.EXI-:(sq,pfl, pf2,xl,x2}V jpfl pf2 pf l.OI{I-:(sq ,pll,pU,pf l) ))

i\ st'<Jlll'nC<' of wffs i s" I'~'"'" tr· ··· il t·itlH·r it consists of a singlt · wll nr tlllt' til tlh· ltllltlw­ ing alt,·rnal ivt·s holt.ls: tht·l·,. ··xi s l s '""'tht'l' Jll'tlt ~ tree and a one premise dt·duct ion rul ,. ha s hcl'n applied; there exist two prooftrecs and one of the two premises rules has been applied; finally, there are three prooftrees and the predicate de­ fining the V-elimination rule is true. Note that the root of a prooftree is not nc>cessarily a theorem in a given theory. i\ predicat e OEP~:NO has been defined which is true' if a given wff is a dependence for the root of a prooftrce. Thl' axioms about DEPEND allow to decide all the dependencie s of a prooftree.

Since some of the deduction rul e s (the impli­ cation introduction, for instance) e liminate depen dencies, not all the leaves of a prooftree pf are­ dependencies for a wff f such that f=scar(pf). The predicatt· DEPEND is trut· only for thosl' J ... ,vt·s of the prooftn·e which tht· formul<l f actually dept·nds on. The· axioms DEPEND stall' which dt·pcndencies do not change by applying thl' dl't.luction rules and arc transferred from one prnoftrel' to the other. Thl' axioms NOEPENO state which rulc>s dicharge depC'ndt·n cies in a given prooftree . -

Using this notion of dependence, the prova­ bility of a formula in a theory is defined as follows:

Yf. (BEW(f): jsq. (PROOFTREE (sq)/\ f=s car(sq)/\ \If 1. (DEPEND ( sq, f 1 ):..>AX !OM ( f l))))

i\ wff.f is a theorem in a given theory if there exists a prooftree whose first element is f and whose only dependencies are axioms in that theory. We have limited our attention to theories in which axioms have no free variables. This pro­ perty is defined by the axiom: Y x f.(AXIOM(f):..> FR(x,f)).

2.3 The Main Proof in tht· ··any Sort<·d Logic

The main theo·rem we hav·· pnwt·d in this axio­ matization of the mC'tamathl'matics statc>s that if \lx f. wff is provable in some tht·ory, then Y y x. wff is also provable. He have chosen this theorem because, even if very simple, it involves basic notions of provability, substitution and universal quantification. Its proof is found in appendix 2. The theorem depends on thL' first three lines of the proof. Tlw first stt·p is a lemma stating that \lx wff.sbt(x,x,wff)=wff, i ··.. suhstitutin1~ a varia hie x for any frl'<' occuurrl'nC<' of x in wff d<wsn '[ changl' that wff. Stt·ps 2 and ·1 !;iVl' simplt· f<1cts about sC'quenct·s. The th<·on·m is tht·n provl'd by instantiating two other lenuuas: a) if \lx.w[[ is a theorem, then wff is also a thcon·m; b) if wff is provable, then x cannot be frl'c in the depc>ndt·ncit·s of tlw proof of wff and so Yx.wff is provab le'. This is of course true' only fur tl'uriL's with no frc>c> variables in their axioms.

The only property of the inference rules used in this proof involves universal quantification. The restriction on the applicability of the V-in­ troduction rule is that the variable to be univer­ sal quantified in a wff must not appear free in any of its dependencies. This restriction is re­ flected in our axiomatization by the predicate APGENI. In this proof APGENI is satisfied because if wff is provable, its dependencies are axioms with no free variables.

The following is an informal proof of the above theorems. If Yx.wff is provable, then there is a prooftree pf whose first string is Yx.wff. The sequence "(Yx.wff) cc pf" is still a prooftree. It is obtained by applying the Y-elimination rule. The application of this rule doesn't add any depen dency to the prooftree. As its only dependencies - are axioms, it follows from the definition of BEW that wff is a theorem. On the other hand, if wff is a theorem there exists a prooftree pf whose first element is wff. By applying the Y-introduc­ tion rule to pf we obtain the prooftre "(Yx.wff) cc pf". This rule is applicable since theorems have no free variables in their dependencies. It follows that Yx.wff is a theorem. If Yx y.wff is provable then Yx.wff and wff are provable using the first lemma. Finally, we can quantify first over x and then over y, obtaining Yy x.wff as a theorem.

2.4 Another Axiomatization.

A different axiomatization has been given in an earlier version of FOL where there was no faci­ lity for creating sorts. We present it here as we want to do some comparisons between proofs, and discuss some of the features of FOL. Some differen ces between the two axiomatizations are due to th; new features available in FOL. They will be dis­ cussed in the next st·ction. Ht're we only discuss the difference betwt·cn the definition of formulas and terms. The list of all the axioms can be found in Aiello Weyhrauch 1974.

In this axiomatizati on, formulas and terms are still represented as the s tring of the symbols ap­ pearing in them. They are defined as strings that can be decomposed into a sequence of substrings recording the construction of that formula or term from elementary formulas and individual variables, according to the usual formation rules (see appendix 3 for the list of axioms). These sequences are def incd by the predicat<· TERMSEQ for terms and FRR for wffs. A sequence satisfies the predicate TERMSEQ if it represents the history of the construction of its first element (the term to be defined), starting from symbols, functions and individual variables. Similarly, a string is a wff if there exists a sequence which satisfies the pre dicate FRR and represents the history of the con-­ struction of that wff from elementary formulas and the logical connectives.

Section 3 The Proofs

In this section WP look at the proofs appear­ ing in the appendices, in order to explore the features of FOL tlwt need improving and their use in carrying out formal proofs.

3.1 A Look At Sorts

As a) roeady noted, tlw primary difference between the two axiomatizations wt· prcsl'ntl·d is the introduction of a many sorted logic. In the earlier version of FOL there was no facility for creating sorts, but it soon became evident that relativization of wffs t o predicates was desirable The notion of partially ordered sorts was a natu­ ral outgrowth. The axioms in the sorted logic ar e simpler and more r eadable and, most important, proofs arc considcrahly shorter. First of all, in the axiomatization done in the earlier version of FOL the partial order of sorts wasn't explicit and was to be derived as a theorem. In the proofs shown in the appendices these theorems appear as dependencies. At the moment FOL has no facility for using already proved statements as lemmas in making new proofs. In FOL there is also the possi­ bility of declaring for each function symbol the sorts of its arguments and of its value. These sorts were defined in the original version by ad­ ditional axioms. For example, together with the definition of the functions sbt and sbv, the sec­ ond axiomatization has two extra axioms.

Yx t fl.((INDVAR(x}ATERM(t}AFORM(fl))~FORM(sbt(x, t,fl)}};

Yxl x2 fl.((INDVAR(xl)AINDVAR(x2)AFORM(fl))~ FORM(sbv(xl,x2,fl))}

Proof s arc shorter i n a many sorted logic. For examples see Aiello and Weyhrauch 1974.

3.2 The Unify And Tautology Commands.

FOL proofs are greatly simplified by the ex­ istence of the commands TAUT and TAUTEQ. They de­ cide if a given formula is a tautological conse - quence of a specified set of wffs. The difference between TAUT and TAUTEQ is that the latter uses properties of the equality and the former doesn't. These commands make proofs shorter since they allow to decide every propositional sentence in one step. As a consequence , the rules of inference most frequently used manipulate quantifiers. The form of almost all the proofs we presented is the same. First of all, the right instantiations of the relevant axioms and theorems are done. Then the propositional consequences are asserted by u­ sing TAUT and TAUTEQ. The tautology commands can­ not of course manipulate the quantifiers appear­ ing in statements. Hence, the statements produced by them have quantifiers as main symbols or it is necessary to introduce a quantifier to proceed in the proof. After the right introductions or elimi nations have be,·n done to them, the tautology co; mands are used again. This process is iterated - until the completion of the proof.

The command UNIFY decides if a given wff can be obtained by instantiation of quantified varia­ bles or introduction of them for free occurrences of variables or terms in a second wff. The code for this command has been written by Ashok Chandra and is still in an experimental stage. In the proofs presented here, this command has been used for the simultaneous introduction of the existen­ tial quantifier. As an example, consider the fol­ lowing as sumption:

1 Yx.(P(x}:..J(Q(fl c f2)A Yt.R(t}}) (I) ASSUME the command

unify jx.(P(x):..J jf.(Q(f}AR(g(t)))),l; deduces in a single step

2 jx.(P(x)~ jf.(Q(f)AR(g(t)))) (6) UNIFY l

A good example of a combined use of these fea tures is found in appendix 1.2:

• 19 FRR(xl gcn f) cc SQ) ~ (SEQUENCE((xl gcn f) cc SQ)A(((xl gen f) cc U)!SLAMBDAA(ELF(scar((xl gen f) cc SQ)V(FRR(scdr((xl gen f) cc SQ))A jsl s2. (STRING(sl)A(STRING(s2)A((scar((sl gen f) cc SQ)=NEG(sl)Afind(l,sl,scdr((xl gen f) cc SQ)))V ((scar((xl gen f) cc SQ)·(sl dis s2)Afind(2,sl c s2,scdr((xl gen f) cc SQ)))V((scar((xl gen f) cc SQ)=(sl con s2)Afind(2,sl c s2,scdr((xl gen f) cc SQ)))V((scar((xl gen f) cc SQ)=(sl impl s2)Afind(2,sl c s2,scdr((xl gen f) cc SQ)))V ((scar((xl gen f) cc SQ)m(sl gen s2)A(INDVAR(sl) Afind(l,s2,scdr((xl gen f) cc SQ))))V(scar((xl gen f) cc SQ)z(sl ex s2)A(INDVAR(sl)Afind(l,s2, scdr((xl gen f) cc SQ)))))))))))))))
• 2¢ STRING(xl)A(STRING(f)A((scar((xl gen f) cc SQ)= NEG(xl)Afind(l,xl,scdr((xl gen f) cc SQ)))V ((scar((xl gen f) cc SQ)·(xl dis f)Afind(2,xl c f,scdr((xl gen f) cc SQ)))V((scar((xl gen f) cc SQ)·(xl con f)Afind(2,xl c f, scdr((xl gen f) cc SQ)))V((scar((xl gen f) cc SQ)=(xl impl f)Afind(2,xl c f,scdr((xl gen f) cc SQ)))V((scar ((xl gen f) cc SQ)=(xl gen f)A(INDVAR(xl)Afind (l,f,scdr((xl gen f) cc SQ))))V(scar((xl gen f) cc SQ)·(xl ex f)A(INDVAR(xl)Afind(l,f,scdr((xl gen f) cc SQ)))))))))) (1 2 3 4 5 6 7 8 11)
• 21 jsl s2.(STRING(sl)A(STRING(s2)A((scar((sl gen f) cc SQ)zNEG(sl)Afind(l,sl,scdr((xl gen f) cc SQ)))V((scar((xl gen f) cc SQ)=(sl dis s2)Afind (2,sl c s2,scdr((xl gen f) cc SQ)))V((scar((xl gen f) cc SQ)=(sl con s2)Afind(2,sl c s2,scdr(( xl gen f) cc SQ)))V((scar((xl gen f) cc SQ)·(sl impl s2)Afind(2,sl c s2,scdr((xl gen f) cc SQ))) V((scar((xl gen f) cc SQ)·(sl gen s2)A(INDVAR (sl)Afind(l,s2,scdr((xl gen f) cc SQ))))V(scar ((xl gen f) cc SQ)·(sl ex s2)A(INDVAR(sl)Afind (l,s2,scdr((xl gen f) cc SQ))))))))))))))) (1 2 3 4 5 6 7 8 11)

Line 19 is the instantiation of an axiom. Line 2¢ is generated by the command,

TAUTEQ 19:*2*2*2#2*2*l*l(sl+f : s2+xl) 1:19;

note how the use of the FOL subpart designators allows us to mention the desired subpart of 19, without having to retype it. In addition we can do the appropriate substitutions. Line 21 is just a use of UNIFY:

2¢;

Because we can mention the conclusion, without writing it down explicitly, the amount of typing necessary is severely reduced. Without UNIFY, line 21 would have required two }-introductions and the commands would have been:

ji 2¢ f+s2 occ 1,5,9,13,17,18,21,22;

We don't enter into details of the command UNIFY. It is our intention to do it elsewhere. It should be thought of as the routine which handles quantifiers in "simple" inferences. As seen above, the saving to a user can be large.

Section 4 Conclusion

The desire to represent mathematics in a computer tn a feasible way certainly requires the· facility to discuss metamathematical notions. The axiomatization presented here only treats the syn tactic part of the problem. Any mention of the models involved needs tlw add ilion of set theory to the axiomatization. Jlowevcr, it is clear from the simple theorems we proved that any practical system needs more extensive features even to do a satisfactory job of writing down the theorems we might want.

An important point for future work is how (in a practical way) to use these theorems. Consider for instance:

Yxl x2 f.(BEW(xl gen f)PBEW(x2 gen(xl gen f)))

What we mean by reflection principle is a rule of FOL which says:

BEl>:( f)

in meta FOL

f

in FOL

That is, if in the axiomatization of the me­ tamathematics of FOL, we can prove the existence of an FOL proof off, then we can assert f in FOL. 3uppose we have a proof in FOL of Yx y.wff. Then instantiating the above theorem gives us

BEW(x gen (y gen wff) :..- BEIHy gen (x gen wff))

Since we started with a proof of Yx y.wff in FOL and BEW represents the proof predicate for FOL, we can conclude BEW(x gen (y gen wff)). Using modus ponens we get BEW(y gen (x gen wff)), and using the above rule we can conclude Yy x.wff in FOL.

The exact form of such a rule requires more examples of proofs and is one of the main reasons for doing the example in the paper. It is not just a proof checking exercise, but a case study for fundamental questions of representing mathematical information in a computer. Using metamathematics also prepares the way for more comprehensive sys­ tems which can formally discuss how they reason. That is exactly what the metamathematics is good for.

Acknowledgement

Our gratitude to Ashok Chandra who contribut ed to the early stages of this research. In partT cular the axioms for strings, sequences and well­ formed formulas in the unsorted logic are due to him.

Appendix 1

The proof of "if f is a WFF. also Yx.f is a WFF.

1.1 FOL commands and printout in the many sorted logic

Commands

YE WFFl, x gen f; TAUTEQ(x gen f·x gen f)V(x gen f·x ex f); Unify --: #2*2#1,-; TAUT ---:#1, 1:-;

Proof

• l FORM(x gen f) =(ELF(x gen f)V(}xl fl.((x gen f)· (xl gen fl)V(x gen f)=(xl ex fl))V(}fl f2.((x gen f)·(fl dis f2)V(x gen f)·(fl con f2)V(x gen f)·(fl impl f2)))V}fl.(x gen f)·neg(fl))))

• 2 (x gen f)·(x gen f}V{x gen f}={x ex f)
• 3 jx1 f1.((x gen f)=(x1 gen f)V(x gen f)=(x1 ex f1))
• 4 FORM(x gen f)
• Printout of the oroof in the second axiomati­ zation
• 1 FORH(f)AINDVAR(x1)
• 2 Ysq s.((SEQUENCE(sq)Asq;SLAMBDA)~(STRIN�(s)~(s cc sq);SLAMBDA)) (2)
• 3 Ys sq. ((STIUNG(s)ASEQUENCE(sq}}_ scar(s cc sq)= s) (3)
• 4 Ys sq. ((STRlNG(s)ASEQUENcE:sq}} , scdr(s cc sq)· sq) (4)
• 5 Ysq.((SEQUENCE{sq}Asq;SLAMDA)=find(1,scar(sq), sq)) (5)
• 6 Yf x.((FORM(f)AINDVAR(x))-·STRING(x gen f)) (6)
• 7 Ys sq.((STRIN�(s)ASEQUENCE(sq})~SEQUENCE(s cc sq)) (7)
• 8 Yx.(1NDVAR(x)~STRIN�(x) (8)
• 9 FORM(f)= (STRING(f)Ajsq.(FRR(sq)Af·scar(sq)))
• 10 jsq.(FRR(sq)Af=scar(sq)) (1 2 3 4 56 7 8)
• 11 FRR(SQ)Af·scar(SQ) (11)
• 12 FRR(SQ~SEQUENCE(SQ)A(SQ;SLAMBDAA(ELF(scar(SQ)) V(FRR(scdr(SQ))Ajs1 s2.(STRING(s1)A(STRING(s2)A ((scar(SQ)·NEG(s1)Afind(1,s1,scdr(SQ)))V((scar (SQ)·(s1 dis s2)Afind(2,s1 c x2,scdr(SQ)))V(( scar(SQ)=(sl con s2}Afind(2,sl c s2,scdr(SQ)))V ((scar(SQ)·(s1 impl s2)Afind(2,s1 c s2,scdr(SQ) ))V((scar(SQ}·(s1 gen s2)A(INDVAR(s1)Afind(1,s2, scdr(SQ))))V(scar(SQ)=(sl ex s2)A(INDVAR(s1)A find(1,s2,scdr(SQ)))))))))))))))
• 13 (SEQUENCE(SQ)ASQ;SLAMBDA)->{STRING(x1 gen f)~ ((xl gen f) cc SQ);SLAMBDA) (2)
• 14 (STRING(xl gen f)ASEQUENCE(SQ)) =scar((xl gen f) cc SQ)(xl gen f) (3)
• 15 (STRING(x1 gen f)ASEQUENCE(SQ)}=scdr((x1 gen f) cc SQ)·SQ (4)
• 16 (SEQUENCE(SQ)ASQ;SLAMBDA)=find(1,scar(SQ),SQ) (5)
• 17 (FORM(f)AINDVAR(x1)}~string(x1 gen f) (6)
• 18 INDVAR(xl)~STRIN�(x1) (8)
• 19 FRR(xl gen f) cc SQ~SEQUENCE({xl gen f) cc SQ) A(((xl gen f) cc U);SLAMBDAA(ELF(scar((x1 gen f) cc SQ))V(FRR(scdr((x1 gen f) cc SQ))Ajsl s2.( STRING(sl)A(STRING(s2)A((scar((s1 gen f) cc SQ)~ NEG(s1)Afind(1,s1,scdr((x1 gen f) cc SQ)))V(( scar((xl gen f) cc SQ)=(sl dis s2~~find(2,s1 c s2,scdr((x1 gen f) cc SQ)))V((scar((x1 gen f) cc SQ)·(s1 con s2)Afind(2,sl c s2,scdr((x1 gen f) cc SQ))}V((scar((xl gen f) cc SQ)=(s1 con s2)A find(2,s1 c s2,scdr((xl gen f) cc SQ}})V((scar ((xl gen f) cc SQ)=(sl imp1 s2)Afind(2,s1 c g2, scdr((x1 gen f) cc SQ)))V((scar((x1 gen f) cc SQ)·(s1 gen s2)A(INDVAR(sl)Afind(1,s2,scdr((x1 gen f) cc SQ))))V(scar((xl gen f) cc SQ)=(s1 ex s2)A(INDVAR(s1)Afind(l,s2,scdr((xl gen f) cc SQ)))))))}))}))))
• 20 STRING(x1)A(STRING(f)A((scar((x1 gen f) cc SQ) =NEG(xl)Afind(1,xl,scdr((x1 gen f) cc SQ)}}V
• ((scar((x1 gen f) cc SQ)=(xl dis f)Afind(2,x1 c f,scdr((xl gen f) cc SQ)))V((scar((x1 gen f) cc SQ)=(xl con f)Afind(2,xl c f,scdr((x1 gen f) cc SQ)))V((scar((xl gen f) cc SQ)=(x1 imp1 f)A find(2,x1 c f,scdr((xl gen f) cc SQ)))Y((scar ((xl gen f) cc SQ)·(x1 gen f)A(INDVAR(xl)Afind (1,f,scdr((x1 gen f) cc SQ))))V(scar((x1 gen f) cc SQ)=(x1 ex f)A(INDVAR(x1)Afind(1,f,scdr((x1 gen f) cc SQ)))))))))) (1 2 3 4 5 6 7 8 11)
• 21 }sl s2.(STRING(s1)A(STRING{s2)A((scar((s1 gen f) cc SQ)·NEG(s1)Afind(l,sl,scdr((x1 gen f) cc SQ)))V((scar((x1 gen f) cc SQ)=(s1 dis s2)A find(2,sl c s2,scdr((x1 gen f) cc SQ)))Y((scar ((x1 gen f) cc SQ)·(s1 con s2)Afind(2,s1 c s2, scdr((xl gen f) cc SQ)))V{(scar((x1 gen f) cc SQ)·(sl impl s2)Afind(2,sl c s2,scdr((xl gen f) cc SQ)))Y((scar((x1 gen f)cc SQ)=(sl gen s2)A (INDVAR(s1)Afind(1,s2,scdr((xl gen f) cc SQ)))) V{scar((xl gen f) cc SQ)=(sl ex s2)A(INDVAR(sl) Afind(l,s2,scdr((x1 gen f) cc SQ))))))))))))))) (1 2 3 4 5 6 7 8 11)
• 22 (STRING(x1 gen)ASEQUENCE(SQ})->SEQUENCE((x1 gen f) cc SQ) (7)
• 23 FORM(x1 gen f) · ( STRING(x1 gen f)Ajsq. (FRR( sq) A(xl gen f)=scar(sq)))
• 24 FRR(x1 gen f) cc SQ)A(~1 gen f)·scar((x1 gen f) cc SQ) (1 2 3 4 5 6 7 B 11) TAUTEQ I: 23
• 25 }sq.(FRR(sq}A(xl gen f)=scar(sq)) (1 2 3 4 5 6 7 8 11)
• 26 FORM(x1 gen f) (1 2 3 4 5 6 7 8 11)
• 27 FORM(x1 gen f) (1 2 3 4 5 6 7 8)
• 28 (FORH(f)AINDVAR(x1))~FORM(x1 gen f) (2 3 4 5 6 7 8)
• 29 Yf x1.((FORM{f)AINDVAR(xl)PFORN(x1 gen f)) (2 3 4 5 6 7 8)

Appendix 2

The proof that universal quantifiers can be interchanged Printout of the proof in the many sorted logic

• 1 Yx f.sbt(x,x,f)·f (1)
• 2 Yf sq.scar(f cc sq)·f (2)
• 3 Yf sq.scdr(f cc sq)·sq (3)
• 4 BEW(x gen f) (4)
• 5 sbt(x,x,f)~f (1)
• 6 BEW(x gen f)=}sq.(PROOFTREE(sq)A((x gen f)·scar (sq}AYfl.(DEPEND(sq,fl)~AXIOM(fl))))
• 7 }sq.(PROFTREE(sq)A((x gen f)·scar(sq)AYfl.( DEPEND(sq,fl)~AXIOM(fl)))) (4)
• 8 PROOFTREE(sq)A((x gen f)·scar(sq)/,Yfl.(DEPEND (sq,f1)~AXIOM(f1))) (8)
• 9 GENE(f cc sq,sq,x,x) =(scdr(f cc sq}=sqn( PROOFTREE(sq)A}f,(scar(sq)=(x gen fl)Ascar(f cc sq)=sbt(x,x,f1))))
• 10 scar(f cc sq)·f (2)
• 11 scdr(f cc sq)=sq (3)
• 12 scar{sq}=(x gen f)Ascar(f cc sq)=sbt(x,x,f) (1 2 3 4 8)
• 13 }fl.{scar{sq)·(x gen f1)Ascar(f cc sq)=sbt(x,

• 14 GENE(f cc sq,sq,x,x) (1 2 3 4 8)
• 15 PROOFTREE(f cc sq)" (FORM(f cc sq)V(fpf. (ORI(f cc sq,pf)V(ANDE(f cc sq,pf)V(FALSEE(f cc sq,pf) V(NOTI(f cc sq,pf)V(NOTE(f cc sq,pf)VIMPLI(f cc sq,pf))))))V(jpf x t.(GENI(f cc sq,pf,x,t) V(GENE(f cc sq,pf,x,t)VEXI(f cc sq,pf,t)))V(j pfl pf2. (ANDI(f cc sq,pfl,pf2)V(FALSEI(f cc sq, pfl,pf2)VI!1PLE(f cc sq,pfl,pf2)))Vjpfl pf2 X t.EXE(f cc sq,pf1,pf2,x,t)VJpf1 pf2 pf3.0RE(f cc sq, pf1,pf2,pf3))))))
• 16 GENI(f cc sq,sq,x,x)V(GENE(f cc sq,sq,x,x)V EXI(f cc sq,sq,x,x)) (1 2 3 4 8)
• 17 jpf x t.(GENI(f cc sq,pf,x,t)V(GENE(f cc sq,pf, x,t)VEXI(f cc sq,pf,t))) (1 2 3 4 8)
• 18 PROOFTREE(f cc sq) (1 2 3 4 8)
• 19 Y f1.(DEPEND{sq,f1)~AXIOM(f1)) (8)
• 20 DEPEND{sq,f1)~AXIOM(f1) (8)
• 21 PROOFTREE(f cc sq)~(PROOFTREE(sq)~((sq=scdr(f cc sq)~(DEPEND(f cc sq,f1~ DEPEND(sq,f1))~ ( ORI(f cc sq,sq)V{ANDE(f cc sq,sq)V(FALSEE(f cc sq,sq)V(jf.((NOTID(f cc sq,sq,f)V{NOTED(f cc sq,sq,f)VIMPLID(f cc sq,sq,f)))Af;f1)Vjx t.( GENI(f cc sq,sq,x,t)V(GENE(f cc sq,sq,x,t)V EXI(f cc sq,sq,x,t)))))))))
• 22 JX t.(GENI(f cc sq,sq,x,t)V(GENE(f cc sq,sq, x,t)VEXI(f cc sq,sq,x,t))) (1 2 3 4 8)
• 23 DEPEND(f cc sq,f1)~AXIOH(f1) (1 2 3 4 8)
• 24 Yf1.(DEPEND(f cc sq,f1)~AXIOM(fl)) (1 2 3 4 8)
• 25 f·scar(f cc sq) (2)
• 26 PROOFTREE(f cc sq)A(f·scar(f cc sq)AYf1.( DEPEND(f cc sq,f1)~AX!OM(f1))) (1 2 3 4 8)
• 27 BEW(f~ jsq.(PROOFTREE(sq)A(f·scar(sq)AYfl.( DEPEND{sq,f1)~AXIOM(f1))))
• 28 jsq.(PROOFTREE(sq)A(f·scar(sq)AYf1.(DEPEND(sq, f1)~AXIOM(fl)))) (1 2 3 4)
• 29 BEW(f) (1 2 3 4)
• 30 BEW(x gen f)~BEW(f) (1 2 3)
• 31 BEW(f) (31)
• 32 )sq.(PROOFTREE(sq)A(f·scar{sq)AYf1.(DEPEND(sq, flPAXIOM(fl)))) (31)
• 33 PROOFTREE(sq)A(f·scar(sq)AYf1.(DEPEND(sq,f1)~ AXIOM(fl))) (33)
• 34 Yf1.(DEPEND(sq,f1)~AXIOM(f1)) (33)
• 35 DEPEND(sq,f1PAXIOM(f1) (33)
• 36 AP�ENI(x,sq):(Yf.(DEPEND(sq,f)~FR(x,f))A PROOFTREE(sq))
• 37 AXIOM(fl)~FR(x,f1)
• 38 DEPEND(sq,fl)~FR(x,f1) (31 33)
• 39 Yf1.(DEPEND(sq,f1)~FR(x,fl)) (31 33)
• 40 APGENI(x,sq) (31 33)
• 41 GENI((x gen f) cc sq,sq,x,x) =(scdr(x gen f) cc sq)·sqA(PROOFTREE{sq)Ajf1.(scar((x gen f) cc sq)·(x gen fl)A(scar(sq)=sbt(x,x,f1)AAPGENI(x, sq)))))
• 42 scar{(~ gen f) cc sq)=(x gen f) (2)
• 43 scdr((x gen f) cc sq)·sq (3)
• 44 scar((x gen f) cc sq)=(x gen f)~(scar(sq)=sbt (x,x,f)AAPGENI(x,sq)) (1 2 3 31 33)
• 45 jfl.(scar((x gen f) cc sq)=(x gcn f1)A(scar(sq) =sbt(x,x,f1)AAPGENI(x,sq))) (1 2 3 31 33)
• 46 GENI((x gen f) cc sq,sq,x,x) (1 2 3 31 33)
• 47 PROOFTREE((x gen f) cc sq)' (FOR.'I((x gen f) cc sq)V(jpf.(ORI((x gen f) cc sq,pf)V(ANDE((x gen f) cc sq,pf)V(FALSEE((x gen f) cc sq,pf)V(NOTI ((x gen f) cc sq,pf)V{NOTE((x gen f) cc sq,pf) VIMPLI((x gen f) cc sq,pf))))))V(jpf x1 t.(GENI ((x gen f) cc sq,pf,x1,t)V(GENE((x gen f) cc sq,pf,x1,t)VEXI((x gen f) cc sq,pf,x1,t)))V (}pt1 pf2.(ANDI((x gen f) cc sq,pfl,pf2)V( FALSEI((x gen f) cc sq,pf1,pf2)VIMPLE((x gen f) cc sq,pfl,pf2)))V(}pf1 pf2 xl t.EXE((x gen f) cc sq,pfl,pf2,x1,t)Vjpf1 pf2 pf3.0RE((x gen f) cc sq,pf1,pf2,pf3))))))
• 48 GENI((x gen f)cc sq,sq,x,x)V(GENE((x gen f) cc sq,sq,x,x)VEXI((x gen f) ci sq,sq,x,x)) (1 2 3 31 33)
• 49 jpf x1 t.(GENI((x gen f) cc sq,pf,x1,t)V(GENE ((x gen f) cc sq,pf,x1,t)VEXI((x gen f) cc sq, pf,x1,t))) (1 2 3 31 33)
• 50 PROOFTREE((x gen f) cc sq) (1 2 3 31 33)
• 51 PROOFTREE(x gen f) cc sq)~(PROOFTREE(sqP((sq· scdr((x gen f) cc sq)~(DEPEND((x gen f) cc sq, f1) (DEPEND(sq,f1))) (ORI((x gen f) cc sq,sq)V (ANDE((x gen f) cc sq,sq)V(FALSEE((x gen f) cc sq,sq)V(jf.((NOTID((x gen f) cc sq,sq,f)V(NOTED ((x gen f) cc sq,sq,f)VIMPLID((x gen f) cc sq, sq,f)))Af;f1)Vjx1 t.(GENI((x gen f) cc sq,sq, x1,t)V(GENE((x gen f) cc sq,sq,x1,t)VEXI(x gen f) cc sq,sq,xl,t)))))))))
• 52 jx1 t.(GENI((x gen f) cc sq,sq,x1,t)V(GENE((x gen f) cc sq,sq,x1,t)VEXI((x gen f) cc sq,sq, xl,t))) (1 2 3 31 33)
• 53 DEPEND((x gen f) cc sq,f1)~AXIOM(fl) (1 2 3 31 33)
• 54 Yf1.(DEPEND((x gen f) cc sq,f1)~AXIOM(f1)) (1 2 3 31 33)
• 55 (x gen f)=scar((x gen f) cc sq) (2)
• 56 PROOFTREE((x gen f) cc sq)A((x gen f)·scar((x gen f) cc sq)AYf1.(DEPEND((x gen f) cc sq,f1)~ AXIOM(f1))) (1 2 3 31 33)
• 57 BEW(x gen fF jsq.(PROOFTREE(sq)A((x gen f)· scar(sq)AYfl. (DEPEND(sq ,fl):..>AXImi(fl))))
• 58 }sq.(PROOFTREE(sq)A((x gen f)=scar(s~)AYf1.( DEPEND(sq,f1)~AXIOM(f1)))) (1 2 3 31)
• 59 BEW(x gen f) (~ 2 3 31)
• 60 BEW(f)~BEW(x gen f) (1 2 3)
• 61 BEW(x gen f): BEW(f) (1 2 3)
• 62 Yx f.(BEW(x gen f):BE\~(f)) (1 2 3)
• 63 BEW(x1 gen(x2 gen f)~BEW(x2 gen f) (1 2 3)
• 64 BEW(x2 gen f) := BEW(f) (1 2 3)
• 65 BEW (x1 gen f)c BEW(f) (1 2 3)
• 66 BEW(x2 gen (xl gen f)): BEW(x1 gen f) (1 2 3)
• .67 BEW(x1 gen (x2 gcn f) )....)BEW(x2 gen (x1 gen f)) (l 2 3)
• 68 Vx1 x2 f. (BEW(x1 gen (x2 gen f) )~BE\o/(x2 gen (x1 gen f))) (l 2 3)

Prawitz 0 D.,

• 1965 Natural deduction, A proof theoretical study Almquist and Wiksell, Stockholm (1965).
• Godel, 193~ K., Die Vollstandingkeit der Axiome des logischen Funktionenkalkuls Monatshefte fur Mathematik und Physik 37, (193~) 34936~.

Godel, K.,

• 1931 Uber formal unentscheidbare Satze der Principia mathematica und verwandter Systeme I, Honatshefte fur Mathematik und Physik 38,(1931) 173-198.
• Weyhrauch, R.W., and Thomas, A.J., 1974 FOL: A Proof Checker for First-order Logic, Stanford Artificial Intelligence Laboratory, Memo AIM-235 (1974).

Aiello, M., and Weyhrauch, R.W.,

• 1974 Checking Proofs in the metamathematics of first order logic, Stanford Artificial Intelligence Laboratory, Memo AIM-222 (1974).

Appendix 3

The axioms for formulas in the unsorted logic

AXIOM FIND:

Ysq.(FIND(~,LAMBDA,sq) = SEQUENCE(sq)), Yn s sq. (FIND(n,s,sq) oiNTEGER(n)/\STRING(s)/\ SEQUENCE(sq)/\Jn sl s2.(INTEGER(n)/\STRING(sl)/\ STRIN�(s2)/\(~<SI\s<slen(sq) )/\(sl=(n sgl sq) )/\ (s·(sl c s2))/\FIND(n-l,s2,sq)));;

AXIOI1 FINDTOP:

Ysq.(FINDTOP(~,SLAMBDA,sq) o SEQUENCE(sq)),Yn s sq.(FINDTOP(n,s,sq) =INTEGER(n)/\STRING(s)/\ SEQUENCE(sq)/\Jsl s2.(STRING(sl)/\STRING(s2)n (sl;LAMBDA)/\(sz(sl c s2))/\(s·scar(sq))/\ FINDTOP(n-l,s2,scar(sq))));;

AXIOM TERM:

Ysq.(TERMSEQ(sq) : SEQUENCE(sq)/\((slen(sq)~ll\ INDVAR(l sgl sq))V(slen(sq)>l/\TERMSEQ(scdr (sq))/\(INDVAR(scar(sq))Vjn s.INTEGER(n)/\ STRING(s)/\(s·car(scar(sq))/\OPCONST(s)/\n·arity (s)/\FIND(n,cdr(scar(sq)),scdr(sq))))))), Yt.(TERM(t) : STRING(t)/\Jsq.(TERMSEQ(sq)/\t=car( sq)));;

AXIOM WFF:

• Yf.(ELF(f)=STRING(f)/\(f=FALSESYMVPREDPARO(f)V Jn sq.(INTEGER(n)/\SEQUENCE(sq)/\PREDPAR(car (f))/\n·arity(car(f))/\TERMSEQ(sq)/\FINDTOP(n, cdr(f), sq)))),

Ysq.(FRR(sq):SEQUENCE(sq)/\(sq;SLAMBDA)/\(ELF( scar(sq))V(FRR(scdr\sq))/\jsl s2.(STRING(sl)/\ STRING(s2)/\(((scar(sq)=neg(sl)/\FIND(l,xl, scdr(sq)))V(scar(sq)=(sl dis s2)/\FIND(2tsl c s2),scdr(sq)))V(scar(sq)=(sl con s2)/\FIND(2, (sl c s2),scdr(sq)))V(s~ar(sq)=(sl impl s2)/\ FIND(2,(sl c s2),scdr(sq)))V(scar(sq)·(sl gen s2)/\INDVAR(sl)/\FIND(l,s2,scdr(sq)))V(scar(sq) ·(sl ex s2)/\INDVAR(sl)/\FIND(l,s2,scdr(sq)))) )))));

• Yf.(FORM(f) : STRING(f)/\jsq.(FRR(sq)/\f=scar(sq)))