Re: Question about extensions of PA

Aatu Koskensilta wrote:
Herman Jurjus <h.jurjus@xxxxxxxxx> writes:

Got time for a question? On the FOM list, you posted (a while ago,
June 3 '07), the following:

> Richard Heck wrote:
[snip]
>> ... We want a system PA* that adds to PA precisely the
>> instances of: Bew_{PA*}('A') --> A. I'm sure this can be done,
but, >> as I said, it doesn't seem trivial.
>
> Nothing but a trivial application of the recursion theorem is needed.
> The axioms of the desired theory T will be recognized by a recursive
> function f(x) with index e, where f(x) is defined by
>
> f(x) = 1 if x is the code of an axiom of PA or a code of "Prov_e('A')
> --> A"
> f(x) = 0 otherwise
>
> where Prov_e('A') is the formalisation of "A is derivable from the set
> of sentences recognized by the recursive function with index e".

In a later post, you also defended this; so you seemed to mean it, too.
But i've become a bit puzzled about it. Please permit me to ask the
following questions:



I'm not sure what the rest of your questions actually mean, but
perhaps they're based on the misconception that the constructed theory
is consistent? The function f is well-defined by the recursion theorem
-- or the Kleene fixed point theorem as it's also known --, if that's
what you're wondering.

I wondered if it really was applicable in this case, because i thought some required condition wasn't met.

2) Are you sure that the function f is a well-defined function from
recursive functions to recursive functions?

f in the above is not a function from recursive functions to recursive
functions, but rather a function from naturals to naturals (from codes
of sentences to {0,1})

Yes, understood.

, obtained by the recursion theorem. As it
results from an application of the recursion theorem, its ancestor
might be said to be a function of recursive functions to recursive
functions, a recursive functional if you wish, taking as an argument
an index e of recursive functions, f being the fixed point of this
ancestor function.

This 'ancestor function', is this really an operator from r.e. functions to r.e. functions?
Suppose we sloppily think of the set of r.e. functions as a quotient of the descriptions-of-r.e.-functions, and we have a operator F from descriptions to descriptions, then we need to know:

if e1 equivalent to e2 then F(e1) equivalent to F(e2)

before it makes sense to say that F is an operator from r.e. functions to r.e. functions. Right?
And as far as i know, the recursion theorem only applies if that condition is met.

Hence my question: is this condition met, in your construction?

if two descriptions of such functions are equivalent, don't
we also require that PA *can prove* they're equivalent, before we can
conclude that f(e1) is equivalent to f(e2)?

--
Cheers,
Herman Jurjus


.