Re: [isabelle] enumerating primes?



Angeliki,

  Whether or not the definition is inductive doesn't affect the end function.  From the existence of any function "N -> Nth prime", one can trivially show the infinitude of primes from the infinitude of the natural numbers.  Indeed, that such a function exists at all *is* a proof that there are infinitely many primes.

  The textbook proof of this should be possible in HOL, if you really want to avoid defining a function.  There's nothing special about inductive functions in HOL, they just happen to be defined as the LFP of a set of recurrent equations.  They're logically exactly equivalent to any other function.

David


On 08/05/18 16:34, Dr A. Koutsoukou-Argyraki wrote:
Dear Isabelle users,

I need a definition of a function taking a natural n as an input and returning the nth prime number. But: I don't want an inductive definition because in my proof I don't want to imply the assumption that primes are infinitely many.

Is anyone aware of such a definition?

(my goal is to give a proof of the infinitude of primes: to this end I want to show that assuming we have r many prime numbers, I can always construct a prime that is bigger than p_r )

Many thanks in advance,
Best wishes,
Angeliki







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.