Formulae you might try
[suggestion: domain size 3 or higher] # DPL-style scope extension ((Ex:(even x)) & (p0 = 2)) iff (Ex:((even x) & (x = 2))) # noncommutative & ((p0 = 1) & (Ex:(even x))) is different from ((Ex:(even x)) & (p0 = 1)) # donkey sentence ~((Ex:(Ey:(x = y))) & ~(p0 = p1)) # nested existentials (Ex:(Ey:(Ez:((prime x) & ((odd y) & (null z)))))) (Ex:(Ey:(Ez:((x = 0) & ((y = 1) & (z = 2))))))
Numbers and their denotations, as usual
The elements of the domain are natural numbers. The user specifies the maximal element with the domain size input. Then properties of these numbers are defined just as one would expect: even, odd, prime, composite, null, and number all have their usual denotations. (The predicate number always denotes the universe of discourse.)
Initial sequence length
This input determines the length of the initial state's sequences. If you enter 3, then your initial state will be the set of all triples formed from elements in you domain. You'll have pronouns p0 ... p2 available for use. If you enter an existential statement, the sequences will increase their length by 1; your pronouns will then be p0 ... p3. This choice is not all that important, since you can always extend the domain with existentials. Entering (Ex:(number x)) will extend it with every element in the domian --- they're all numbers.
Where X and Y are args or pronouns, B and C are well-formed formulae, and x is a variable
THE USUAL CLASSICAL DEFINITIONS HOLD: