How to give formal proof in logic?

I am taking a course on mathematical logic and am struggling to give formal proofs of theorems or claims. Currently doing first order logic. Here, an example:

Claim: $\models (\exists x)\big(A(x)\Rightarrow (\forall y)(A(y))\big)$

where $A$ is an unary predicate. I am asked to prove this. This is how I would reason:

By the rule of propositional logic $P\Rightarrow Q$ is equivallent to $\neg P\vee Q$. So we wish to show that $$\models(\exists x)\big(\neg A(x)\vee (\forall y)(A(y))\big)$$
So, assume we have an arbitrary interpretation of language $\mathcal{L}=\{A\}$, that is a nonempty set $M$ together with unary predicate $A$.. By Tarski's definition of truth, there is some $m\in M$ for which is $\neg A(m)$ or for all $n\in M$ $A(n)$ holds. But this is clearly true (logically valid). Because whenever there is some $m\in M$ for which $\neg A(m)$, then the formula is satisfied. If not, then for all $n\in M$ for which $A(n)$, which makes it also satisfied.

Now, I am wondering whether this can be taken as a formal proof of the claim that the formula is logically valid in any interpretation of the language $\mathcal{L}=\{A\}$. It seems really trivial, but I am afraid I am using too much of set theory.

Another reasoning could be: In fact, when $A$ is an unary predicate, that means $A$ is a subset of $M$. Now distinguish two cases: 1. $A=M$, then $(\forall y)((y\in M) \Leftrightarrow (y\in A))$ in other words $(\forall y)(A(y))$. If $A\subsetneq M$ then it is clear there is some $m\in M$ that is not in $A$, in this case the part $(\exists x)(\neg A(x))$ is true. Now, this uses the definition of equality between sets and what is a subset.

Another idea: Using a contradiction. Assume this was not logically valid, so there exists some interpretation $\mathcal{M}$ and value assignment $e$ for which $\mathcal{M}\models \neg(\exists x)\big(A(x)\Rightarrow (\forall y)(A(y))\big)$, that is $\mathcal{M}\models(\forall x)(A(x)\wedge (\exists y)(\neg A(y))$, thus for all $m$ $\mathcal{M}\models A(m)\wedge (\exists y)(\neg A(y))$, by definition again there is some $n\in M$ for which $\mathcal{M}\models A(m)\wedge \neg A(n)$, this gives $\mathcal{M}\models A(n)$ (the $n$ must be one of all of the $m$'s) but also $\mathcal{M}\models \neg A(n)$. Which is contradiction by the law of excluded middle, so the statement before was logically valid.

Or just by looking: It is clear that either for all $x$ $A(x)$ holds, or there is some $x$ for which $A(x)$ doesn't hold...

All this seems like a handwaving...

So, what tools/methods/kind of reasoning should I use at most when proving such claims and theorems in logic/model theory? I would be grateful for opinions and/or more examples (sources).

Answer

Your proof is correct. You used the mathematical definitions of all the terms involved, like "valid", "interpretation", and "true in an interpretation" and came up with a rigorous argument that the statement was in fact valid according to those definitions.

People often are under the mistaken impression that just cause we're studying logic, we need to stop being mathematicians and turn into C++ compilers. (Mathematical) logic is a branch of mathematics like any other, where we argue informally$^*$ but rigorously about mathematical constructions. It's just that in the case of logic, our arguments are often about formal proofs, which are themselves mathematical constructions. However, in a certain sense, the whole point of semantics and model theory is to eschew formal proofs and to instead think about sentences in their 'plain meaning' within mathematical structures they might talk about.

Semantics do require stronger philosophical precepts than syntactical proofs (as you allude to, there is some set theory involved). You could also construct a formal proof of your statement in some proof calculus for first order logic, and such a construction would only involve finitary ideas. If we do this we would say that $\vdash (\exists x)\big(\neg A(x)\vee (\forall y)(A(y))\big)$ (with a $\vdash$ meaning "provable (in some given deductive system)" rather than a $\models$ meaning "valid").

Remarkably, the standard proof systems for first order logic are complete and sound, i.e. they can prove a sentence if and only if it is semantically valid, i.e. $\vdash \phi\iff \models\phi$. While formal proofs are less of a philosophical burden, as a practical matter it is generally harder to construct formal proofs than to make semantic arguments. But formal proofs are very important philosophically, especially if you're worried about foundational matters. They are also interesting objects of study in their own right. (And the notion that “true in all models” and “effectively provable in a formal system” are equivalent is particular to first order logic, anyway.)

$^*$Here we might have a clash of terminology between the way you’re using the term "formal" vs the way logicians typically use the term. To a logician, a formal proof of a logical sentence is a mathematical object constructed according to some formal mathematical rules for proof construction. A rigorous natural language argument that a certain mathematical statement is true is an informal proof, regardless of how water-tight and well-explained the reasoning is. (Although you will still hear logicians occasionally use 'formal' to mean 'careful / detailed / rigorous'). Formal proofs are meant as models of well-reasoned arguments, and of course the more careful / detailed / rigorous - ly an informal proof is phrased, the easier it is to imagine it being translated into a formal proof in some suitable system.