;;; file:hao_term.scm (display" Begin of hao_term.scm ") (begin (add-alg "ord" '("ø" "ord") '("OP" "ord=>ord=>ord")) (display" We define the algebra ord of Ordinals as follows: O , α,β -> ω^α + β So we have: O : ø 1 : OP NULL NULL 2 : OP NULL (OP NULL NULL) n+1 : OP NULL n ω : OP (OP NULL NULL) NULL ω+1 : OP (OP NULL NULL) (OP NULL NULL) 1+ω+1 : OP NULL (OP (OP NULL NULL) (OP NULL NULL)) 1+α : OP NULL α ") (begin (display" We introduce some ordinal constants ") (add-token "①" 'const (pt "OP ø ø")) (add-token "②" 'const (pt "OP ø ①")) (add-token "③" 'const (pt "OP ø ②")) (add-token "④" 'const (pt "OP ø ③")) (add-token "⑤" 'const (pt "OP ø ④")) (add-token "⑥" 'const (pt "OP ø ⑤")) (add-token "⑦" 'const (pt "OP ø ⑥")) (add-token "⑧" 'const (pt "OP ø ⑦")) (add-token "⑨" 'const (pt "OP ø ⑧")) (add-token "⑩" 'const (pt "OP ø ⑨")) (add-token "⑪" 'const (pt "OP ø ⑩")) (add-token "⑫" 'const (pt "OP ø ⑪")) (add-token "⑬" 'const (pt "OP ø ⑫")) (add-token "⑭" 'const (pt "OP ø ⑬")) (add-token "⑮" 'const (pt "OP ø ⑭")) (add-token "ω" 'const (pt "OP ① ø")) (add-token "ω²" 'const (pt "OP ② ø")) (add-token "ω³" 'const (pt "OP ③ ø")) (add-token "ω⁴" 'const (pt "OP ④ ø")) (add-token "ω⁵" 'const (pt "OP ⑤ ø")) (add-token "ω⁶" 'const (pt "OP ⑥ ø")) (add-token "ω⁷" 'const (pt "OP ⑦ ø")) (add-token "ω⁸" 'const (pt "OP ⑧ ø")) (add-token "ω⁹" 'const (pt "OP ⑨ ø")) (add-token "ω₂" 'const (pt "OP ω ø")) (add-token "ω₃" 'const (pt "OP ω₂ ø")) (add-token "ω₄" 'const (pt "OP ω₃ ø")) (add-token "ω₅" 'const (pt "OP ω₄ ø")) (add-token "ω₆" 'const (pt "OP ω₅ ø")) (add-token "ω₇" 'const (pt "OP ω₆ ø")) (add-token "ω₈" 'const (pt "OP ω₇ ø")) (add-token "ω₉" 'const (pt "OP ω₈ ø")) (add-display (py "ord") (lambda (x) (cond ((equal? x (pt "ø"))(list 'const "ø")) ((equal? x (pt "OP ø ø"))(list 'const "①")) ((equal? x (pt "OP ø ①"))(list 'const "②")) ((equal? x (pt "OP ø ②"))(list 'const "③")) ((equal? x (pt "OP ø ③"))(list 'const "④")) ((equal? x (pt "OP ø ④"))(list 'const "⑤")) ((equal? x (pt "OP ø ⑤"))(list 'const "⑥")) ((equal? x (pt "OP ø ⑥"))(list 'const "⑦")) ((equal? x (pt "OP ø ⑦"))(list 'const "⑧")) ((equal? x (pt "OP ø ⑧"))(list 'const "⑨")) ((equal? x (pt "OP ø ⑨"))(list 'const "⑩")) ((equal? x (pt "OP ø ⑩"))(list 'const "⑪")) ((equal? x (pt "OP ø ⑪"))(list 'const "⑫")) ((equal? x (pt "OP ø ⑫"))(list 'const "⑬")) ((equal? x (pt "OP ø ⑬"))(list 'const "⑭")) ((equal? x (pt "OP ø ⑭"))(list 'const "⑮")) ((equal? x (pt "OP ① ø"))(list 'const "ω")) ((equal? x (pt "OP ② ø"))(list 'const "ω²")) ((equal? x (pt "OP ③ ø"))(list 'const "ω³")) ((equal? x (pt "OP ④ ø"))(list 'const "ω⁴")) ((equal? x (pt "OP ⑤ ø"))(list 'const "ω⁵")) ((equal? x (pt "OP ⑥ ø"))(list 'const "ω⁶")) ((equal? x (pt "OP ⑦ ø"))(list 'const "ω⁷")) ((equal? x (pt "OP ⑧ ø"))(list 'const "ω⁸")) ((equal? x (pt "OP ⑨ ø"))(list 'const "ω⁹")) ((equal? x (pt "OP ω ø"))(list 'const "ω₂")) ((equal? x (pt "OP ω₂ ø"))(list 'const "ω₃")) ((equal? x (pt "OP ω₃ ø"))(list 'const "ω₄")) ((equal? x (pt "OP ω₄ ø"))(list 'const "ω₅")) ((equal? x (pt "OP ω₅ ø"))(list 'const "ω₆")) ((equal? x (pt "OP ω₆ ø"))(list 'const "ω₇")) ((equal? x (pt "OP ω₇ ø"))(list 'const "ω₈")) ((equal? x (pt "OP ω₈ ø"))(list 'const "ω₉")) (else #f)))) (newline) (display "ø\t\t\t\t") (pp (pt "ø")) (display "OP ø ø\t\t\t\t")(pp (pt "OP ø ø")) (display "OP ø ①\t\t\t\t")(pp (pt "OP ø ①")) (display "OP ø ⑭\t\t\t\t")(pp (pt "OP ø ⑭")) (display "OP ① ø\t\t\t\t")(pp (pt "OP ① ø")) (display "OP ② ø\t\t\t\t")(pp (pt "OP ② ø")) (display "OP ⑨ ø\t\t\t\t")(pp (pt "OP ⑨ ø")) (display "ω\t\t\t\t")(pp (pt "ω")) (display "OP ω ø\t\t\t\t")(pp (pt "OP ω ø")) (display "OP ω₈ ø\t\t\t\t")(pp (pt "OP ω₈ ø")) (newline) ) (add-program-constant "ordSubterm" (mk-arrow (make-alg "ord") (make-alg "ord") (make-alg "boole")) 1 'const 2) (add-token "⊏" 'rel-op (lambda (x y) (mk-term-in-app-form (make-term-in-const-form (pconst-name-to-pconst "ordSubterm")) x y))) (add-display (py "boole") (lambda (x) (if (term-in-app-form? x) (let* ((op (term-in-app-form-to-final-op x)) (args (term-in-app-form-to-args x))) (if (and (term-in-const-form? op) (string=? "ordSubterm" (const-to-name (term-in-const-form-to-const op))) (= 2 (length args))) (list 'rel-op "⊏" (term-to-token-tree (car args)) (term-to-token-tree (cadr args))) #f)) #f))) (acr "ord ⊏ ø" "ord = ø") (acr "ord ⊏ (OP ord1 ord2)" "(((ord=ord1) ∨ (ord=ord2)) ∨ (ord ⊏ ord1)) ∨ (ord ⊏ ord2)") (add-program-constant "ω⋆" (mk-arrow (make-alg "ord")(make-alg "ord")) 1 'const 1) (acr "ω⋆ ø" "ø") (acr "ω⋆(OP ord1 ord2)" "OP (OP ø ord1) (ω⋆ord2)") (add-program-constant "ω^" (mk-arrow (make-alg "ord")(make-alg "ord")) 1 'const 1) (acr "ω^ ord" "OP ord ø") (add-program-constant "℧" (mk-arrow (py "nat") (py "ord")) 1 'const 1) (acr "℧ 0" "①") (acr "℧ (SUCC nat)" "OP (℧ nat) ø") (set! OLD-COMMENT-FLAG COMMENT-FLAG) (set! COMMENT-FLAG #t) (display-constructors "ord") (display " ordSubterm relation ⊏ ") (display-program-constants "ordSubterm") (display " ω-multiplication ") (display-program-constants "ω⋆") (display" ω-exponentiation ") (display-program-constants "ω^") (display" ω-Tower ℧ ") (display-program-constants "℧") (set! COMMENT-FLAG OLD-COMMENT-FLAG) (display" In order to test extracted programmes we define the functions (test-extracted-unary THM) (test-extracted-binary THM) (test-extracted-mixed THM) ") (define (test-extracted-unary THM) (deanimate THM) (set! OLD-COMMENT-FLAG COMMENT-FLAG) (set! COMMENT-FLAG #t) (newline) (newline) (animate THM) (display (string-append " Test of extracted function c" THM " ")) (display"ø ")(pnt (string-append "c" THM "ø")) (display"① ")(pnt (string-append "c" THM "①")) (display"⑭ ")(pnt (string-append "c" THM "⑭")) (display"ω⁶ ")(pnt (string-append "c" THM "ω⁶")) (display"OP ω⁷ ② ")(pnt (string-append "c" THM "(OP ω⁷ ②)")) (display"OP ② ω⁷ ")(pnt (string-append "c" THM "(OP ② ω⁷)")) (display"ω₇ ")(pnt (string-append "c" THM "ω₇")) (display"OP ω₉ ⑧ ")(pnt (string-append "c" THM "(OP ω₉ ⑧)")) (display"OP ⑧ ω₉ ")(pnt (string-append "c" THM "(OP ⑧ ω₉)")) (newline) (display-theorems THM) (newline) (set! COMMENT-FLAG OLD-COMMENT-FLAG) (deanimate THM)) (define (test-extracted-binary THM) (deanimate THM) (set! OLD-COMMENT-FLAG COMMENT-FLAG) (set! COMMENT-FLAG #t) (newline) (newline) (animate THM) (display (string-append " Test of extracted function c" THM " ")) (display"ø ø ")(pnt (string-append "c" THM "ø ø")) (display"ø ① ")(pnt (string-append "c" THM "ø ①")) (display"① ø ")(pnt (string-append "c" THM "① ø")) (display"① ⑭ ")(pnt (string-append "c" THM "① ⑭")) (display"ω₇ ω₇ ")(pnt (string-append "c" THM "ω₇ ω₇")) (display"ω₅ ω₇ ")(pnt (string-append "c" THM "ω₅ ω₇")) (display"ω₇ ω₅ ")(pnt (string-append "c" THM "ω₇ ω₅")) (display"ω⁶ ω⁶ ")(pnt (string-append "c" THM "ω⁶ ω⁶")) (display"ω⁶ ω⁹ ")(pnt (string-append "c" THM "ω⁶ ω⁹")) (display"ω⁹ ω⁶ ")(pnt (string-append "c" THM "ω⁹ ω⁶")) (display"OP ⑨ ⑩ OP ⑨ ⑩ ")(pnt (string-append "c" THM "(OP ⑨ ⑩) (OP ⑨ ⑩)")) (display"OP ⑨ ⑩ ⑨ ")(pnt (string-append "c" THM "(OP ⑨ ⑩) ⑨")) (display"⑨ OP ⑨ ⑩ ")(pnt (string-append "c" THM "⑨ (OP ⑨ ⑩)")) (newline) (display-theorems THM) (newline) (set! COMMENT-FLAG OLD-COMMENT-FLAG) (deanimate THM)) (define (test-extracted-mixed THM) (deanimate THM) (set! OLD-COMMENT-FLAG COMMENT-FLAG) (set! COMMENT-FLAG #t) (newline) (newline) (animate THM) (display (string-append " Test of extracted function c" THM " ")) (display"ø 0 ")(pnt (string-append "c" THM "ø 0")) (display"ø 1 ")(pnt (string-append "c" THM "ø 1")) (display"① 0 ")(pnt (string-append "c" THM "① 0")) (display"① 14 ")(pnt (string-append "c" THM "① 14")) (display"ω₇ 7 ")(pnt (string-append "c" THM "ω₇ 7")) (display"ω₅ 7 ")(pnt (string-append "c" THM "ω₅ 7")) (display"ω₇ 5 ")(pnt (string-append "c" THM "ω₇ 5")) (display"ω⁶ 6 ")(pnt (string-append "c" THM "ω⁶ 6")) (display"ω⁶ 6 ")(pnt (string-append "c" THM "ω⁶ 9")) (display"ω⁹ 6 ")(pnt (string-append "c" THM "ω⁹ 6")) (display"OP ⑨ ⑩ 19 ")(pnt (string-append "c" THM "(OP ⑨ ⑩) 19")) (display"OP ⑨ ⑩ 9 ")(pnt (string-append "c" THM "(OP ⑨ ⑩) 9")) (display"⑨ 19 ")(pnt (string-append "c" THM "⑨ 19")) (newline) (display-theorems THM) (newline) (set! COMMENT-FLAG OLD-COMMENT-FLAG) (deanimate THM)) ) (display" Some ordinal term RW-rules: ") (begin ; ordEQsym: (α=β) = (β=α) (sg "(ord1=ord2) = (ord2=ord1)") (ca "all ord1,ord2.(ord1=ord2) -> (ord2=ord1)" "->") (assume "ord1" "ord2") (cd "ord1=ord2" "1=2") (simp "<-" "1=2") (use "Truth-Axiom") (assume "1≠2") (cut(pf"ord2=ord1->F")) (cases(pt"ord2=ord1")) (auto) (assume "ord1" "ord2") (assume "1=2") (simp "1=2") (use "Truth-Axiom") ; Proof finished. (save "ordEQsym") (display-theorems "ordEQsym") ; ø subterm aller (sg "ø ⊏ ord") (ind) (use "Truth-Axiom") (assume "ord1" "ord2" "IH1" "IH2") (drop "IH1") (ng) (simp "IH2") (use "Truth-Axiom") ; Proof finished. (trw "ø ⊏ ord") ; STtrans: ST relation is transitive (sg "all ord2,ord1.ord1⊏ord2 ∧ ord2⊏ord3 → ord1⊏ord3") (ind) (cases) (auto) (assume "ord31" "ord32" "IH31" "IH32" "ord2" "ord1") (ng) (ass "hyp") (inst-with-to "hyp" 'left 'left 'left 'left "1st2") (inst-with-to "hyp" 'left 'left 'left 'right "2st32") (ca "F=(ord1⊏ord31)" "F=1st31") (ca "¬(ord2⊏ord31)" "¬2st31") (cds "ord32=ord2" "32=2") (use "1st2") (assume "32≠2") (booleimp "ord1⊏ord2∧ord2⊏ord32") (use "IH32") (drop "IH31" "IH32" "hyp") (simp "1st2") (ng) (booleimp "¬(ord2=ord31)∧ ¬(ord2=ord32)∧ ¬(ord2⊏ord31)") (use "2st32") (simp(pf"(ord2=ord31)=F")) (simp-with "ordEQsym" (pt"ord2") (pt"ord32")) (simp-with "32≠2" ) (use "¬2st31") (cd "ord2=ord31" "2=31") (ng) (simp "F=1st31") (simp "<-" "2=31") (auto) (cd "ord2⊏ord31" "2st31") (ng) (simp "F=1st31") (booleimp "ord1⊏ord2∧ord2⊏ord31") (use "IH31") (simp "1st2") (auto) (simp "BooleFalseLeft") (use-with "hyp" 'right) ; Proof finished (nrw "ord1⊏ord2 ∧ ord2⊏ord3 → ord1⊏ord3") (sg "ord1⊏ord2∧(¬(ord2=ord3)∧ ¬(ord2=ord4)∧ ¬(ord2⊏ord3)→ord2⊏ord4)∧ ¬(ord1⊏ord3)→ord1⊏ord4") (assume "ord1" "ord2" "ord3" "ord4") (ass "hyp") (cds "ord4=ord2" "4=2") (use-with "hyp" 'left 'left) (assume "4≠2") (trans "ord2") (simp-with "hyp" 'left 'left) (ng) (booleimp "¬(ord2=ord3)∧ ¬(ord2=ord4)∧ ¬(ord2⊏ord3)") (use-with "hyp" 'left 'right) (simp-with "ordEQsym" (pt"ord2") (pt"ord4")) (simp "4≠2") (ng) (split) (cd "ord2=ord3" "2=3") (booleimp "ord1⊏ord3") (ng) (use-with "hyp" 'right) (simp "<-" "2=3") (use-with "hyp" 'left 'left) (search) (simp (pf "(ord2⊏ord3)=(ord1⊏ord2∧ord2⊏ord3)")) (booleimp "¬(ord1⊏ord3)") (simp (pf"all boole1,boole2.(boole1∨(¬boole2))=(boole2→boole1)")) (use "Truth-Axiom") (cases) (auto) (use-with "hyp" 'right) (simp-with "hyp" 'left 'left) (use "Truth-Axiom") ; Proof finished. (nrw "ord1⊏ord2∧(¬(ord2=ord3)∧ ¬(ord2=ord4)∧ ¬(ord2⊏ord3)→ord2⊏ord4)∧ ¬(ord1⊏ord3)→ord1⊏ord4") (set! OLD-COMMENT-FLAG COMMENT-FLAG) (set! COMMENT-FLAG #t) (display " ⊏ is transitive ord1 ⊏ ord2 ∧ ord2 ⊏ ord3 → ord1⊏ord3 ") (pnt "ord1 ⊏ ord2 ∧ ord2 ⊏ ord3 → ord1⊏ord3") (set! COMMENT-FLAG OLD-COMMENT-FLAG) ) (newline) (display " Some Theorems Comp: α=ø ∨ (∃ξ₁,ξ₂) α=OP ξ₁ ξ₂ ") (newline) (begin (sg "all ord.ex boole,ord0,ord1. (¬boole → ord= ø) ∧ (boole→ord=OP ord0 ord1)") (cases) (ex-intro (pt "F")) (ex-intro (pt "ø")) (ex-intro (pt "ø")) (use "Truth-Axiom") (assume "ord2" "ord3") (ex-intro (pt "T")) (ex-intro (pt"ord2")) (ex-intro (pt"ord3")) (use "Truth-Axiom") ; Proof finished. (save "Comp") (display-theorems "Comp") (add-theorem "CompSoundness" (np(proof-to-soundness-proof (theorem-name-to-proof "Comp")))) ; (display-theorems "CompSoundness") (test-extracted-unary "Comp") ) (animate "Comp") (display" NonZeroConstructed: α=ø ∨ α = OP left (right cComp α) right (right cComp α) ") (sg "(ord= ø) ∨ (ord=OP (left (right (cComp ord))) (right (right (cComp ord))))") (cases) (auto) ; Proof finished. (nrw "(ord= ø) ∨ (ord=OP (left (right (cComp ord))) (right (right (cComp ord))))") (nrw "ord= ø ∨ord=OP[if ord ø ([ord0,ord1]ord0)][if ord ø ([ord0,ord1]ord1)]") (display " FINITE ORDINALS We define inductively the predicate FORD ⊆ nat @ ord for finite ordinal. ") (add-ids (list (list "FORD" (make-arity (py "nat") (py "ord")))) '("FORD 0 ø") '("allnc nat,ord.FORD nat ord -> FORD (SUCC nat) (OP ø ord)")) (sg "FORD nat ord -> nat=0 -> ord= ø") (assume "nat" "ord") (elim) (auto) ; Proof finished. (save "FORD0") (display-theorems "FORD0") (display" We extract an embedding of nat -> ord: ") (begin (sg "all nat.ex ord.FORD nat ord") (ind) (ex-intro(pt"ø")) (intro 0) (assume "nat" "IH") (by-assume-with "IH" "ord" "IHord") (ex-intro(pt"OP ø ord")) (intro 1) (use "IHord") ; ; Proof finished. (save "FO") (display-theorems "FO") (animate "FO") (display" Test of cFO: ") (display "cFO 1 ") (pnt"cFO 1 ") (display "cFO 8 ") (pnt"cFO 8 ") (display "cFO 13 ") (pnt"cFO 13 ") (newline) (deanimate "FO") ) (display " ordSTind: F^ ø → [ ∀α (∀β⊏α F^β) → F^ α ] → ∀γ F^ γ ") (begin (sg "(Pvar ord)^ ø -> (all ord1.(all ord2.ord2⊏ord1 -> (Pvar ord)^ ord2) -> (Pvar ord)^ ord1) -> all ord (Pvar ord)^ ord") (assume "A0" "PROG" "ord") (ca "all ord1,ord2.ord2⊏ord1 -> (Pvar ord)^ ord2" "aux") (use "aux" (pt"OP ord ord")) (use "Truth-Axiom") ; ?_4: all ord1,ord2.ord2⊏ord1 -> (Pvar ord)^ord2 (ind) (drop "PROG") (ng) (assume "ord2" "2=0") (simp "2=0") (use "A0") (assume "ord3" "ord4" "IH3" "IH4" "ord2" "st") (use "PROG") (drop "A0" "PROG") (assume "ord1" "1st2") (cd "ord1⊏ord3" "1st3") (use "IH3") (use "1st3") (assume "¬1st3") (use "IH4") (booleimp "ord1⊏ord2 ∧ ord2⊏OP ord3 ord4 ∧ ¬(ord1⊏ord3)") (use "Truth-Axiom") (simp "¬1st3") (simp "st") (use "1st2") ; Proof finished. (save "ordSTind") (display-theorems "ordSTind") ) (display " End of hao_term.scm ") ;EOF