Tutorial on Proof by Reflection in the seminal FOL

Fork me on GitHub

This tutorial demonstrates computational proof by reflection in GETFOL, implementing Weyhrauch's slogan: "Change theorem proving in the theory into evaluation in the metatheory".

Instead of proving that numbers are even through logical deduction, we'll compute their evenness and automatically convert valid computations into theorems.

← Back to main FOL Software Archaeology

What We'll Build

A system that:

Step 1: Object-Level Setup

First, we establish the basic even predicate and its computational semantics:

fetch ../tst/prolegomena/appa.tst; comment | Define even predicate axiomatically | declare predconst even 1; axiom EVEN0: even(zro); axiom EVEN: forall n.(even(suc(suc(n))) iff even(n)); comment | Attach computational semantics | deflam evenp(x) (= (MOD x 2) 0); attach even to [NATNUM] evenp; comment | Create test claims | axiom CLAIM_EVEN0: even(zro); comment | 0 is even - TRUE | axiom CLAIM_EVEN2: even(suc(suc(zro))); comment | 2 is even - TRUE | axiom CLAIM_EVEN4: even(suc(suc(suc(suc(zro))))); comment | 4 is even - TRUE | axiom CLAIM_EVEN1: even(suc(zro)); comment | 1 is even - FALSE |

Step 2: Meta-Level Context

Now we create the meta-level context where we'll analyze WFF structure:

comment | Set up meta-level reasoning | NAMECONTEXT OBJ; MAKECONTEXT META; SWITCHCONTEXT META; DECLARE PREDCONST THEOREM 1; DECLARE SORT WFF FACT TERM PREDSYM FUNSYM; DECREP WFF FACT TERM PREDSYM FUNSYM; REPRESENT {WFF} AS WFF; REPRESENT {FACT} AS FACT; REPRESENT {TERM} AS TERM; REPRESENT {PREDSYM} AS PREDSYM; REPRESENT {FUNSYM} AS FUNSYM; DECLARE FUNCONST wffof (FACT)=WFF; ATTACH wffof TO [FACT=WFF] fact\-get\-wff;

Step 3: WFF Structure Analysis

We need functions to parse WFF structure and extract predicate information:

comment | Parse predicate symbols from WFFs | DECLARE FUNCONST mainpred (WFF)=PREDSYM; DECLARE INDCONST evenPRED [PREDSYM]; MATTACH evenPRED dar [PREDSYM] OBJ::PREDCONST:even; DEFLAM mainpred (X) (AND (PREDAPPL X) (predappl\-get\-pred X)); ATTACH mainpred to [WFF=PREDSYM] mainpred; comment | Extract arguments from predicate applications | DECLARE FUNCONST arg (WFF)=TERM; ATTACH arg TO [WFF=TERM] predappl1\-get\-arg;

Step 4: Numeral Recognition and Conversion

We need to recognize natural number terms and convert them to integers:

comment | Recognize numeral patterns | DECLARE PREDCONST NUMERAL 1; DECLARE PREDCONST numeral 3; DECLARE INDCONST zro [TERM]; DECLARE INDCONST suc [FUNSYM]; MATTACH zro dar [TERM] OBJ::INDCONST:zro; MATTACH suc dar [FUNSYM] OBJ::FUNCONST:suc; 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; DECLARE indvar x [TERM]; AXIOM AX_NUMERAL: forall x.(NUMERAL(x) iff numeral(x,zro,suc)); comment | Convert terms to numbers | 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;

Step 5: Even Claim Recognition

Define what constitutes a valid even claim:

comment | Define even claims | DECLARE PREDCONST EVENCLAIM 1; DECLARE indvar w [WFF]; AXIOM AX_EVENCLAIM: forall w.(EVENCLAIM(w) iff ( mainpred(w)=evenPRED and NUMERAL(arg(w))));

Step 6: Computational Validation

The heart of the system - computational even checking:

comment | Computational even checker | DECLARE PREDCONST COMPUTEEVEN 1; DEFLAM computeeven (t) (= (MOD (mknum t) 2) 0); ATTACH COMPUTEEVEN TO [TERM] computeeven;

Step 7: Reflection Principle

The key axiom that bridges computation and proof:

comment | Reflection principle | DECLARE indvar vl [FACT]; AXIOM EVENREFLECT: forall vl.(EVENCLAIM(wffof(vl)) and COMPUTEEVEN(arg(wffof(vl))) imp THEOREM(wffof(vl))); comment | Essential: Enable computational evaluation | SETBASICSIMP meta\-axioms at facts {AX_EVENCLAIM,AX_NUMERAL}; SETCOMPSIMP EVALSS AT LOGICTREE uni meta\-axioms;

Step 8: Testing Computational Reflection

Now let's test our reflection system:

First, we switch back to the object context.

SWITCHCONTEXT OBJ;
comment | Test reflection on even numbers | reflect EVENREFLECT CLAIM_EVEN0; theorem THM_EVEN0 1; reflect EVENREFLECT CLAIM_EVEN2; theorem THM_EVEN2 2; reflect EVENREFLECT CLAIM_EVEN4; theorem THM_EVEN4 3; show axiom;

How It Works

When reflect EVENREFLECT CLAIM_EVEN4 executes:

  1. Parse WFF: mainpred(wffof(FACT)) = evenPRED ✓
  2. Extract argument: arg(wffof(FACT)) → suc(suc(suc(suc(zro))))
  3. Convert to number: mknum(arg(...)) → 4
  4. Compute evenness: (= (MOD 4 2) 0) → TRUE ✓
  5. Create theorem: Reflection succeeds, generates THM_EVEN4

For odd numbers, step 4 returns FALSE, so reflection fails with "Sorry!! Simplified result was not of the form THEOREM(---)".

comment | This should fail - 1 is odd | reflect EVENREFLECT CLAIM_EVEN1;

Recap

fetch ../tst/prolegomena/appa.tst; comment | True computational proof by reflection for even numbers - following sec91.tst pattern | declare predconst even 1; axiom EVEN0: even(zro); axiom EVEN: forall n.(even(suc(suc(n))) iff even(n)); comment | Attach computational semantics | deflam evenp(x) (= (MOD x 2) 0); attach even to [NATNUM] evenp; comment | Test facts | axiom CLAIM_EVEN0: even(zro); comment | 0 is even - TRUE | axiom CLAIM_EVEN2: even(suc(suc(zro))); comment | 2 is even - TRUE | axiom CLAIM_EVEN4: even(suc(suc(suc(suc(zro))))); comment | 4 is even - TRUE | axiom CLAIM_EVEN1: even(suc(zro)); comment | 1 is even - FALSE | comment | Meta level setup | NAMECONTEXT OBJ; MAKECONTEXT META; SWITCHCONTEXT META; DECLARE PREDCONST THEOREM 1; DECLARE SORT WFF FACT TERM PREDSYM FUNSYM; DECREP WFF FACT TERM PREDSYM FUNSYM; REPRESENT {WFF} AS WFF; REPRESENT {FACT} AS FACT; REPRESENT {TERM} AS TERM; REPRESENT {PREDSYM} AS PREDSYM; REPRESENT {FUNSYM} AS FUNSYM; DECLARE FUNCONST wffof (FACT)=WFF; ATTACH wffof TO [FACT=WFF] fact\-get\-wff; comment | Following sec91 pattern exactly - declare mainpred | DECLARE FUNCONST mainpred (WFF)=PREDSYM; DECLARE INDCONST evenPRED [PREDSYM]; MATTACH evenPRED dar [PREDSYM] OBJ::PREDCONST:even; DEFLAM mainpred (X) (AND (PREDAPPL X) (predappl\-get\-pred X)); ATTACH mainpred to [WFF=PREDSYM] mainpred; comment | Following sec91 pattern - numeral checking | DECLARE PREDCONST NUMERAL 1; DECLARE PREDCONST numeral 3; DECLARE INDCONST zro [TERM]; DECLARE INDCONST suc [FUNSYM]; MATTACH zro dar [TERM] OBJ::INDCONST:zro; MATTACH suc dar [FUNSYM] OBJ::FUNCONST:suc; 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; DECLARE indvar x [TERM]; AXIOM AX_NUMERAL: forall x.(NUMERAL(x) iff numeral(x,zro,suc)); comment | Following sec91 pattern - mknum function | 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; comment | Define EVENCLAIM following LINEAREQ pattern | DECLARE PREDCONST EVENCLAIM 1; DECLARE FUNCONST arg (WFF)=TERM; ATTACH arg TO [WFF=TERM] predappl1\-get\-arg; DECLARE indvar w [WFF]; AXIOM AX_EVENCLAIM: forall w.(EVENCLAIM(w) iff ( mainpred(w)=evenPRED and NUMERAL(arg(w)))); comment | The computational even checker | DECLARE PREDCONST COMPUTEEVEN 1; DEFLAM computeeven (t) (= (MOD (mknum t) 2) 0); ATTACH COMPUTEEVEN TO [TERM] computeeven; comment | Reflection principle following SOLVE pattern | DECLARE indvar vl [FACT]; AXIOM EVENREFLECT: forall vl.(EVENCLAIM(wffof(vl)) and COMPUTEEVEN(arg(wffof(vl))) imp THEOREM(wffof(vl))); comment | Set up simplification like sec91 | SETBASICSIMP meta\-axioms at facts {AX_EVENCLAIM,AX_NUMERAL}; SETCOMPSIMP EVALSS AT LOGICTREE uni meta\-axioms; SWITCHCONTEXT OBJ; comment | Test computational reflection | reflect EVENREFLECT CLAIM_EVEN0; theorem THM_EVEN0 1; reflect EVENREFLECT CLAIM_EVEN2; theorem THM_EVEN2 2; reflect EVENREFLECT CLAIM_EVEN4; theorem THM_EVEN4 3; comment | This should fail | comment | reflect EVENREFLECT CLAIM_EVEN1; | show axiom;

← Back to main GETFOL tutorial

powered by io.livecode.ch