| |
 |
|
|
Science Forum Index » Logic Forum » Relevant Arithmetic...
Page 1 of 1
|
| Author |
Message |
| Ralf Kozian... |
 Posted: Sun Jun 01, 2008 11:55 am |
|
|
|
Guest
|
I am a little puzzled about a rather marginal theorem in Bob Meyer's
Relevant Arithmetic R#.
This theory is formulated by substituting all the material implications
in the standard Peano Axioms with relevant implications and closing this
set of formulae under provable consequence in the logic RQ.
One property of the theory is that it is /relatively PA-complete/ --
which means that there exists a translation function T from the language
of classical PA to the language of R# such that for any formula A: If A
is a PA-theorem, T(A) is an R# theorem. This is a result for which there
is no complete proof to be found in the published literature, it is
usually only reported. (But it's important nevertheless because it is
needed in the proof that R# does not admit Ackermann's gamma rule.)
The proof is supposed to go as follows:
Define T(A) as A v ~(0=0) for atomic A and as preserving truth functions
and quantifiers for the rest. (T(A & B) = T(A) & T(B) etc.)
Then by an easy induction on the complexity of formulae it can be shown
that any T(A) is RQ-equivalent to either (A & 0=0) v ~(0=0) or (A v
~(0=0)) & (0=0).
Thanks to the fact that in R# 0=0 behaves like the truth constant t of
relevant logics -- we have the characteristic theorem scheme A <-> (0=0
-> A) -- we can prove a "restricted gamma theorem"
((T(~A) v T(B)) & T(A)) -> T(B)
which secures the admissibility of PA's only rule, modus ponens for
material implication, in our translation.
Knowing this, all we need to do to complete our proof is to verify for
all the axioms of PA, that their translations are theorems of R#. This
is trivial for the axioms that are not instances of the induction scheme.
And the induction scheme is where I am stuck. We need an R#-proof for
(~T(A0) v ~\forall x (~T(Ax) v ~T(Ax'))) v \forall x (T(Ax))
It seems to me that the crucial step in producing such a proof would be
to show that the implication (~T(A) v T(B))->(T(A)->T(B)) holds in R#
but I failed miserably in doing that. (It also looks like a paradigm
case of irrelevance...) Though I did manage to find partial results when
trying to prove the contrapositive of this formula: It turns out that
either ~(T(A)->T(B)) -> T(A) or ~(T(A)->T(B)) -> ~T(B) depending on
which one of the aforementioned equivalences holds for T(A) and T(B),
but I could not get both. (Remember that, bearing in mind our context of
application, T(A) and T(B) must be equivalent to instances of the very
same scheme, because Ax and Ax' differ only at the level of terms and
not in sentential complexity.)
What am I missing?
RK |
|
|
| Back to top |
|
| |
|
Page 1 of 1
All times are GMT - 5 Hours
The time now is Sat Aug 30, 2008 12:22 am
|
|