Cardinality of well-formed formulae on a multi-sorted signature

Question

I had some questions regarding the cardinality of the sets of well-formed formulae and terms on a multi-sorted signature. I will give first the usual definitions.

A signature Σ is a triple〈S;F;R〉 where:

• S is a (non-empty) set of symbols for types;
• F is a set of symbols for functions (each symbol f∈F is associated with a type s1×···×sn→s0, where si∈S for every 0≤i≤n (in particular, when n=0 we say that f is a constant symbol);
• R is a (non-empty) set of relation symbols. Each symbol r∈R is only associated with a type s1×···×sn, where si∈S for every 1≤i≤n. When n=0 we say that r is a propositional constant;
• S∩F∩R = ∅

For simplicity, from now on, we assume only signatures with at least one non-0-ary relation symbol (otherwise we would fall back into non-first-order languages).

We define terms and formulae inductively in this way.

Let Σ =〈S;F;R〉be a signature and let Var be a set of symbols, called variables, such that Var∩(S∪F∪R) = ∅. We assume that each variable x∈Var has a uniquely associated type s∈S, and use the notation x:s to indicate that the variable x is of type s. We also make sure that there is a countably infinite quantity of variables for each type s∈S (that is, |Var|=|S|•ℵ0).

Given a signature Σ =〈S;F;R〉and a set of variables Var, a term and its relative type on 〈Σ; Var〉 are inductively defined in this way:

• if x:s∈Var then x is a term of type s;
• if f:s1×···×sn→s0∈F and t1,...,tn are terms respectively of type s1,...,sn then f(t1, ..., tn) is a term of type s0.

Well-formed formulas are instead defined like this: Given a signature Σ =〈S;F;R〉 and a set of variables Var, a well-formed formula on〈Σ; Var〉is inductively defined as:

• if r:s1×···×sn∈R is a relation symbol and t1:s1,...,tn:sn are terms then r(t1, ..., tn) is a well-formed formula;
• if A and B are well-formed formulas, then ¬A, A∧B, A∨B, and A→B are well-formed formulas;
• if x:s is a variable and A is a well-formed formula, then ∀x:s.A and ∃x:s.A are well-formed formulas.

Let Ter(〈Σ;Var〉) and Var(〈Σ;Var〉) be the sets, respectively, of the terms and of the well-formed formulae on〈Σ;Var〉.

I was wondering if these two propositions hold true:

1. |Ter(〈Σ;Var〉)|=max(|F|,|S|•ℵ0)
2. |For(〈Σ;Var〉)|=max(|Σ|,|S|•ℵ0) where |Σ|:=|S|+|F|+|R| (assuming that in R there is at least one non-0-ary relation symbol).

Does somebody have a hint on how to prove them, if they indeed are correct? Thanks a lot.

Answer 1

Here are two strategies for proving that two sets have the same cardinality.

• Construct an explicit bijection.
• Construct a pair of injections and invoke the Cantor-Schröder-Bernstein theorem.

Let's look at the first example.

First, we'll assume that $\text{Var}$ is infinite, as is commonly done.

I claim that $|\text{Term}(\Sigma, \text{Var})|$ is $\max(|F|, |S|, |\text{Var}|)$.

To prove $\ge$, take the terms and well-order them and do the same to the symbols on the right. Associate to each symbol the first term that isn't associated with any previous symbol. This gives us an injection from the right to the left.

To prove $\le$.

Let $L \sup F \cup S \cup \text{Var}$ be the set of all symbols including improper symbols like $($, $,$, and $)$. Note that there are finitely many improper symbols.

Since $|\text{Term}(\Sigma, \text{Var})|$ is infinite, there's a map $n \mapsto i(n)$ from the natural numbers to $L$.

Also, since $L$ is infinite, there's an injection from $L \times L$ to $(F \cup S \cup \text{Var})$. Let's call the injection $(x, y) \mapsto [x, y]$.

A term is a sequence of symbols $l_1, l_2, l_3, \cdots$ of symbols taken from $L$.

Let's encode it as $[i(n), [t_1, [t_2, [t_3, \cdots]]]]$.

This gives us an injection into $(F \cup S \cup \text{Var})$.

Now we invoke Cantor-Schröder-Bernstein and conclude that the same sets have the same cardinality.