#|
 Copyright (C) 1994 by Natarajan Shankar.  All Rights Reserved.
 This script is hereby placed in the public domain, and therefore unlimited
 editing and redistribution is permitted.
 NO WARRANTY
 Natarajan Shankar PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT IS
 PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED,
 INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND
 FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND
 PERFORMANCE OF THE SCRIPT IS WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU
 ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
 IN NO EVENT WILL Natarajan Shankar BE LIABLE TO YOU FOR ANY DAMAGES, ANY LOST
 PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES
 ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT NOT
 LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED
 BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF SUCH
 DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.
|#

Event: Start with the initial thm theory.

;Annotated script for mechanical proof of the Tautology theorem.
;Proof involves -
;Definition of proof-checker for Schoenfield's FOL.
;Proof of several derived inference rules, primarily the
;subset lemma.
;Definition of tautology-checker.
;Every tautology has a proof.
;Correctness of tautology-checker - every tautology is
;always logically-true, and all logical-truths are tautologies.
;First, functions, variables and predicate symbols.

Definition: function (fn) = ((fn = list ('f, cadr (fn), caddr (fn)))

∧ (cadr (fn) ∈ N) ∧ (caddr (fn) ∈ N))

Definition: variable (x) = ((x = list ('x, cadr (x))) ∧ (cadr (x) ∈ N))

Definition: predicate (p) = (((p = list ('p, cadr (p), caddr (p)))

∧ (cadr (p) ∈ N)

∧ (caddr (p) ∈ N))

    ∨ (p = 'equal))

Definition: degree (fn) = if fn = 'equal then 2

else caddr (fn) endif

Definition: index (fn) = cadr (fn)

Definition: func-pred (x) = (function (x) ∨ predicate (x))

Definition: v (x) = list ('x, fix (x))

Theorem: numberp-fix fix (x) ∈ N

Theorem: variable-v variable (v (x))

Definition: fn (x, y) = list ('f, fix (x), fix (y))

Definition: p (x, y) = list ('p, fix (x), fix (y))

Theorem: function-fn function (fn (x, y))

Theorem: predicate-p predicate (p (x, y))

;quantifer, there exists.

Definition: quantifier (x) = (x = 'forsome)

Definition: (x ∪ y) = if listp (x)

then if car (x) ∈ y then cdr (x) ∪ y

else cons (car (x), cdr (x) ∪ y) endif else y endif Event: Enable variable; name this event ‘g0223’.

Event: Enable quantifier; name this event ‘g0224’.

Theorem: predicate-f-equal predicate ('equal)

Event: Enable function; name this event ‘g0225’.

Event: Enable predicate; name this event ‘g0226’.

Definition: append (x, y) = if listp (x) then cons (car (x), append (cdr (x), y))

else y endif

Definition: delete (x, y) = if listp (y)

then if x = car (y) then delete (x, cdr (y))

else cons (car (y), delete (x, cdr (y))) endif else y endif

Theorem: not-member-delete x ∉ delete (x, y)

;returns list of free variables in EXP.

Definition: collect-free (exp, flg) = if listp (exp)

then if flg = t

then if variable (exp) then cons (exp, nil) elseif quantifier (car (exp)) ∧ listp (cdr (exp)) then delete (cadr (exp), collect-free (cddr (exp), 'list)) elseif func-pred (car (exp))

∨ (car (exp) = 'not) ∨ (car (exp) = 'or) then collect-free (cdr (exp), 'list) else nil endif

else append (collect-free (car (exp), t),

collect-free (cdr (exp), 'list)) endif

else nil endif Definition: sentence (exp) = (collect-free (exp, t) = nil)

;returns bound variables in EXP that surround free occurrences of VAR.

Definition: covering (exp, var, flg) = if listp (exp)

then if flg = t

then if variable (exp) then nil elseif quantifier (car (exp)) ∧ listp (cdr (exp)) then if cadr (exp) = var then nil

elseif var ∈ collect-free (cddr (exp), 'list)

then cons (cadr (exp), covering (cddr (exp), var, 'list)) else nil endif elseif func-pred (car (exp))

∨ (car (exp) = 'not) ∨ (car (exp) = 'or) then covering (cdr (exp), var, 'list) else nil endif

else append (covering (car (exp), var, t),

covering (cdr (exp), var, 'list)) endif

else nil endif

;X and Y are disjoint.

Definition: nil-intersect (x, y) = if listp (x) then (car (x) ∉ y) ∧ nil-intersect (cdr (x), y)

else t endif

;TERM is free for VAR in EXP.

Definition: free-for (exp, var, term, flg) = nil-intersect (covering (exp, var, flg), collect-free (term, t))

Definition: f-equal (x, y) = list ('equal, x, y)

Definition: f-not (x) = list ('not, x)

Definition: f-or (x, y) = list ('or, x, y)

Definition: forsome (x, y) = list ('forsome, x, y)

Definition: f-and (x, y) = f-not (f-or (f-not (x), f-not (y)))

Definition: f-implies (x, y) = f-or (f-not (x), y)

Definition: ∀ var exp = f-not (forsome (var, f-not (exp)))

Definition: f-iff (x, y) = f-and (f-implies (x, y), f-implies (y, x))

Definition: var-list (list, n) = if n ≃ 0 then list = nil

else variable (car (list)) ∧ var-list (cdr (list), n − 1) endif

Definition: var-set (list, n) = if n ≃ 0 then list = nil

else variable (car (list))

∧ (car (list) ∉ cdr (list))

∧ var-set (cdr (list), n − 1) endif

;Recognizer for terms.

Definition: termp (exp, flg, count) = if flg = t

then if exp ≃ nil then f else variable (exp)

∨ (function (car (exp))

∧ termp (cdr (exp),

                          'list,

degree (car (exp)))) endif

elseif (exp ≃ nil) ∨ (count ≃ 0) then (exp = nil) ∧ (count ≃ 0)

else termp (car (exp), t, 0) ∧ termp (cdr (exp), 'list, count − 1) endif

Definition: arg1 (x) = cadr (x)

Definition: arg2 (x) = caddr (x)

;EXP is an atom, pred. symbol followed by list of terms.

Definition: atomp (exp) = (predicate (car (exp)) ∧ termp (cdr (exp), 'list, degree (car (exp))))

Event: Enable atomp; name this event ‘g0253’.

;EXP is a formula

Definition: formula (exp, flg, count) = if flg = t

then if exp ≃ nil then f else atomp (exp)

∨ ((car (exp) = 'not)

∧ formula (cdr (exp), 'list, 1)) ∨ ((car (exp) = 'or)

∧ formula (cdr (exp), 'list, 2)) ∨ ((car (exp) = 'forsome)

∧ variable (cadr (exp))

∧ formula (cddr (exp), 'list, 1)) endif

elseif (exp ≃ nil) ∨ (count ≃ 0) then (exp = nil) ∧ (count ≃ 0) else formula (car (exp), t, 0)

∧ formula (cdr (exp), 'list, count − 1) endif

;Result of substituting TERM for VAR in EXP.

Definition: subst (exp, var, term, flg) = if listp (exp)

then if flg = t

then if variable (exp)

then if exp = var then term else exp endif

elseif quantifier (car (exp)) ∧ listp (cdr (exp))

then if cadr (exp) = var then exp else cons (car (exp),

cons (cadr (exp),

subst (cddr (exp), var, term, 'list))) endif

elseif func-pred (car (exp))

∨ (car (exp) = 'not) ∨ (car (exp) = 'or)

then cons (car (exp), subst (cdr (exp), var, term, 'list)) else exp endif

else cons (subst (car (exp), var, term, t),

subst (cdr (exp), var, term, 'list)) endif

else exp endif

Definition: neg (exp1 , exp2 ) = ((exp1 = f-not (exp2 )) ∨ (exp2 = f-not (exp1 )))

Definition: conc (pf , flg) = if pf ≃ nil then nil elseif flg = t then caddr (pf ) else cons (conc (car (pf ), t), conc (cdr (pf ), 'list)) endif

Definition: subset (x, y) = if listp (x) then (car (x) ∈ y) ∧ subset (cdr (x), y)

else t endif

Definition: set-equal (x, y) = (subset (x, y) ∧ subset (y, x))

;The axioms: propositional, substitution, identity, equality for functions and predicates.

Definition: prop-axiom (exp) = f-or (f-not (exp), exp)

Definition: subst-axiom (exp, var, term) = f-implies (subst (exp, var, term, t), forsome (var, exp))

Definition: ident-axiom (var) = f-equal (var, var)

Definition: pairequals (vars1 , vars2 , exp) = if listp (vars1 )

then f-implies (f-equal (car (vars1 ), car (vars2 )),

pairequals (cdr (vars1 ), cdr (vars2 ), exp))

else exp endif

Definition: equal-axiom2 (vars1 , vars2 , pr) = pairequals (vars1 , vars2 , f-implies (cons (pr, vars1 ), cons (pr, vars2 )))

Definition: assume (exp, list, flg) = if listp (list)

then if (caaar (list) = flg) ∧ (exp = cadar (list)) then cdr (list) else assume (exp, cdr (list), flg) endif

else f endif

;Proof-constructors

Definition: prop-axiom-proof (exp) = list ('axiom, list ('prop-axiom, exp), prop-axiom (exp))

Definition: subst-axiom-proof (exp, var, term) = list ('axiom,

list ('subst-axiom, exp, var, term), subst-axiom (exp, var, term))

Definition: ident-axiom-proof (var) = list ('axiom, list ('ident-axiom, var), f-equal (var, var))

Definition: equal-axiom1 (vars1 , vars2 , fn) = pairequals (vars1 , vars2 , f-equal (cons (fn, vars1 ), cons (fn, vars2 )))

Definition: equal-axiom1-proof (fn, vars1 , vars2 ) = list ('axiom,

list ('equal-axiom1, fn, vars1 , vars2 ), equal-axiom1 (vars1 , vars2 , fn))

Definition: equal-axiom2-proof (pr, vars1 , vars2 ) = list ('axiom,

list ('equal-axiom2, pr, vars1 , vars2 ), equal-axiom2 (vars1 , vars2 , pr))

Definition: expan-proof (a, b, pf ) = list ('rule, list ('expan, a, b), f-or (a, b), pf )

Definition: contrac-proof (a, pf ) = list ('rule, list ('contrac, a), a, pf )

Definition: assoc-proof (a, b, c, pf ) = list ('rule, list ('assoc, a, b, c), f-or (f-or (a, b), c), pf )

Definition: cut-proof (a, b, c, pf1 , pf2 ) = list ('rule, list ('cut, a, b, c), f-or (b, c), list (pf1 , pf2 ))

Definition: forsome-intro-proof (var, a, b, pf ) = list ('rule, list ('e-intro, var, a, b), f-implies (forsome (var, a), b), pf )

Event: Disable atomp; name this event ‘g2737’.

Definition: hint1 (pf ) = caadr (pf )

Definition: hint2 (pf ) = cadadr (pf )

Definition: hint3 (pf ) = caddadr (pf )

Definition: hint4 (pf ) = cadddadr (pf )

Definition: sub-proof (pf ) = cadddr (pf )

;The proof-checker, PF is a proof.

Definition: prf (pf ) = if pf ≃ nil then f

elseif car (pf ) = 'axiom then if hint1 (pf ) = 'prop-axiom

then formula (hint2 (pf ), t, 0)

∧ (pf = prop-axiom-proof (hint2 (pf ))) elseif hint1 (pf ) = 'subst-axiom then formula (hint2 (pf ), t, 0)

∧ variable (hint3 (pf )) ∧ termp (hint4 (pf ), t, 0) ∧ free-for (hint2 (pf ), hint3 (pf ), hint4 (pf ), t) ∧ (pf = subst-axiom-proof (hint2 (pf ),

hint3 (pf ), hint4 (pf )))

elseif hint1 (pf ) = 'ident-axiom then variable (hint2 (pf ))

∧ (pf = ident-axiom-proof (hint2 (pf ))) elseif hint1 (pf ) = 'equal-axiom1 then function (hint2 (pf ))

∧ var-list (hint3 (pf ), degree (hint2 (pf ))) ∧ var-list (hint4 (pf ), degree (hint2 (pf ))) ∧ (pf = equal-axiom1-proof (hint2 (pf ),

hint3 (pf ), hint4 (pf )))

elseif hint1 (pf ) = 'equal-axiom2 then predicate (hint2 (pf ))

∧ var-list (hint3 (pf ), degree (hint2 (pf ))) ∧ var-list (hint4 (pf ), degree (hint2 (pf ))) ∧ (pf = equal-axiom2-proof (hint2 (pf ),

hint3 (pf ), hint4 (pf )))

else f endif elseif car (pf ) = 'rule then if hint1 (pf ) = 'expan

then formula (hint2 (pf ), t, 0)

∧ (pf = expan-proof (hint2 (pf ), hint3 (pf ), sub-proof (pf )))

∧ (conc (sub-proof (pf ), t) = hint3 (pf )) ∧ prf (sub-proof (pf ))

elseif hint1 (pf ) = 'contrac then (pf = contrac-proof (hint2 (pf ), sub-proof (pf )))

∧ (conc (sub-proof (pf ), t) = f-or (hint2 (pf ), hint2 (pf ))) ∧ prf (sub-proof (pf ))

elseif hint1 (pf ) = 'assoc then (pf = assoc-proof (hint2 (pf ),

hint3 (pf ), hint4 (pf ), sub-proof (pf )))

∧ (conc (sub-proof (pf ), t)

= f-or (hint2 (pf ), f-or (hint3 (pf ), hint4 (pf )))) ∧ prf (sub-proof (pf ))

elseif hint1 (pf ) = 'cut then (pf = cut-proof (hint2 (pf ),

hint3 (pf ), hint4 (pf ), car (sub-proof (pf )), cadr (sub-proof (pf ))))

∧ (conc (sub-proof (pf ), 'list)

= list (f-or (hint2 (pf ), hint3 (pf )),

f-or (f-not (hint2 (pf )), hint4 (pf ))))

∧ prf (car (sub-proof (pf ))) ∧ prf (cadr (sub-proof (pf )))

elseif hint1 (pf ) = 'e-intro then variable (hint2 (pf ))

∧ (pf = forsome-intro-proof (hint2 (pf ), hint3 (pf ), hint4 (pf ), sub-proof (pf )))

∧ (hint2 (pf ) ∉ collect-free (hint4 (pf ), t)) ∧ (conc (sub-proof (pf ), t)

= f-implies (hint3 (pf ), hint4 (pf ))) ∧ prf (sub-proof (pf ))

else f endif else f endif Theorem: formula-or-reduc formula (list ('or, a, b), t, 0) = (formula (a, t, 0) ∧ formula (b, t, 0))

Theorem: formula-not-reduc formula (list ('not, a), t, 0) = formula (a, t, 0)

Theorem: formula-forsome-reduc formula (list ('forsome, x, a), t, 0) = (variable (x) ∧ formula (a, t, 0))

;PF is a valid proof of EXP.

Definition: proves (pf , exp) = ((conc (pf , t) = exp) ∧ formula (exp, t, 0) ∧ prf (pf ))

Theorem: proves-is-formula proves (pf , exp) → formula (exp, t, 0)

Theorem: proves-is-formula-again (¬ formula (exp, t, 0)) → (¬ proves (pf , exp))

;Getting rid of PRF by lemmas.

Theorem: prop-axiom-proves (formula (exp, t, 0) ∧ (concl = f-or (f-not (exp), exp))) → proves (prop-axiom-proof (exp), concl)

Theorem: subst-axiom-proves (formula (concl, t, 0) ∧ variable (var) ∧ termp (term, t, 0) ∧ free-for (exp, var, term, t) ∧ (concl = subst-axiom (exp, var, term))) → proves (subst-axiom-proof (exp, var, term), concl)

Theorem: equal-axiom1-proves (function (fn) ∧ var-list (vars1 , degree (fn)) ∧ var-list (vars2 , degree (fn)) ∧ formula (concl, t, 0) ∧ (concl = equal-axiom1 (vars1 , vars2 , fn))) → proves (equal-axiom1-proof (fn, vars1 , vars2 ), concl)

Theorem: equal-axiom2-proves (predicate (pr) ∧ var-list (vars1 , degree (pr)) ∧ var-list (vars2 , degree (pr)) ∧ formula (concl, t, 0) ∧ (concl = equal-axiom2 (vars1 , vars2 , pr))) → proves (equal-axiom2-proof (pr, vars1 , vars2 ), concl)

Theorem: ident-axiom-proves (variable (var) ∧ (concl = ident-axiom (var)) ∧ formula (concl, t, 0)) → proves (ident-axiom-proof (var), concl)

Theorem: expan-proof-proves (formula (a, t, 0) ∧ proves (pf , b) ∧ (concl = f-or (a, b))) → proves (expan-proof (a, b, pf ), concl)

Theorem: contrac-proof-proves proves (pf , f-or (a, a)) → proves (contrac-proof (a, pf ), a)

Theorem: assoc-proof-proves (proves (pf , f-or (a, f-or (b, c))) ∧ (concl = f-or (f-or (a, b), c))) → proves (assoc-proof (a, b, c, pf ), concl)

Theorem: cut-proof-proves (proves (pf1 , f-or (a, b)) ∧ proves (pf2 , f-or (f-not (a), c)) ∧ (concl = f-or (b, c))) → proves (cut-proof (a, b, c, pf1 , pf2 ), concl)

;disabling the proof-constructors since the lemmas above show they work.

Event: Enable prop-axiom-proof; name this event ‘g2752’.

Event: Enable subst-axiom-proof; name this event ‘g2753’.

Event: Enable equal-axiom1-proof; name this event ‘g2754’.

Event: Enable equal-axiom2-proof; name this event ‘g2755’.

Event: Enable ident-axiom-proof; name this event ‘g2756’.

Event: Enable expan-proof; name this event ‘g2759’.

Event: Enable contrac-proof; name this event ‘g2760’.

Event: Enable assoc-proof; name this event ‘g2761’.

Event: Enable cut-proof; name this event ‘g2762’.

Theorem: forsome-intro-proves (proves (pf , f-implies (a, b)) ∧ (var ∉ collect-free (b, t)) ∧ variable (var) ∧ (a-prime = f-implies (forsome (var, a), b))) → proves (forsome-intro-proof (var, a, b, pf ), a-prime)

Event: Enable forsome-intro-proof; name this event ‘g2763’.

Event: Enable prf; name this event ‘g2764’.

Event: Enable proves; name this event ‘g2765’.

Definition: commut-proof (a, b, pf ) = cut-proof (a, b, a, pf , prop-axiom-proof (a))

;The first derived inference rule - commutativity of disjunction.

Theorem: commut-proof-proves (proves (pf , f-or (a, b)) ∧ formula (f-or (a, b), t, 0) ∧ (concl = f-or (b, a))) → proves (commut-proof (a, b, pf ), concl)

Event: Enable commut-proof; name this event ‘g2766’.

;Modus Ponens.

Definition: detach-proof (a, b, pf1 , pf2 ) = contrac-proof (b,

cut-proof (a, b, b, commut-proof (b, a, expan-proof (b, a, pf1 )), pf2 ))

Theorem: detach-proof-proves1 (proves (pf1 , a) ∧ proves (pf2 , f-implies (a, b)) ∧ formula (b, t, 0)) → proves (detach-proof (a, b, pf1 , pf2 ), b)

Event: Enable detach-proof; name this event ‘g2767’.

Definition: proves-list (pflist, explist)

= if explist ≃ nil then pflist = nil

else proves (car (pflist), car (explist))

∧ proves-list (cdr (pflist), cdr (explist)) endif

Definition: list-implies (list, conc) = if list ≃ nil then conc

elseif cdr (list) ≃ nil then f-implies (car (list), conc)

else f-implies (car (list), list-implies (cdr (list), conc)) endif

Definition: list-detach-proof (alist, b, pflist, pf2 ) = if alist ≃ nil then pf2

elseif cdr (alist) ≃ nil then detach-proof (car (alist), b, car (pflist), pf2 ) else list-detach-proof (cdr (alist),

b,

cdr (pflist),

detach-proof (car (alist), list-implies (cdr (alist), b), car (pflist), pf2 )) endif

;Chained Modus Ponens.

Theorem: detach-list-implies (list (c) ∧ proves (pf , a) ∧ proves (pf2 , list-implies (cons (a, c), b)) ∧ formula (a, t, 0) ∧ formula (list-implies (c, b), t, 0)) → proves (detach-proof (a, list-implies (c, b), pf , pf2 ), list-implies (c, b))

Theorem: formula-list-implies (formula (list-implies (alist, b), t, 0) ∧ listp (alist)) → formula (list-implies (cdr (alist), b), t, 0)

Theorem: detach-rule-corr (proves-list (pflist, alist) ∧ proves (pf2 , list-implies (alist, b)) ∧ formula (b, t, 0)) → proves (list-detach-proof (alist, b, pflist, pf2 ), b)

Event: Enable list-detach-proof; name this event ‘g0220’.

Event: Enable detach-list-implies; name this event ‘g0221’.

Definition: rt-expan-proof (a, b, pf ) = commut-proof (b, a, expan-proof (b, a, pf ))

Theorem: rt-expan-proof-proves (proves (pf , a) ∧ formula (b, t, 0) ∧ (concl = f-or (a, b))) → proves (rt-expan-proof (a, b, pf ), concl)

Event: Enable rt-expan-proof; name this event ‘g0227’.

;Takes list of formulas and returns disjunction.

Definition: make-disjunct (flist) = if flist ≃ nil then nil

elseif cdr (flist) ≃ nil then car (flist)

else f-or (car (flist), make-disjunct (cdr (flist))) endif

Definition: m1-proof (exp, flist, pf ) = if flist ≃ nil then nil

elseif cdr (flist) ≃ nil then pf

elseif exp = car (flist)

then rt-expan-proof (car (flist), make-disjunct (cdr (flist)), pf )

else expan-proof (car (flist), make-disjunct (cdr (flist)), m1-proof (exp, cdr (flist), pf )) endif

Theorem: m1-proof-proves1 (formula (make-disjunct (flist), t, 0) ∧ (exp ∈ flist) ∧ proves (pf , exp)) → proves (m1-proof (exp, flist, pf ), make-disjunct (flist))

Event: Enable m1-proof; name this event ‘g0228’.

Definition: rt-assoc-proof (a, b, c, pf ) = commut-proof (f-or (b, c),

a,

assoc-proof (b, c, a, commut-proof (f-or (c, a),

b,

assoc-proof (c, a, b, commut-proof (f-or (a,

b), c, pf )))))

Theorem: rt-assoc-proof-proves (proves (pf , f-or (f-or (a, b), c)) ∧ formula (a, t, 0) ∧ formula (b, t, 0) ∧ formula (c, t, 0) ∧ (concl = f-or (a, f-or (b, c)))) → proves (rt-assoc-proof (a, b, c, pf ), concl)

Event: Enable rt-assoc-proof; name this event ‘g0231’.

Definition: insert-proof (a, b, c, pf ) = commut-proof (f-or (a, c),

b,

assoc-proof (a, c, b, expan-proof (a, f-or (c, b), commut-proof (b, c, pf ))))

Theorem: insert-proof-proves (proves (pf , f-or (b, c)) ∧ formula (a, t, 0) ∧ formula (b, t, 0) ∧ formula (c, t, 0) ∧ (concl = f-or (b, f-or (a, c)))) → proves (insert-proof (a, b, c, pf ), concl)

Event: Enable insert-proof; name this event ‘g0232’.

Definition: m2-proof-step (exp1 , exp2 , flist, pf ) = if flist ≃ nil then nil

elseif cdr (flist) ≃ nil

then if exp2 = car (flist) then pf

else nil endif elseif exp2 = car (flist) then rt-assoc-proof (exp1 ,

exp2 , make-disjunct (cdr (flist)), rt-expan-proof (f-or (exp1 , exp2 ),

make-disjunct (cdr (flist)), pf ))

else insert-proof (car (flist), exp1 , make-disjunct (cdr (flist)), m2-proof-step (exp1 , exp2 , cdr (flist), pf )) endif

Theorem: m2-proof-step-proves (formula (make-disjunct (flist), t, 0) ∧ (exp2 ∈ flist) ∧ formula (exp1 , t, 0) ∧ formula (exp2 , t, 0) ∧ proves (pf , f-or (exp1 , exp2 ))) → proves (m2-proof-step (exp1 , exp2 , flist, pf ),

f-or (exp1 , make-disjunct (flist)))

Theorem: m2-proof-step-proves1 (formula (make-disjunct (flist), t, 0) ∧ (exp2 ∈ flist) ∧ formula (exp1 , t, 0) ∧ formula (exp2 , t, 0) ∧ proves (pf , f-or (exp1 , exp2 )) ∧ (concl = f-or (exp1 , make-disjunct (flist)))) → proves (m2-proof-step (exp1 , exp2 , flist, pf ), concl)

Event: Enable m2-proof-step; name this event ‘g0233’.

Event: Enable m2-proof-step-proves; name this event ‘g0234’.

Definition: m2-proof (exp1 , exp2 , flist, pf ) = if flist ≃ nil then nil

elseif exp1 = exp2 then m1-proof (exp1 , flist, contrac-proof (exp1 , pf )) elseif exp1 = car (flist) then m2-proof-step (exp1 , exp2 , cdr (flist), pf ) elseif exp2 = car (flist) then m2-proof-step (exp2 , exp1 , cdr (flist), commut-proof (exp1 , exp2 , pf )) else expan-proof (car (flist),

make-disjunct (cdr (flist)),

m2-proof (exp1 , exp2 , cdr (flist), pf )) endif

Theorem: m1-proof-proves (formula (make-disjunct (flist), t, 0) ∧ (exp ∈ flist) ∧ proves (pf , exp) ∧ (concl = make-disjunct (flist))) → proves (m1-proof (exp, flist, pf ), concl)

Theorem: m2-proof-proves (formula (make-disjunct (flist), t, 0) ∧ formula (exp1 , t, 0) ∧ formula (exp2 , t, 0) ∧ (exp1 ∈ flist) ∧ (exp2 ∈ flist) ∧ proves (pf , f-or (exp1 , exp2 ))) → proves (m2-proof (exp1 , exp2 , flist, pf ), make-disjunct (flist))

Theorem: m2-proof-proves1 (formula (make-disjunct (flist), t, 0) ∧ formula (exp1 , t, 0) ∧ formula (exp2 , t, 0) ∧ (exp1 ∈ flist) ∧ (exp2 ∈ flist) ∧ proves (pf , f-or (exp1 , exp2 )) ∧ (concl = make-disjunct (flist))) → proves (m2-proof (exp1 , exp2 , flist, pf ), concl)

Event: Enable m2-proof; name this event ‘g0235’.

Event: Enable m2-proof-proves; name this event ‘g0236’.

Definition: m3-proof (exp1 , exp2 , flist2 , pf ) = contrac-proof (make-disjunct (flist2 ),

contrac-proof (f-or (make-disjunct (flist2 ),

make-disjunct (flist2 )), m2-proof (f-or (make-disjunct (flist2 ),

make-disjunct (flist2 )), exp1 , cons (f-or (make-disjunct (flist2 ),

make-disjunct (flist2 )), cons (make-disjunct (flist2 ),

flist2 )), assoc-proof (make-disjunct (flist2 ),

make-disjunct (flist2 ), exp1 , commut-proof (f-or (make-disjunct (flist2 ), exp1 ),

make-disjunct (flist2 ),

m2-proof (f-or (make-disjunct (flist2 ), exp1 ),

exp2 ,

cons (f-or (make-disjunct (flist2 ), exp1 ),

flist2 ), assoc-proof (make-disjunct (flist2 ), exp1 , exp2 , commut-proof (f-or (exp1 ,

exp2 ), make-disjunct (flist2 ), pf ))))))))

Definition: m-proof (flist1 , flist2 , pf ) = if flist1 ≃ nil then nil

elseif cdr (flist1 ) ≃ nil then m1-proof (car (flist1 ), flist2 , pf ) elseif cddr (flist1 ) ≃ nil then m2-proof (car (flist1 ), cadr (flist1 ), flist2 , pf ) else m3-proof (car (flist1 ),

cadr (flist1 ),

flist2 ,

m-proof (cons (f-or (car (flist1 ), cadr (flist1 )), cddr (flist1 )),

cons (f-or (car (flist1 ), cadr (flist1 )),

flist2 ), assoc-proof (car (flist1 ),

cadr (flist1 ),

make-disjunct (cddr (flist1 )), pf ))) endif

Theorem: subset-cons subset (x, y) → subset (x, cons (z, y))

Definition: form-list (flist) = if listp (flist)

then formula (car (flist), t, 0) ∧ form-list (cdr (flist))

else t endif

Theorem: formlist-formula-make-disj (form-list (flist) ∧ listp (flist)) → formula (make-disjunct (flist), t, 0)

Theorem: m3-proof-proves (formula (exp1 , t, 0) ∧ formula (exp2 , t, 0) ∧ form-list (flist2 ) ∧ proves (pf , make-disjunct (cons (f-or (exp1 , exp2 ), flist2 ))) ∧ (exp1 ∈ flist2 ) ∧ (exp2 ∈ flist2 )) → proves (m3-proof (exp1 , exp2 , flist2 , pf ), make-disjunct (flist2 ))

Event: Enable m3-proof; name this event ‘g0222’.

Theorem: m3-proof-proves1 (formula (exp1 , t, 0) ∧ formula (exp2 , t, 0) ∧ form-list (flist2 ) ∧ proves (pf , make-disjunct (cons (f-or (exp1 , exp2 ), flist2 ))) ∧ (exp1 ∈ flist2 ) ∧ (exp2 ∈ flist2 ) ∧ (concl = make-disjunct (flist2 ))) → proves (m3-proof (exp1 , exp2 , flist2 , pf ), concl)

Event: Enable m3-proof-proves; name this event ‘g0229’.

;The subset lemma

Theorem: m-proof-proves (form-list (flist1 ) ∧ listp (flist1 ) ∧ form-list (flist2 ) ∧ listp (flist2 ) ∧ subset (flist1 , flist2 ) ∧ proves (pf , make-disjunct (flist1 ))) → proves (m-proof (flist1 , flist2 , pf ), make-disjunct (flist2 ))

Event: Enable m-proof; name this event ‘g0247’.

Theorem: m-proof-proves1 (form-list (flist1 ) ∧ form-list (flist2 ) ∧ subset (flist1 , flist2 ) ∧ proves (pf , make-disjunct (flist1 )) ∧ (concl = make-disjunct (flist2 ))) → proves (m-proof (flist1 , flist2 , pf ), concl)

;Disjunctions.

Definition: or-type (exp) = (exp = f-or (cadr (exp), caddr (exp)))

;Negation of disjunctions.

Definition: nor-type (exp) = (exp = f-not (f-or (cadadr (exp), caddadr (exp)))) Event: Enable atomp; name this event ‘g0250’.

;Elementary and negation of elementary formulas

Definition: elem-form (exp) = (atomp (exp) ∨ (exp = forsome (cadr (exp), caddr (exp)))) Definition: neg-elem-form (exp) = ((exp = f-not (cadr (exp))) ∧ elem-form (arg1 (exp))) Definition: prop-atomp (exp) = (elem-form (exp) ∨ neg-elem-form (exp))

;Double-negations

Definition: dble-neg-type (exp) = (exp = f-not (f-not (cadadr (exp)))) Event: Disable atomp; name this event ‘g0251’.

Theorem: dble-neg-not-prop-atomp dble-neg-type (exp) → (¬ prop-atomp (exp)) Theorem: or-type-not-prop-atomp or-type (exp) → (¬ prop-atomp (exp)) Theorem: nor-type-not-prop-atomp nor-type (exp) → (¬ prop-atomp (exp)) Definition: list-count (list) = if list ≃ nil then 0

else (1 + count (car (list))) + list-count (cdr (list)) endif Definition: neg-list (exp, list) = if list ≃ nil then f

else neg (exp, car (list)) ∨ neg-list (exp, cdr (list)) endif

Theorem: lessp-list-count listp (flist) → (list-count (cdr (flist)) < list-count (flist))

Theorem: or-type-list-count (or-type (car (flist)) ∧ listp (flist)) → (list-count (cons (cadar (flist), cons (caddar (flist), cdr (flist))))

< list-count (flist))

Theorem: nor-type-list-count1 (listp (flist) ∧ nor-type (car (flist))) → (list-count (cons (list ('not, cadadar (flist)), cdr (flist)))

< list-count (flist))

Theorem: nor-type-list-count2 (listp (flist) ∧ nor-type (car (flist))) → (list-count (cons (list ('not, caddadar (flist)), cdr (flist)))

< list-count (flist))

Theorem: dble-neg-list-count (listp (flist) ∧ dble-neg-type (car (flist))) → (list-count (cons (cadadar (flist), cdr (flist))) < list-count (flist))

Event: Enable prop-atomp; name this event ‘g0230’.

Event: Enable or-type; name this event ‘g0237’.

Event: Enable nor-type; name this event ‘g0238’.

Event: Enable dble-neg-type; name this event ‘g0239’.

Event: Enable list-count; name this event ‘g0240’.

;The tautology-checker.

Definition: tautologyp1 (flist, auxlist) = if flist ≃ nil then f

elseif prop-atomp (car (flist)) then neg-list (car (flist), auxlist)

∨ tautologyp1 (cdr (flist), cons (car (flist), auxlist)) elseif or-type (car (flist)) then tautologyp1 (cons (arg1 (car (flist)),

cons (arg2 (car (flist)), cdr (flist))), auxlist)

elseif nor-type (car (flist)) then tautologyp1 (cons (f-not (arg1 (arg1 (car (flist)))), cdr (flist)),

auxlist)

∧ tautologyp1 (cons (f-not (arg2 (arg1 (car (flist)))), cdr (flist)),

auxlist)

elseif dble-neg-type (car (flist)) then tautologyp1 (cons (arg1 (arg1 (car (flist))), cdr (flist)), auxlist) else f endif

Theorem: form-list-append (form-list (x) ∧ form-list (y)) → form-list (append (x, y))

Definition: neg-proof (exp1 , exp2 ) = if exp1 = f-not (exp2 ) then prop-axiom-proof (exp2 )

else commut-proof (exp2 , exp1 , prop-axiom-proof (exp1 )) endif

Theorem: neg-proof-proves (formula (exp1 , t, 0) ∧ formula (exp2 , t, 0) ∧ neg (exp1 , exp2 ) ∧ (concl = f-or (exp1 , exp2 ))) → proves (neg-proof (exp1 , exp2 ), concl)

Event: Enable neg-proof; name this event ‘g0245’.

Theorem: neg-list-reduc neg-list (exp, flist) = ((f-not (exp) ∈ flist)

∨ ((exp = f-not (cadr (exp))) ∧ (cadr (exp) ∈ flist)))

Definition: neg-list-proof (exp, flist) = if f-not (exp) ∈ flist

then m2-proof (exp, f-not (exp), cons (exp, flist), neg-proof (exp, f-not (exp))) else m2-proof (exp,

cadr (exp), cons (exp, flist), neg-proof (exp, cadr (exp))) endif

Theorem: neg-list-proof-proves (formula (exp, t, 0) ∧ form-list (flist) ∧ neg-list (exp, flist) ∧ (concl = make-disjunct (cons (exp, flist)))) → proves (neg-list-proof (exp, flist), concl)

Event: Enable neg-list-proof; name this event ‘g0256’.

Theorem: subset-ident subset (x, x)

Theorem: subset-car subset (x, cons (y, x))

Theorem: subset-append subset (cons (exp, list2 ), append (cons (exp, list1 ), list2 ))

Theorem: nlistp-neg-list (list ≃ nil) → (¬ neg-list (exp, list))

Definition: prop-atom-proof1 (flist1 , flist2 ) = m-proof (cons (car (flist1 ), flist2 ),

append (flist1 , flist2 ),

neg-list-proof (car (flist1 ), flist2 ))

Theorem: prop-atom-proof1-proves (form-list (flist1 ) ∧ listp (flist1 ) ∧ form-list (flist2 ) ∧ neg-list (car (flist1 ), flist2 ) ∧ (concl = make-disjunct (append (flist1 , flist2 )))) → proves (prop-atom-proof1 (flist1 , flist2 ), concl)

Event: Enable prop-atom-proof1; name this event ‘g0259’.

Theorem: subset-append-car subset (append (list1 , cons (exp, list2 )), append (cons (exp, list1 ), list2 ))

Theorem: form-list-append-car (form-list (cons (exp, list1 )) ∧ form-list (list2 )) → form-list (append (list1 , cons (exp, list2 )))

Definition: prop-atom-proof2 (flist1 , flist2 , pf ) = m-proof (append (cdr (flist1 ), cons (car (flist1 ), flist2 )),

append (flist1 , flist2 ), pf )

Theorem: prop-atom-proof2-proves (form-list (flist1 ) ∧ listp (flist1 ) ∧ form-list (flist2 ) ∧ proves (pf ,

make-disjunct (append (cdr (flist1 ), cons (car (flist1 ), flist2 ))))

∧ (concl = make-disjunct (append (flist1 , flist2 )))) → proves (prop-atom-proof2 (flist1 , flist2 , pf ), concl)

Event: Enable prop-atom-proof2; name this event ‘g0258’.

Definition: cancel-proof (a, b, pf1 , pf2 ) = contrac-proof (b, cut-proof (a, b, b, pf2 , rt-expan-proof (f-not (a), b, pf1 )))

Theorem: cancel-proof-proves (proves (pf1 , f-not (a)) ∧ proves (pf2 , f-or (a, b)) ∧ formula (a, t, 0) ∧ formula (b, t, 0)) → proves (cancel-proof (a, b, pf1 , pf2 ), b)

Event: Enable cancel-proof; name this event ‘g0255’.

Definition: nlistp-nor-type-proof (a, b, pf1 , pf2 ) = cancel-proof (b,

f-not (f-or (a, b)), pf2 , cancel-proof (a,

f-or (b, f-not (f-or (a, b))),

pf1 ,

m-proof (list (f-not (f-or (a, b)), a, b), list (a, b, f-not (f-or (a, b))), prop-axiom-proof (f-or (a, b)))))

Theorem: nlistp-nor-type-proof-proves (formula (a, t, 0) ∧ formula (b, t, 0) ∧ proves (pf1 , f-not (a)) ∧ proves (pf2 , f-not (b)) ∧ (concl = f-not (f-or (a, b)))) → proves (nlistp-nor-type-proof (a, b, pf1 , pf2 ), concl)

Definition: listp-nor-type-proof (a, b, c, pf1 , pf2 ) = m-proof (list (f-not (f-or (a, b)), c, c),

list (f-not (f-or (a, b)), c),

rt-assoc-proof (f-not (f-or (a, b)), c, c, cut-proof (b,

f-or (f-not (f-or (a, b)), c), c, rt-assoc-proof (b,

f-not (f-or (a, b)), c, cut-proof (a,

f-or (b,

f-not (f-or (a,

b))),

c,

m-proof (list (f-not (f-or (a,

b)),

a, b), list (a, b, f-not (f-or (a,

b))),

prop-axiom-proof (f-or (a,

b))),

pf1 )),

pf2 )))

Theorem: listp-nor-type-proof-proves (formula (a, t, 0) ∧ formula (b, t, 0) ∧ formula (c, t, 0) ∧ proves (pf1 , f-or (f-not (a), c))

∧ proves (pf2 , f-or (f-not (b), c)) ∧ (concl = f-or (f-not (f-or (a, b)), c))) → proves (listp-nor-type-proof (a, b, c, pf1 , pf2 ), concl)

Event: Enable m-proof-proves; name this event ‘g0242’.

Event: Enable nlistp-nor-type-proof; name this event ‘g0243’.

Event: Enable listp-nor-type-proof; name this event ‘g0244’.

Definition: nor-type-proof (a, b, clist, pf1 , pf2 ) = if clist ≃ nil then nlistp-nor-type-proof (a, b, pf1 , pf2 )

else listp-nor-type-proof (a, b, make-disjunct (clist), pf1 , pf2 ) endif

Event: Disable nor-type; name this event ‘g0292’.

Theorem: nor-type-proof-proves (nor-type (exp) ∧ formula (exp, t, 0) ∧ form-list (clist) ∧ proves (pf1 , make-disjunct (cons (f-not (cadadr (exp)), clist))) ∧ proves (pf2 , make-disjunct (cons (f-not (caddadr (exp)), clist))) ∧ (concl = make-disjunct (cons (exp, clist)))) → proves (nor-type-proof (cadadr (exp), caddadr (exp), clist, pf1 , pf2 ), concl)

Definition: nlistp-dble-neg-proof (a, pf ) = contrac-proof (f-not (f-not (a)),

cut-proof (a, f-not (f-not (a)), f-not (f-not (a)), rt-expan-proof (a, f-not (f-not (a)), pf ), commut-proof (f-not (f-not (a)),

f-not (a),

prop-axiom-proof (f-not (a)))))

Event: Enable nor-type-proof; name this event ‘g0248’.

Theorem: nlistp-dble-neg-proof-proves (formula (a, t, 0) ∧ proves (pf , a) ∧ (concl = f-not (f-not (a)))) → proves (nlistp-dble-neg-proof (a, pf ), concl)

Event: Enable nlistp-dble-neg-proof; name this event ‘g0249’.

Definition: listp-dble-neg-proof (a, c, pf ) = commut-proof (c,

f-not (f-not (a)), cut-proof (a,

c,

f-not (f-not (a)),

pf ,

commut-proof (f-not (f-not (a)), f-not (a), prop-axiom-proof (f-not (a)))))

Theorem: listp-dble-neg-proof-proves (formula (a, t, 0) ∧ formula (c, t, 0) ∧ proves (pf , f-or (a, c)) ∧ (concl = f-or (f-not (f-not (a)), c))) → proves (listp-dble-neg-proof (a, c, pf ), concl)

Event: Enable listp-dble-neg-proof; name this event ‘g0203’.

Definition: dble-neg-type-proof (a, clist, pf ) = if clist ≃ nil then nlistp-dble-neg-proof (a, pf )

else listp-dble-neg-proof (a, make-disjunct (clist), pf ) endif

Event: Disable dble-neg-type; name this event ‘g0252’.

Theorem: dble-neg-type-proof-proves (dble-neg-type (exp) ∧ formula (exp, t, 0) ∧ form-list (clist) ∧ proves (pf , make-disjunct (cons (cadadr (exp), clist))) ∧ (concl = make-disjunct (cons (exp, clist)))) → proves (dble-neg-type-proof (cadadr (exp), clist, pf ), concl)

Definition: or-type-proof (a, b, clist, pf ) = if clist ≃ nil then pf

else assoc-proof (a, b, make-disjunct (clist), pf ) endif

Event: Disable or-type; name this event ‘g0260’.

Theorem: or-type-proof-proves (or-type (car (flist1 )) ∧ form-list (flist1 ) ∧ listp (flist1 ) ∧ form-list (flist2 ) ∧ proves (pf ,

make-disjunct (append (cons (cadar (flist1 ),

cons (caddar (flist1 ), cdr (flist1 ))), flist2 )))

∧ (concl = make-disjunct (append (flist1 , flist2 )))) → proves (or-type-proof (cadar (flist1 ),

caddar (flist1 ),

append (cdr (flist1 ), flist2 ), pf ),

concl)

Event: Enable or-type-proof; name this event ‘g0271’.

Theorem: or-type-form-list (or-type (car (flist)) ∧ form-list (flist) ∧ listp (flist)) → form-list (cons (cadar (flist), cons (caddar (flist), cdr (flist))))

Theorem: nor-type-form-list (nor-type (car (flist)) ∧ form-list (flist) ∧ listp (flist)) → form-list (cons (list ('not, cadadar (flist)), cdr (flist)))

Theorem: nor-type-form-list2 (nor-type (car (flist)) ∧ form-list (flist) ∧ listp (flist)) → form-list (cons (list ('not, caddadar (flist)), cdr (flist)))

Theorem: dble-neg-type-form-list (dble-neg-type (car (flist)) ∧ form-list (flist) ∧ listp (flist)) → form-list (cons (cadadar (flist), cdr (flist)))

Event: Enable or-type; name this event ‘g0272’.

Event: Enable nor-type; name this event ‘g0273’.

Event: Enable dble-neg-type; name this event ‘g0274’.

Event: Enable dble-neg-type-proof; name this event ‘g0254’.

;The proof-constructor for tautologies.

Definition: taut-proof1 (flist, auxlist) = if flist ≃ nil then nil

elseif prop-atomp (car (flist)) then if neg-list (car (flist), auxlist)

then prop-atom-proof1 (flist, auxlist) else prop-atom-proof2 (flist,

auxlist,

taut-proof1 (cdr (flist),

cons (car (flist), auxlist))) endif

elseif or-type (car (flist)) then or-type-proof (arg1 (car (flist)),

arg2 (car (flist)),

append (cdr (flist), auxlist),

taut-proof1 (cons (arg1 (car (flist)),

cons (arg2 (car (flist)), cdr (flist))), auxlist))

elseif nor-type (car (flist)) then nor-type-proof (arg1 (arg1 (car (flist))),

arg2 (arg1 (car (flist))), append (cdr (flist), auxlist), taut-proof1 (cons (f-not (arg1 (arg1 (car (flist)))), cdr (flist)),

auxlist),

taut-proof1 (cons (f-not (arg2 (arg1 (car (flist)))), cdr (flist)),

auxlist))

elseif dble-neg-type (car (flist)) then dble-neg-type-proof (arg1 (arg1 (car (flist))),

append (cdr (flist), auxlist),

taut-proof1 (cons (arg1 (arg1 (car (flist))),

cdr (flist)), auxlist))

else nil endif

;Every tautology has a proof (when AUXLIST is NIL)

Theorem: taut-thm1 (form-list (flist) ∧ form-list (auxlist) ∧ tautologyp1 (flist, auxlist)) → proves (taut-proof1 (flist, auxlist),

make-disjunct (append (flist, auxlist)))

Event: Enable taut-proof1; name this event ‘g0275’.

Theorem: taut-thm2 (form-list (flist) ∧ form-list (auxlist) ∧ tautologyp1 (flist, auxlist) ∧ (concl = make-disjunct (append (flist, auxlist)))) → proves (taut-proof1 (flist, auxlist), concl)

Theorem: listp-elem-form (exp ≃ nil) → (¬ elem-form (exp))

;Truth value evaluator.

Definition: eval (exp, alist) = if exp ≃ nil then f

elseif elem-form (exp) then exp ∈ alist

elseif car (exp) = 'not then ¬ eval (cadr (exp), alist)

elseif car (exp) = 'or

then eval (cadr (exp), alist) ∨ eval (caddr (exp), alist)

else f endif

Theorem: elem-form-eval elem-form (exp) → (eval (exp, alist) = (exp ∈ alist))

Theorem: nlistp-eval (exp ≃ nil) → (¬ eval (exp, alist))

Theorem: not-eval (listp (exp) ∧ (car (exp) = 'not)) → (eval (exp, alist) = (¬ eval (cadr (exp), alist)))

Theorem: or-eval (listp (exp) ∧ (car (exp) = 'or)) → (eval (exp, alist)

= (eval (cadr (exp), alist) ∨ eval (caddr (exp), alist)))

Theorem: member-eval ((exp ∈ flist) ∧ eval (exp, alist)) → eval (make-disjunct (flist), alist)

Theorem: eval-elem-form (elem-form (exp) ∧ (exp ∈ list) ∧ (exp ∈ alist) ∧ (concl = make-disjunct (list))) → eval (concl, alist)

Event: Disable or-type; name this event ‘g0278’.

Event: Disable nor-type; name this event ‘g0279’.

Event: Disable dble-neg-type; name this event ‘g0280’.

Event: Disable prop-atomp; name this event ‘g0281’.

Theorem: member-append (exp ∈ append (flist1 , flist2 )) = ((exp ∈ flist1 ) ∨ (exp ∈ flist2 ))

Theorem: eval-neg-elem-form ((exp ∈ list) ∧ (f-not (exp) ∈ list) ∧ (concl = make-disjunct (list))) → eval (concl, alist)

Theorem: eval-make-disjunct eval (make-disjunct (append (list1 , list2 )), alist) = (eval (make-disjunct (list1 ), alist)

∨ eval (make-disjunct (list2 ), alist))

Theorem: neg-list-eval (listp (flist1 ) ∧ neg-list (car (flist1 ), flist2 ) ∧ (concl = make-disjunct (append (flist1 , flist2 )))) → eval (concl, alist)

Theorem: eval-prop-atomp (listp (flist1 ) ∧ eval (make-disjunct (append (cdr (flist1 ), cons (car (flist1 ), flist2 ))),

alist))

→ eval (make-disjunct (append (flist1 , flist2 )), alist)

Event: Enable eval; name this event ‘g1253’.

Theorem: eval-or-type (listp (flist1 ) ∧ or-type (car (flist1 ))) → (eval (make-disjunct (append (flist1 , flist2 )), alist)

= eval (make-disjunct (append (cons (cadar (flist1 ),

cons (caddar (flist1 ), cdr (flist1 ))),

flist2 )),

alist))

Theorem: eval-nor-type (listp (flist1 ) ∧ nor-type (car (flist1 ))) → (eval (make-disjunct (append (flist1 , flist2 )), alist)

= (eval (make-disjunct (append (cons (f-not (cadadar (flist1 )),

cdr (flist1 )), flist2 )),

alist) ∧ eval (make-disjunct (append (cons (f-not (caddadar (flist1 )),

cdr (flist1 )), flist2 )),

alist)))

Theorem: eval-dble-neg-type (listp (flist1 ) ∧ dble-neg-type (car (flist1 ))) → (eval (make-disjunct (append (flist1 , flist2 )), alist)

= eval (make-disjunct (append (cons (cadadar (flist1 ), cdr (flist1 )),

flist2 )),

alist))

;All tautologies are logically-true.

Theorem: taut-eval tautologyp1 (flist, auxlist) → eval (make-disjunct (append (flist, auxlist)), alist)

Theorem: not-eval-prop-atomp (listp (flist1 ) ∧ (¬ eval (make-disjunct (append (cdr (flist1 ), cons (car (flist1 ), flist2 ))),

alist)))

→ (¬ eval (make-disjunct (append (flist1 , flist2 )), alist))

Theorem: prop-atomp-reduc prop-atomp (exp) = (elem-form (exp)

∨ ((exp = f-not (cadr (exp))) ∧ elem-form (cadr (exp))))

Event: Enable elem-form; name this event ‘g0263’.

Event: Enable prop-atomp; name this event ‘g0264’.

Definition: prop-atomp-list (list) = if list ≃ nil then t

else prop-atomp (car (list)) ∧ prop-atomp-list (cdr (list)) endif Definition: falsify (list) = if list ≃ nil then nil

elseif car (list) = f-not (cadar (list)) then cons (cadar (list), falsify (cdr (list))) else falsify (cdr (list)) endif

Theorem: falsify-step (f-not (exp) ∉ auxlist) → (exp ∉ falsify (auxlist))

Theorem: prop-atomp-auxlist (prop-atomp (exp) ∧ (¬ neg-list (exp, auxlist)) ∧ prop-atomp-list (auxlist)) → (¬ eval (exp, falsify (cons (exp, auxlist))))

Theorem: prop-atomp-auxlist2 ((¬ neg-list (exp, auxlist)) ∧ prop-atomp-list (auxlist) ∧ prop-atomp (exp) ∧ (¬ eval (make-disjunct (auxlist), falsify (alist)))) → (¬ eval (make-disjunct (auxlist), falsify (cons (exp, alist))))

Theorem: prop-atomp-falsify (prop-atomp (exp) ∧ (¬ neg-list (exp, auxlist)) ∧ prop-atomp-list (auxlist) ∧ (¬ eval (make-disjunct (auxlist), falsify (auxlist)))) → (¬ eval (make-disjunct (cons (exp, auxlist)), falsify (cons (exp, auxlist))))

Event: Disable prop-atomp; name this event ‘g0268’.

Event: Disable elem-form; name this event ‘g0269’.

Event: Enable atomp; name this event ‘g0204’.

Theorem: formula-cases1 formula (exp, t, 0) → (prop-atomp (exp)

∨ or-type (exp) ∨ nor-type (exp) ∨ dble-neg-type (exp))

Event: Disable atomp; name this event ‘g0205’.

Event: Enable prop-atomp; name this event ‘g0296’.

Event: Enable or-type; name this event ‘g0297’.

Event: Enable nor-type; name this event ‘g0298’.

Event: Enable dble-neg-type; name this event ‘g0299’.

Theorem: formula-cases ((¬ dble-neg-type (exp)) ∧ (¬ nor-type (exp)) ∧ (¬ or-type (exp)) ∧ (¬ prop-atomp (exp))) → (¬ formula (exp, t, 0))

Definition: falsify-taut (flist, auxlist) = if flist ≃ nil then falsify (auxlist)

elseif prop-atomp (car (flist))

then if neg-list (car (flist), auxlist) then f

else falsify-taut (cdr (flist), cons (car (flist), auxlist)) endif elseif or-type (car (flist)) then falsify-taut (cons (cadar (flist), cons (caddar (flist), cdr (flist))),

auxlist)

elseif nor-type (car (flist))

then if falsify-taut (cons (f-not (caddadar (flist)), cdr (flist)), auxlist) then falsify-taut (cons (f-not (caddadar (flist)), cdr (flist)),

auxlist)

else falsify-taut (cons (f-not (cadadar (flist)), cdr (flist)),

auxlist) endif

elseif dble-neg-type (car (flist))

then falsify-taut (cons (cadadar (flist), cdr (flist)), auxlist)

else nil endif

Theorem: append-nlistp (x ≃ nil) → (append (x, y) = y)

Theorem: not-falsify-taut tautologyp1 (flist, auxlist) = (¬ falsify-taut (flist, auxlist))

;Non-tautologies are falsifiable.

Theorem: not-taut-false (form-list (flist) ∧ prop-atomp-list (auxlist) ∧ (¬ eval (make-disjunct (auxlist), falsify (auxlist))) ∧ (¬ tautologyp1 (flist, auxlist))) → (¬ eval (make-disjunct (append (flist, auxlist)),

falsify-taut (flist, auxlist)))

Definition: tautologyp (flist) = tautologyp1 (flist, nil)

Definition: taut-proof (flist) = taut-proof1 (flist, nil)

Event: Disable append; name this event ‘g0300’.

Theorem: form-list-append-nil make-disjunct (append (flist, nil)) = make-disjunct (flist)

Theorem: tautology-theorem (form-list (flist) ∧ tautologyp (flist) ∧ (concl = make-disjunct (flist))) → proves (taut-proof (flist), concl)

Theorem: taut-eval2 (tautologyp1 (flist, auxlist) ∧ (concl = make-disjunct (append (flist, auxlist)))) → eval (concl, alist)

Theorem: tautologies-are-true (form-list (flist) ∧ tautologyp (flist)) → eval (make-disjunct (flist), alist)

Theorem: not-taut-falsify2 (form-list (flist) ∧ prop-atomp-list (auxlist) ∧ (¬ eval (make-disjunct (auxlist), falsify (auxlist))) ∧ (¬ tautologyp1 (flist, auxlist)) ∧ (concl = make-disjunct (append (flist, auxlist)))) → (¬ eval (concl, falsify-taut (flist, auxlist)))

Theorem: truths-are-tautologies (form-list (flist) ∧ (¬ tautologyp (flist))) → (¬ eval (make-disjunct (flist), falsify-taut (flist, nil)))

Event: Enable truths-are-tautologies; name this event ‘g2439’.

Event: Enable not-taut-falsify2; name this event ‘g2440’.

Event: Enable tautologies-are-true; name this event ‘g2441’. Event: Enable taut-eval2; name this event ‘g2442’. Event: Enable form-list-append-nil; name this event ‘g2443’. Event: Enable taut-proof; name this event ‘g2444’. Event: Enable not-taut-false; name this event ‘g2445’. Event: Enable not-falsify-taut; name this event ‘g2446’. Event: Enable append-nlistp; name this event ‘g2447’. Event: Enable falsify-taut; name this event ‘g2448’. Event: Enable formula-cases; name this event ‘g2449’. Event: Enable formula-cases1; name this event ‘g2450’. Event: Enable prop-atomp-falsify; name this event ‘g2451’. Event: Enable prop-atomp-auxlist; name this event ‘g2453’. Event: Enable prop-atomp-list; name this event ‘g2454’. Event: Enable falsify-step; name this event ‘g2455’. Event: Enable falsify; name this event ‘g2456’. Event: Enable not-eval-prop-atomp; name this event ‘g2457’. Event: Enable taut-eval; name this event ‘g2458’. Event: Enable eval-dble-neg-type; name this event ‘g2459’.

Event: Enable eval-nor-type; name this event ‘g2460’.

Event: Enable eval-or-type; name this event ‘g2461’.

Event: Enable eval-prop-atomp; name this event ‘g2463’.

Event: Enable neg-list-eval; name this event ‘g2464’.

Event: Enable eval-neg-elem-form; name this event ‘g2465’.

Event: Enable elem-form-eval; name this event ‘g2471’.

Event: Enable eval; name this event ‘g2472’.

Theorem: eval-tautologyp (form-list (flist) ∧ eval (make-disjunct (flist), falsify-taut (flist, nil))) → tautologyp (flist)

Definition: lis-not (flist) = if flist ≃ nil then nil

else cons (f-not (car (flist)), lis-not (cdr (flist))) endif

Definition: taut-conseq (flist, exp) = tautologyp (append (lis-not (flist), cons (exp, nil)))

Definition: tautconseq-proof (flist, exp, pflist) = list-detach-proof (flist,

exp, pflist, taut-proof (append (lis-not (flist), cons (exp, nil))))

Theorem: list-implies-reduc list-implies (flist, exp) = make-disjunct (append (lis-not (flist), cons (exp, nil)))

Theorem: append-exp-form-list (form-list (flist) ∧ formula (exp, t, 0)) → form-list (append (lis-not (flist), cons (exp, nil)))

Theorem: taut-conseq-proves (form-list (flist) ∧ formula (exp, t, 0) ∧ taut-conseq (flist, exp) ∧ proves-list (pflist, flist)) → proves (tautconseq-proof (flist, exp, pflist), exp)

Event: Enable tautconseq-proof; name this event ‘g0276’.

Theorem: eval-tautconseq (form-list (flist) ∧ formula (exp, t, 0) ∧ eval (make-disjunct (append (lis-not (flist), cons (exp, nil))),

falsify-taut (append (lis-not (flist), cons (exp, nil)), nil)))

→ taut-conseq (flist, exp)

Event: Enable taut-conseq; name this event ‘g0277’.

Event: Enable falsify-taut; name this event ‘g0282’.

Event: Enable formula; name this event ‘g0295’.

Theorem: eval-tautconseq-proof-proves (eval (make-disjunct (append (lis-not (flist), cons (exp, nil))),

falsify-taut (append (lis-not (flist), cons (exp, nil)), nil)) ∧ proves-list (pflist, flist) ∧ form-list (flist) ∧ formula (exp, t, 0)) → proves (tautconseq-proof (flist, exp, pflist), exp)

Event: Enable taut-conseq-proves; name this event ‘g0283’.

Definition: f-iff-reduc-proof (a, b, pf1 , pf2 ) = tautconseq-proof (list (f-iff (a, b), a), b, list (pf1 , pf2 ))

Index

append, 3 append-exp-form-list, 38 append-nlistp, 35 arg1, 5, 21, 23, 30 arg2, 5, 23, 30 assoc-proof, 8, 10, 12, 16, 19, 28 assoc-proof-proves, 12 assume, 7 atomp, 5, 6, 21

cancel-proof, 25 cancel-proof-proves, 25 collect-free, 3, 4, 10, 13 commut-proof, 13, 15–17, 19, 23, 27,

28 commut-proof-proves, 13 conc, 6, 7, 10, 11 contrac-proof, 8, 10, 12, 13, 17, 19,

25, 27 contrac-proof-proves, 12 covering, 4 cut-proof, 8, 10, 12, 13, 25–28 cut-proof-proves, 12

dble-neg-list-count, 22 dble-neg-not-prop-atomp, 21 dble-neg-type, 21–23, 28–30, 33–35 dble-neg-type-form-list, 29 dble-neg-type-proof, 28, 30 dble-neg-type-proof-proves, 28 degree, 2, 5, 9, 11 delete, 3 detach-list-implies, 14 detach-proof, 13, 14 detach-proof-proves1, 13 detach-rule-corr, 14

elem-form, 21, 31, 33 elem-form-eval, 31 equal-axiom1, 8, 11 equal-axiom1-proof, 8, 9, 11 equal-axiom1-proves, 11 equal-axiom2, 7, 8, 11 equal-axiom2-proof, 8, 9, 11 equal-axiom2-proves, 11 eval, 31–34, 36, 38, 39 eval-dble-neg-type, 33 eval-elem-form, 31 eval-make-disjunct, 32 eval-neg-elem-form, 32 eval-nor-type, 33 eval-or-type, 32 eval-prop-atomp, 32 eval-tautconseq, 39 eval-tautconseq-proof-proves, 39 eval-tautologyp, 38 expan-proof, 8, 10, 12, 13, 15–17 expan-proof-proves, 12

f-and, 4, 5 f-equal, 4, 7, 8 f-iff, 5, 39 f-iff-reduc-proof, 39 f-implies, 5, 7, 8, 10, 13, 14 f-not, 4–7, 10–12, 21, 23, 25–28, 30,

32–35, 38 f-or, 4, 5, 7, 8, 10–13, 15–21, 23, 25–

28 falsify, 34–36 falsify-step, 34 falsify-taut, 35, 36, 38, 39 fn, 2 forall, 5 form-list, 19, 20, 23–25, 27–31, 36,

38, 39 form-list-append, 23 form-list-append-car, 25 form-list-append-nil, 36 formlist-formula-make-disj, 19 formula, 6, 9–20, 23–28, 34, 35, 38,

39 formula-cases, 35 formula-cases1, 34 formula-forsome-reduc, 11 formula-list-implies, 14 formula-not-reduc, 11 formula-or-reduc, 11 forsome, 4, 5, 7, 8, 13, 21 forsome-intro-proof, 8, 10, 13 forsome-intro-proves, 13 free-for, 4, 9, 11 func-pred, 2–4, 6 function, 1, 2, 5, 9, 11 function-fn, 2

g0203, 28 g0204, 34 g0205, 35 g0220, 14 g0221, 14 g0222, 20 g0223, 3 g0224, 3 g0225, 3 g0226, 3 g0227, 15 g0228, 15 g0229, 20 g0230, 22 g0231, 16 g0232, 16 g0233, 17 g0234, 17 g0235, 18 g0236, 18 g0237, 22 g0238, 22 g0239, 22 g0240, 22 g0242, 27 g0243, 27 g0244, 27 g0245, 23 g0247, 20 g0248, 27 g0249, 28 g0250, 21 g0251, 21 g0252, 28 g0253, 5 g0254, 29 g0255, 25 g0256, 24 g0258, 25 g0259, 24 g0260, 28 g0263, 33 g0264, 33 g0268, 34 g0269, 34 g0271, 29 g0272, 29 g0273, 29 g0274, 29 g0275, 30 g0276, 39 g0277, 39 g0278, 32 g0279, 32 g0280, 32 g0281, 32 g0282, 39 g0283, 39 g0292, 27 g0295, 39 g0296, 35 g0297, 35 g0298, 35 g0299, 35 g0300, 36 g1253, 32 g2439, 36 g2440, 36 g2441, 37 g2442, 37 g2443, 37 g2444, 37 g2445, 37 g2446, 37 g2447, 37 g2448, 37 g2449, 37 g2450, 37 g2451, 37 g2453, 37 g2454, 37 g2455, 37 g2456, 37 g2457, 37 g2458, 37 g2459, 37 g2460, 38 g2461, 38 g2463, 38 g2464, 38 g2465, 38 g2471, 38 g2472, 38 g2737, 8 g2752, 12 g2753, 12 g2754, 12 g2755, 12 g2756, 12 g2759, 12 g2760, 12 g2761, 12 g2762, 12 g2763, 13 g2764, 13 g2765, 13 g2766, 13 g2767, 13

hint1, 9, 10 hint2, 9, 10 hint3, 9, 10 hint4, 9, 10

ident-axiom, 7, 12 ident-axiom-proof, 8, 9, 12 ident-axiom-proves, 12 index, 2 insert-proof, 16, 17 insert-proof-proves, 16

lessp-list-count, 22 lis-not, 38, 39 list-count, 21, 22 list-detach-proof, 14, 38 list-implies, 14, 38 list-implies-reduc, 38 listp-dble-neg-proof, 28 listp-dble-neg-proof-proves, 28 listp-elem-form, 31 listp-nor-type-proof, 26, 27 listp-nor-type-proof-proves, 26

m-proof, 19, 20, 24–26 m-proof-proves, 20 m-proof-proves1, 20 m1-proof, 15, 17–19 m1-proof-proves, 18 m1-proof-proves1, 15 m2-proof, 17–19, 23, 24 m2-proof-proves, 18 m2-proof-proves1, 18 m2-proof-step, 16, 17 m2-proof-step-proves, 17 m2-proof-step-proves1, 17 m3-proof, 18–20 m3-proof-proves, 20 m3-proof-proves1, 20 make-disjunct, 15, 17–20, 24, 25, 27– 34, 36, 38, 39

member-append, 32 member-eval, 31

neg, 6, 22, 23 neg-elem-form, 21 neg-list, 22–24, 30, 32, 34, 35 neg-list-eval, 32 neg-list-proof, 23, 24 neg-list-proof-proves, 24 neg-list-reduc, 23 neg-proof, 23, 24 neg-proof-proves, 23 nil-intersect, 4 nlistp-dble-neg-proof, 27, 28 nlistp-dble-neg-proof-proves, 27 nlistp-eval, 31 nlistp-neg-list, 24 nlistp-nor-type-proof, 25–27 nlistp-nor-type-proof-proves, 26 nor-type, 21–23, 27, 29, 30, 33–35 nor-type-form-list, 29 nor-type-form-list2, 29 nor-type-list-count1, 22 nor-type-list-count2, 22 nor-type-not-prop-atomp, 21 nor-type-proof, 27, 30 nor-type-proof-proves, 27 not-eval, 31 not-eval-prop-atomp, 33 not-falsify-taut, 35 not-member-delete, 3 not-taut-false, 36 not-taut-falsify2, 36 numberp-fix, 2

or-eval, 31 or-type, 21–23, 29, 30, 32, 34, 35 or-type-form-list, 29 or-type-list-count, 22 or-type-not-prop-atomp, 21 or-type-proof, 28–30 or-type-proof-proves, 29

p, 2 pairequals, 7, 8 predicate, 2, 3, 5, 9, 11 predicate-f-equal, 3 predicate-p, 2 prf, 9–11 prop-atom-proof1, 24, 30 prop-atom-proof1-proves, 24 prop-atom-proof2, 25, 30 prop-atom-proof2-proves, 25 prop-atomp, 21, 22, 30, 33–35 prop-atomp-auxlist, 34 prop-atomp-auxlist2, 34 prop-atomp-falsify, 34 prop-atomp-list, 33, 34, 36 prop-atomp-reduc, 33 prop-axiom, 7 prop-axiom-proof, 7, 9, 11, 13, 23,

25–28 prop-axiom-proves, 11 proves, 11–18, 20, 23–31, 36, 39 proves-is-formula, 11 proves-is-formula-again, 11 proves-list, 13, 14, 39

quantifier, 2–4, 6

rt-assoc-proof, 15–17, 26 rt-assoc-proof-proves, 16 rt-expan-proof, 15, 17, 25, 27 rt-expan-proof-proves, 15

sentence, 4 set-equal, 7 sub-proof, 9, 10 subset, 7, 19, 20, 24 subset-append, 24 subset-append-car, 24 subset-car, 24 subset-cons, 19 subset-ident, 24 subst, 6, 7 subst-axiom, 7, 8, 11 subst-axiom-proof, 8, 9, 11 subst-axiom-proves, 11

taut-conseq, 38, 39 taut-conseq-proves, 39 taut-eval, 33 taut-eval2, 36 taut-proof, 36, 38 taut-proof1, 30, 31, 36 taut-thm1, 30 taut-thm2, 31 tautconseq-proof, 38, 39 tautologies-are-true, 36 tautology-theorem, 36 tautologyp, 36, 38 tautologyp1, 22, 23, 30, 31, 33, 35,

36 termp, 5, 9, 11 truths-are-tautologies, 36

union, 2

v, 2 var-list, 5, 9, 11 var-set, 5 variable, 2–6, 9–13 variable-v, 2