What does it means for a metatheory to be finitary?

Question

In a finitary metatheory it is claimed that object variables of the formal language are generated by finitary methods. What does this finitary method mean?

Also all the object variables of a formal language are not available prior to the construction of the formal mathematical theory since they are generated when new ones are required. So how does the alphabet of a formal language is defined if we don't know all the symbols in it?

Answer 1

Regarding meta-theory, finitism is linked to Hilbert's program :

the finitary standpoint [...] consists in a restriction of mathematical thought to those objects which are “intuitively present as immediate experience prior to all thought,” and to those operations on and methods of reasoning about such objects which do not require the introduction of abstract concepts, in particular, without appeal to completed infinite totalities.

According to the most mature presentations of finitism (Hilbert and Bernays, 1939):

the objects of finitism are characterized as formal objects which are recursively generated by a process of repetition; the stroke symbols are then concrete representations of these formal objects.

According to some authors, a reasonable candidate to implement the finitistic point of view is the primitive recursive arithmetic $\mathsf {PRA}$.

See also the post : what is finitistic reasoning ?

---

A formal language is finitary because it is producible or surveyable in a finite number of steps.

The symbols of e.g. first-order language belong to a countable set:

a finite set of symbols for the logical connectives;

a (possibly empty) set of symbols for constants;

a (possibly empty) set of symbols for predicate symbols or relation symbols for each possible “arity” $n >0$;

a (possibly empty) set of symbols for functions for each possible “arity” $n >0$;

finally:

an unlimited sequence : $v_0, v_1, \ldots$ of individual variables.

We can use only two symbols to "implement" the entire sequence of variables: $v$ and $|$, saying that $v_i$ is the abbreviation for the symbol sequence “$v | \ldots |$", i.e. the symbol "$v$" followed by $i$ copies of the symbol "$|$".

Due to the fact that a formula is an expression (i.e. a string of symbols) of finite lenght, the number of different individual variables occurring in a formula will be always finite.

But the mechanism of implementing the coding-schema for naming variables guarantees an unlimited supply of them.

In conclusion, the usual syntax of first-order language is based on a countable set of symbols, but we can shrink it to a finite set.