How would you write ∀ y ∈ R+, ∃ z ∈ R, e^z = y in pseudocode?

Question

I’m reading about proofs, currently reading Mathematics for Computer Science by Eric Lehman and Tom Leighton, they illustrate in a sample proposition that "as z ranges over the real numbers, e^z takes on every positive, real value at least once". I'm having trouble fully grasping this proposition.

I am trying to approach this is as a programmer and think of what it would look like in pseudocode if I were to see if it was true.

pr = [ N naught ]
r  = [ all real numbers ]

for y in pr:
    for z in r:

        e = pow(y, z)
        if e != y:
            goto outer
    
        print "this is true";

    outer

Is this what they are proposing?

Answer 1

∀ y ∈ R+, ∃ z ∈ R, e^z = y

Is saying that for all y in the set of positive real numbers, there exists a z in the set of real numbers, such that exp(z) = y.

You can't really create a program to verify that this is true. Most basically because you will encounter one of the following problems

1. Floating point math imprecision (essential read Is floating point math broken?)
2. The reals are infinite

You could check this over every floating point number (which would take a very long time but is still theoretically able to be computed), but you would

1. Likely come up with a situation where there is no z such that exp(z) = y because such a z does not exist exactly enough in the set of floating point numbers to give you exp(z) = y
2. Even if there was a z for every y in the set of floating point numbers, this would not prove exp(z) = y for all y in R+ and z in R.

So on the whole, yes you're pseudocode somewhat represents the idea, but it's not viable or logical to check this on a computer or really as much think about this as a computing problem.

Edit: The best way to think about this programmatically would be like this

R = [SET OF ALL REALS]
R+ = FILTER (> 0) R
(MAP (exp) R) == R+

N.B. exp means e^n where e^x = SUM [ (x^k)/(k!) | k <- [SET OF ALL NATURALS]] which is approximately 2.718^x.

Answer 2

If you imagine that it were possible to enumerate all the positive real numbers, and moreover to do so in finite time, then pseudocode for your thought experiment might look more like this:

pr = [ all real positive numbers ]
r  = [ all real numbers ]

for y in pr:
    for z in r:
        e = exp(z)
        if e == y:
            goto outer

    print "false"
    stop

    outer:

print "true"

The key differences from your pseudocode are:

• (technical) changing pow(y, z) to exp(z). This is the exponential function on z, or equivalently, the number e raised to the z^th power

• The proposition is found to be true (and the algorithm prints that result) only if the outer loop runs to completion

• If on any iteration of the outer loop, the inner one does run to completion (indicating that y for that iteration is not the exponential of any real number) then the proposition is proved false. In that case the algorithm prints that result and stops. Only one such real number y is needed for the whole proposition to fail.

Of course, an entirely different, mathematical way to describe the proposition is that it says the natural logarithm is defined and evaluates to a real number for all positive real arguments. That follows because the natural logarithm is the inverse of the exponential, so if you take the logarithm of both sides of e^z = y, you get z = log(y).

Answer 3

The proposition is proven by a program that will find z ∈ R given any y ∈ R+, so:

z = log(y);