[FOM] questions on recursive functions and independence

[William.Piper@colorado.edu]

Hello all, 
    

I have a couple of questions that I can't find answers to in any of the
literature. Perhaps there are some on the list that can answer them for me. I
do, however, need to develop some notation, so please bear with me:


I."A" denotes a set of logical axioms constructible form the standard language
of number theory (which I denote by L). I am going to assume that A contains
the standard axioms of Peano Arithmetic. 

II."A(x)" is a formula that designates the set A, and is binumerable in P, i.e.
if n is the code for a sentence in A, then P|- A(n) and if n is not the code of
a sentence in A, then P|- ~A(n). I will use the S(x) notation to denote
formulas
designating sets S in general. 

III. I want to "extend" A to a new set A_L by including a new logical operator
M. The details aren't important; I know this extension is recursive if A is
recursive (which it is). It includes new axiom schema for dealing with the
operator M as well
as modifications for the notions of term, formula, sentence, etc. which I call
L'-terms, L'formulas, etc.

IV. I define a mapping f from the set of L-formulas to the set of L'-formulas
as
f(phi) = Mphi. Since the set L-fmla is recursive, f is also
recursive. 

V. "-->T(x)" denotes the set of all deductions from the set T of sentences
designated by T(x). 

Of course, I'm assuming there are coding functions that will relate formulae
and
proofs to unique natural numbers.

Okay, now for the questions:

1. Let T(x) be a formula which designates some recursive extension of P. Let
lambda=f[-->T(x)] UNION A_L, i.e. lambda is the set of all deductions from T
("translated" via f into the expanded language) together with the new set of
axioms A_L. Can we find a recursive formula D(x) designating a set D which
axiomatizes lambda?

2. As an alternative to the previous question, let T(x) be as above and let
lambda=f[T] UNION A_L. Since both f[T] and A_L are recursive, I can find a
recursive 
formula D(x) which designates lamda. Can we ensure the
following two conditions?
   a). f[-->T(x)] is a subset of -->D(x) and 
   b.) P|- Con_T IMPLIES Con_D

for some recursive formula D(x) which designates lambda? I.e. does there
exist a D(x) which is recursive satisfying both a) and b)? 

For both of these questions, I am using Feferman's notation: "Con_T" means "the
set designated by T(x) and binumerable in P is consistent."

My suspicions concerning both scenarios oscillates frequently and I have no
idea how I would go about establishing either of these. Can you point me in the
direction of some references? Or perhaps give me your opinions (or actual
knowledge) if you have it?

Also, I want to solicit your opinions on the following scenario. Would a
general
method for deciding sentences (in a specified formal language) independent of a
given axiomatization be useful for foundational studies? Has work in this area
been done already and if so, what are some of the results? I have looked far
and wide (but perhaps not enough) and cannot find any results which deal with
this idea, at least as far as "absolute" generality is concerned. Perhaps I am
being dense and simply not interpreting some of the subtle implications of
several well-known results in this area.  

Thanks, 
Everett