# Just For Fun: Model-Theoretic Semantics of First-Order Logic Expressed in Racket

**URL:** <https://racket.discourse.group/t/just-for-fun-model-theoretic-semantics-of-first-order-logic-expressed-in-racket/4207>\
**Category:** Show & Tell\
**Created:** [May 10, 2026, 11:29pm UTC](https://racket.discourse.group/t/just-for-fun-model-theoretic-semantics-of-first-order-logic-expressed-in-racket/4207 "2026-05-10T23:29:09Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![ulambda](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/ulambda/32/1495_2.png) [@ulambda](https://racket.discourse.group/u/ulambda)\
**Post date:** [May 10, 2026, 11:29pm UTC](https://racket.discourse.group/t/just-for-fun-model-theoretic-semantics-of-first-order-logic-expressed-in-racket/4207/1 "2026-05-10T23:29:09Z")

</div>

This is a faithful implementation of the (uninteresting) model-theoretic (Tarskian) semantics of first-order logic in Racket. We assume that domains are finite. This program is written for people to read, and only incidentally for machines to execute.

Syntax:

```scheme
<term> ::= <var> | (<func> <term>*)
<predicate> ::= (<pred> <term>*)
<exp> ::= <bool>
       | <predicate>
       | (not <exp>)
       | (and <exp> <exp>)
       | (or <exp> <exp>)
       | (=> <exp> <exp>)
       | (<=> <exp> <exp>)
       | (forall <var> <exp>)
       | (exists <var> <exp>)

```

Preliminaries:

```scheme
(define (forall? pred lst)
  (cond ((null? lst) #t)
        ((pred (car lst))
         (forall? pred (cdr lst)))
        (else #f)))
(define (exists? pred lst)
  (cond ((null? lst) #f)
        ((pred (car lst)) #t)
        (else
         (exists? pred (cdr lst)))))
(struct interp (domain func pred))
(define (funcval m f)
  ((interp-func m) f))
(define (predval m p)
  ((interp-pred m) p))
(define ((termval m v) term)
  (match term
    (,x (guard (symbol? x)) (v x))
    ((,func . ,term*)
     (apply (funcval m func)
            (map (termval m v) term*)))))
(define undefined
  (lambda (x)
    (error 'undefined "unknown variable ~s" x)))
(define (extend v x a)
  (lambda (y)
    (if (eq? y x)
        a
        (v y))))

```

Semantics:

```scheme
(define (holds? m v exp)
  (match exp
    (,b (guard (boolean? b)) b)
    ((not ,e) (not (holds? m v e)))
    ((and ,e1 ,e2) (and (holds? m v e1)
                        (holds? m v e2)))
    ((or ,e1 ,e2) (or (holds? m v e1)
                      (holds? m v e2)))
    ((=> ,e1 ,e2) (or (not (holds? m v e1))
                      (holds? m v e2)))
    ((<=> ,e1 ,e2) (eq? (holds? m v e1)
                        (holds? m v e2)))
    ((forall ,x ,e)
     (forall? (lambda (a)
                (holds? m (extend v x a) e))
              (interp-domain m)))
    ((exists ,x ,e)
     (exists? (lambda (a)
                (holds? m (extend v x a) e))
              (interp-domain m)))
    ((,pred . ,term*)
     (apply (predval m pred)
            (map (termval m v) term*)))))

```

Note that I do not use the `match` of Racket.

An Example (Modular Arithmetic):

```scheme
(define (mod-interp n)
  (interp (range n)
          (lambda (f)
            (case f
              ((zero) (lambda () 0))
              ((one) (lambda () (modulo 1 n)))
              ((+) (lambda (a b)
                     (modulo (+ a b) n)))
              ((*) (lambda (a b)
                     (modulo (* a b) n)))
              (else (error 'mod-interp "unknown func symbol ~s" f))))
          (lambda (p)
            (case p
              ((=) (lambda (a b) (= a b)))
              (else (error 'mod-interp "unknown pred symbol ~s" p))))))

```

```scheme
> (define modulo_inverse_existence
    '(forall x (=> (not (= x (zero)))
                   (exists y (= (* x y) (one))))))
> (filter (lambda (n)
            (holds? (mod-interp n) undefined
                    modulo_inverse_existence))
          (range 1 100))
'(1 2 3 5 7 11 13 17 19 23 29 31 37 41 43 47 53 59 61 67 71 73 79 83 89 97)

```

---

<div class="post-metadata">

**Author:** ![bakgatviooldoos](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/bakgatviooldoos/32/1381_2.png) [@bakgatviooldoos](https://racket.discourse.group/u/bakgatviooldoos)\
**Post date:** [May 11, 2026, 9:50am UTC](https://racket.discourse.group/t/just-for-fun-model-theoretic-semantics-of-first-order-logic-expressed-in-racket/4207/2 "2026-05-11T09:50:58Z")

</div>

@ulambda, this is really cool.

When you say "uninteresting", what do you mean by that?

---

<div class="post-metadata">

**Author:** ![ulambda](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/ulambda/32/1495_2.png) [@ulambda](https://racket.discourse.group/u/ulambda)\
**Post date:** [May 11, 2026, 2:15pm UTC](https://racket.discourse.group/t/just-for-fun-model-theoretic-semantics-of-first-order-logic-expressed-in-racket/4207/3 "2026-05-11T14:15:39Z")

</div>

I say it in the sense of Jean-Yves Girard, a proof theorist. I refer you to his books "Proofs and Types" and "The Blind Spot".