命題論理の定理の真理値

Clojure

次回の「ゲーデルを読もう」の担当範囲。
命題論理の定理はすべて恒真式である。

(comment 
  「ゲーデル　不完全性発見への道」 北田均　より
　3.3 命題論理の定理の真理値
)

(defn implies [x y]
  (if (and (= x true) (= y false))
    false
    true))

(defn third [lst]
  (first (next (next lst))))

(defn parse [expr]
  (if (coll? expr)
    (cond (= '! (first expr))       (list 'not (parse (second expr)))
          (= '=> (second expr))     (list 'implies (parse (first expr)) (parse (third expr)))
          (= 'and (second expr))     (list 'and (parse (first expr)) (parse (third expr)))
          (= 'or (second expr))     (list 'or (parse (first expr)) (parse (third expr)))
          :else                     (throw (Exception. "parse error")))
    expr))

(defn parse-axiom-a [axiom]
  (let [parsed (parse axiom)]
    (conj '() parsed '[A [true false]] 'for)))

(defn parse-axiom-ab [axiom]
  (let [parsed (parse axiom)]
    (conj '() parsed '[A [true false] B [true false]] 'for)))

(defn parse-axiom-abc [axiom]
  (let [parsed (parse axiom)]
    (conj '() parsed '[A [true false] B [true false] C [true false]] 'for)))

(eval (parse-axiom-ab  '(A => (B => A))) )
(eval (parse-axiom-abc '((A => B) => ((A => (B => C)) => (A => C)))) )
(eval (parse-axiom-ab  '(A => ((A => B) => B))) )
(eval (parse-axiom-ab  '(A => (B => (A and B)))) )
(eval (parse-axiom-ab  '((A and B) => A)) )
(eval (parse-axiom-ab  '((A and B) => B)) )
(eval (parse-axiom-ab  '(A => (A or B))) )
(eval (parse-axiom-ab  '(B => (A or B))) )
(eval (parse-axiom-abc '((A => C) => ((B => C) => ((A or B) => C)))) )
(eval (parse-axiom-ab  '((A => B) => ((A => (! B)) => (! A)))) )
(eval (parse-axiom-a   '((! (! A)) => A)) )