# Lists and predicates on lists in classical first order logic

I have to express some basic Prolog code in classical first order logic (FOL). In Prolog i use lists, together with member/2 and append/3 a lot. Could you give me some tips for writing clauses like the ones in the toy example below in FOL? The xs are intended as variables...

Family(Parents(marge, homer), Kids(bart, lisa, maggie))
Family(Parents(kirk, luann), Kids(milhouse))

Family(Parents(_, _), Kids(x1)) ^ Member(x2, x1) -> SomeKid(x2)
Family(Parents(x1, x2), Kids(x3)) ^ Append(x1, x2, x3, xresult) -> WholeFamily(xresult)

Expected output SomeKid(x) x = bart (and so on)
Expected output WholeFamily(x) x = marge, homer, bart, lisa, maggie and so on

I know i could do parent(bart, homer), parent(lisa, homer) and so on, but in my application I have to write predicates and functions that take lists of variable arity, where any list could contain functions (e.g. [Person(Name(bart), Age(12)), ..., Person(Name(lisa), Age(10))].

/JCR

• Totally unclear... In FOL there are no lists. – Mauro ALLEGRANZA Feb 17 at 13:20
• To express Kids(bart, lisa, maggie) we need a unary predicate Kid(x) and add the "axiom" : Kid(bart) ∧ Kid(lisa) ∧ Kid(maggie). – Mauro ALLEGRANZA Feb 17 at 13:21
• SomeKid(x2) can be ∃x Kid(x). Similar for Married(marge,homer) and Parent_of(x,y), from which Parent-of(marge,bart) and Parent_of(homer,bart). – Mauro ALLEGRANZA Feb 17 at 13:26
• With it we can try to define the relationship of Belong_to_the_same_Family(x,y) : ∀x∀y [Married(x,y) ∨ ∃z ∃w (Parent_of(z,x) ∧ Parent_of(w,x) ...]. – Mauro ALLEGRANZA Feb 17 at 13:28
• @MauroALLEGRANZA Thanks. What i was after is something like a variable-arity predicate. Married, for example, is usually arity 2, but one could think of marriages with three people and so on. And then functions which take a variable number of arguments. But, if I understand you correctly, this is not possible with classic FOL... – JCR Feb 17 at 18:43

Might this pass as classic FOL? Where the Member function gets items recursively...

List(a, end)
List(a, List(b, end))
List(a, List(b, List(c, end)))

x1 = List(x2, -) -> Member(x2, x1)
x1 = List(-, x1) ^ Member(x2, x1) -> Member(x2, x1)

• No, that doesn't work. In your second formula, the first "List" is a predicate symbol, but the second one must be a function symbol. You cannot use the same symbol for both in FOL. However, you can introduce list constructors, say "cons/2" and "nil/0", and then specify that List(nil) holds and that ∀x∀y (List(y) -> List(cons(x,y))) holds. (The Prolog [..|..] notation is just syntactic sugar for such list constructors.) – Uwe Mar 19 at 22:57
• What exactly is a list in predicate logic? Did you just add it on a whim? If you did, is the new system complete and consistent? If not, then its useless. – Bertrand Wittgenstein's Ghost Nov 15 at 8:12

There is no notion of definition by example in most grammars for any FOL, and very little other syntactic sugar. You have to look at your data structures in purely relational terms.

Something like

Person(Name(bart), Age(12))

is really

Exists x: Person(x) & Name(x, 'bart') & Age(x, 12)

(Officially Exists is the inverted E, each predicate we have named has to be a subscripted phi and all constants are subscripted a's with a separate axiom stating the assigned value, and all variables are subscripted x's. But I am just not typing that.)

If this is the only sort of list relation you have in mind, then you don't need the lists because they are just a mechanism providing uniformity, and do not affect the content.

In theory there is not anything that rules out lists or even lists of lists. You can introduce a schema, like the one for induction.

The axioms of an FOL do not have to be finite, just recursively enumerable. So you can define a function in infinitely many steps, as long as the steps are stereotyped enough to be emitted by some template. What constitutes a template varies between versions of FOL. But all of them admit some mechanism allowing arbitrary repetition, usually via indexing, because induction is crucial to all arithmetic and stating the induction axioms generally requires a polymorphic function that takes every different number of arguments.

So this kind of mechanism is not outside the spirit of FOL. But it might be impossible to express in any way that is not ambiguous or hopelessly confusing unless you explicitly write the recursive function that enumerates your axioms. All of these systems generally contain just one scheme. Some generalizations to real closed fields with convergence, or other advanced mathematics, may have two or three schemata at the outside. So the expressive power is severely limited to just handle those few cases. For instance the definition of convergence, or lexicographical ordering.

Using the language that Schoenfield introduces to express the Peano axioms in his version of Goedel's theorem, if you really need to define a function that takes two lists, you have to pass the lists 'zipped' and do something like:

Less(x[1], y[1], x[2], y[2] ... x[n], y[n]) <-> x[1] < y[1] & x[2] < y[2] ... x[n] < y[n]

(Again x and y are syntactic sugar, officially there is only x, so these are x[0, 1]...x[0, n] and x[1, 1]...x[1, n].)

If you want to handle two different length lists you need to pad them out with some 'nil' marker, etc.

A precondition that asserts a list of lists is lexicographically ordered already becomes insane:

Sorted(x[1, 1], x[1, 2], x[1, 3]... x[2, 1], x[2, 2], x[2, 3]... x[n, m]) <-> Less(x[1, 1], x[2, 1]) & Less(x[1, 2], x[2, 2]) & ... Less(x[1, n], x[2,n]) & Less(x[2, 1], x[3, 1]) & Less(x[2, 2], x[3, 2]) & ... Less(x[2, n], x[3,n]) ... ... Less(x[m - 1, 1], x[m, 1]) & Less(x[m-1, 2], x[m, 2]) & ... Less(x[m - 1, n], x[m,n])

So it is hardly worthwhile. FOL languages are not meant to be used to say anything meaningful. They are meant to express a few well-rehearsed proofs about extremely simple systems or nail down some very limited axioms so that we can enumerate their models.

What is the goal of this enterprise?

I am not sure what prolog is, but here are my two cents:

You can define a Predicate P^k(x_1,...,x_k) to have k (=<) l arity; given |Dom(P)|=l; furthermore, define k=f(x_1); This should technically give you a predicate whose arity depends on the first term of the predicate.

The problem is: this system is absolutely useless. We can not derive anything useful in it. Even if we suppose each instance of predicate P is synonymous with the other semantically. There is no, absolutely no way, they would be syntactically equivalent. In fact, given two predicates P^m and P^n, and m=/=n, we can be certain P^m and P^n are, at the very least least, in terms of provability inequivalent because we will not be able to instantiate P^n from P^m or vise versa.