What is a finitary proof? I started reading "mathematical logic", by J.R. Shoenfield, but I cannot quite understand a sentence in the very first chapter:

Proofs which deal with concrete objects in a constructive manner are said to be finitary. Another description, suggested by Kreisel, is this: a proof is finitary if we can visualize the proof. Of course neither description is very precise;

I cannot understand what exactly is a finitary proof, is it a synonym of a constructive proof?
 A: I wonder if Schoenfield has the Hilbert-Bernays metamathematical finitism program in mind. If so, the "finitary" bit is meant at the syntactic level (formalisation of proofs), whereas the semantic content could be anything, including classical (nonconstructive) mathematics.
A: I 'm reading this book and i don't understand this statement but i found this in wiki Finitary

A finitary argument is one which can be translated into a finite set of symbolic propositions starting from a finite1 set of axioms. In other words, it is a proof (including all assumptions) that can be written on a large enough sheet of paper.

And i think this what kreisel meant by : a proof is finitary if we can visualize the proof 
A: For example we can prove the Fermat last theorem by writing down every instance and checking it numerically. This is not finitary. 
A: I was recently puzzled by this as well, and things clarified a bit after reading (parts of) [1]. In the introduction, a distinction is made between three types of formulae, which the author claims to be relevant to understanding the difference between finitist and non-finitist:

*

*Formulae without variables, e.g. $2 + 2 = 4$;

*Formulae with only free variables for individuals and computable functions: e.g. $2 \times x = f(y)$;

*Formulae with bound variables: e.g. $\forall x \exists y (x < y)$.

The first two types are considered "decidable" in the sense that type 1 formulae can be mechanically verified and closed instances of type 2 formulae become type 1 and thus can also be verified. The role of type 2 formulae being that they serve as schemata for generating type 1 formulae. Finally, the author puts forward the thesis that an argument is not considered finitist if it contains formulas with bound variables (type 3).
Overall, I don't think there is a concrete definition of what a finitist argument is, and it certainly has a large overlap with constructiveness. But the way it is employed in Shoenfield's book seems consistent with this interpretation, especially when considering section 4.3 on the Consistency Theorem.

[1] Kreisel, G. (1951). On the interpretation of non-finitist proofs—Part I. Journal of Symbolic Logic, 16(4), 241-267. doi:10.1017/S0022481200100581
