What mathematics do you think could be developed if existential instantiation was only allowed from sets and if the predicate is true for only finite/countable many elements in the given set?
Any reference is appreciated as well!
EDIT: To be specific, the altered rule would look like this: ∃xP(x)⟹P(a) where P is a predicate such that P=x∈A∧... and P only holds for finite/countable elements in A. Intiutively, I think, this would mean that an element with a given property of a set can only be chosen if there are a finite/countable elements with that property.