sci.logic
[Top] [All Lists]

Re: how to define Thm in PRA

Subject: Re: how to define Thm in PRA
From: "george"
Date: 17 Oct 2006 20:57:17 -0700
Newsgroups: sci.logic

> > I agree that if you are talking about a theory with no free
> > variables, you get something fully quantifier-free and therefore
> > negation-complete.  But I do NOT agree that it is EVEN POSSIBLE
> > to write down "schemata for defining all p.r. functions" under any
> > limitation THAT severe.

Peter_Smith wrote:
> But it is.

No, it isn't.

> There's a p.r. enumeration of the p.r. functions, where each function
> is either an initial function or is defined by one application of
> composition or recursion from functions earlier on the list.

Of course there is, but every mode of function definition that
you know of (except maybe combinators) HAS A VARIABLE for
the argument.

> Suppose
> (just for example) the enumeration starts (after some initial
> functions) with addition, multiplication, exponentiation, factorial ...

You don't know how to define any of those without variables.

> Take a language lacking quantifiers

Easy enought.

> and variables,

Not so easy.

>  but with identity

Not even ADVISABLE.
You WILL be able to DEFINE identity via reflexivity and
substitution.  More to the point, if you take identity as primitive,
you will wind up saying when one generic thing can be equal
to another, i.e., in order to avoid purely atomic individual
equations, you WILL have to use SOME VARIABLES sometime.

> and the usual connectives, with a primitive function sign for each
> function in the enumeration, and a theory with corresponding axioms all
> instances of the following schemata
> 
> 0 =/= Sm

m is  a variable.


<Prev in Thread] Current Thread [Next in Thread>
Privacy Policy