?FOL Transitive Closures
Richard Kimberly Heck
richard_heck at brown.edu
Wed Mar 15 11:20:40 EDT 2023
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
More information about the FOM
mailing list