1
$\begingroup$

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.)

$\endgroup$
3
  • 1
    $\begingroup$ This is a rather unusual treatment. Typically, constant symbols are treated as $0$-ary function symbols. The idea is that $\mu$ is a meta-theoretic function. It takes an $n$-ary function symbol $f_j$ and outputs $n$. $f_j$ is not necessarily a $j$-ary function. It is just the $j$th function to be listed. This is a bit unusual as well - normally, it's not necessarily assumed that there is some indexing set for the function symbols. $\endgroup$ Sep 15, 2021 at 23:22
  • $\begingroup$ I figured that the whole thing would be obsolete if it is merely meant to be a meta notion (which is what I suspect also...). I understand how it works, I more so want to know if this is even valid treatment or good treatment of indexing in this situation. My current impression tells me that it could really just be avoided. The reason constants are not 0-arity is because the author wants to create a $\mathrm{Tm}$ set which is the smallest sets of all terms, and it will be easily called if it is indexed, and also can pull arbitrary functions whenever they exist in the set $\mathrm{Tm}$. $\endgroup$
    – Math3147
    Sep 15, 2021 at 23:27
  • $\begingroup$ @MarkSaving Up ^ (since there is no space to ping you in my comment...) $\endgroup$
    – Math3147
    Sep 15, 2021 at 23:27

2 Answers 2

3
$\begingroup$

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.

$\endgroup$
5
  • $\begingroup$ Assume that this is our first logical system that we build, are we permitted to use this set theory which is based on that logical system itself? $\endgroup$
    – Math3147
    Sep 17, 2021 at 20:23
  • $\begingroup$ Yes, because we already understand the logic underlying set theory well enough to use it, even if we haven't yet formally defined it as a mathematical object. Ultimately we're always relying on some informal shared notion of what constitutes a sufficiently precise development of an idea. $\endgroup$
    – Karl
    Sep 17, 2021 at 21:47
  • $\begingroup$ Thank you very much! :) $\endgroup$
    – Math3147
    Sep 17, 2021 at 21:47
  • $\begingroup$ We could try to use natural language as a starting point and just explain in words how symbolic logic works (i.e. what the valid expressions and manipulations are) and avoid mentioning sets, but it's helpful to use basic set theory concepts and notation to make this exposition more precise. Augmenting informal natural language with well-understood mathematical tools certainly doesn't make anything less rigorous. $\endgroup$
    – Karl
    Sep 17, 2021 at 22:04
  • $\begingroup$ Do you think one of them is better? (Also, like the more set-theoretic approach because it makes me feel like I can connect with what the reader is saying, my only problem with it is that, often it is hard for me to see the gap between it and the meta side, because some words just seem to be blend in well-enough to seem like logical concepts to me unless the author makes it explicitly clear, I usually resolve that by comparing it to another "reference textbook", cf. Manin.) $\endgroup$
    – Math3147
    Sep 17, 2021 at 22:07
2
$\begingroup$

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.

$\endgroup$
4
  • $\begingroup$ Thinks for the insight on the many-sorted types, although it is somewhat tangential to my question. Do we have to keep recursively defining it in the same way as the non-meta function or can we stop, and just say, this is meta, we're cool with it? And I agree, it seems unnecessary, and that was part of my concern. $\endgroup$
    – Math3147
    Sep 15, 2021 at 23:51
  • $\begingroup$ @Math3147 The point of defining one set of functions for each possible number of inputs is that we don't need $\mu$ at all. What is the "it" you're referring to? $\endgroup$ Sep 15, 2021 at 23:52
  • $\begingroup$ It => starting from "many-sorted (...)". It is fine, I truly appreciate it... it simply goes beyond my concern of "why is it is needed" and "if it causes recursive trouble". Thank you, I'm satisfied with the answer, will mark it. $\endgroup$
    – Math3147
    Sep 15, 2021 at 23:55
  • $\begingroup$ @Math3147 We always have to define our terms using an inductive (or recursive) definition. This allows us to use induction and recursion on our terms. For example, when we discuss models, we will discuss the interpretation of a term in a model. This interpretation function is always defined using recursion on the definition of a term. $\endgroup$ Sep 15, 2021 at 23:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.