Finite methods in 1-order formalisms Original Research Article

Familiar proof theoretical and especially automated deduction methods sometimes accept infinity where, in fact, it can be omitted. Our first example (Section 1 in the text) deals with the infinite supply of individual variables admitted in 1-order deductions, the second one (Section 2 in the text) deals with infinite-branching rules in sequent calculi with number-theoretical induction. The contents of Section 1 summarize and extend basic ideas and results published elsewhere, whereas basic ideas and results of Section 2 are exposed for the first time in the present paper. We consider classical formalisms only, to which constructive formalisms can be reduced by Shanin-style interpretations.