First order language with only unary functions

Question

A (first order) predicative language consists of:

1. parentheses $ ( $ and $ ) $;
2. connectives $ {\land} $, $ \rightarrow $, etc.;
3. variables $ x_1,x_2,\dots $;
4. quantifiers $ {\forall} $, $ {\exists} $;

and optionally

1. for each natural number $ n = 0,1,\dots $, some $ n $-ary function symbols $ f_1^n,f_2^n,\dots $;
2. for each natural number $ n = 0,1,\dots $, some $ n $-ary relation symbols $ R_1^n,f_2^n,\dots $;

The terms of a predicative language are defined "inductively" in the following manner: the variables are terms, and if $ t_1,\dots,t_n $ are terms, then $ f(t_1,\dots,t_n) $ is a term for each $ n $-ary function symbol $ f $.

Now, let's suppose that I do not accept the previous definition, since it does not give me a way to inductively build the symbols $ f(t_1,\dots,t_n) $. What I mean is that, while it is intuitively clear what $ f(t_1,\dots,t_n) $ means, it is not obvious to a machine how to form the string $ f(t_1,\dots,t_n) $ when $ f $ is an $ n $-ary function symbol and $ t_1,\dots,t_n $ are terms.

Let's suppose for simplicity that I only want in my terms expressions like $$ f^0,\quad f^1(f^0),\quad f^2(f^0),\quad f^2(f^0)(f^0), \quad f^2(f^1(f^0)),\quad \dots $$ that is, let's suppose that I only want to work with unary functions.

One way to define the terms would then be declare that:

• every variable is a $ 0 $-ary term;
• every $ 0 $-ary function symbol is a $ 0 $-ary term (intuitively, a $ 0 $-ary function symbol is nothing but a constant);
• for every $ n $, if $ f $ is an $ n + 1 $-ary term and $ t_0 $ is a $ 0 $-ary term, then $ f(t_0) $ is an $ n $-ary term;
• for every $ n $, if $ t $ is an $ n + 1 $-ary term and $ t_0 $ is a $ 0 $-ary term, then $ t(t_0) $ is an $ n $-ary term;
• for every $ n $, an $ n $-ary term is a term.

My first question now is: at this point, am I allowed to use an induction argument to prove facts about all terms? In other words, is the set of all terms an inductively generated one?

My second question is a more philosophical one. I wrote the garbage above in a difficult moment; I never see anyone defining the terms of a language like I did in this post. Is this even the right way to define things if I want to avoid writing things like $ f(t_1,\dots,t_n) $ and be more "machine-friendly" (whatever this means; my machine can only manipulate finite list of strings and unpack inductive definitions) as possible?

My third question is: I somewhat like to mess up with formal stuff. Should I read more about things like $ \lambda $-calculus etc.?