Re: Question about extensions of PA

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 point is simply to obtain a set of sentences A
with the following properties

A is recursive
A contains the axioms of PA
A contains every instance of "if Prov_A('P') then P", for some
suitable definition of Prov_A

This set is an axiomatisation of the highly interesting set of all
arithmetical sentences, i.e. the inconsistent theory, as follows from
the second incompleteness theorem. Still, producing a set of sentences
having these properties is not in itself an utterly trivial task if
one does not happen to think of the recursion theorem.

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.

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}), 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.

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)?

I'm afraid I don't quite see what you're asking here.

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.)

Yep. The axiomatisation is of the inconsistent theory, though a
particularly interesting axiomatisation from a certain theoretical
point of view. It illustrates the fact that the incompleteness theorem
shows not only that formal theories are too weak to prove their
consistency, but also that they simply can't, on pain of
inconsistency, prove their own consistency even by stipulation,
i.e. by adopting it as an axiom, just as a man can't truthfully assert
he never speaks of himself.

--
Aatu Koskensilta (aatu.koskensilta@xxxxxxxxx)

"Wovon man nicht sprechen kann, daruber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
.

Relevant Pages

  • Re: The modern mathematical concept of infinity is indefensible
    ... Not what I think of as the recursion theorem, ... since mr. de Bruijn seems to have chosen not to answer this or any other of mny objections. ...
    (sci.math)
  • Re: Countably infinite Hausdorff topology?
    ... forced to face with the ugly details of "transfinite recursion". ... On the Application of the Transfinite Recursion Theorem (specialized to ... "set theory" appendix to his General Topology ...
    (sci.math)
  • Re: For All x
    ... system will prove the needed definition by recursion theorem (or even ... inductivity, since you don't have unions or intersections, etc. that ... chain of predecessors ...
    (sci.logic)
  • Re: Absolute Continuity
    ... recursion (just go and ask ... recursion theorem is well known to topos theorists. ... definitions of infinite object are equivalent) but if it gives you any ...
    (sci.math)
  • Re: Question about extensions of PA
    ... > Nothing but a trivial application of the recursion theorem is needed. ... The axiomatisation is of the inconsistent theory ... In the context of that FOM post, don't you think this is a relevant additional remark to make? ... Given that it is an inconsistent theory, i fail to see that it's very interesting. ...
    (sci.logic)