|
|
koboldpupil@xxxxxxxxxxx wrote:
> I heard PRA can apply godel's theorem,
Where did you hear that?
I don't see how it could, if it doesn't even rise to the
level of being a first-order theory.
> then i wonder how to define Thm
> in PRA which is quantifier-free?
Well, maybe you could STILL define Thm in it;
you just wouldn't be using Godel's Theorem.
Godel's Theorem alleges that certain theories
whose axiom-sets are recursive have theorem-sets
that are NOT recursive, but recursively enumerable
instead. Peter Smith gave a very nice demonstration
of why a usual axiom-set for PRA is recursive.
But I strongly doubt that the consequent theorem-set is
any less recursive. If Thm is definable in this context then
it will be because the axiom-set that Peter gave is primitive
recursive, and beacuse the set of theorems following from
it is primitive recursive as well. If that is what is happening,
then Godel's theorem is NOT being applied, not even if Godel
numbering is being used.
|
|