@F.Zer It's a good attempt. However, there was no need or reason to use the abs function. Earlier you already ought to have known how to handle an equation of the form "E^2 = F". You should have done the same here. Almost all proofs that rely on ∀x∈ℝ ( abs(x) = sqrt(x^2) ) are not the right approach, though it's a bit hard to explain why.

Also, you may have noticed that you didn't actually prove the quadratic formula. Although you can get from your formula to the quadratic formula, it is better to simply avoid division in the first place. From a·x^2+b·x+c = 0 deduce (2·a·x)^2+4·a·b·x+4·a·c = 0 and then (2·a·x+b)^2 = b^2−4·a·c, and then use what I just said above.

@shintuku I didn't mean to suggest you should look at those. I don't think it makes sense for you to look at them at this point, because they are far more complicated systems than the one I gave you (say ≈10 times as much complexity).

@shintuku F.Zer pointed out one error. But in general you are not actually following the rules. For example at line 11 you resort to intuition to deduce the truth value of φ(n,m) from line 10. While your intuition is correct, doing this kind of reasoning completely defeats the purpose of using a deductive system. As I said before, if you don't fully follow the rules, nobody can tell whether you actually know how to do a formal proof, and I am temporarily inclined to believe that you cannot.

An even bigger error is that you seem to believe that your PA1* can be easily obtained from PA1, which is simply wrong.

So I conclude that it would be far better for you now to actually work through the FOL exercises first before even touching PA or set theory.

@F.Zer: I forgot to ask you, independently of my above feedback on your quadratic equation, do you now know why you can get ⊥ when you have x∈ℝ and x^2+x+1 = 0? If not, try following the same reasoning as for the quadratic equation and see when you can apply the simple fact about real squares.

@user21820 Thank you ! I will carefully review your insights and answer your questions.

@user21820 thank you very much for the feedback! and yeah, I seem to be hurrying too much in these.. thanks for the tips, I will do the FOL exercises