@MaxH What does "anything" in English mean?

It is quite hard to explain without further context, don't you think? I mean when you say something like: For anything X is true, then it means that given any "thing"/object X is true about that thing, right?

@MaxH That's not saying anything at all about "anything". I ask you about "anything", and you tell me something using the same word "any thing".

But does it matter? As long as "anything" does not exclude any thing, that is what it means.

Same for "object". I don't care what you define, as long as you can define it, I will say it is an object.

Yes, I see.

So the thing is, I guess, that it doesnt matter what exactly an object is, as long as I only make statements about objects, I can do so.

I hope I formulated this right?

@MaxH What you say is fine, but the point is that there is no reason to think that you can make statements about anything other than objects. Everything is an object.

Yes, that is clear.

@Prithubiswas 1/(1+o(1)) ⊆ 1+o(1). This is usually taken as an axiom in asymptotic analysis. Then given constant v ≠ 0 we would have 1/(v+o(1)) = 1/(v+o(v)) = 1/v · 1/(1+o(1)) ⊆ 1/v · (1+o(1)) = 1/v+o(1).

1/(1+o(1)) ⊆ 1+o(1). (._.)

That was anti-climactic

Alternatively, and more generally, you can take as an axiom 1/(1+x) ∈ 1−x+o(x) for x ≈ 0. Actually you have higher expansions as well, such as 1/(1+x) ∈ 1−x+O(x^2) for x ≈ 0.

From this we get 1/(1+o(1)) ⊆ 1−o(1)+o(o(1)) = 1+o(1). We also get 1/(1+x^3) ∈ 1−x^3+O(x^6) as x → 0.

Asymptotic analysis is basically about using asymptotic expansions as axiomatic, and this can be done rigorously as above. So for this we are actually using the asymptotic expansion for 1/(1+x) for x ≈ 0.

@Prithubiswas As for turning the asymptotic analysis into a proof of the limit theorem, we can apply the same technique as before; we wish to bound the x so as to bound the −x+o(x). One easy way for real analysis is to simply find concrete bounds: 1−x ≤ 1/(1+x) ≤ 1−x+2·x^2 for every x∈ℝ[≥−1/2].

This doesn't work for complex x. For that you would need manipulation of abs.

If you use 1/(1+x) ∈ 1+O(x), then you need abs( 1/(1+x) − 1 ) = abs(x) / abs(1+x) ≤ abs(x) / ( abs(1) − abs(−x) ).

If you use 1/(1+x) ∈ 1−x+O(x^2), then you need abs( 1/(1+x) − (1−x) ) = abs(x^2) / abs(1+x) ≤ abs(x^2) / ( abs(1) − abs(−x) ).

@Prithubiswas: Incidentally, the more general asymptotic expansion can be derived from the 'trivial' 1/(1+o(1)) ⊆ 1+o(1).

For example, for x ≈ 0 we have 1/(1+x) = 1−x+x^2/(1+x) ∈ 1−x+x^2/(1+o(1)) ⊆ 1−x+x^2·(1+o(1)) ⊆ 1−x+O(x^2).

So if you set out to axiomatize asymptotic analysis, you would find that you can get a lot using simple axioms for arithmetic with asymptotic expressions. The ones for addition and subtraction and multiplication are obvious. The above 'trivial' axiom is for division.

@user21820 I think I will try on my own to turn the asymptotic proof into an ε-δ proof.

# ∀x,y ∈ ℝ (abs(x+y) ≤ abs(x) + abs(y))	[triangle inequality]

Given a,b ∈ ℝ

	If 	a ≥ 0 ∧ b ≥ 0 :
		a + b ≥ 0
		abs(a + b) = a + b = abs(a) + abs(b)

	If 	a < 0 ∧ b < 0 :
		a + b < 0
		abs(a + b) = -(a + b)
						= -a + -b
						= abs(a) + abs(b)
		abs(a + b) = a + b = abs(a) + abs(b)

	If 	a ≥ 0 ∧ b < 0 :
		If 	a + b ≥ 0 :
			abs(a + b)	= a + b
							< a + -b [b < 0 < -b]
							= abs(a) + abs(b)
			abs(a + b) < abs(a) + abs(b)

		If 	a + b < 0 :
			abs(a + b) = -a + -b
							≤  a + -b [-a ≤ 0 ≤ a]

@user21820 attempt #1 at proving the Triangle Inequality for abs(x).

@Prithubiswas Looks good. You can factor out the symmetric proof by first proving ∀x,y∈ℝ ( x < 0 ≤ y ⇒ abs(x+y) ≤ abs(x)+abs(y) ) and then applying it twice to get your last two cases.

I discussed this same issue with F.Zer as well:

@user21820 So you mean my proof is correct but I can shorten the symmetric part by using a lemma as you mentioned ?

Right!

@Prithubiswas @F.Zer @MaxH: I just wrote a short time-travel story continuation outline for fun:

Do you see any plot-hole? (Suppressing disbelief about time-travel fixing futures; I have a way to fix that but it's not relevant to the story.)

@user21820 Idk anything about Sci-fi :P

@user21820 Now , what about min(x,y) and max(x,y) ?

@Prithubiswas What about them?

@user21820 That's good ! Bookmarked to read later.

@user21820 I mean , so far we have defined abs(x) . What about the definition of min(x,y) and max(x,y) ?

@Prithubiswas Easiest way is as I described for abs; use definitorial expansion followed by function-notation.

Also, you would need some syntax sugar to deal with multiple inputs.

Formally, min : ℝ^2→ℝ, and "min(x,y)" actually means "min(⟨x,y⟩)".

We can drop tuple-brackets inside a multiple-input function without ambiguity.

Extracting the inputs from the combined input can be done directly; ∀t∈ℝ^2 ∃!m∈ℝ ∃x,y∈ℝ ( t = ⟨x,y⟩ ∧ x ≥ m ∧ y ≥ m ∧ ( x = m ∨ y = m ) ).

This might be considered ugly. A more general solution would be to define projection function-symbols (not functions):

Define the type Pairs = { p : ∃S,T∈set ( p∈S×T ) }. Note that this cannot be a set.

∀p∈Pairs ∃!x∈obj ∃y∈obj ( p = ⟨x,y⟩ ).

Define first : Pairs→obj such that ∀p∈Pairs ∃y∈obj ( p = ⟨first(p),y⟩ ).

∀p∈Pairs ∃!y∈obj ∃x∈obj ( p = ⟨x,y⟩ ).

Define second : Pairs→obj such that ∀p∈Pairs ∃x∈obj ( p = ⟨x,second(p)⟩ ).

∀p∈Pairs ( p = ⟨first(p),second(p)⟩ ).

∀S,T∈set ∀p∈S×T ( first(p)∈S ∧ second(p)∈T ).

Now you can use these freely to unpack any pairs.

∀p∈ℝ^2 ∃!m∈ℝ ( m ≤ first(p) ∧ m ≤ second(p) ∧ ( m = first(p) ∨ m = second(p) ) ).

Define min0 : ℝ^2→ℝ such that ∀p∈ℝ^2 ( min0(p) ≤ first(p) ∧ min0(p) ≤ second(p) ∧ ( min0(p) = first(p) ∨ min0(p) = second(p) ) ).

Define min = ( ℝ^2 p ↦ min0(p) ).

Done.

Now this still looks ugly, because the underlying system does not have conditional expressions, which are well-known to any programmer but somehow didn't make it into logic texts. "( C ? x : y )" is a well-known programming syntax that means ( x if C but y otherwise ). If we had this, we could simply let min = ( ℝ^2 p ↦ ( first(p) < second(p) ? first(p) : second(p) ) ) and be done with it.

Oh well...