Pure Implicational Calculus in Lisp

;;; I will implement an assistent to develop proofs in
;;; Pure Positive Implicational Propositional Logic

;;; 1. AXIOMS, due to Jan Lukasiewicz
;;; For any well-formed implicational formulae P,Q,R:
;;;
;;; P1) (P => (Q => P))
;;; P2) ((P => (Q => R)) => ((P => Q) => (P => R)))

;;; 2. WELL-FORMED FORMULAE (wff)
;;; Any Lisp symbol will be considered an atomic formula
;;; eg: propositional variable
;;;
;;; W1) Any propositional variable is a wff
;;; W2) given P and Q well-formed-formulae, (P => Q) is a wff

;;; 3. RULES OF INFERENCE
;;;
;;;  I) Substitutivity, for any theorem T containing a propositional
;;;     variable A, the result of swapping every occurence of A for a
;;;    given wff Q, will be a Theorem T'
;;; II) MODUS PONENS (Detachment): for any two previus proved theorems
;;;     in the following form:
;;;
;;;      H        "Minor premisse",
;;;     (H => C)  "Major premisse", C is itself alone, a theorem.

;;; Predicate to verify if a proposition is a well-formed formula
(defun wff-p (prop)
  (or (symbolp prop)
      (and (listp prop)
       (= (length prop) 3)
       (wff-p (first prop))
       (eq (second prop) '=>)
       (wff-p (third prop)))))

;;; Function to check if two proposition are the same
(defun prop-equal (p q)
  (if (or (symbolp p)
      (symbolp q))
      (eq p q)
    (and (prop-equal (first p)
             (first q))
     (eq (second p)
         (second q))
     (prop-equal (third p)
             (third q)))))

;;;Macro to apply substitutivity in Axiom P1
(defmacro axiom-1 (p q)
  `'(,(if (wff-p p) p  (cadr (macroexpand p)))
     => (,(if (wff-p q) q  (cadr (macroexpand q)))
     => ,(if (wff-p p) p (cadr (macroexpand p)))
     )))

;;;Macro to apply substitutivity in Axiom P2
(defmacro axiom-2 (p q r)
  `'((,(if (wff-p p) p (cadr (macroexpand p)))
       => ( ,(if (wff-p q) q (cadr (macroexpand q)))
        => ,(if (wff-p r) r (cadr (macroexpand r)))
        )) => ((,(if (wff-p p) p (cadr (macroexpand p)))
            => ,(if (wff-p q) q (cadr (macroexpand q)))
            ) => (,(if (wff-p p) p (cadr (macroexpand p)))
              => ,(if (wff-p r) r (cadr (macroexpand r)))
              ))))

;;;Fuction to apply Substitutivity
(defun sb (sub-lst prop)
  (cond ((consp prop)
     (cons (sb sub-lst (first prop))
           (sb sub-lst (cdr prop))))
    ((symbolp prop)
     (if (assoc prop sub-lst)
         (cadr (assoc prop sub-lst))
       prop))
    (t prop)))

;;;Function to apply MODUS PONENS
(defun mp (minor major)
  (if (prop-equal minor (first major))
      (third major)
      nil))

;;;Struct to represent a single line of a proof
(defstruct line
  formula
  (follows-from nil))

;;;Struct to represent a proof
(defstruct proof
  (name "")
  (lines nil))

;;;Function to add a line into a proof
(defun add-line (line proof)
  (setf (proof-lines proof)
    (append (proof-lines proof) (list line))))

;;;Return the formula at line n in a proof
(defun proof-line (n proof)
  (line-formula (nth n (proof-lines proof))))

;;;Function to display the lines of a proof
(defun show-proof (proof)
  (let ((n -1))
    (mapc #'(lambda (line)
          (format t "|~2D| ~A ~65T[~A]"
              (incf n)
              (line-formula line)
              (line-follows-from line))
          (terpri))
      (proof-lines proof)))
  nil)

;;;Showing Peirce's Law is not provable...

(defparameter *domain* '(1 2 3))

(defparameter *interpretation*
  '( ((1 1) 1)
     ((1 2) 2)
     ((1 3) 3)
     ((2 1) 1)
     ((2 2) 1)
     ((2 3) 3)
     ((3 1) 1)
     ((3 2) 1)
     ((3 3) 1)))

(defun interpret (interpretation proposition)
  (if (atom proposition) proposition
    (cadr (assoc (list
          (interpret interpretation (first proposition))
          (interpret interpretation (third proposition)))
          interpretation :test #'equal))))

(defparameter *tmp-tuples*
  (let ((tuples nil))
    (dolist (a *domain*)
      (dolist (b *domain*)
    (push (list a b) tuples)))
    (nreverse tuples)))

(defparameter *subst-ab*
  (mapcar #'(lambda (tuple) `((a ,(car tuple))
                  (b ,(cadr tuple))))
      *tmp-tuples*))

(defparameter *tmp-tuples*
  (let ((tuples nil))
    (dolist (a *domain*)
      (dolist (b *domain*)
    (dolist (c *domain*)
      (push (list a b c) tuples))))
    (nreverse tuples)))

(defparameter *subst-abc*
  (mapcar #'(lambda (tuple) `((a ,(car tuple))
                  (b ,(cadr tuple))
                  (c ,(caddr tuple))))
      *tmp-tuples*))

;;;testing Axiom-1
(format t "Testing Axiom-1:~%")
(mapc #'(lambda (tuple)
      (format t "~A : ~A~%" (sb tuple (axiom-1 a b))
          (interpret *interpretation*
                 (sb tuple (axiom-1 a b)))))
      *subst-ab*)

;;;testing Axiom-2
(format t "Testing Axiom-2:~%")
(mapc #'(lambda (tuple)
      (format t "~A : ~A~%" (sb tuple (axiom-2 a b c))
          (interpret *interpretation*
                 (sb tuple (axiom-2 a b c)))))
      *subst-abc*)

;;;And finally Peirce's Law
(format t "Testing Peirce's Law:~%")
(mapc #'(lambda (tuple)
      (format t "~A : ~A~%" (sb tuple '(((a => b) => a) => a))
          (interpret *interpretation*
                 (sb tuple '(((a => b) => a) => a) ))))
      *subst-abc*)