sci.logic
[Top] [All Lists]

Re: how to define Thm in PRA

Subject: Re: how to define Thm in PRA
From: Daryl McCullough
Date: 18 Oct 2006 14:26:35 -0700
Newsgroups: sci.logic
george says...

>I am sad about the fact that you seem not to know
>a universally quantified variable when you see one,
>and I am even sadder that ranting is the only thing I
>can do about it.

George, you are completely mistaken here. What is
going on is that Peter is *describing* a language
whose axioms have no variables (free or otherwise).
He is *using* a different language to describe this
first language. This second language is the *metalanguage*.
Metalanguage is used to talk about an object language.

There are no variables in the object language, but there
*are* variables in the metalanguage. I know that's a
little hard to understand, but that isn't Peter's fault.

Once again, Peter is *describing* a language with no
variables occurring in any of the axioms. The axioms
of this language includes formulas such as

    not (0 = S(0))
    not (0 = S(S(0)))
    not (0 = S(S(S(0))))
    not (0 = S(S(S(S(0)))))

Since Peter doesn't have the time to write down the
entire infinite list of axioms, he is instead using
a shorthand, under the (false, in your case) assumption
that people reading this newsgroup will understand that
shorthand.

He summarizes the entire infinite list of axioms by
giving the pattern

    not (0 = S(m))

Any instance of the infinite list of axioms can
be obtained from this pattern by substituting
a closed term for m. The pattern is *not* an
axiom of the object language. It's Peter's way
of telling you, in a finite amount of time,
what are the axioms of the object language.

If it didn't work in your case, that's unfortunate.

--
Daryl McCullough
Ithaca, NY


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