?FOL Transitive Closures

[Richard Kimberly Heck]

On 3/14/23 20:23, dennis.hamilton at acm.org wrote:
> I'm missing something.  Given N as the domain of discourse, and having 0 and successor and the minimum axioms for Peano Arithmetic, I don't understand how
> 	a < S(a)
> 	a < b & b < c -> a < c
> doesn't establish a transitive closure using FOL (ok, with induction
> schema), and to even emphasize the potential infinity (although I think
> that's already established via S(x)),
> 	(a)(exists b[orcmid] ) [ a < b ].
>
> So is the claim more about set-theoretic relations in FOL and an inability
> to achieve something similar given a (suitable?) relation, R ?

First, given the usual definition of < as:

     x < y iff (Ez)(Sz + x = y)

which is commonly treated as an axiom, the mentioned principles about < 
can be proven using quantifier-free induction. (If you treat the above 
as a definition, then you need more induction.) So it's induction that's 
doing all the work here.

And the common complaint will be that first-order induction doesn't pin 
down the standard model, so it doesn't really characterize the 
transitive closure: The transitive closure of S from 0 just is the set 
of standard numbers. If you can't capture that in FOL, then you can't 
capture the transitive closure.

This is equivalent, in some sense, to saying that the notion of finitude 
cannot be characterized in FOL, since (intuitively) the transitive 
closure can be defined in terms of finitude: It contains all and only 
the things that are a finite number of S-steps away from 0. The basic 
problem, therefore, is the compactness theorem.

Let me take the opportunity to mention a paper of my own here, titled 
"Is Frege's Definition of the Ancestral Adequate?" [1] that is relevant 
to this discussion. It's a common complaint about the Frege-Dedekind 
second-order definition of transitive closure (i.e., of the ancestral) 
that the proof that it is adequate is impredicative, not just in the 
sense that it requires impredicative comprehension but in a deeper 
sense. In the mentioned paper, I show how that complaint can be avoided 
(and why a few others are just wrong-headed). In particular, I show that 
by making use of a different definition of the ancestral (one that 
itself makes use of a definition of finitude that Frege gives) and then 
giving a 'squeezing' argument to prove its adequacy. The use of a 
squeezing argument here is itself interesting, since there are so few 
examples of such arguments.

Riki

[1] https://philpapers.org/rec/HECIFD