One intuitive explanation for $\bot$ is "I am insane". Thus, the rule:
Given $A$ and $\neg A$, one may infer $\bot$
expresses that:
Accepting something as true and false at the same time is insane.
And when we're insane, nothing is out of the question, so we obtain $\bot$-elimination:
Given $\bot$, one may infer $A$, for any $A$.
The distinction between RAA and $\neg$-I is a bit more subtle. For the purpose of classical logic, we may treat them as the same. We may do this due to the acceptance of the following:
"Something is either true or false": $A \lor \neg A$. Equivalently, $\neg \neg A \leftrightarrow A$ ("if something is not false, then it must be true").
In this sense, the distinction between RAA and $\neg$-I is indeed syntactical, and semantically, there is no difference.
However, in different semantics, such as Intuitionistic Logic, the rule mentioned above does no longer hold. This is because in intuitionism, one only accepts $A \lor B$ as true when one knows which of $A$ and $B$ holds (more accurately, that we either have proven $A$, or have proven $B$). We take the expression $A \to \bot$ a definition of $\neg A$ ("$A$ is demonstrably false").
Now, there is a difference between the two:
- "Given $A \to \bot$, then $\neg A$" ($\neg$-I) is tautologous;
- "Given $\neg A \to \bot$, then $A$" does not hold. Suppose that $A = B \lor C$. Then $\neg A \to \bot$ expresses "$B$ and $C$ cannot both be false". However, a proof of $A$ now requires proving one of $B$ or $C$, but $\neg A \to \bot$ provides us no clue as to which of $B$ and $C$ could be provable.
If you enjoy logic, I encourage you to study intuitionistic logic and its bewildering implications once you've got a firm understanding of classical logic.
Unfortunately, different formal proof systems will do things differently .... but here is how the book I am using ('Language, Proof, and Logic') defines these rules:
First, the system makes the difference between constants and variables by declaring letters in the beginning of the alphabet ($a$, $b$, $c$, ...) to be constants, and letters at the end ($x$, $y$, $z$) to be variables.
With this difference in mind, we can immediately make sense of the following two formal inference rules:
Existential Introduction
$P(a)$
$\therefore \exists x \ P(x)$
This rule says that if some specific object has property $P$, then we know that there is some object that has property $P$ ($P$ here can of course be any property (formula) ... and the $a$ is any constant (variable-free term)
Universal Elimination
$\forall x \ P(x)$
$\therefore P(a)$
This rule says that if everything has property $P$, then any specific one object will have property $P$
Ok, now let's do Universal Introduction. So, here is where you want to be able to prove that all objects have property $P$. How to do this? The strategy the LPL book uses is to say: "Let $a$ be some arbitrary object from the domain. Now, if we can prove that this $a$ has property $P$, then given that we assumed nothing about this object other than that it is some object of the domain, it must be true that all objects have property $P$"
Formalized, this is what it looks like:
Universal Introduction
$\quad a$
$\quad ...$
$\quad P(a)$
$\forall x \ P(x)$
So, notice that we are using a subproof structure here. Indeed, the line with $a$ is not a claim, hut rather a kind of assumption that effectively says "let $a$ be an arbitrary object from the domain". Also, to make sure that $a$ is indeed an arbitrary object, you have to make sure that when $a$ is 'introduced' at the start of the subproof, the $a$ is not used outside of that subproof; the use of $a$ is thus limited to the scope of the subproof.
The last rule is:
Existential Elimination
$\exists x \ P(x)$
$\quad a \ P(a)$
$\quad ...$
$\quad Q$
$Q$
Ok, so here we are also using a subproof, and again use that a constant $a$ whose use is limited to the scope of that subproof (i.e. does not occur before or after that subproof). As such, we are once again guaranteed that we are not assuming anything about $a$ other than that it is some object from the domain ... except in this subproof we are assuming that $a$ has property $P$. So, the first line of the subproof basically says: "Let $a$ be one of those objects that have property $P$ (whose existence is guaranteed by the $\exists x \ P(x)$)".
Now, $Q$ is any arbitrary statement (except, it cannot contain any reference to $a$). And, since the subproofs demonstrates that $Q$ be inferred from the assumption that some object $a$ has property $P$, that means that $Q$ also follows from $\exists x \ P(x)$, because the arbitrariness of $a$ makes $P(a)$ not any stronger of a statement than $\exists x \ P(x)$
Hope that helps!
Here are some sample proofs, btw:
\begin{array}{lll}
1&\forall x (P(x) \to Q(x))&Assumption\\
2&\forall x (Q(x) \to R(x))&Assumption\\
3&\quad a&\\
4&\quad P(a) \to Q(a)&\forall \ Elim \ 1\\
5&\quad Q(a) \to R(a)&\forall \ Elim \ 2\\
6&\quad \quad P(a)&Assumption\\
7&\quad \quad Q(a)&\to \ Elim \ 4,6\\
8&\quad \quad R(a)&\to \ Elim \ 5,7\\
9&\quad P(a) \to R(a)&\to \ Intro \ 6-8\\
10&\forall x (P(x) \to R(x))&\forall \ Intro \ 3-9\\
\end{array}
Note that in the above proof it is important to first introduce the cnstant used for the universal proof (line 3) and then instantiate the universals with that constant (lines 4 and 5); had you put lines 4 and 5 before line 3 then the $a$ would occur outside the scope of the subproof to which its use should be restricted.
\begin{array}{lll}
1&\exists x \ P(x)&Assumption\\
2&\forall x (P(x) \to Q(x))&Assumption\\
3&\quad a \ P(a)&Assumption\\
4&\quad P(a) \to Q(a)&\forall \ Elim \ 2\\
5&\quad Q(a) & \to \ Elim \ 3,4\\
6&\quad \exists x \ Q(x)& \exists \ Intro \ 5\\
7&\exists x \ Q(x)&\exists \ Elim \ 1,2-6\\
\end{array}
Also in this proof we made sure to do the universal elimination (line 4) after the introduction of the temporary constant (line 3) used to set up the existential elimination. This is something you will learn very quickly: whenever presented with both an existential and a universal, instantiate the existential before the universal.
OK! One more:
\begin{array}{lll}
1&\exists x \ \neg P(x)&Assumption\\
2&\quad \forall x \ P(x)&Assumption\\
3&\quad \quad a \ \neg P(a)&Assumption\\
4&\quad \quad P(a)&\forall \ Elim \ 2\\
5&\quad \quad \bot & \bot \ Intro \ 3,4\\
6&\quad \bot & \exists \ Elim \ 1,3-5\\
7&\neg \forall x \ P(x)&\neg \ Intro \ 2-6\\
\end{array}
This one is interesting in that it shows that you can 'pull out' a contradiction using Existential Elimination.
All right, last one:
\begin{array}{lll}
1&\exists x \ \forall y \ R(x,y)&Assumption\\
2&\quad a \ \forall y \ R(a,y)&Assumption\\
3&\quad \quad b & Assumption\\
4&\quad \quad R(a,b) &\forall \ Elim \ 2\\
5&\quad \quad \exists x \ R(x,b)& \exists \ Intro \ 4\\
6&\quad \forall y \ \exists x \ R(x,y)& \forall \ Intro \ 3-5\\
7&\forall y \ \exists x \ R(x,y)&\exists \ Elim \ 1,2-6\\
\end{array}
Cool ... it uses all four quantifier rules!
Best Answer
tl;dr In the first section I explain what you need to do. In the second section I explain the importance of doing this. Since you didn't want to see the solution, in the third section I give the solution of a similar (but not identical) example problem.
I. The existential quantifier satisfies two rules. The first is existential introduction $\exists$-I, which allows you to start from the premise $A(t)$, and arrive at the conclusion $\exists x. A(x)$.
The exercise is asking you to show that you can still do the same thing if you have $\neg\forall\neg$ in place of $\exists$: i.e., you can start from the premise $A(t)$, and eventually arrive at the conclusion $\neg\forall x.\neg A(x)$, while using only the rules of the universal quantifier ($\forall$-I, $\forall$-E) and the negation connective ($\neg$-I and some classical rule, probably $\neg\neg$-E) at each step.
Similarly, to prove that the $\exists$-E rule is derivable from the rules of the universal quantifier and the rules of negation, you will need to show that starting from $\neg \forall x.\neg A(x)$ and a subproof deducing $C$ from $A(a)$, you can conclude $C$ using only the rules of the universal quantifier and the negation connective at each step.
II. Why does this matter? Because it allows you to eliminate the use of the existential quantifier from every proof/derivation: first you replace $\exists x. A(x)$ with $\neg\forall x.\neg A(x)$ throughout the derivation (which breaks the proof since the rules you apply are no longer valid), then replace each use of the $\exists$-I/E rule with a sequence of $\forall$-I/E and $\neg$-I/E rules (thus repairing the proof).
III. a. Since you don't want to see a solution, let me solve a similar example problem instead.
The introduction rule $\vee$-I1 states that from $P$ you can derive $P \vee Q$. I will show that given the classical rules for $\neg$, the $\vee$-I1 rule is derivable from the rules of $\wedge$, by defining $P \vee Q$ as $\neg (\neg P \wedge \neg Q)$.
The $\vee$-I1 rule lets us start from $P$, and allows us to conclude $P \vee Q$. So we need to show that we can start from $P$, and using only the rules $\wedge$-I/E1/E2, $\neg$-I and $\neg\neg$-E, we can conclude $\neg (\neg P \wedge \neg Q)$.
So start from $P$. Assume $\neg P \wedge \neg Q$. From this assumption, we can get $\neg P$ by $\wedge$-E1. We now have both $P$ and $\neg P$, a contradiction. By $\neg$-I, we can now discharge the assumption $\neg P \wedge \neg Q$ and conclude $\neg (\neg P \wedge \neg Q)$. This is what we had to show: starting from $P$, we concluded $\neg (\neg P \wedge \neg Q)$, using only the rules of $\wedge$ and $\neg$.
III. b. The elimination rule $\vee$-E states that starting from $P \vee Q$, and two subproofs, one deducing $C$ from the assumption $P$, and another deducing $C$ from the assumption $Q$, we can deduce $C$.
I will now show that starting from $\neg (\neg P \wedge \neg Q$), and given two subproofs, one deducing $C$ from the assumption $P$, and another deducing $C$ from the assumption $Q$, we can deduce $C$ using only the classical rules for $\neg$ and $\wedge$.
Call the given subproof deducing $C$ from the assumption $P$ "subproof 1". Similarly, call the subproof deducing $C$ from the assumption $Q$ "subproof 2".
Start from $\neg (\neg P \wedge \neg Q)$. Assume $\neg C$.
Assume $P$. Copy subproof 1 below this assumption to deduce $C$. This contradicts our assumption of $\neg C$, so we can use $\neg$-I to discharge the assumption $P$ and conclude $\neg P$.
Now assume $Q$. Copy subproof 2 below this assumption to deduce $C$. This contradicts our assumption of $\neg C$, so we can use $\neg$-I to discharge the assumption $Q$ and conclude $\neg Q$.
We have derived $\neg P$ and $\neg Q$ above. So we can use $\wedge$-I to deduce $\neg P \wedge \neg Q$. But this contradicts our starting point $\neg (\neg P \wedge \neg Q)$. Therefore, we can use $\neg$-I to discharge the assumption $\neg C$ and get $\neg \neg C$. Finally, we can apply the classical rule $\neg\neg$-E to get $C$, as desired.