@famesyasd Yes, and it may use more than a fixed number of previous terms. Actually, you can recover my 'ordinary' variant from your variant by first defining (by your variant) a recursive function J whose terms are the finite approximations of the desired function, namely J(0) = {} and J(n+1) = ( N[≤n] k ↦ k<n ? J(n)(k) : F(J(n)) ), and then define h = ( N k ↦ J(k+1)(k) ) and prove that h is the desired function.

@famesyasd The idea is correct, and I assume you can carry out the proof for your claims. Indeed that is one way to do it. In general there are two ways in ordinary mathematics to construct an object that is defined by closure rules. One way is to find a set that contains at least one solution and take the intersection of all solutions in that set. In your proof you chose the set N·A. In the case of constructing N, that set is provided by the axiom of infinity.

The other way is to build partial approximations and then take the union of them. If I'm not mistaken, this second way is essentially the only way to prove the full recursion meta-theorem for ZFC. The first way does not work because we cannot find a priori a suitable set containing a solution.

Lol I just posted a long answer before I realized that the question was 3 years old. Oh well. At least the nice ideas can get better known.

@user21820 I know, right??? I wasted 3 hourds to answer some question and then realised that it was 4 years old

I was on m.se a few weeks before I actually noticed the dates on the questions. Turns out I'd resurrected like, three ancient questions in the mean time.

But I think the OP answered me in the end!

Hahaha..

Being observant is not a strong suit of mine.

@famesyasd Honestly, I'm lazy to read formal proofs of what I consider to be foundational, so I generally only skim for the ideas to see whether it can work. Here contradiction should not be necessary. Uniqueness should be provable using exactly the same kind of induction as the normal one. Namely, given any two relations f,g that satisfy your Recursive thing, the set of all inputs where they agree on the outputs (namely the mappings of the input) can be shown to be an inductive set.

@famesyasd: In any case, the answer I posted may be of interest to you since the ideas are really nice. One proof via analysis and one proof via combinatorics. I've used both kinds of arguments very frequently in my own research too.

@user21820 the only thing that bothers me that I have used existence to prove uniqueness, is that okay?

@famesyasd Well, in most such situations you have to prove existence separately. However, if you literally constructed h as some set of pairs, permitted by the axioms, then of course h already exists. And if you prove that h satisfies the desired property, then you're done with the existence part.

did you mean uniqueness in your first sentence?

No I meant existence.

separately from what?

Uniqueness of course. =)

You wrote "we can immediately prove that Rec_F,a(h)", which I assume is exactly what I'm talking about.

yes, that's basically existence

Exactly.

so?

So why are you concerned?

that they should be separate

I mean you said it bothers you, but I don't see why you should be bothered if you have indeed proven existence of a desired h.

yes, I have proved existence and used that to prove uniqueness, but uniqueness should be separate from existence

like when we show that {a,b} is unique we don't use existence

Hmm I still don't see what is bothering you. I presume you are aware of the following theorem in pure first-order logic for any 1-parameter sentence Q:

> exists x ( Q(x) and forall y ( Q(y) implies x=y ) ) iff exists x ( Q(x) ) and forall x,y ( Q(x) and Q(y) implies x=y ).

I usually give this as an exercise when learning Fitch-style, because it is one of the simplest non-trivial pure first-order logic theorem (schema).

I find "should be separate" an odd thing to fixate on if it proves what you want it to prove. Proving things is about being correct.... BY ANY MEANS NECESSARY.

puts on shades

@user21820 yes, but you don't use the existence of x to prove that forall y (Q(y) implies x =y) and etc Okay so what I mean you should be able either to prove existence adn then uniqueness or firstly uniqueness and then existsence in any proof, right? But in my proof it seems that I have to prove existence first otherwise I can't prove uniqueness

it seems like it anyway

@MaliceVidrine Hahaha..

@famesyasd Aha so your question is why you can't seem to do it the other way, namely the 'separately' way. Well, the answer is that you can unfold the proof of the above pure first-order fact and inline it into your proof!

And being a logician is often about proving things by every means necessary.

@MaliceVidrine It's also about trying to figure out the logical bottlenecks, and so I get what @famesyasd is asking about here now.

But... my one-liners!

Hahaha...

@famesyasd: To be a bit more concrete, you want to prove that there is a unique h such that Q(h). You already proved the existence part, and have a proof that uses such an existing h to prove that there are no others. But you could equally have proven the 'uniqueness' part, namely "forall x,y ( Q(x) and Q(y) implies x=y )" as follows:

Given x,y:
  If Q(x) and Q(y):
    [Use your proof here but replace h with y.]
    ...
    y=x.

@famesyasd Wait, it seems that here you're doing a different thing from what I thought you were asking. You are not proving uniqueness of the desired h, but merely proving that your h is a function.

right

That is characteristic of this way, namely the first way I described here.

Without that 'bigger' container, you can't construct any object with the desired property at all.

@user21820 Okay, but I had a bigger container this time

@famesyasd In ordinary mathematics, you almost always do, via the union and powerset axioms. In set theory, sometimes you don't, such as for the full recursion theorem, and in that case you use the replacement axiom.

@user21820 I don't understand what this has to do with uniqueness and existence

@famesyasd Nothing. Ignore everything I said in response to your question until I said "Wait".

okay

I misread your intent as proving the uniqueness of the function with the desired property (that it satisfies the recursive relation).

You weren't doing that; you were just proving that it existed, and part of that involved proving that the relation you constructed is a function.

So you shouldn't say "proving the uniqueness of h" but just "proving that h is a function".

It confused me. =P

@user21820 sorry, so you think I can rework my proof that h is a fucntion in the uniqueness part?

to not use the fact that h satisfies existence part

in the fucntions properties

Are you saying you did not prove that for each n in N you have a pair in h with first item n?

If so, then you're indeed not done.

no I have proved that and THEN used this fact to prove that for each n in N I have in fact a single pair

@famesyasd Um then everything I said (which I previously told you to ignore) is now relevant...

This is amusing.

Look again at the logical fact:

@user21820 okay so I just need to rewrite my part in this style?

Every proof that you have which proves uniqueness by proving one side can be easily transformed into a proof that goes by proving the other side.

Because they are provably logically equivalent.

Instead of using the x that you proved existed to prove "forall y ( Q(y) implies x=y )" (to obtain the left-hand side), use the y given to you in the condition "Q(x) and Q(y)" to prove "x=y" (to obtain the right-hand side).

@user21820 why do I need uniqueness of h? To be able to define notation such as +(x,y)?

@famesyasd No you don't need uniqueness of h for almost all practical purposes.

right

so it's useless

as I thought

I mean, you kind of want things like +(x,y) to be unique. It would be super weird if it satisfied a recursive definition and you could meaningfully ask if a theorem depended on "which addition" you've been using.

@famesyasd Well... here is one use. If you want to prove:

> exists R in func(A·func(A,A),func(N,A)) ( forall c in A and f in func(A,A) ( R([c,f])(0) = c and forall n in N ( R([c,f])(n+1) = f(R([c,f])(n)) ) ) ).

You can do so either by using choice or by proving uniqueness of the function that satisfies any given starting point c and closure function f.

@MaliceVidrine Weird, but in practice you can't ask such a question, because once you have defined addition everything that you write using addition from that point onwards is just using the one you defined; it doesn't matter whether there is another one that has the same properties.

And in fact, that weirdness happens necessarily in other cases, since you use N as a model of PA but there are non-standard models. Though this is not really the same issue I guess.

@user21820 - But you're not, from set theory's viewpoint, going to have two different additions over the standard naturals.

Or better to phrase it, over the same minimal inductive set.

@MaliceVidrine Yea. But I've not seen a student ask, after defining say the fibonacci function, whether what we prove about it pertains to another function satisfying the same recursive relation.

And technically, the answer from a logic point of view is "of course", because once you hide the implementation (the actual object you constructed) behind an interface (the existential claim of an object that satisfies the recursive relation), everything you prove about that interface is automatically true for everything else satisfying the same interface.

The fact that they can get away with not asking that question is only a side effect of us having done a good job characterizing how recursive things work, rather than it being the case that it wouldn't matter if that uniqueness did fail to be the case.

At least my natural reaction seeing something that looks like recursive definition is "of course that's unique with that property," but I have had occasion to think seriously about situations where uniqueness fails. Like the "subobject classifier" of the category of assemblies (to go for a deep cut)

@MaliceVidrine Hmm. I'm not so sure about that. It may be an artifact of the foundational system we choose. In the current convention, ZFC is based on classical logic and does not support 'non-termination' in the semantics of the objects it is intended to be about. Hence the only way to construct long sequences are to do it recursively along a well-ordering. However, if the foundational system permits 'non-terminating' semantics then things are different.

I'll take your word on that, but I would be surprised if I encountered such a system that did not seem deeply pathological.

From the little that LeakyNun has showed me, there are type theories such as Lean where the inductive definitions can be recursive, and the intended interpretation is something like the minimal fixed point. This means that one does not have to internally prove 'termination' before setting up a recursive definition!

One can within ZFC prove that Lean's recursive types don't run into trouble, by using transfinite induction to construct the intended semantics. Of course, one might object to ZFC and hence to Lean. =)

@user21820 Okay, so I tried to rewrite the exist part into uniq one but it doesn't seem to work, causing me a great concern.

@user21820 it is not simply "instead of x use y1"

I'm not sure what the comment about Lean is intended to establish in this context (I'm getting sleepy, this is probably on me). I'm aware of how inductive types are usually interpreted in dependent type theories, but usually the syntax reads off pretty squarely as the initiality condition for the object in the semantics.

Unless Lean uses some kind of intensional equality, in which case I throw up my hands and give up understanding the semantics forever :P

@MaliceVidrine Oh it's just that we don't have to care about 'termination' in defining inductive types in Lean. As opposed to ZFC where we do have to construct it in a bottom-up (via partial approximations) or top-down (via minimal candidate) fashion.

Ah, yes, I see what you mean.

And in ZFC we always have to use uniqueness of partial approximations in the bottom-up way.

So when LeakyNun showed me Lean's inductive types I felt it was cheating.

It was 'out-sourcing' the foundational work to the meta-system...

@user21820 nvm, I think I can

@famesyasd Great! =)

And I do have to concede that the type theoretic implementations of inductive types are one of the most compelling arguments in favor of type theoretic foundations.

Not that you can always get by without partial approximations, but NNOs streamline it so much.

Compelling for pragmatic reasons or ontological reasons?

Pragmatic reasons, and ontological insofar as the maxim that misunderstanding something is often what makes it harder applies.

Hahaha..

The ontology of type theory troubles me somewhat philosophically, but I'm pretty sure it's more my problem than type theory's.

For me, I agree that allowing full recursion is pragmatically clean and also intuitive, but I am wary of its ontological underpinnings because it depends on the rest of the system. If the system additionally permits impredicativity, then it is philosophically problematic because the minimal type interpretation sort of works only when the definitions are 'well-founded' in a sense.

Since most existing type theories actually have (in their core) less impredicativity than ZFC, I think that is actually a point in their favour.

And historically that's explicitly by design, so points to Martin-Löf.

Okay, time to enter my dormant state. Cheers, all.

@MaliceVidrine Okay good night!

@user21820 nope, I don't see how I can rewrite this

@famesyasd Hmm that's because you're inducting on the wrong thing.

Last sentence is what you need.

hmm, okay, but my proof doesn't seem to be wrong

@famesyasd If you want me to check, can you write your proof more formally, such as in Fitch-style? You can take whatever shortcuts you wish as long as it is obvious how I should fill them in, but at least the contexts and claims must be 100% clear.

@user21820 I'm pretty sure what I did is correct or at max there is some tiny mistake that I should be able to fix. I'll do that later.

Yes, you'd still need to use the uniqueness one or the other way

to prove that you can introduce this functional symbol

@famesyasd Yes if you want to define this function-symbol, but no if you just want to deal with a single F (which is often the case), since the recursion theorem (without uniqueness) already guarantees the existence of F* = ( N n ↦ n=0 ? a : F*(n−1) ).

right

now everything makes sense

nice

Ah good.

ehh I'm still a little bit sad that I need to patch my proof on recursion :(

@user21820 so "+" in +(m,n) is a function, not a definatorial symbol if you say that I do not need uniqueness to use it

@famesyasd You found an error?

@famesyasd No according to my post you can safely create a new constant-symbol for +, once you have shown that there is an object with the desired properties.

@user21820 In my proof? I believe that it's correct but I guess it would break easily if you change some conditions or something due to that little logical inconsistency with uniq and existence, I've already had similar situations so It would be better to rework it to make it even nicer

I see.

constant symbols require uniqueness, do they not?

ah right I forgot that you said that they don't

ehh but you'd need to remember which constant symbols have uniqueness and which don't....

@famesyasd There is no need to 'remember'. Suppose you have constructed +, and hence can introduce it as a constant-symbol into the language. You can then prove that every other object with the same desired properties is actually equal to +.

The introduction of the new symbol does not prevent you from keeping track of the facts about it.

"You can then prove that every other object with the same desired properties is actually equal to +" so basically you can later prove that it's unique lol

Yep, if you wish. It's often unnecessary, such as in the case of +.

For another related example, you can in ZFC construct the reals R and show that it satisfies all the (second-order) real field axioms. You can then introduce R as a new symbol along with an axiom stating that it satisfies all the real field axioms, and then do all your real analysis.

It so happens that you can also prove that every other structure satisfying the same real field axioms is isomorphic to R, but who cares.

Here it is not exactly unique, but it's a related phenomenon. "unique up to isomorphism" is called "essentially unique".

Anyway I got to go. See you later!

You can introduce R as a constant symbol where uniqueness would be related to how it was constructed and then check that R satisfies all the needed properties

tha'ts what I did with naturals

so obviously it wouldn't be the only set satisfying the needed properties but it would be unique in the sense of how it was constructed (what sets it constists of etc)

@famesyasd Right. Another example is that suppose we start with my favourite axiomatization of PA, and then want to define exponentiation. We can define ^ via recursion as follows. Let A = func(N,N), and let F = ( A g ↦ ( N x ↦ x·g(x) ) ). Then apply the simple recursion theorem to A,F to get some h in func(N,A) such that h(0) = ( N y ↦ 1 ) and forall n in N ( h(n+1) = F(h(n)) ). Then define x^y = h(y)(x) for every x,y in N.

Note that this does not require choice or proving uniqueness of ^, and I do not recall ever needing the uniqueness of ^ in satisfying the basic properties of exponentiation.

@user21820 I don't get how we obtain a multiplication function in ZFC, it seems that I have to define summing functions for every n in N I know that I can but I cannot formalize this process to obtain single m*n = A_m(n) or something because m in A_m wouldbe a part of its symbol not an argument to my function that gives me A_m or can I do that?