@user21820 Alright, I'd like to move on whenever you have time.

limit(f,a) = v
As d → 0
f(a+d) ≈ v + o(1)
1 / f(a+d)
≈ 1 / (v+o(1))
⊆ 1 / (v+v.o(1))
⊆ 1 / (v(1+o(1))
⊆ (1 / v).(1 / (1+o(1)))
⊆ (1 / v).(1+o(1))
⊆ 1/v + (1 / v).o(1)
⊆ 1/v + o(1)

@Prithubiswas The content is correct, but I personally won't use "≈" since it is actually "∈". I use "≈" for single values on both sides; x ≈ y ≡ x−y ∈ o(1).

Also, take note that your manipulations only work when v ≠ 0.

In your case, it happened at o(1) ⊆ v·o(1).

And if you want to write in Fitch-style, make sure you subsume all the asymptotic notation under the appropriate limiting condition, which in this case is "As d → 0:".

limit(f,a) = v ≠ 0.
As d → 0:
  1/f(a+d) ∈ 1/(v+o(1)) = 1/(v+v·o(1)) = 1/v·1/(1+o(1)) ⊆ 1/v·(1+o(1)) = 1/v+o(1).
Therefore 1/f(a+d) ∈ 1/v+o(1) as d → 0.
Thus limit(1/f,a) = 1/v.

@MaxH I assume that you're completely satisfied with the PL rules, and understand that they are sound? If so, then we can move on. We define a theorem to be a statement that you can deduce in the outermost context (i.e. not under any subcontext). By soundness of PL, every theorem is absolutely true (i.e. true regardless of the truth-values of the PL atoms). When we extend PL to FOL, we want to maintain the same soundness, so you should check that each rule is sound.

As before, you've to try the exercises to learn the finer details.

Note that the post I linked you to is not a 100% formal description of the system, otherwise it would be at least 3 times as long and 5 times as obscure, so if you're not sure whether you can or cannot do something in the system, ask.

Ah, with moving on I meant moving on from last time, where we were discussing the rules as far as I remember.

I think it would also be beneficial to learn something about the language, since I already asked questions as to what it exactly means when I write something like "let $V$ be a vector space" and also I wanted to know about variables, which we have not really discussed yet.

@MaxH Yes we cannot talk about quantifying over vector spaces yet, and it's far more complicated than you might think at first glance. Right now you need to fully internalize how PL's deductive system is sound for PL's semantics (which is how you evaluate the truth-value of a boolean statement given the truth-values of its atoms).

Once you're done with that, and are satisfied with the ⊥ rules, then you should just start solving the exercises (Q1) onwards.

@user21820 My attempt to go backwards:

Express x in terms of y and you should be able to bound x under some extra conditions on ε.

@user21820 This is what I tried to do for (4).

@Prithubiswas Your first line is wrong.

You keep forgetting that the bound is on the absolute value.

So just do what I did instead.

It's not 'rigorous', but it's how you can find the way before checking that it works.

@user21820 Tomorrow, I will start a trip that would last a few weeks. I wish you all the best and thank you for all your teachings and insights ! Stay safe ! I will be back here.

@Prithubiswas Good bye, Prithu ! Good luck with your math journey !

@F.Zer Same to you. Take care and stay safe from the coronavirus!

@user21820 I'll do my best !

See you when you're back! =)

Of course ! I'll be back :-)

@user21820 Ok, so if I understand you correctly, I will again read your post and try to explain to myself why the rules are sound (of PL). Afterwards do the exercises.

@F.Zer Stay safe and healthy, have a good time!

@F.Zer I hope you'll be back

@MaxH Thank you ! The same to you !

@user21820 So in order to do the other exercises I need some knowledge about the language and variables in particular. I think it would be useful to talk about those first, right?

@F.Zer Have a wonder time!

@amWhy Thank you so much ! Best wishes and stay safe !