Isn't this definition sort of recursive (isn't it a bad thing)?

Question

I was going through some of my intro maths logic textbooks, and tried to re-read them to kill sometime, but then I saw this

(a) All variables $v_n$ and all constant symbols $c_k$ are terms.

(b) If $t_1, \dots, t_{\mu(j)}$ are terms, then so is $f_j(t_1, \dots, t_{\mu(j)})$.

(c) No other strings of symbols are terms.

Here $\mu$ is a function that, to each $j \in J$, assigns the "arity" (= number of arguments) $\mu(j)$ to the function symbol $f_j$; thus, $\mu(j) \ge 1$.

This $\mu(j)$ was concerning. If $f_j$ is a function with $j$-arity, then isn't valid to say that $\mu_1(j_{\mu'(1)})$ is a $1$-arity function? Then, it means that there is another $\mu'$ function to do the work (and the cycle keeps repeating...)? This seems circular to me, and I don't see why it is even needed. We could just assume that this is some indexing without needing to define a function for it (i.e. notation with some meta interpretation which shouldn't be syntactically formed and is just there for readability), or does that guarantee some sort of distinctiveness (although, it is not clear how this "function" works so far)?

Also, it seems bad to use $\in$ this early on but I do get the author's intention here, and how it is not a part of FOL (first-order logic). Can someone tell me if this circular method causes any trouble, and if so, how could it be fixed (I think I already know how, but I want to see what other peeps have to say)? And also, whether this should be a primitive notion (i.e. the function) or not? (Ps. a primitive is an unbreakable/intuitive idea... for example, logical connectives like "AND" which are just primitives.)

Answer 1

The function $\mu$ and the expression $\mu(j)$, as well as the set $J$ and notational shorthand like the ellipses, are not part of the language being defined, they're part of the metalanguage being used to state the definition.

To define a given logical system in order to study it, we need a way to establish definitions and reason about them, so we always need a metatheory. The goal isn't to formalize every logical rule before using it (a nonsensical task if you have no formal system to start with), it's just to describe logic as a mathematical object so that we can prove things about it. The metatheory doesn't need to be "primitive"--it's often set theory--and doesn't even need to be based on the formal logic being studied.

Answer 2

Elaborating on my comment:

This is not the typical treatment of function symbols for a few reasons.

First, it treats constant symbols and $0$-ary function symbols separately.

Second, it throws all the function symbols together and then indexes all the functions by some $j$, even though this is totally unnecessary.

The author then defines a meta-theoretic function $\mu$ which takes as input a function $f_j$ and outputs the arity of the function.

In 1-sorted first-order logic, the treatment is usually as follows:

For each natural number $n \in \mathbb{N}$ (including $n = 0$), we have a set $Functions_n$ of $n$-ary function symbols.

We also have a set $V$ of variables.

A context is a list $v_1, ..., v_{n}$ of distinct variables.

In a context $\Gamma = v_1, ..., v_n$, the terms are inductively given by

• $v_i$ is a term for all $1 \leq i \leq n$
• For any terms $t_1, ..., t_n$ and any $n$-ary function symbol $f \in Functions_n$, there is a term $f(t_1, ..., t_n)$

One sometimes also sometimes sees all terms in any context defined at once. One then defines the free variables of a term. A term then occurs in context $\Gamma$ iff all its free variables occur in $\Gamma$.

In many-sorted first-order logic, the situation is slightly more complex. We are given a set $S$ of basic sorts.

Define a "complex type" to be a list $s_1, ..., s_n$ of elements of $S$.

For each complex type $T$ and sort $s \in S$, we have a set $Functions_{T \to s}$ of function symbols.

We also have, for each sort $S$, a set of variables $V_S$.

A context is a list of pairs $(v_1, s_1), ..., (v_n, s_n)$ such that $v_i \in S_{s_i}$ for all $i$.

In context $\Gamma = (v_1, s_1), ..., (v_n, s_n)$, we inductively define a term of a sort by

• $v_i$ is a term of sort $s_i$ for all $1 \leq i \leq n$
• Given a complex type $R = r_1, ..., r_n$ and sort $s \in S$; terms $t_1 \in r_1, ..., t_n \in t_n$; and a function symbol $f : Functions_{R \to s}$; $f(t_1, ..., t_n)$ is a term of sort $s$

For a good book on introductory 1st-order logic with a focus on model theory, I'd recommend Alex Kruckman's Model Theory Lecture Notes.