Re: [isabelle] enumerating primes?

On 08/05/18 18:13, Dr A. Koutsoukou-Argyraki wrote:

On 2018-05-08 15:50, David Cock wrote:

  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.

indeed- so let me rephrase my question: I should have written that I want this enumerating function to be defined only on a segment of the naturals, i.e. up to some r \in nat , having assumed that there exist r many primes

How about "f(r) = THE n. |{m. m <=n  /\ prime m }| = r".  When you try to prove anything about it you'll be forced to show that there exists a unique n satisfying the predicate (and by implication all smaller r).  I *think* you won't have said anything about any larger r, but it's gonna be hard to avoid sneaking the assumption in if you're already inside HOL.  In principle the proof automation might be able to infer it by itself if you let it (but probably wouldn't).  Sticking to manual deduction should be safe.


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