; A predicate spec is a pair of a symbol and a non-negative int indicating its arity.
; A predicate list is a list of predicate-specs.
; ps is the predicate-specs.
(define ps '((= . 2) (p . 0)))
; Below, s is a putative well formed formula and
; fl is the list of allowed free variables therein.
(define (wff s fl) (let ((h (car s))
   (vn (lambda (n pl) (let y ((n n)(pl pl)) (if (zero? n) (null? pl)
      (and (pair? pl) (wff (car pl) fl) (y (- n 1)(cdr pl))))))))
(cond
  ((or (eq? 'and h) (eq? 'or h))
     (let alls ((k (cdr s))) (or (null? k) (and (wff (car k) fl) (alls (cdr k))))))
  ((eq? 'not h) (vn 1 (cdr s)))
  ((or (eq? 'implies h) (eq? 'iff h)) (vn 2 (cdr s)))
  ((or (eq? 'all h) (eq? 'is h))
     (let ((v (cadr s))) (and
        (symbol? v)
     ;   (not (let nkw ((l '(and or not implies iff all is)))
     ;      (and (pair? l) (or (eq? v (car l)) (nkw (cdr l))))))
        (wff (caddr s) (cons v fl))
        (null? (cdddr s)))))
  (#t (let isp ((p ps)) (and (pair? p) (or (and (eq? h (caar p))
        (let y ((al (cdr s))(n (cdar p))) (if (zero? n) (null? al)
           (and (pair? al)
           (let y ((sl fl)) (and (pair? sl)
              (or (eq? (car al) (car sl)) (y (cdr sl)))))
           (y (cdr al) (- n 1))))))
     (isp (cdr p)))))))))
   
; tests:

(map (lambda (x) (let ((v (wff x '(a b c)))) (display (list v x)) (newline) v)) '(
   (p) (= a b)
   (= 3 a) ; 3 isn't a valid ident
   (all and (p))
   (is x (= x c))
   (P) ; undefined predicate
   (p b) ; too many operands
   (= a b c) ; too many operands
   (= b) ; too few operands
   (iff (p) (= a b))
   (iff (p)) ; too few phrases
   (implies (p) (p) (= c c)) ; too many phrases
   (not) ; too few phrases
   (and) (or (is x (= x c)) (p))
   )) ; => (#t #t #f #t #t #f #f #f #f #t #f #f #f #t #t)
   
   ; before we can do the stuff below we need a version of predicate calculus with functions.
   ; (all x (all y (all z (= (+ (+ a b) c) (+ a (+ b c))))))