Asking logic questions using SUBTYPEP

subtypep-set-arithmetic.lisp

CL-USER> (defun true? (p) 
           "Is P the universal set, i.e. is our statement P true?"
           (subtypep 't p))
TRUE?
CL-USER> (deftype implies (p q) 
            "Are all elements of P elements of Q? (This is basically SUBTYPEP again.)"
            `(or (not ,p) ,q))
IMPLIES
CL-USER> (true? '(implies cons list)) ; Does CONS imply LIST? 
;; Note that SUBTYPEP returns:
;; - T   and T,   if it is certain we have the universal set,
;; - NIL and T,   if it is certain we do not, and
;; - NIL and NIL, if it is not certain
T
T
CL-USER> (true? '(implies list cons)) ; Does LIST imply CONS?
NIL
T
CL-USER> (deftype not-in-both (p q)
           "The set of objects that are of types P or Q, but not both."
           `(or (and ,p (not ,q))
                (and (not ,p) ,q)))
NOT-IN-BOTH
CL-USER> (deftype equals (p q) 
           "The set of objects that are in both P and Q, or neither of them. 
            This is T (the top type) if they are the same set."
           `(not (not-in-both ,p ,q)))
EQUALS
CL-USER> (true? '(equals cons cons))
T
T
CL-USER> (true? '(equals integer (or (integer * 2) (integer 2 *))))
;; Is ℤ = ℤ ∩ ((-∞, 2] ∪ [2, ∞))?
T
T
CL-USER> (true? '(equals cons list))
;; Is CONS = LIST?
NIL
T
CL-USER> (true? '(equals (and p q) (not (or (not q) (not p)))))
;; Is P∧Q = ¬(¬Q ∨ ¬P)? (Basically one of De Morgan's laws.)
T
T