kb84tkhrのブログ

何を書こうか考え中です あ、あと組織とは関係ないってやつです 個人的なやつ

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (16)

「10.8.4 変数・記号・論理式」の続き

定義21 "¬(a)"または"(a)∨(b)"または"∀v(a)"である

とりあえずそのまま

(define (IsNotOp x a) (= x (Not a)))

(define (IsOrOp x a b) (= x (Or a b)))

(define (IsForallOp x a)
  (∃ v ≦ x (and (IsVar v) (= x (ForAll v a)))))

(define (IsOp x a b)
  (or (IsNotOp x a)
      (IsOrOp x a b)
      (IsForallOp x a)))

案の定IsForallOpが(#fになるときに)遅いので書き直し

(define (IsForallOp x a)
  (let ((v (elm x 2)))
    (and (IsVar v)
         (= x (ForAll v a)))))

今日はこれだけ!