FOM: Finitist Dirichlet

[Olivier Gerard]

Steve,

I have found in my archives his preprint and it appears
that Patrick Cegielski does use the analytic road but limiting
himself to recursive reals.

He constructs a tower of conservative extensions of Sigma_1 where
he can semantically express objects required for a semi-classic Dirichlet
theorem demonstration (using complex characters)

I have not yet an electronic
reference for you. I will be able to contact him
this week and suggest him to send you his paper
and join the mailing list. In view of his research
interests, he will certainly join us.

Olivier


Steve wrote:

> Olivier Gerard writes:
>
>  > "Le theoreme de Dirichlet est finitiste"  Patrick CEGIELSKI,
>  > Jussieu IBP-LITP Internal Report  92.90  (May 1992)
>  >
>  > and is certainly available electronically (I can lookup if anyone is
>
> Ah, good!  Could you please post the exact references to Cegielski's
> paper, including the electronic one.  Does Cegielski do anything with
> the prime number theorem?  Other theorems of number theory?
>
>  > I remember he uses Parsons work on Sigma_1 induction.
>
> This fits with what I was saying about Dirichlet's theorem.  Parsons'
> result is that Sigma_1 induction is conservative over PRA for Pi^0_2
> sentences.  Sigma_1 induction is known to be just the first order part
> of WKL_0.
>
> On the other hand, the nice thing about WKL_0 is that it supports a
> great deal of elementary real and complex analysis, so it's
> illuminating with respect to the question of eliminating complex
> function theory in favor of elementary methods.  From your description
> of Cegielski's work, it appears that Cegielski is not taking this
> analytic approach, rather he is working directly with Sigma_1
> induction.  But let me look at his paper before I comment further.
>
> -- Steve