FOM: intuitionistic and classical arithmetic

[Torkel Franzen]

  Neil Tennant says:

  >if S is Pi_0_2 then (if PA|-S then HA|-S)
  >If this is so, then Torkel's claim: [..]
  >can be strengthened: it will be *impossible* to find an example of
such a P.

  The theorem you quote, and similar theorems for other systems (see
e.g. M.J.Beeson, Foundations of Constructive Mathematics), make it
seem pretty unlikely that any example will ever be found. But such
theorems can't prove that it is impossible to find such a P, since the
intuitionistic interpretation of the logical constants leaves this
possibility open. Since at the same time - I would argue - there is
nothing in the intuitionistic line of thought that allows us to assert
Markov's principle as intuitionistically valid, the question whether
there is any such P may well be intuitionistically undecidable.

---
Torkel Franzen
Computer science, Lulea technical university