Given S1 ∈ set
	Given c1 ∈ S1
		Given f1 ∈ S1→S1
			Q(m) ≡ ∃g ∈ ℕ[≤m] → S1 ( g(0) = c1 ∧ ∀n ∈ ℕ[<m] ( g(n+1) = f1(g(n)) )
			Let g' ∈ ℕ[≤0]→S1 such that g = {(0,c1)}
			g'(0) = c1 ∧ ∀n ∈ ℕ[<0] ( g'(n+1) = f1(g'(n))
			Q(0)
			Given k ∈ ℕ
				If Q(k)
					∃g ∈ ℕ[≤k]→S1 ( g(0) = c1 ∧ ∀n ∈ ℕ[<k] ( g(n+1) = f1(g(n)) )
					Let h' ∈ ℕ[≤k]→S1 such that g(0) = c1 ∧ ∀n ∈ ℕ[<k] ( g(n+1) = f1(g(n)) )
					Let h'' ∈ set such that h'' = {(k+1,f1(g'(k))}
					Let H ∈ set such that H = {h',h''}
					Let g'' ∈ set such that g'' = union(H)

@Prithubiswas I don't understand why you don't want to use function-notation as I told you to.

Also, since you already know you can do "let x = E" for any fresh variable x and object expression E, it makes no sense not to use that if you want to. That causes your proof to be unnecessarily unreadable, and also increases your error rate (e.g. "g" instead of "g'").

I am asking because I am unsure.

Use the function-notation rule. Don't use any set theory.

@Prithubiswas Well that's acceptable in ordinary mathematical writing, so it's fine, but actually what I meant was:

Let g' = ( ℕ[≤0] k ↦ c ).

Ohhhh

It's not standard mathematical notation, but it's precisely what the system provides.

And although non-standard, it's very close to standard lambda notation "Let g' = ( λk:ℕ[≤0]. c )".

Similarly, later on you have some h'∈ℕ[≤k]→S and can easily construct ( ℕ[≤k+1] x ↦ ( x≤k ? h'(x) : f(h'(k)) ) ).

@user21820 I am not quite familiar with that "?" notation yet.

Yes I'm using the conditional expression. If you don't like it, you have two options:

First option is to define new function-symbol e0 such that ∀x∈[≤k+1] ∃!y∈S ( ( x≤k ⇒ e0(x) = h'(x) ) ∧ ( x = k+1 ⇒ e0(x) = f(h'(k)) ) ), and then construct ( ℕ[≤k+1] x ↦ e0(x) ).

This is completely without set theory, so it is in my opinion conceptually preferable.

Second option is to use a bit of set theory like you were attempting, but your use of "union" is unclear. It's definitely not what the Union axiom of ST provides.

@user21820 I have to think about this. Maybe I have messed up somewhere.

@Prithubiswas You want to construct h'⋃⟨k+1,f(h'(k))⟩. This is { ⟨x,y⟩ : x∈ℕ[≤k+1] ∧ y∈S ∧ ( x≤k ⇒ y = h'(x) ) ∧ ( x = k+1 ⇒ y = f(h'(k)) ) }. I presume you know by now how to translate such notation to the base system, namely { t : t∈ℕ[≤k+1]×S ∧ ∃x,y∈obj ( ⟨x,y⟩ = t ∧ ... ) }.

@Prithubiswas Oh whoops I messed up, not you. Your use of Union is fine... I just got confused by your proof. As I said, use the clean let syntax.

If you want to say "Let g'' = Union({h',h''})" just say that.

I guess your use of Union is conceptually better than my use of Comprehension.

I was just blindly translating the set-theory-less approach to ST, which as you can see is a systematic translation.

@Prithubiswas In case it isn't clear, any usage of a conditional expression ( E ? x : y ) can be translated to definitorial expansion and function-notation. You just need to define an appropriate new function-symbol (as I did above) to represent that conditional expression and then use function-notation to finish.

Okay I will read up all of this and come back to you if I don't understand something.

Sure.

The key point is that if you want a concrete set-representation of what you're doing to extend the function by one input, then the Union-based approach you were trying is probably the best, but do use the cleaner syntax.

But if you want the conceptual core of what you're doing, not restricted to a set theory foundation, then the function-notation approach (especially with conditional expressions) is the best, because it clearly says exactly what you're doing.

@Prithubiswas: By the way, did you just turn into a baby (your new avatar)? =P

Buraian also asked the same question lol.

@Prithubiswas Lol.

*portrays.

And I'm not an expert either. I'm somewhere in-between graduate-level and expert.

@Prithubiswas Lol it isn't; I accidentally mixed both the condition and the result of definitorial expansion.

∀x∈[≤k+1] ( ( x≤k ⇒ e0(x) = h'(x) ) ∧ ( x = k+1 ⇒ e0(x) = f(h'(k)) ) ).

Yeah just a minor typo.

Allowed because ∀x∈[≤k+1] ∃!y∈S ( ( x≤k ⇒ y = h'(x) ) ∧ ( x = k+1 ⇒ y = f(h'(k)) ) ).

@user21820 To me , the difference between an expert and a novice is that , an expert can fix his/her mistake on there own and the novice can't.

@Prithubiswas Nah, that's not "expert", just "competent".

I think a good rule of thumb is that one needs roughly 1000 hours of related effort to reach competence, and roughly 10000 hours to reach expertise.

@Prithubiswas You'd have to test them to know.

@user21820 What about multiple nested conditionals?

@Prithubiswas It doesn't matter. As long as your newly defined function-symbols have the same inputs as the function you wish to define, then whether they are nested or not won't prevent you from translating.

@user21820 I meant what the syntax would look like.

Oh. Like sgn = ( ℝ x ↦ ( x = 0 ? 0 : ( x > 0 ? 1 : −1 ) ) ).

I'm sure you've seen the multiline version that most mathematicians use, right?

@user21820 Which thing are you referring to?

You mean this ?

@Prithubiswas Yes I was just going to give you an example. The point is that the usual multiline notation can also be nested. There is no conceptual difference except that the 1-line notation is 1-line.

@user21820 I now like the conditional notation because it is compact and easy to read than multiple if and conjunction statements.

If we wanted to translate it we have to have three seperate cases in conjunction.right?

@Prithubiswas Right, that's the best way without conditional expressions, which is why I called it "still ugly". Ironically, having 3 or more cases does make the conditional expression look slightly ugly, but it's so rare to need more than 2 cases that it doesn't really matter much.

In fact, some programming languages drop brackets around conditional expressions and give the right-most one the highest precedence. For example in javascript it would be "sgn = function(x) { return x==0 ? 0 : x>0 ? 1 : -1; }".

So it's no wonder that my notation looks almost identical; I'm borrowing the best syntax from programming!

Also worth noting is that when people use the multiline notation they usually give the condition for each case, like you just saw on wikipedia. Technically, such definition would only be well-defined if those conditions are disjoint and cover the whole domain, so logically there is a bit of handwaving sometimes. To see what I mean, see Wikipedia's definition of Thomae's function.

@user21820 So the handwaving part is "Since every rational number has a unique representation with coprime..." ?

@Prithubiswas Yep.

@user21820 But isn't that a different kind of handwaving than "Technically, such definition would only be well-defined if those conditions are disjoint and cover the whole domain" ?

@Prithubiswas It's not really different. For sgn, you need ∀x∈ℝ ( x < 0 ∨ x = 0 ∨ x > 0 ). For Thomae's function, you could split by ( rational or irrational ), but you then need ( rational ⇔ exists unique reduced fraction with positive denominator ).

Hi. I am having a hard time proving AC implies Zorn's lemma. If you'd taken a close look at the topic, what good reference article do you recommend to read? I really want to understand the essence of AC!

@user21820 OK... before getting into your proof, is < a strict partial order?

I mean, Zorn's lemma is not necessarily about strict partial order, right?

@Hermis14 Yes, that's what "<" always means, otherwise we would use "≤".

@Hermis14 "≤" is nothing more than "< or =", so it doesn't really make sense to say Zorn's lemma is not necessarily about strict partial orders.

I think I don't get the point... If the poset of interest is $(S, \le)$, the corresponding proof will also apply to the case of $(S, <)$ but not vice versa? (because the former condition is weaker than the latter?)

@Hermis14 I don't get what you don't get. As I said, "≤" is nothing more than "< or =", so any theorem about non-strict partial orders can obviously be translated to a theorem about strict partial orders. Not just Zorn's lemma. So what's the problem?

No problem, sir! I sometimes forget that identity relations are taken for granted.

@Hermis14 Why do you assume I'm a "sir"? Just use my username. As for equality, although in modern mathematics any FOL structure is assumed to have equality, it's not even needed here because "<" can be translated to "≤ and not ≥" to go from strict to non-strict.

I didn't mean to offend you. My bad. I am not good at English as you might notice.

Wait I take back what I said about equality not being needed; stating Zorn's lemma for (S,<) does require "=".

Since you don't seem familiar with this, you probably should leave Zorn's lemma aside and first prove the basic stuff about partial orders. Specifically relevant here is:

> (1) Take any partial order (S,<). For each x,y∈S define x ◁ y ≡ x < y ∨ x = y. Then (S,◁) is a non-strict partial order.

> (2) Take any non-strict partial order (S,≤). For each x,y∈S define x ≪ y ≡ x ≤ y ∧ ¬ y ≤ x. Then (S,≪) is a strict partial order.

Definitions of strict/non-strict partial orders should be easy to find on wikipedia.

Given S1 ∈ set
	Given c1 ∈ S1
		Given f1 ∈ S1→S1
			Q(m) ≡ ∃g ∈ ℕ[≤m] → S1 ( g(0) = c1 ∧ ∀n ∈ ℕ[<m] ( g(n+1) = f1(g(n)) )
			Let g' = ( ℕ[≤0] k ↦ c ).
			g'(0) = c1 ∧ ∀n ∈ ℕ[<0] ( g'(n+1) = f1(g'(n))
			Q(0)
			Given k ∈ ℕ
				If Q(k)
					∃g ∈ ℕ[≤k]→S1 ( g(0) = c1 ∧ ∀n ∈ ℕ[<k] ( g(n+1) = f1(g(n)) )
					Let h' ∈ ℕ[≤k]→S1 such that h'(0) = c1 ∧ ∀n ∈ ℕ[<k] ( h'(n+1) = f1(h'(n)) )
					Let h'' = ( ℕ[≤k+1] x ↦ ( x≤k ? h'(x) : f(h'(k))) )
					h'' ∈ ℕ[≤k+1]→S1 ∧ h''(0) = c1 ∧ ∀n ∈ ℕ[<k+1] ( h''(n+1) = f1(h''(n)) )

@user21820 Does it look good now?

@Prithubiswas Indeed that's the right outline, except you missed a ")" at line 6. The conditional expression can be handled using the following rules:

Then it should be clear that all the intermediate steps can be easily formally proven.

So you can see that you have the first part of the recursion theorem, namely the existence of finite approximations of arbitrary length.

@user21820 Now we have to take the union of all of the finite sequences?

Right! Now all that remains is to glue them together, and for this you cannot avoid some foundation-aware steps (in contrast to the previous reasoning which is more or less foundation-agnostic). In ST we can use Union or Comprehension.

To be clear, you have proven this:

Now you can construct h = Union( { g : g⊆ℕ×S ∧ ∃k∈ℕ ( g∈ℕ[≤k]→S ∧ g(0) = c ∧ ∀n ∈ ℕ[<k] ( g(n+1) = f(g(n)) ) } ).

Here "g⊆ℕ×S" is of course "g∈Pow(ℕ×S)" where "Pow" stands for powerset.

@user21820 Well , it seems like we need both Union and Comprehension.

Comprehension to contruct the set , union to take the union.

Actually you don't need Union. It's just that "glue" invokes the idea of "union".

@user21820 Is there a unionless approach?

You can use just comprehension: Let h = { ⟨k,x⟩ : k∈ℕ ∧ x∈S ∧ ∃g∈ℕ[≤k]→S ( g(0) = c ∧ ∀n ∈ ℕ[<k] ( g(n+1) = f(g(n)) ) }.

No matter which way, you would have to do a bit of work to prove that h∈ℕ→S. Once you do that, then the desired result follows quite fast from the definition of h.

Anyone know how to find out, how many times a line touches a circle (0, 1 or 2 times) solely using a vector, "v", a point on the line, "P", and the equation for the circle, "C"?

This idea of gluing compatible pieces is very general. It is exactly the core idea behind the proof I linked earlier of Zorn's lemma.

@NemanjaVuksanovic What did you try?

@NemanjaVuksanovic It seems someone has already addressed your question. However, if you want a more geometric approach, first translate the circle and line such that the circle centre is now at the origin, and then all you need to know is how far the line now is from the origin.