What is a ?non-constructive proof??

[Joe Shipman]

It’s not non-constructive. It is a very fast-growing function, but everything is completely constructive or can be made so. Thus, if you define a non-fast-growing function such as 

f(a,b) = the middle base-10-digit (adding one leading 0 if necessary) of the number of steps to reduce “a expressed in pure base b” to 0 by the Goodstein procedure “increase base then subtract 1”

then you are guaranteed to find a solution to f(a,b)=c, given a and b, constructively but slowly.

— JS

Sent from my iPhone

> On Feb 20, 2020, at 2:46 PM, José Manuel Rodríguez Caballero <josephcmac at gmail.com> wrote:
> 
> 
> JS wrote:
>> 
>> There are at least three kinds of ?non-constructive proofs? that I have seen:
>> (1) A theorem that certain equations have finitely many solutions, with no bound given that would allow one to exhaustively search for them
>> (2) A theorem that a certain equation has a solution, with no bound given, but a guarantee that searching will eventually find one
>> (3) A counting argument that an object with certain properties of a certain size must exist, which comes with an implicit exponential bound on the search but no efficient construction.  
> 
> I do not see how Goodstein theorem, which is the prototypical example of a non-constructive result, fits into this classification.
> 
> Kind regards,
> Jose M.
> 
> 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20200220/af531351/attachment-0001.html>