while success == False:
success = try_again( with_enthusiasm = True )
Let F be the set of all failures, and suppose that enthusiasm can be denoted by a single real-valued variable. Let G = F cross R, the set of all failure-enthusiasm pairs. Let H be the set of all functions which map G onto itself. We may then define the set of all successes, S, as a subset of G. A member s of S must satisfy the following property: there exists at least one f in F and r in R such that, if s(f, r) = (f', r'), r' >= r.
Note that we only require the existence of one f, since the invented Churchill quotation only wants the ability to go from failure to failure without diminution of enthusiasm -- for a stricter criterion, just replace the existential quantifiers with universal ones in the final condition.