I’m not sure about the claim “there are infinite many different notions of finiteness”; on that particular page I count 10 notions of “finite set” (although I’m not going to claim the collection of all such notions is a finite set), most of which are rarely useful. In the OP I assume finiteness means Bishop-finiteness, which that page calls the “standard definition”. I’ve also found Kuratowski-finiteness useful, and the categorical generalization to finitely generated and finitely presented objects.
By far the most useful generalization of finiteness, in my view, is compactness. From a realizability perspective, a compact space X is one where universal quantification (i.e. testing whether a semidecidable predicate holds throughout all of X) is itself semidecidable. This is discussed in various places by Andrej Bauer (MO answer), Paul Taylor (monograph), and Martín Escardó (slideshow). A typical geometric or intuitive way to establish that a metric space is compact is to see it as isometric to a bounded and closed subset of Rn and use the Heine–Borel theorem (although not all compact metric spaces, and certainly not all compact Hausdorff spaces, can be established as compact in such a way).
I strongly recommend Escardó′s Seemingly impossible functional programs, which constructs a function search : ((Nat -> Bool) -> Bool) -> (Nat -> Bool) which, given a predicate on infinite bitstrings, finds an infinite bitstring satisfying the predicate if one exists. (In other words, if p : (Nat -> Bool) -> Bool and any bitstring at all satisfies p, then p (search p) == True
(Here I’m intending Nat to be the type of natural numbers, of course) .
Perhaps relevant: Constructively there are a infinitely many different notions of finiteness.
see also: FIVE STAGES OF ACCEPTING CONSTRUCTIVE MATHEMATICS
Yes, I highly recommend that second link, and Andrej Bauer’s work in general.
I’m not sure about the claim “there are infinite many different notions of finiteness”; on that particular page I count 10 notions of “finite set” (although I’m not going to claim the collection of all such notions is a finite set), most of which are rarely useful. In the OP I assume finiteness means Bishop-finiteness, which that page calls the “standard definition”. I’ve also found Kuratowski-finiteness useful, and the categorical generalization to finitely generated and finitely presented objects.
By far the most useful generalization of finiteness, in my view, is compactness. From a realizability perspective, a compact space X is one where universal quantification (i.e. testing whether a semidecidable predicate holds throughout all of X) is itself semidecidable. This is discussed in various places by Andrej Bauer (MO answer), Paul Taylor (monograph), and Martín Escardó (slideshow). A typical geometric or intuitive way to establish that a metric space is compact is to see it as isometric to a bounded and closed subset of Rn and use the Heine–Borel theorem (although not all compact metric spaces, and certainly not all compact Hausdorff spaces, can be established as compact in such a way).
I strongly recommend Escardó′s Seemingly impossible functional programs, which constructs a function
search : ((Nat -> Bool) -> Bool) -> (Nat -> Bool)which, given a predicate on infinite bitstrings, finds an infinite bitstring satisfying the predicate if one exists. (In other words, ifp : (Nat -> Bool) -> Booland any bitstring at all satisfiesp, thenp (search p) == True(Here I’m intending
Natto be the type of natural numbers, of course) .