[FOM] questions on recursive functions and independence

William.Piper@colorado.edu William.Piper at colorado.edu
Mon Nov 10 20:45:50 EST 2003

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
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
f(phi) = Mphi. Since the set L-fmla is recursive, f is also

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


More information about the FOM mailing list