First-order logic with finitistic approach

Question

I would like to read some book, or at least some essential reference papers, about first-order logic where there is no infinite elements in any sense. By example, where the "set" of symbols of the formal language is finite, that is, no infinite list of symbols for variables, predicates, functions or constants.

Also, it cannot be any kind of infinity in the metalanguage or the methods used to "prove" metatheorems.

EDIT: some trolls downvoted this completely correct question by no reasons at all.

Answer 1

Here is as paper on a formal system for "feasible" numbers. As Alex Kruckman suggests, the paper often just refers to existing theory on formal logic for background. The main novel requirement is that all deductions must be cut-free, in terms of sequent calculus. Aside from that, there are limitations on the number of symbols allowed to occur in a term and such.

The axioms are various ordinary arithmetic statements, plus:

$$∀n. \lfloor\log_2 \lfloor \log_2 n \rfloor \rfloor < 10$$

I.E. every number $n$ is less than $2^{1024}$. Because of the rules of the proof system, any contradiction derivable from this assumption would require too large of a proof to actually write down. So, it is practically consistent.