Vanilla 1.1.9 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 3 of 3
As Joel David Hamkins noted in an answer, you can pass between eventual counterexamples and properties with finitely many examples using a single quantifier and an inequality sign. For example, the property P(n) = "there exists a sporadic simple group of order greater than n" has an eventual counterexample in 808017424794512875886459904961710757005754368000000000.
I closed the question as a duplicate, because I didn't think a logically equivalent rephrasing merited a separate question.