A prototypical example is intuitionistic type theory, which retains ramification (without the explicit levels) so as to discard impredicativity.
This definition quantifies over the set (potentially infinite, depending on the order in question) whose members are the lower bounds of X, one of which being the glb itself.
[2] The vicious circle principle was suggested by Henri Poincaré (1905–6, 1908)[3] and Bertrand Russell in the wake of the paradoxes as a requirement on legitimate set specifications.
Russell promptly wrote Frege a letter pointing out that: You state ... that a function too, can act as the indeterminate element.
[7]Frege promptly wrote back to Russell acknowledging the problem: Your discovery of the contradiction caused me the greatest surprise and, I would almost say, consternation, since it has shaken the basis on which I intended to build arithmetic.
[8]While the problem had adverse personal consequences for both men (both had works at the printers that had to be emended), van Heijenoort observes that "The paradox shook the logicians' world, and the rumbles are still felt today.
[9] Russell, after six years of false starts, would eventually answer the matter with his 1908 theory of types by "propounding his axiom of reducibility.
[12] He gives two examples of impredicative definitions – (i) the notion of Dedekind chains and (ii) "in analysis wherever the maximum or minimum of a previously defined "completed" set of numbers Z is used for further inferences.
Concerning mathematics, an example of an impredicative definition is the smallest number in a set, which is formally defined as: y = min(X) if and only if for all elements x of X, y is less than or equal to x, and y is in X. Burgess (2005) discusses predicative and impredicative theories at some length, in the context of Frege's logic, Peano arithmetic, second-order arithmetic, and axiomatic set theory.