I suppose the primitive recursive functions are supposed
to be those functions that provably terminate, is that right?

But there are functions that are not primitive recursive that provably
terminate.

I suppose the primitive recursive functions are supposed
to be those functions that provably terminate, is that right?
But there are functions that are not primitive recursive
that provably terminate.

It seems like the more useful approach would be just
to speak in terms of what provably terminates. That's
the important quality, is it not? For example, structurally
recursive functions provably always terminate, but I don't
see that they meet the definition of primitive recursive.
Any function with an algorithm that is recursive, has a
nonrecursive base case, and for which an order exists
for some subset of its arguments, such that recursive
invocations of the function (i.e., not the base case) uses
arguments that are strictly less than the previous invocation,
and whose domain is a set of elements greater than or
equal than the base case, provably terminates. This
is old hat stuff, but isn't covered by "primitive recursive."

(Also, is there any possible sense in which, say, a projection
function can be considered in any way "recursive"? I don't
see how. And yet it is "primitive recursive.")

On a related note, it seems that often the idea of totality
and termination are conflated. That seems wrong to me.
That a theorem prover may not return a result when asked
to prove a theorem is a very different case than a division
algorithm being asked to divide two arbitrary rational
numbers. Even though either one might fail to return a
value, in the first case you don't know if that's what's
happening, and in the second case you always do.

If I'm missing something, feel free to point and laugh,
only please be sure to tell me what it is I'm missing if
you do. Thanks.

Marshall

I suppose the primitive recursive functions are supposed
to be those functions that provably terminate, is that right?

But there are functions that are not primitive recursive
that provably terminate.

It seems like the more useful approach would be just
to speak in terms of what provably terminates. That's
the important quality, is it not?

For example, structurally
recursive functions provably always terminate, but I don't
see that they meet the definition of primitive recursive.

Any function with an algorithm that is recursive, has a
nonrecursive base case,

and for which an order exists
for some subset of its arguments, such that recursive
invocations of the function (i.e., not the base case) uses
arguments that are strictly less than the previous invocation,

and whose domain is a set of elements greater than or
equal than the base case, provably terminates. This
is old hat stuff, but isn't covered by "primitive recursive."

(Also, is there any possible sense in which, say, a projection
function can be considered in any way "recursive"? I don't
see how. And yet it is "primitive recursive.")

On a related note, it seems that often the idea of totality
and termination are conflated. That seems wrong to me.
That a theorem prover may not return a result when asked
to prove a theorem is a very different case than a division
algorithm being asked to divide two arbitrary rational
numbers. Even though either one might fail to return a
value, in the first case you don't know if that's what's
happening, and in the second case you always do.

MoeBlee wrote:

the
primitive recursive functions all have algorithms that require only a
"do for" loop and don't require a "do while" loop

I meant 'do until' not 'do while' there.

On May 7, 4:54 pm, MoeBlee <jazzm... at (no spam) hotmail.com> wrote:

the primitive recursive functions all have algorithms that require
only a "do for" loop and don't require a "do while" loop

I meant 'do until' not 'do while' there.

On Thu, 8 May 2008 09:46:45 -0700 (PDT), MoeBlee <jazzm... at (no spam) hotmail.com> said:

On May 7, 4:54 pm, MoeBlee <jazzm... at (no spam) hotmail.com> wrote:

the primitive recursive functions all have algorithms that require
only a "do for" loop and don't require a "do while" loop

I meant 'do until' not 'do while' there.

Either would do, no?  They differ slightly in behavior, but those
constructs are exactly equivalent in terms of computational strength.
Anything you can program in terms of the one you can program in terms of
the other.

Do you have any thoughts on my question about the notion of
'finitistic'. Why do people limit 'finitistic' to primitive recursive?
Why not take finitistic as anything total recursive?

On 2008-05-09, in sci.logic, MoeBlee wrote:

Do you have any thoughts on my question about the notion of
'finitistic'. Why do people limit 'finitistic' to primitive recursive?
Why not take finitistic as anything total recursive?

Because not all total recursive functions are recognisable as such by
finitistic principles.

The restriction to primitive recursive functions stems from the fact
that the principle of definition by primitive recursion is equivalent
to the principle of induction. Solely on basis of our basic
understanding of the naturals as what one obtains from 0 by repeatedly
applying the "add one"-operation the principle of induction and the
principle of definition by primitive recursive induction are equally
compelling. This is the reason for taking primitive recursive
arithmetic as the canonical formalisation for finitism; if we further
allow that properties definable from primitive recursive properties by
means of the usual logical operations of first-order logic --
including unrestricted quantification --, in effect accepting the
totality of the naturals as something determinate, we get PA.

--
Aatu Koskensilta (aatu.koskensi... at (no spam) xortec.fi)

"Wovon man nicht sprechen kann, daruber muss man schweigen"
 - Ludwig Wittgenstein, Tractatus Logico-Philosophicus

MoeBlee wrote:
MoeBlee wrote:

the primitive recursive functions all have algorithms that require
only a "do for" loop and don't require a "do while" loop

I meant 'do until' not 'do while' there.

"Do while X" = "Do until not-X".

On Thu, 08 May 2008 21:49:21 -0400, herbzet <herb... at (no spam) gmail.com> said:

I meant 'do until' not 'do while' there.

"Do while X" = "Do until not-X".

Well, yeah, 'cept if X is false, "Do while X" will skip the associated
procedure whilst "Do until not-X" will run through it once.

On 2008-05-10, in sci.logic, Chris Menzel wrote:
Well, yeah, 'cept if X is false, "Do while X" will skip the
associated procedure whilst "Do until not-X" will run through it
once.

That might well be. I'm not au courant on the intricacies of Pascal
and other such horrors of the programming language Pantheon.

MoeBlee's original point was, presumably, that primitive recursive
functions are those functions expressible in a programming language
with as its sole looping construct one that allows one to loop from n
to m, where m is a constant that must be determined prior to entering
the loop. That is, we can't have loping constructs of the kind "do
until condition X holds" or "do while condition X holds".

On May 11, 2:39 am, William Hale <h... at (no spam) tulane.edu> wrote:
In article
326dd4b2-5f53-45e8-a8dd-05e3d044e... at (no spam) w5g2000prd.googlegroups.com>,

Marshall <marshall.spi... at (no spam) gmail.com> wrote:
On May 10, 2:38 pm, Chris Menzel <cmen... at (no spam) remove-this.tamu.edu
wrote:
On Thu, 08 May 2008 21:49:21 -0400, herbzet <herb... at (no spam) gmail.com
said:

I meant 'do until' not 'do while' there.

"Do while X" = "Do until not-X".

Well, yeah, 'cept if X is false, "Do while X" will skip the
associated procedure whilst "Do until not-X" will run through it
once.

I'm feeling a bit of disorientation. We're talking Pascal
terminology now, right?

The above distinction between "do while" and "do until" applies not
only to Pascal, but to all the common programming languages.

Sure. Or anyway, the distinction between a loop construct that
executes at least once and one that doesn't is common. The Pascal-y
flavor of the choice of terms I still find disorienting, though.
Pascal as a thought-leader! It is as if I woke up and found that
teenagers now think John Wayne is cool.

On Thu, 08 May 2008 21:49:21 -0400, herbzet <herbzet at (no spam) gmail.com> said:
MoeBlee wrote:
MoeBlee wrote:

the primitive recursive functions all have algorithms that require
only a "do for" loop and don't require a "do while" loop

I meant 'do until' not 'do while' there.

"Do while X" = "Do until not-X".

Well, yeah, 'cept if X is false, "Do while X" will skip the associated
procedure whilst "Do until not-X" will run through it once.

On May 17, 9:10 am, "Nam D. Nguyen" <namducngu... at (no spam) shaw.ca> wrote:

Then re-read what he wrote which is quoted above, the one that has
"Solely on basis of ... repeatedly applying the "add one"-operation ...".
If that doesn't sound like Presburger artihmetic to you then that's
your own reading, not mine!

No, Presburger arithmetic has the two axioms for addition:

x+0=x
x+(Sy)=S(x+y).

That is not what Aatu mentioned.

The "add one" operation is the
successor operation. The "add one" operation in this sense is
characteristic of Peano systems,

from which we THEN go on to prove the
existence of certain functions such as addition (i.e., addition of two
natural numbers not JUST adding 1 to any given number), as Presburger
arithmetic axiomatizes.

I am asking what do you mean by 'arithmetic' as a THEORY. I.e., what
particular theory do you refer to when you say 'arithmetic' in the
phrase 'strong as arithmetic'.

Canonically it's an extension of Q, though in the thread
"Pseudo Negation - A Formal Definition of "As Strong as Arithmetic"
I did have a refined definition.

If you feel generous, you might mention that defintion here and
restate whatever point you were trying to make but now based on that
definiiton.

There is the theory of
all true sentences of arithmetic in the language of PA.

Are you sure you'd know exactly what that theory is? For example,
what are some examples of its *non-trivial* theorems? [Hint: one
can actually define "true" sentences even for an inconsistent theory!]

I spent about two straight weeks explaining this to you already. It's
found in just about any textbook on mathematical logic.
Yeah you did. But I also spend 2-3 weeks in a row giving out my
counter-explanation to you.

There is no "counterexample" to the fact that in ordinary mathematical
logic we define the set of sentences true in the standard model of PA
and that that set is a consistent, negation complete theory, though
not a recursively axiomatizable one.

Notwithstanding all that, I asked a very simple question: "what are some
examples of its *non-trivial* theorems?". Can't you just simply answer
that question, without going back to what was debated in the past?

What is the point of the question? Whether I can name "non-trivial
theorems" or not has no bearing on the fact that what I said is
correct: we define the set of sentences true in the standard model of
PA and that set is a consistent, negation complete theory, though not
a recursively axiomatizable one.

And you'd have to define "non-trivial" in this context, if you want a
formal answer. Is "1+1=2" trivial?

Meanwhile, if you gave an example
of what you consider to be a non-trivial theorem (of some theory) in
the language of PA, then perhaps I can tell you whether it's also a
member of the set of sentences true in the standard model for the
language of PA.

It is the
theory that is the set of sentences true in the standard model of the
language of PA. It is not a decidable theory and not even recursively
axiomatizable. It is a consistent theory though, as I explained to you
several times several months ago.
And I've explained to you in many post of the past that one could
*only assume it's consistent*!

You're ill-informed. By definition, it can't be an inconsistent
theory. There is no such thing as both a sentence P and ~P being true
in any model.

Eiher GC or ~GC is provable in that theory, though it is not a recursively
axiomatized theory.
You wouldn't know "that theory" enough to assert this kind of provability
"fact"!
I don't know what you're trying to say.

What I said is simple: a theory is a formal system which must have *known*
axioms.

That's a another definition of 'theory', not the defintion of 'theory'
that I've been using. If you insist on using your defintion rather
than mine, then okay, I'll use 'set_closed_under_entailment' instead.
Then where I've used 'theory', just substitute
'set_closed_under_entailment', or better yet, just recognize, as
reasonable people do, that different authors use different definitions
and that in this context, by 'theory' I mean 'set of sentences closed
under entailment'.

IF you don't *know* enough about these axioms you wouldn't necessarily
know if a particular F, say, GC or ~GC, is provable!

What are you so excited about? It's already been granted from the
start of this discussion that we do not know whether GC is a member of
ThN (where 'ThN' stands for the set of sentences true in the standard
model for the language of PA).

Also from the beginning it it
recognized that the notion of 'provability' as being recursive whether
a string of formulas is a proof does not apply to ThN since it is not
recursively axiomatizable. But, if GC is decided in, say, ZFC, then,
even though we might not know which way the decision goes, still, we
know that either GC or ~GC is a member of ThN.

And if GC is not
decided in ZFC, then there is something of a "puzzling" situation,
which I've discussed before and even as part of my reason for admiring
Hilbert's finitistic distinction between the contentual and the ideal.

What I said is correct: The
set of sentences true in the standard model of the language of PA is
negation complete but not a recursively axiomatizable theory.
Is that "theory" is Q then?

Of course not!!! That you even ask that question, after I explained
over and over and over for about a month, shows that you weren't even
reading what I wrote back then.

If not, then I don't know what you meant by
"that theory", despite the fact that we have a canonical definition of
the set of true sentences.

You don't know, because you're an arrogant snot who doesn't LISTEN to
what other people say: I explained over and over and over, for about a
MONTH, that "that theory" is EXACTLY the set of sentences true in the
standard model for the language of PA. This is common mathematical
logic. Look at, e.g., Enderton's logic book in which he makes this
central to his treatment of the subject of incompleteness.

Meanwhile, if GC is true then there is a
recursively axiomatized theory in which GC is provable and true and if
GC is false then there is a recursively axiomatized theory in which
~GC is provable and true. We can devise such theories in two seconds,
just by taking either GC or ~GC as axioms.
You had "taking either GC or ~GC as axioms" but "axioms" is plural!
Thanks for the proof reading.
And I don't think you meant {GC} and {~GC} since they're not considered
as "arithmetic theories"! So, I don't really understand what you said above!
I mean take GC or ~GC as an axiom, but not both.
So what are the other axioms?

I said EXPLICITLY, over and over and over, for about a month, that I
am using 'theory' in the sense NOT of a set of axioms and its
consequences, but rather in the sense of a set of sentences closed
under entailment. ThN is not recursively axiomatizable. However,
trivially, one axiomatization of ThN, which is NOT recursive, is ThN
itself.

And - one more time - what are some examples
of *non-trivial* theorems? How would you know that syntactically GC /\ ~GC
is not a theorem?

How many times am I going to explain this while you DON'T even listen?
No contradiction is a theorem of ThN since no contradiction is true in
any model whatsoever.

This challenges the notion that the set of FOL rules of inference is adequate
enough to make it possible to solve all the provability problems.
I don't know what you mean by "all the provability problems".
It should be simple: the collection of "all the provability problems"
would include the question about GC's provability in, say, Q!

Okay. But then I dont know what exact claim in mathematical logic you
read as "the set of FOL rules of inference is adequate enough to make
it possible to solve all the provability problems." Please cite for me
the exact claim, as found in ordinary mathematical logic or as posted
by someone, that needs to be "challenged" in this regard. For example,
it's well recognized that Q is incomplete and that there is no
decision procedure that determines whether GC is a theorem of Q. So I
don't know what exactly you wish to "challenge".

The shortcoming of FOL is that it doesn't even formally admit this shortcoming.
I didn't know that it is even within the scope of deductive calculus
to "admit" its own "shortcomings".
I hope that you do know that by now!

So, your mathematical point is...?

MoeBlee