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:

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

It obviously isn't. ...
The axiomatisation is of the inconsistent theory

This answers my puzzlement, thanks.
In the context of that FOM post, don't you think this is a relevant additional remark to make?

, though a
particularly interesting axiomatisation from a certain theoretical
point of view.

Given that it is an inconsistent theory, i fail to see that it's very interesting. But that's a matter of taste, perhaps.

Anyway, thanks once again for your answer.

--
Cheers,
Herman Jurjus

.