Is it possible to create a formal system with a definitional loop that still allowed proofs.

Question

In standard mathematics we have definitions that are created using the language created by previous definitions which in turn are defined. Until some point where we run into axioms.

So for example, a function can be defined in terms of relations which in turn are defined as cross products which in turn are defined in sets which in turn are defined by the axioms (At least in some formal systems).

However would it be possible to create a system which had a pair (or more) of axiom like statements that where defined in terms of each other?

Answer 1

We can define things relatively to each other using recursive definitions (see @Stefan's answer), but we typically only accept such definitions (and call them 'well-defined') if the recursion is sure to 'bottom out' in a 'base case', so we don't get into some kind of infinite loop, i.e. it is 'Well-founded' as @Stefan says.

So, I will take your question to be: is it possible to have a definition that has no such 'base' at all, i.e. where we really are forever stuck in a loop ... And still have proofs using them?

Well, I suppose that yes, with such a definition we may be able to prove that if two kinds of things are or behave a certain way relatively to each other, then maybe we can prove that they are or behave in some other way relatively to each other.

But we have other (well-defined!) ways to do that in mathematics as well. And in the end, it is really not clear what kinds of thing we are talking about in some 'absolute' sense, so it is not clear how you would apply this to concrete situations in the real world.

Answer 2

Yes and this is in fact quite common. Consider these examples:

1. A finite ordinal $n$ is a set such that $n = \emptyset$ or such that there is a finite ordinal $m$ with $n = m \cup \{m \}$.

2. A finite binary tree $(T;E)$ is a structure such that

   • $T = \{*\}$ for some set $*$ and $E = \emptyset$ or
   • $T = (S \cup \{*\}; D \cup \{ (d, *) \})$ for some set $* \not \in S$ where $(S;E)$ is a finite binary tree, $d \in S$ and there is at most one $e \in S$ with $(d,e) \in D$.

3. Let $\mathbb P$ be a poset. A $\mathbb P$-name is a set $\tau$ all of whose elements are of the form $(p, \sigma)$ where $p \in \mathbb P$ and $\sigma$ is a $\mathbb P$-name. (So, in particular, $\emptyset$ is a $\mathbb P$-name.)

4. A premouse $\mathcal M$ is a $\mathcal J$-structure $\mathcal M = (J_\rho^{\vec{E}}; \in, \vec{E}, E_{\rho})$ such that $\vec{E}$ is a fine extender sequence, $E_\rho$ is, unless empty, a suitable $\mathcal M$-extender and such that for all $\nu < \rho$ the structure $\mathcal M \| \nu$ is a premouse which, in addition, is sound.

However, one has to be careful when writing down these kinds of requirements. They have to be well-founded in some suitable way. Otherwise one might end up with pure nonsense. For example:

5. A cat is a set $C$ for which there is a cat $D$ with $C \in D$.