I am trying to better understand the introduction and elimination rules for quantifiers and in particular the syntax / proof system aspect. I'm currently using Fitch-style proofs.
I asked a recent question with a sample proof and got an answer here https://math.stackexchange.com/a/3115673/525966 that I think is a good example.
The rules for $\forall$ and $\exists$ elimination and introduction still confuse me especially since there seems to be a lot of quirky rules about what letters we can use for the… variables, or predicates, or whatever. I honestly can't keep it all straight anymore because I'm so confused. Wikipedia also feels unclear to me. The jump from propositional logic feels massive and rules often seem unclear.
Is there a good explanation somewhere explaining how we can use $\forall$ and $\exists$ introduction and elimination?
Best Answer
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!