|
|
> koboldpupil@xxxxxxxxxxx wrote:
> > i wonder how to define Thm
> > in PRA which is quantifier-free?
Peter_Smith wrote:
> ... you need ... [to] ... represent p.r. functions (PRA can do that),
> and have an > initial *universal* quantifier
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
> to form the sentence that says `for all
> x, it isn't the case that x is the g.n. of a proof of blah, blah'
> (and PRA allows [the equivalent of] initial universal quantifiers).
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
I'm still waiting for somebody (preferably Peter Smith) to put up
or shut up on THIS theory. Peter is being too broadly disagreeable
here. First he disagreed with the original poster by insisting that
"PRA allows [the equivalent of] initial universal quantifers."
Then, the only version of PRA that he actually presented was one
that was completely quantifier-free and appeared NOT to allow
anything vaguely equivalent to quantifiers, and he disagreed with
me about whether the variables in his axiom-schemata were "an
equivalent" of initial universal quantifiers. Peter can't have this
one both ways unless he presents two theories and explains
why they are both PRA.
|
|