"finite" means what you think it means: a program that halts. Look at Peano Axioms: https://en.m.wikipedia.org/wiki/Peano_axioms https://en.m.wikipedia.org/wi

"finite" means what you think it means: a program that halts. Look at Peano Axioms: https://en.m.wikipedia.org/wiki/Peano_axioms https://en.m.wikipedia.org/wiki/Peano_axioms The Induction axiom allows us to write finite proofs of otherwise infinite facts, like every positive integer has a predecessor. Without it, you'd be stuck with finitism (since only a finite number of numbers can be constructed in finite time, there is only a finite number of numbers.)