THIS QUESTION IS NOT A DUPLICATE OF THESE ONES!!!
- $\exists x. P(x) \to\lnot \forall x. \lnot P(x)$
- $\neg \forall x P(x) \leftrightarrow \exists x \neg P(x)$
- $\forall x P(x) \vdash \exists xP(x)$
- $\lnot\exists xP(x)\rightarrow\forall x\lnot P(x)$
- $\forall x\neg P(x) ⊢\neg \exists xP(x)$
So on the first chapter of the text Set theory for the mathematician by Jean E. Rubin there is a brief summary of mathematical logic and there it is stated that the double implications $$ \Big(\big(\neg(\exists x)\big)P(x)\Big)\iff\Big((\forall x)\big(\neg(P(x)\big)\Big) $$ and $$ \Big(\neg\big((\forall x)P(x)\big)\Big)\iff\Big((\exists x)\big(\neg(P(x)\big)\Big) $$ are tautology but this is not proved so that I thought to ask a question where I ask how prove them using propositional calculus. Actually here I found a possibile answer but unfortunately I did not understood: indeed, although I perfectly know Law of Excluded Middle (LEM) and although I know I can do some "algebraic" manipulation with symbol $\neg$, $\wedge$ and $\vee$ I did not understand the linked proof; moreover, even here I found a possibile answer but (I do not really why) I feel like it is not rigorous. Finally, I admit it is not completely clear the meaning of universal quantifier by Rudin arguments: indeed, I surely can realize that the sentence $(\exists x)\big(P(x)\big)$ "exists any $x$ with respect $P$ is true" is a primitive so that I would define $(\forall x)\big(P(x)\big)$ true whether $\exists x\to P(x)$ is a tautology but I do not really know if this is rigorous.
Anyway I understanding the proof can require some particular notions in Mathematical Logic so that I even ask a textbook where I can study into 50-100 pages the most important results to apply rigorously the more common and "natural" logical arguments: it seems to me that into the first two chapter of this textbook there is what I looking for but I am not sure it actually presents the subject rigorously.
So could someone help me, please?
N.B:
Obviously if you believe that by Rudin's rudiments I can actually understand any answer I linked above you can try to explain it here better so that I can understand it.
Every example you provided is either not a formal proof or not a proof using propositional logic (PL) alone. You could certainly construct an informal, intuitive explanation for why these equivalencies hold true, but a formal proof of the equivalencies
$\neg \exists x P(x) \leftrightarrow \forall x \neg P(x)$ and $\neg \forall x P(x) \leftrightarrow \exists x \neg P(x)$
requires first-order logic (FOL). This is because the equivalencies depend on the internal grammatical structure of the formulas involved, and PL does not possess the necessary machinery for abstracting the internal grammatical structure of formulas. PL is only useful for representing an argument whose validity depends on the relative arrangement of the formulas involved.
On the other hand, FOL does possess the necessary machinery for representing the internal grammatical structure of formulas, particularly those asserting one of the following: $(1)$ that all, none, or some elements of a given domain possess (or do not possess) certain properties, or $(2)$ that all, none, or some elements of a given domain bear (or do not bear) some relation to all, none, or some elements of the domain. Those branches of FOL dealing with $(1)$ and $(2)$ are known as monadic FOL and polyadic FOL, respectively.
That is not to say that some arguments in the language of FOL cannot be proven using PL alone. Indeed, some arguments in FOL can be proven in PL alone. However, the validity of such arguments must depend on the relative arrangement of the formulas involved and not the internal grammatical structure of the formulas. For instance, a proof of $\forall x Px \to \exists x Qx, \forall x Px \vdash \exists x Qx$ requires nothing more than Modus Ponens, an inference rule of PL. Proving an argument in a "higher-level" formal system, such as FOL, using only the inference rules of a "lower-level" system, such as PL, is referred to as shallow analysis.
In order to understand or construct a formal proof of the equivalencies you provided, you need to learn PL and monadic FOL at a minimum. FOL is a generalization of PL that $(a)$ inherits all inference rules of PL and $(b)$ defines a few more inference rules, namely, elimination and introduction rules for the quantifiers $\forall$ and $\exists$. Polyadic FOL deals with relational predicates and requires two more inference rules, that is, identity introduction and identity elimination, but polyadic FOL is not necessary for proofs of the above equivalencies. Any textbook covering PL and FOL will give you the necessary background. I recommend A Concise Introduction to Logic by Hurley ($13$th ed).