In first-order model theory an interpretation for a propositional atom is a truth-value (true or false). An interpretation I of a first-order atom P(t1,...,tn) requires a domain (non-empty set) D. I assigns to P an n-ary relation I(P) drawn from D and an object I(ti) from D for each ti. The truth-conditions can now be stated simply. P(t1,...,tn) is true under I just when the tuple <I(t1),...,I(tn)> is in I(P).
Thus if we fix D to the set of natural numbers and assign to the relation symbol R the relation > occupied by all pairs of number <m, n> such that m > n, and to a the number 5 and to b the number 3, then the resulting interpretation is true (is a model) for R(a, b). From then on the model theory for the logical connectives follows the expected pattern.
I(~ p) = true if I(p) =
When it comes to the quantifiers, first-order model theory introduces us to the idea of the domain D of a quantifier. exists x P(t1,..., x,...,tn) is true under I just when there is an object d in D such that <I (t1), ..., d,..., I (tn)> is in I(P). forall x P(t1,...,x,...,tn) is true under I just when for every object d in D <I(t1), ..., d,..., I(tn)> is in I(P).
The model checker in this package operates with the concept that quantifiers have domains which are effectively enumerable by means of data structures called series (sometimes called streams or progressions elsewhere). A series has
This data structure is represented here by a parametric type series over three element lists.
For example the 3 element list [0 (+ 1) (/. E false)] represents the natural number series and has the type (series number). The numbers 0 to 1000 can be reprsented by [0 (+ 1) (< 1001)].
The two quantifiers in the package are represented by exists? and forall?. For instance (exists? X [0 (+ 1) (< 15)] (= (+ X X) 10)) claims that there exists a number within the interval 0-14 which when added to itself gives 10. (exists? X [200 (+ 1) (< 230)] (prime? X)) claims a number within the interval 200-229 is prime. (forall? X [0 (+ 1) (< 15)] (even? (+ X X) 10)) claims every member of this interval is even. These functions return boolean results.
Multiple quantifiers are allowed and quantified variables can appear in a series; (exists? X [0 (+ 1) (/. E false)] (forall? Y [0 (+ 1) (< X)] (not (= (* Y Y) X)))) states that there is a natural number X such that for every natural number Y less than X, X is not identical to the square of Y.
There is no facility in this version to return values for X in such cases though the user can arrange for them to be printed; e.g.
(exists? X [0 (+ 1) (< 15)] (show X (= (+ X X) 10)))
prints 5 and returns true.