FOL

Fork me on GitHub

What's here:

Prolegomena

What's here:

These examples are inspired from Weyhrauch's Prolegomena to a Theory of Formal Reasoning (PDF).

Section 2: Syllogism

declare indconst Socrates; declare predconst Mortal Man 1; declare indvar x; assume (Man(Socrates) and (forall x. (Man(x) imp Mortal(x)))); taut forall x. (Man(x) imp Mortal(x)) by 1; alle 2 Socrates; taut Mortal(Socrates) by 1 3; impi 1 imp 4;

Section 6: Rewrites

declare funconst fact(NATNUM)=NATNUM; axiom FACT: forall n.fact(n)=trmif zro=n then suc(zro) else n*fact(prd(n)); axiom PRDSUC: forall n. prd(suc(n))=n; simplify (zro=zro iff TRUE); rewrite forall n.(zro=suc(n) iff FALSE) by PEANO uni LOGICTREE; setbasicsimp FACT_RULES at facts {1, 2, FACT, PRDSUC}; rewrite (fact(zro)) by FACT_RULES uni PEANO uni LOGICTREE; rewrite (fact(suc(suc(suc(zro))))) by FACT_RULES uni PEANO uni LOGICTREE; rewrite (fact(suc(suc(suc(suc(zro)))))) by FACT_RULES uni PEANO uni LOGICTREE;

Section 9: Reflection Principle

“Change theorem proving in the theory into evaluation in the metatheory.”

We can create object theorems at the meta level. We are free, though not encouraged, to create erroneous ones! Here, we have sound and unsound versions of a reflective procedure that asserts the conjunction of two arguments. In the sound version, these arguments must be given as facts, which are guaranteed to be true, while in the unsound version, these arguments are given as well-formed formulas, which can be either true or false.

NAMECONTEXT META; DECLARE sort WFF FACT; DECREP WFF FACT; REPRESENT {WFF} as WFF; REPRESENT {FACT} as FACT; DECLARE predconst THEOREM 1; DECLARE funconst mkand (WFF,WFF)=WFF; DECLARE funconst wffof (FACT)=WFF; DECLARE indvar A B [WFF]; DECLARE indvar T1 T2 [FACT]; AXIOM ANDI: forall A B.THEOREM(mkand(A,B)); AXIOM ANDI_SOUND: forall T1 T2.THEOREM(mkand(wffof(T1),wffof(T2))); ATTACH mkand TO [WFF,WFF=WFF] mkand; deflam wffof(x) (CADR x); ATTACH wffof TO [FACT=WFF] wffof; MAKECONTEXT OBJ; SWITCHCONTEXT OBJ; declare sentconst A B; reflect ANDI A B; nameproof P_AND_UNSOUND; makeproof P1; switchproof P1; assume A; impi 1 1; theorem T1 2; makeproof P2; switchproof P2; assume B; impi 1 1; theorem T2 2; makeproof P_ANDS; switchproof P_ANDS; andi T1 T2; reflect ANDI A B; reflect ANDI_SOUND T1 T2; reflect ANDI FALSE FALSE;

Section 9.1: Linear Equations

We add a theory of minus \(-\).

declare funconst -(NATNUM,NATNUM) = NATNUM [inf = 450 455]; deflam minus (N M) (LET ((R (- N M))) (COND ((> R 0) R) (T 0))); attach - to [NATNUM,NATNUM=NATNUM] minus; axiom MINUS0R: forall n. n - zro = n; axiom MINUS0L: forall n. zro - n = zro; axiom MINUS: forall n m. suc(n) - suc(m) = n - m; setbasicsimp TMINUS at facts {MINUS0R,MINUS0L,MINUS};

We have some linear equations.

declare indconst x y z [NATNUM]; axiom Ex: x + suc(suc(zro)) = suc(suc(suc(suc(suc(zro))))); axiom Ey: y - suc(suc(zro)) = zro; axiom Ez: z - suc(suc(zro)) = suc(suc(suc(zro)));

Assuming the following theorems, we can solve by hand.

axiom THM1: forall p q m.(p=q imp p-m=q-m); axiom THM2: forall p q m.(m<suc(q) imp (p+q)-m=p+(q-m)); theorem THM3 PLUS0; setbasicsimp THM1 at facts {THM1}; setbasicsimp THM3 at facts {THM3}; alle THM2 x,suc(suc(zro)),suc(suc(zro)); simplify suc(suc(zro))<suc(suc(suc(zro))); impe 2 1; theorem THM2instance 3; setbasicsimp THM2instance at facts {THM2instance}; alle THM1 x+suc(suc(zro)),suc(suc(suc(suc(suc(zro))))),suc(suc(zro)); rewrite 4 by TMINUS uni THM2instance uni THM3 uni LOGICTREE; iffe 5 1; impe 6 4; impe 7 Ex; theorem THMx 8;

Let us switch to the meta level, and do some algebra.

namecontext OBJ; MAKECONTEXT META; SWITCHCONTEXT META; DECLARE PREDCONST THEOREM 1; DECLARE SORT TERM WFF FACT PREDSYM FUNSYM; DECREP TERM WFF FACT PREDSYM FUNSYM; REPRESENT {TERM} AS TERM; REPRESENT {WFF} AS WFF; REPRESENT {FACT} AS FACT; REPRESENT {PREDSYM} AS PREDSYM; REPRESENT {FUNSYM} AS FUNSYM; DECLARE FUNCONST wffof (FACT)=WFF; ATTACH wffof TO [FACT=WFF] fact\-get\-wff; DECLARE FUNCONST lhs rhs (WFF)=TERM; DECLARE FUNCONST larg rarg (TERM)=TERM; ATTACH lhs TO [WFF=TERM] lhs; ATTACH rhs TO [WFF=TERM] rhs; DEFLAM larg (t) (CAR (appl\-get\-args t)); ATTACH larg TO [TERM=TERM] larg; DEFLAM rarg (t) (CADR (appl\-get\-args t)); ATTACH rarg TO [TERM=TERM] rarg; DECLARE FUNCONST mainpred (WFF)=PREDSYM; DECLARE FUNCONST pred2apply (PREDSYM TERM TERM)=WFF; DECLARE INDCONST Equal [PREDSYM]; MATTACH Equal dar [PREDSYM] OBJ::PREDCONST:=; DEFLAM mainpred (X) (AND (PREDAPPL X) (predappl\-get\-pred X)); ATTACH mainpred to [WFF=PREDSYM] mainpred; ATTACH pred2apply TO [PREDSYM,TERM,TERM=WFF] predappl2\-mak; DECLARE FUNCONST mainfun (TERM)=FUNSYM; DECLARE FUNCONST fun1apply (FUNSYM TERM)=TERM; DECLARE FUNCONST fun2apply (FUNSYM TERM TERM)=TERM; DECLARE INDCONST zro [TERM]; DECLARE INDCONST suc + - [FUNSYM]; MATTACH zro dar [TERM] OBJ::INDCONST:zro; MATTACH suc dar [FUNSYM] OBJ::FUNCONST:suc; MATTACH + dar [FUNSYM] OBJ::FUNCONST:+; MATTACH - dar [FUNSYM] OBJ::FUNCONST:-; DEFLAM mainfun (X) (AND (FUNAPPL X) (funappl\-get\-fun X)); ATTACH mainfun to [TERM=FUNSYM] mainfun; ATTACH fun1apply TO [FUNSYM,TERM=TERM] funappl1\-mak; ATTACH fun2apply TO [FUNSYM,TERM,TERM=TERM] funappl2\-mak; DECLARE indvar x y z [TERM]; DECLARE indvar w [WFF]; DECLARE indvar vl [FACT]; DECLARE PREDCONST NUMERAL 1; DECLARE PREDCONST numeral 3; DEFLAM numeral (X zro suc) (OR (EQ X zro) (AND (FUNAPPL X) (EQ (funappl\-get\-fun X) suc) (numeral (funappl1\-get\-arg X) zro suc))); ATTACH numeral TO [TERM,TERM,FUNSYM] numeral; AXIOM AX_NUMERAL: forall x.(NUMERAL(x) iff numeral(x,zro,suc)); KNOW natnums; declare indvar n [NATNUMSORT]; DECLARE FUNCONST mknum (TERM)=NATNUMSORT; DEFLAM mknum (X) (IF (FUNAPPL X) (ADD1 (mknum (funappl1\-get\-arg X))) 0); ATTACH mknum TO [TERM=NATNUMREP] mknum; DECLARE FUNCONST mknumerali (NATNUMSORT,TERM,FUNSYM)=TERM; DECLARE FUNCONST mknumeral (NATNUMSORT)=TERM; DEFLAM mknumerali (X zro suc) (IF (= X 0) zro (funappl1\-mak suc (mknumerali (SUB1 X) zro suc))); ATTACH mknumerali TO [NATNUMREP,TERM,FUNSYM=TERM] mknumerali; AXIOM AX_MKNUMERAL: forall n.(mknumeral(n)=mknumerali(n,zro,suc)); DECLARE PREDCONST LEQ 2; DEFLAM leq (X Y) (OR (< X Y) (= X Y)); ATTACH LEQ TO [NATNUMREP,NATNUMREP] leq; DECLARE FUNCONST plus minus (NATNUMSORT NATNUMSORT)=NATNUMSORT; ATTACH plus TO [NATNUMREP,NATNUMREP=NATNUMREP] +; ATTACH minus TO [NATNUMREP,NATNUMREP=NATNUMREP] -; DECLARE FUNCONST mkequal (TERM TERM)=WFF; AXIOM AX_MKEQUAL: forall x y.mkequal(x,y)=pred2apply(Equal,x,y); DECLARE PREDCONST LINEAREQ 2; DECLARE FUNCONST solve (WFF TERM)=TERM;

The 3 next axioms are close to the formulation in the paper.

AXIOM AX_LINEAREQ: forall w x.(LINEAREQ(w,x) iff ( mainpred(w)=Equal and (mainfun(lhs(w))=+ or mainfun(lhs(w))=-) and larg(lhs(w))=x and (NUMERAL(rarg(lhs(w))) and NUMERAL(rhs(w))) and (mainfun(lhs(w))=+ imp LEQ(mknum(larg(lhs(w))),mknum(rhs(w)))))); AXIOM AX_SOLVE: forall w x.(solve(w, x)= trmif mainfun(lhs(w))=+ then mknumeral(minus(mknum(rhs(w)),mknum(rarg(lhs(w))))) else mknumeral(plus(mknum(rhs(w)),mknum(rarg(lhs(w)))))); AXIOM SOLVE: forall vl x.(LINEAREQ(wffof(vl),x) imp THEOREM(mkequal(x,solve(wffof(vl),x)))); SETBASICSIMP meta\-axioms at facts {AX_LINEAREQ,AX_SOLVE,AX_NUMERAL,AX_MKNUMERAL,AX_MKEQUAL}; SETCOMPSIMP EVALSS AT LOGICTREE uni meta\-axioms; SWITCHCONTEXT OBJ;

Back at the object level, we can solve the linear equations with a single reflective call.

reflect SOLVE Ey y; theorem THMy 1; reflect SOLVE Ex x; theorem THx 2; reflect SOLVE Ez z; theorem THMz 3; show axiom;

Appendix A: An Axiomatization of Natural Numbers

declare sort NATNUM; declare indvar n m p q [NATNUM]; declare indconst zro [NATNUM]; declare funconst suc prd (NATNUM) = NATNUM; declare funconst +(NATNUM,NATNUM) = NATNUM [inf = 450 455]; declare funconst *(NATNUM,NATNUM) = NATNUM [inf = 550 555]; declare predconst < 2 [inf]; declare predpar P 1; axiom ONEONE: forall n m.(suc(n)=suc(m) imp n=m); axiom SUCC1: forall n.not(zro=suc(n)); axiom SUCC2: forall n.not(zro=n) imp exists m.n=suc(m); axiom PLUS0: forall n. n + zro = n; axiom PLUS: forall n m. n+suc(m)=suc(n+m); axiom TIMES0: forall n. n * zro = zro; axiom TIMES: forall n m. n*suc(m)=(n*m)+n; axiom INDUCT: P(zro) and forall n.(P(n) imp P(suc(n))) imp forall n.P(n); setbasicsimp PEANO at facts {ONEONE,SUCC1,SUCC2,PLUS0,PLUS,TIMES0,TIMES}; decrep NATNUM; represent {NATNUM} as NATNUM; attach zro to [NATNUM] 0; attach suc to [NATNUM=NATNUM] ADD1; deflam prd(x) (COND ((> x 0) (SUB1 x)) (T 0)); attach prd to [NATNUM=NATNUM] prd; attach + to [NATNUM,NATNUM=NATNUM] +; attach * to [NATNUM,NATNUM=NATNUM] *; attach < to [NATNUM,NATNUM] <;

Appendix B: An Axiomatization of S-Expressions

declare sort Sexp Lisp Null Atom; declare indvar x y z [Sexp]; declare indvar u v w [List]; declare indconst nil [Null]; declare funconst car cdr 1; declare funconst cons(Sexp,List)=List; declare funconst rev 1; declare funconst @ 2 [inf]; moregeneral Sexp < List, Atom, Null >; moregeneral List < Null >; decrep Sexp; represent {Sexp} as Sexp; represent {List} as Sexp; represent {Atom} as Sexp; represent {Null} as Sexp; axiom CAR: forall x y. car(cons(x,y))=x; axiom CDR: forall x y. cdr(cons(x,y))=y; axiom CONS: forall x y. not(Null(cons(x,y))); setbasicsimp Basic at facts {CAR,CDR,CONS}; axiom REV: forall u.(rev(u) = trmif Null(u) then u else rev(cdr(u)) @ cons(car(u),nil)); axiom APPEND: forall u v.(u@v = trmif Null(u) then v else cons(car(u),cdr(u)@v)); setbasicsimp Funs at facts {REV,APPEND};

Appendix D: Semantic Evaluations

declare funconst length (List)=NATNUM; attach cons to [Sexp,Sexp=Sexp] CONS; attach car to [Sexp=Sexp] CAR; attach cdr to [Sexp=Sexp] CDR; attach nil to [Sexp] NIL; attach length to [Sexp=NATNUM] LENGTH; simplify length(cons(nil, cons(nil, nil)))=suc(suc(zro)); simplify suc(zro)+zro=zro; simplify zro < prd(suc(suc(zro)));

Appendix E: Syntactic Simplification

simplify Null(nil); setbasicsimp S1 at facts {1}; rewrite rev(cons(x,nil)) by Basic uni Funs uni S1 uni LOGICTREE;

(top, beg)

Diagonalisation Lemma

By Alex Simpson, October 1989. Based on the original version by Fausto Giunchiglia.

Would be nicer with reflection up and a mechanism for definitions.

What's here:

Unformalised Theorem

The diagonalisation lemma is a major step in the proof of many important metamathematical results such as Godel's two theorems. Although not explicitly formulated by Godel the result is just an application of the methods which he developed in his proof.

In its usual form the lemma applies to any first order theory with enough expressive power to represent all primitive recursive functions. The proper proof of the lemma requires a laborious encoding of the expressions of the language as objects of the theory (Godel numbering). Due to the expressive power of the theory meta-theoretical operations on expressions of the language (in particular substitution) are representable in the theory as functions operating on the codes of those expressions. Once the relevant substitution function is established the interesting part of the proof, the diagonal construction, is possible.

The theorem states that for any wff \(\Psi\) with one free variable there is a sentence \(\Phi\) such that:

\(\vdash \Phi \longleftrightarrow \Psi[\sim\Phi\sim]\) (DIAG)

Here \(\sim.\sim\) represents the code of its argument, \(\Psi[t]\) represents the wff \(\Phi\) with each occurence of its free variable replaced by the term t, and \(\vdash\) is the provability turnstile.

The GETFOL proof will start with the assumption that the relevant substitution function exists. An encoding of the language into the theory is thus assumed (it is necessary for a substitution function to be possible) but the details of the encoding need not be made explicit. The only requirement is that the following holds for each wff \(W\), variable \(v\) and code \(n\):

\(\vdash \text{subst}(\sim W\sim,\sim v\sim,n)\ =\ \sim W[n/v]\sim\) (*)

Here \(W[n/v]\) represents the wff \(W\) with all free occurrences of \(v\) replaced by \(n\).

The stipulation that \(n\) be a code in (*) is crucial. The basic substitution function, subst', satisfies:

\(\vdash \text{subst'}(\sim W\sim,\sim v\sim,\sim t\sim)\ =\ \sim W[t/v]\sim\) (**)

where \(t\) is an arbitrary term. However this substitution is not sufficient for diagonalisation because the proof requires the third argument itself to be substituted, rather than what it encodes.

It is obviously impossible to have a function subst'' satisfying:

\(\vdash \text{subst''}(\sim W\sim,\sim v\sim,t)\ =\ \sim W[t/v]\sim\)

because different terms representing the same object evaluate equally on the left and differently on the right. The problem is solved in Peano Arithmetic, for example, because only natural numbers are dealt with. Each natural number is canonically represented by its numeral and so the existence of subst satisfying (*) (where \(n\) represents a numeral) follows from subst' satisfying (**) because the encoding of the numerals is primitive recursive and thus representable in the theory.

To make the setting of the diagonalisation lemma as general as possible only the existence of a coding and substitution function satisfying (*) are assumed. Perhaps a more elegant way would be to have a substitution satisfying (**) and a function which encodes a code and then to define:

\(\text{subst}(x,y,n) = \text{subst'}(x,y,encode(n))\)

Proof

Given an arbitrary wff \(\Psi\) with one free variable the construction of a sentence \(\Phi\) which satisfies (DIAG) proceeds in the folowing way:

First an arbitrary variable, say \(v_0\), is selected. It must have a code \(\sim v_0\sim\) so it is possible to construct the wff:

\(\Theta \iff \Psi[\text{subst}(v_0,\sim v_0\sim,v_0)]\) (1)

Here the \(\iff\) means that \(\Theta\) is defined to be this wff. \(\Theta\) is not part of the language, it is meta-level abbreviation for the wff it represents.

Putting \(W = \Theta, v = v_0, n = \sim\Theta\sim\) in (*) gives:

\(\vdash \text{subst}(\sim\Theta\sim,\sim v_0\sim,\sim\Theta\sim) = \sim\Theta[\sim\Theta\sim/v_0]\sim\) (A)

Using the definition of \(\Theta\) the following holds:

\(\Theta[\sim\Theta\sim/v_0] == \Psi[\text{subst}(\sim\Theta\sim,\sim v_0\sim,\sim\Theta\sim)]\) (B)

Here the \(==\) means that the two sides are identical wffs, and the equivalence is derived by performing the substitution on the left hand side.

Because the two sides of (B) are identical wffs their codes are identical, therefore substituting in (A) gives:

\(\vdash \text{subst}(\sim\Theta\sim,\sim v0\sim,\sim\Theta\sim) = \sim\Psi[\text{subst}(\sim\Theta\sim,\sim v0\sim,\sim\Theta\sim)]\sim\) (C)

Defining \(\Phi\) by

\(\Phi \iff \Psi[\text{subst}(\sim\Theta\sim,\sim v_0\sim,\sim\Theta\sim)]\) (2)

gives:

\(\vdash \text{subst}(\sim\Theta\sim,\sim v_0\sim,\sim\Theta\sim) = \sim\Phi\sim\) (D)

which is just (C) rewriten using the definition.

But trivially:

\(\vdash \Phi \longleftrightarrow \Psi[\text{subst}(\sim\Theta\sim,\sim v_0\sim,\sim\Theta\sim)]\) (E)

because the left hand side is just an abbreviation for the right.

Now substituting via (D) in (E) shows that \(\Phi\) is indeed the required wff.

\(\vdash \Phi \longleftrightarrow \Psi[\sim\Phi\sim]\) (DIAG)

GETFOL Formalisation

Basic Object Theory

The object theory is a standard unsorted (ie. one sort only) first order theory. For now no assumptions are being made about the language.

NAMECONTEXT OBJECT; DECLARE SORT OBJ;

Basic Meta Theory

The objects of the meta theory are the names of the object theory expressions - ie. a representation of the lexical forms of the expressions.

MAKECONTEXT META; SWITCHCONTEXT META;

Syntax

DECLARE SORT WFF TERM INDVAR PREDCONST FUNCONST; MOREGENERAL TERM <INDVAR>; DECLARE INDVAR W [WFF]; DECLARE INDVAR v [INDVAR]; DECLARE PREDCONST THEOREM 1; DECLARE INDCONST Equality [PREDCONST]; DECLARE FUNCONST pred2apply (PREDCONST,TERM,TERM)=WFF; DECLARE FUNCONST mkiff (WFF,WFF)=WFF; DECLARE FUNCONST pred1apply (PREDCONST,TERM)=WFF; DECLARE FUNCONST fun3appl (FUNCONST,TERM,TERM,TERM)=TERM;

Semantics

MATTACH Equality dar OBJECT::PREDCONST:=; ATTACH mkiff TO mkiff; ATTACH pred1apply TO predappl1\-mak; ATTACH pred2apply TO predappl2\-mak; ATTACH fun3appl TO appl3\-mak;

Basic Axiom

If there was reflection up this axiom would not be necessary.

AXIOM A1: forall W. THEOREM(mkiff(W,W));

Encoding

The encoding is a mapping from the names of expressions onto the names of the canonical terms (codes) representing them in the object theory. It is thus an operation entirely at the meta level. It is necessary to have a new sort at the meta level containing the names of codes (it is therefore a subsort of the sort containing names of terms).

Note, there cannot be a sort of codes at the object level because the codes are terms in a certain canonical form. Thus of two terms representing the same object one might be a code and the other not, but these two terms must necessarily have the same sort at the object level.

DECLARE SORT CODE; MOREGENERAL TERM <CODE>; DECLARE INDVAR n [CODE]; DECLARE FUNCONST encodewff (WFF)=CODE; DECLARE FUNCONST encodevar (INDVAR)=CODE;

Substitution Function

OBJECT THEORY

SWITCHCONTEXT OBJECT;

The substitution function is a function of the object theory.

DECLARE FUNCONST subst (OBJ,OBJ,OBJ)=OBJ;

META THEORETICAL DEFINITION

SWITCHCONTEXT META;

The only property required of subst is that it satisfies (*). It is necessary to express this property as an axiom at the meta level.

The right hand side of (*) requires the computation of \(W[n/v]\) which is basically the substitution function for names of expressions. The function which performs this is provided by semantic attachment to a GETFOL substitution routine via the function substfree.

DEFLAM substfree (WFF VAR TRM) (clist\-get\-ctext&applfun (QUOTE OBJECT) (QUOTE substexp) (LIST VAR TRM WFF) );
DECLARE FUNCONST substfree (WFF,INDVAR,CODE)=WFF; ATTACH substfree TO substfree;

To state the substitution axiom it is necessary to have a name for subst.

DECLARE INDCONST "subst" [FUNCONST]; MATTACH "subst" TO OBJECT::FUNCONST:subst;

The axiom is a direct translation of (*).

AXIOM AX_subst: forall W v n. THEOREM( pred2apply(Equality fun3appl("subst",encodewff(W),encodevar(v),n), encodewff(substfree(W,v,n)) ));

Proof

The GETFOL formalisation of the proof is interesting because it enforces a separation between the meta-theoretic and object-theoretic steps. As a matter of fact practically all the proof is performed at the meta level, because that is the only level at which the intensional equivalence (ie. same name and therefore same code) can be expressed.

OBJECT LANGUAGE

SWITCHCONTEXT OBJECT;

The informal proof starts with the wff \(\Psi\) (which is to be diagonalised) and a selected variable. To simplify matters the formalised proof will be given for an arbitrary unary predicate instead of a wff with one free variable.

DECLARE PREDCONST PSI 1; DECLARE INDVAR v0 [OBJ];

The code of \(v_0\) exists at the object level. As the coding is purely hypothetical it is necessary to declare a constant to represent this code.

DECLARE INDCONST ~v0~ [OBJ];

META REPRESENTATION

SWITCHCONTEXT META;

The meta language must have names for the alphabet of the object language.

DECLARE INDCONST "PSI" [PREDCONST]; DECLARE INDCONST "v0" [INDVAR]; DECLARE INDCONST "~v0~" [CODE]; MATTACH "PSI" TO OBJECT::PREDCONST:PSI; MATTACH "v0" TO OBJECT::INDVAR:v0; MATTACH "~v0~" TO OBJECT::INDCONST:~v0~;

\(\sim v_0\sim\) is defined to be the code of \(v_0\) by an axiom.

AXIOM CODE_v0: "~v0~" = encodevar("v0");

DEFINITION OF \(\Theta\)

There is no mechanism for making an abbreviating definition in GETFOL. Thus to force \(\Theta\) to be the same wff as \(\Psi(v_0,\sim v_0\sim,v_0)\) it is necessary to define the name of \(\Theta\) as equal to the name of \(\Psi(v_0,\sim v_0\sim,v_0)\). Thus \(\Theta\) is defined at the meta level.

DECLARE INDCONST "THETA" [WFF]; AXIOM DEF_THETA: "THETA" = pred1apply("PSI", fun3appl("subst","v0","~v0~","v0"));

It turns out that \(\Theta\) is not needed at the object level, however its code is.

SWITCHCONTEXT OBJECT; DECLARE INDCONST ~THETA~ [OBJ]; SWITCHCONTEXT META; DECLARE INDCONST "~THETA~" [CODE]; MATTACH "~THETA~" TO OBJECT::INDCONST:~THETA~; AXIOM CODE_THETA: "~THETA~" = encodewff("THETA");

PROOF STEPS (A) - (C)

(A) is obtained as an instance of (*) (ie. AX_subst) by doing forall elimination using "THETA", "v0" and "~THETA~", then substituting the occurrence of encodewff("THETA") with the identical "~THETA~", and the occurrence of encodevar("v0") with the identical "~v0~".

ALLE AX_subst "THETA" "v0" "~THETA~"; SUBST ^1 with CODE_THETA right; LABEL FACT A; SUBST ^1 with CODE_v0 right;

(B) is derived precisely by means of computing the substitution using the definition of \(\Theta\) and the GETFOL substitution function which is attached to substfree.

LABEL FACT B; SETBASICSIMP DEF\-THETA at facts {DEF_THETA}; EVAL substfree("THETA","v0","~THETA~") = pred1apply("PSI",fun3appl("subst","~THETA~","~v0~","~THETA~")) BY DEF\-THETA;

(C) follows by a simple substitution.

LABEL FACT C; SUBST A with B;

DEFINITION OF \(\Phi\)

\(\Phi\) is defined by a meta level axiom in the same way as \(\Theta\). This time \(\Phi\) is also required as a sentence at the object level. Note that actually \(\Phi\) already exists at the object level in its expanded form, however it is nice to make things readable ...

SWITCHCONTEXT OBJECT; DECLARE SENTCONST PHI; DECLARE INDCONST ~PHI~ [OBJ]; SWITCHCONTEXT META; DECLARE INDCONST "PHI" [WFF]; DECLARE INDCONST "~PHI~" [CODE]; MATTACH "PHI" TO OBJECT::SENTCONST:PHI; MATTACH "~PHI~" TO OBJECT::INDCONST:~PHI~; AXIOM DEF_PHI: "PHI" = pred1apply("PSI",fun3appl("subst","~THETA~","~v0~","~THETA~")); AXIOM CODE_PHI: "~PHI~" = encodewff("PHI");

PROOF STEPS (D) & (E)

(D) follows from the abbreviation of \(\Phi\) in (C) and the substitution of encodewff("PHI") with the identical "~PHI~".

SUBST C with DEF_PHI right; LABEL FACT D; SUBST ^1 with CODE_PHI right;

(E) is an instance of the trivial (A1) after substitution of identities.

ALLE A1 "PHI"; LABEL FACT E; SUBST ^1 with DEF_PHI OCC 2;

DEDUCING (DIAG)

The last part of the proof is the only part at the object level. (D) and (E) are reflected into theorems at the object level. (DIAG) then follows by substitution of equals at the object level. Note this is an essentially object level step because the equality does not hold at the meta level.

SWITCHCONTEXT OBJECT; REFLECT D; REFLECT E; LABEL FACT DIAG; SUBST ^1 with ^2;

(top, beg)

Playground