I used "Introduction to Mathematical Logic" by Mendelson, but it may not be the best choice. I am not sure about newer editions, but it used Hilbert proof calculus, which is extremely difficult to use in practice. Also, its proofs of GŲdel's completeness and incompleteness theorems were detailed, but pretty dense and not very illuminating.
I would say that the meaning of "I don't like everyone" is similar to that of "I don't like someone," however strange this may seem. Granted, there is an a priori ambiguity concerning the place of the universal quantifier ("everyone") with respect to the negation. I found an article "Navigating negative quantificational space" that says the following (pp. 3-4). When a universally quantified noun phrase is the subject, as in "Every student didnít solve the problem," then there is indeed an ambiguity. (I've often seen this interpreted as "Not every student solved the problem," but I personally much rather prefer the latter way of saying this.) However, the article says that when a universally quantified phrase is in object position, there is no ambiguity and the quantifier is inside the scope of negation, so "The students didnít solve every problem" is interpreted as "It is not the case that the students solved every problem."
However, the article also claims that the "some" in the object position must be interpreted outside the scope of negation. So, "John didnít see some students" means "There are some students that John did not see." Interestingly, "any" is left inside negation: "John didnít see any students" means "It is not the case that John saw some students."
You are right that the left-hand side should start with \neg\forall, not \neg\exists, as in the OP. The scope of the universal quantifier should be the rest of the statement. Then we have the following.
~∀x (P(x) -> ∃y (M(x,y) /\ Q(y))) <=>
∃x ~(P(x) -> ∃y (M(x,y) /\ Q(y))) <=>
∃x (P(x) /\ ~∃y (M(x,y) /\ Q(y))) <=>
∃x (P(x) /\ ∀y ~(M(x,y) /\ Q(y))) <=>
∃x (P(x) /\ ∀y (M(x,y) -> ~Q(x,y)))
In this problem we are using equivalences, e.g., ~∀x P(x) <=> ∃x ~P(x). I am not sure what UE and UI stand for, but if it is universal elimination and universal introduction, then those are things of completely different nature. In any case, quantifier rules are propositional rules are sufficient to derive any true formula.
The proof in post #21 used the following equivalences:
~∀x P(x) <=> ∃x ~P(x)
~∃x P(x) <=> ∀x ~P(x)
~(A /\ B) <=> A -> ~B
~~A <=> A
However, I think that you may be asking a more historical type question.
A question that has many centuries of thought behind it.
Here is a good reference to The Square of Opposition.
natural deduction (ND) in mind. However, the following:
confuses me. If you are talking about ND, then it is not "any" system; it is a specific system. Also, it is not axiomatic; it uses inference rules instead of axioms. If, on the other hand you take some system like Hilbert calculus, then it does not have introduction and elimination rules.In any system whether axiomatic or not
Could you state more precisely which calculus you are using? For example, are your rules similar to the ones from the ND link above?
Here is a Fitch-style natural deduction derivation of ∃x ~P(x) from ~∀x P(x). The other direction is easier because it does not use double-negation elimination.
Code:~∀x P(x) ~∃x ~P(x) ~P(x) ∃x ~P(x) ⊥ ~~P(x) P(x) ∀x P(x) ⊥ ~~∃x ~P(x) ∃x ~P(x)
For example instead of x we could have used, a ,for Antony and proceed in part of the proof as follows:
...........................Let Pa stand for : Antony is a phony
Hence : and
Thus we proved that:
IF Antony is not phony ,then every body is phony
Is that reasonable??