Question about extensions of PA

Aatu Koskensilta wrote:
(This post is part of the campaign to save logic in Usenet. You can
contribute by posting sense).

Hi Aatu,

Good to see that you're still around.
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:

1) What guarantees that the resulting fixed point is consistent?

2) Are you sure that the function f is a well-defined function from recursive functions to recursive functions?
I mean, 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)?

3) Isn't it a core point of exhaustion theory that PA-extensions like
the one asked for can't possibly be r.e.? (Unless they're inconsistent.)

As a matter of fact, if an r.e. set E can prove every instance of
pr(E, 'p') -> p,
then E can prove it's own consistency, it seems.
Just take any p such that E |- -p, and you get E |- -pr(E, 'p')
(And hence, if E is also a superset of PA, it's inconsistent,
by the Goedel-Rosser theorem.)

Am i overlooking something?
Many thanks in advance for any enlightenment,

--
Cheers,
Herman Jurjus
.

Relevant Pages

  • Re: All panduks are green
    ... *If* you can represent all primitive recursive functions, ... and your theory is consistent, and your theory is r.e., ... But T cannot prove the statement "forall x, ...
    (sci.logic)
  • Re: All panduks are green
    ... *If* you can represent all primitive recursive functions, ... and your theory is consistent, and your theory is r.e., ... But T cannot prove the statement "forall x, ...
    (sci.logic)
  • Re: All panduks are green
    ... *If* you can represent all primitive recursive functions, ... and your theory is consistent, and your theory is r.e., ... But T cannot prove the statement "forall x, ...
    (sci.logic)