What is the best way to define a generically finite set?

Question

I'm trying to write a proof to show that a tree structure of finite nodes terminate.

Suppose we can say that either a node is a parent of another node ($Pqp$: $q$ is the parent of $p$), or it is a terminal node ($Tp$: $p$ does not have a parent).

1. $\forall_p \space Tp \otimes \exists_q Pqp$

Every node that has a parent only has one parent.

2. $\forall_{pqr} \space (Pqp \space \land \space Prp) \rightarrow q=r$

We say that if node $q$ comes before node $p$ ($Bqp$), then any node that comes before $q$ also comes before $p$. Additionally, we deny that $p$ comes before $q$. This avoids cyclical chains.

3. $\forall_{pqr} \space Bqp \rightarrow ((Brq \rightarrow Brp) \space \land \space \lnot Bpq)$

Any node that is the parent of a nother node must also come before it.

4. $\forall_{pq} \space Ppq \rightarrow Bpq$

Suppose we know that at least one node exists.

5. $\exists p$

I want to conclude that there must be a terminal node $\therefore \exists_p \space Tp$ however, one can always find a counter-example using premise 1 in that $p$ has a parent -- resulting in an infinite regress.

(tl;dr)

So my struggle is, I want to formalise the assumption that there are finite nodes. In all of the definitions of a finite set that I've seen, you need to specify some maximum N. In this case, I want to be intentionally vague about it -- only claiming that it's finite; not how it's finite.

An idea I had was to assume that the domain of discourse is positive integers with something like $N\in \mathbb{N_1}$ and $\forall_p \space p < N$ but something about this solution feels kind of hacky.

So is there a better way to do this and, if so what is it?

Answer 1

What you want to do cannot be formalised in first-order logic.

The Compactness theorem states this: if every finite subset of axioms of a first-order theory has a model, then the whole set has a model.

Let $A_n$ be the axiom "there are at least $n$ elements", which can be expressed in first order logic:

$$(\exists x_1)(\exists x_2)\cdots(\exists x_n)\lnot(x_1=x_2)\land\lnot(x_1=x_3)\land\ldots\land\lnot(x_{n-1}=x_n)$$

(there are $\binom{n}{2}$ terms in the conjunction). Let's suppose that you have found a first order theory $\Phi$ that axiomatises the class of all the finite trees. Then add to your theory finitely many of those axioms $A_n$ and it will have a model. (There are trees of any finite size.) Then the compactness theorem implies that there is a model of all of those axioms. That model satisfies $\Phi$ and has to be infinite. Thus $\Phi$ fails to capture "just the finite trees".

Once you depart from first-order theories, you need to specify which framework you will use. As a general advice, unless you are interested in set-theoretical or logical aspects of the story, it doesn't matter too much, why not just say "$X$ is finite"?

Answer 2

As mentioned by Stinking Bishop, finiteness cannot be formalised in first-order logic.

If you are willing to work with second-order logic, a useful notion is well-foundedness. This notion can also be expressed as a form of induction. The second-order induction axiom is

$$\forall_Q (\forall_x (Tx \to Qx) \land \forall_{pq} (Ppq \land Qx \to Qp) \implies \forall_x Qx)$$

Here, the quantifier $\forall_Q$ ranges over all unary predicates. The corresponding classical statement of well-foundedness is

$$\forall_Q (\exists_x Qx \implies \exists_x (Qx \land \neg \exists y (Qy \land Pyx)))$$

These two axioms are equivalent to each other.

To use the induction scheme to show $\exists_x Tx$, we simply define $Qy :\equiv \exists_x Tx$. The base case and inductive steps are straightforward, so we see $\forall_y \exists_x Tx$. Since we know some $y$ exists, we know $\exists_x Tx$.

To use the well-foundedness scheme, we take $Qx :\equiv \top$. Then we can conclude $\exists_x \neg \exists_y Pyx$. Such an $x$ must satisfy $Tx$.

This notion does not guarantee there are finitely many nodes. In particular, $\mathbb{N}$ is a model, where $Tx :\equiv x = 0$ and $Pxy :\equiv y = Sx$, and $S$ is the successor function. But it is strong enough to trace a tree back to its root.

If we wish to confine ourselves to first-order logic, we could throw in all first-order instances of induction. Of course, just like with Peano arithmetic, this is still not enough to capture the notion of induction.