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?


1 Answer 1


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


$\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$


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!

  • 1
    $\begingroup$ A constant being "some specific/unique thing we actually know the value of" as opposed to a variable whose status is unknown / could-be-anything? Can we re-use constants as long as we're not overlapping contexts? Like could we use $a$ again in some other subproof after your existential elimination example? $\endgroup$
    – user525966
    Feb 17, 2019 at 1:37
  • 1
    $\begingroup$ @user525966 Yes! We can reuse constants exactly in that manner! I didn't want to add that since I felt it was technical enough already, so I am very glad you made this realisation yourself! :) $\endgroup$
    – Bram28
    Feb 17, 2019 at 1:40
  • 1
    $\begingroup$ And yes, the use of 'constant' is actually a little ambiguous .... outside a subproof the $a$ is used to denote a specific object ... so much like the number $0$ ... but when you use a constant in the temporary context of a subproof for doing universal introduction or existential elimination, it is really much more like a variable ... I compare it to the use of $n$ as in when we do a proof involving numbers and say "Let $n$ be some number" .... it's not a specific number ... and yet it's not quite a variable either .... $\endgroup$
    – Bram28
    Feb 17, 2019 at 1:45
  • 3
    $\begingroup$ Would this be a valid proof then, using these rules? $\begin{array}{lll} 1&\forall x \ P(x) & Hypothesis\\ 2& P(a)& \forall \ Elim \ 1\\ 3&\exists x \ P(x) & \exists \ Intro \ 2\\ \end{array}$ $\endgroup$
    – user525966
    Feb 17, 2019 at 2:13
  • 2
    $\begingroup$ @user525966 Perfect! Note that this proof does have to assume that there is at least one object in the domain so that the $a$ can actually refer to something ... but most logics make that very assumption ... it's called the Assumption of Existential Import. Logics that do not make this assumption are called free logics ... and so in free logics the rules will need to be defined a little differently. $\endgroup$
    – Bram28
    Feb 17, 2019 at 2:16

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .