FOM: Question: Aximoatizing PA-rnt and EL(c)-rft

[Peter Lietz]

Dear readers of the FOM list,


I would like to ask you two questions concerning the axiomatization of
"realizability combined with truth" interpreted in classical systems.
In the following, I will adhere to the notation used in A.S. Troelstra
`Realizability', Chapter VI of the Handbook of Proof Theory.


INTRODUCTION

Kleene's numerical realizability interpretation is a translation of a
formula `A' of Heyting arithmetic into a formula `x rn A' of Heyting
arithmetic. The class of formulae A such that `HA |- \exists x. x rn
A' is axiomatized by the scheme ECT_0 (the so called Extended
Church's Thesis). Such axiomatizations are known for various flavors
of the realizability interpretation.

There is one variation of realizability called `realizability combined
with truth', which differs from standard numerical realizability only
in the clause for implication:

     x rnt A->B   :=   (\forall y. y rnt A -> x*y rnt B) /\ (A->B)


REMARK  This variant of the realizability interpretation serves a
  similar purpose as and sometimes also goes by the name of
  q-realizability. However, the original q-realizability is different
  in the respect that the class of q-realizable formulas is not closed
  under derivation.


By its definition, rnt-realizability entails truth, i.e.

     HA |- (\exists x. x rnt A) -> A

so asking for an axiomatization is of course pointless, as long as we
interpret in HA. But this is no longer so when we interpret in Peano
arithmetic (PA).


QUESTION 1

Now, the question I would like to ask is the following:

     +-----------------------------------------+
     | Axiomatize the class of formulae A such |
     | that PA |- _n_ rnt A for some n\in\N.   |
     +-----------------------------------------+

By _n_ I mean the numeral associated with the natural number n.
Alternatively, one might ask for an axiomatization of those formulae
A such that `PA |- \exists x. x rnt A' but I am more interested in the
former question.


So, why am I interested in this question at all and what does this
have to do with foundations of mathematics?

The class of all formulae A with the above stated property can in my
opinion be thought of as the class of formulae such that we have an
algorithm along with a classical proof of the fact that the algorithm
witnesses the (in some natural sense) algorithmic content of the
formula.


This class of formulae lies somewhere between HA and PA. One can
readily check that Markov's Principle is realized in the above
sense. However, HA + M is not yet an axiomatization. From the fact
that

     HA |- (x rnt \neg A) <-> \neg A

one can conclude that any axiomatization has to prove the same negated
formulae as PA (which is not the case for HA + M).


Next, one can observe that (some instance of) the Independence of
premise (IP) principle is not validated, i.e. there is in general no
number that realizes the formula

     (\neg A -> \exists x. B) -> (exists x. \neg A -> B)

     (for x not free in A)

In order to see this, set `A:=\neg\exists x. Teex' and `B:=Teex',
T being Kleene's T-predicate. Then the hypothesis of this instance of
IP is an instance of M. If the conclusion was realized, then PA would
prove the existence of a recursive function deciding the halting set.


Non-constructive principles like e.g. the `Lesser principle of
omniscience' (LPO, see Bishop) are neither falsified in this theory
(because PA proves LPO) nor validated.


By its definition, the set of formulae enjoys the Existence
Property and Church's rule.





QUESTION 2

One can ask a corresponding question regarding Kleene's function
realizability combined with truth.

     +--------------------------------------------+
     | Axiomatize the class of formulae A such    |
     | that EL(c) |- {_n_} rft A for some n\in\N. |
     +--------------------------------------------+

By EL(c) I mean elementary analysis (EL) augmented with the principle
of the excluded middle. The symbol {_n_} is supposed to mean the
partial recursive function associated with the numeral _n_. This is of
course not official syntax of EL but can easily be translated into such.


In addition to the aforementioned ones, another interesting example of
a principle validated by the latter interpretation is the boundedness
principle BD-N (see Hajime Ishihara `Continuity properties in
constructive mathematics', JSL 57).


-----------------


A related problem is mentioned already in [Tro73]. It is proved that:

    PA |- \exists n. n rn A
      if and only if
    HA + ECT_0 + M |- \neg\neg A

It is in fact even easier to see that

    PA |- _n_ rn A for some n in N
      if and only if
    HA + ECT_0 + M |- A

This completely solves the problem for realizability (not combined
with truth) interpreted in PA. I want a version of the latter
proposition for the truth-variant of realizability, but the usual
proof technique for axiomatizations of realizability interpretations
just does not seem to work.


This is as much as I know as of now. I would be grateful for hints
leading towards axiomatizations but also for comments or criticism
on my basic assumptions.


Respectfully yours,

Peter Lietz.



Peter Lietz, PhD student
FB Mathematik, TU Darmstadt
Darmstadt, Germany