I'm studying the inference rules of natural deduction for the first-order logic. I cannot understand why universal introduction and existential elimination are valid rules. The first one says that if $\Sigma\models\theta[k/x]$ then $\Sigma\models\forall x\theta[x]$; the second one says that if $\Sigma\models\exists x\theta[x]$ then $\Sigma\models\theta[k/x]$.

Universal introduction would allow the following deduction: if $1$ is odd, then every number is odd. Existential elimination would allow the following deduction: if there exists an odd number, then $2$ is odd.

I read about some restrictions you should check before applying such rules, but they are also not so clear to me.

Some notes about the notation I used: $\Sigma$ is a set of sentences; $\theta$ is a formula such that the only free variable is $x$ and such that $x$ is not in the set of bounded variables; $\theta[k/x]$ is the formula you obtain from $\theta[x]$ by substituting every free instance of $x$ with $k$; of course, $x$ is a variable and $k$ is a constant.


  • 3
    $\begingroup$ Certainly 1 is not a free variable. $\endgroup$ – Harry Gindi Feb 4 '10 at 13:20

You are getting tripped up by some very traditional, yet very bad, notation.

The $k$ in these formulas are not true constants of the domain of individuals, but rather are Skolem constant. The idea is that if we have, say, the knowledge that an existential formula $\exists x. \theta(x)$ is true, we can treat it as if it were the formula $\theta(k)$, where $k$ is some particular arbitrary constant about which we know nothing. Conversely, if we know that $\theta(k)$ holds for any arbitrary constant $k$, then we can conclude $\forall x.\; \theta(x)$. These made-up constants are called Skolem constants.

If we explicitly manage the free variables with a context of free variables $\Gamma$, then the introduction and elimiantion rules look the way you expect, and agree with Andrej Bauer's rules.

$$\frac{\Gamma; \Sigma \vdash \forall x.\theta(x) \qquad FV(t) \subseteq \Gamma} {\Gamma; \Sigma \vdash \theta(t)}$$

$$\frac{\Gamma, x; \Sigma \vdash \theta \qquad \qquad x \not\in FV(\Sigma)} {\Gamma; \Sigma \vdash \forall x.\; \theta}$$

| cite | improve this answer | |
  • $\begingroup$ Andrej probably just realized that the first question was about introduction, so he deleted all of his answers and comments. $\endgroup$ – Harry Gindi Feb 4 '10 at 13:41
  • $\begingroup$ Well, that seemed like the best thing to do. Why would I spread my own confusion? $\endgroup$ – Andrej Bauer Feb 4 '10 at 13:49
  • $\begingroup$ I wasn't faulting you for it, I was just letting Neel know where your answer went, since he noted your post in his. $\endgroup$ – Harry Gindi Feb 4 '10 at 14:19
  • 1
    $\begingroup$ @NeelKrishnaswami: Do you know any good book or set of notes that uses a coherent notation and deals with Skolem constants? Thanks. $\endgroup$ – Francesco Turco Feb 4 '10 at 14:31
  • 3
    $\begingroup$ But is the notation really bad? Surely this method is used throughout ordinary mathematical practice. For example, a group theorist wants to prove that every group has a certain property, so she says "Let G be a group..." and then proves it just for G. To conclude that every group has the property is exactly the universal introduction rule as stated. $\endgroup$ – Joel David Hamkins Feb 4 '10 at 22:00

In FOL there is no such existential elimination rule which would be generally valid. Although there are some cases where such a rule is indeed valid, for example some logic programs, for arbitrary theories the inference rule does not hold.

A simple counter example is the following theory:

p(a) \/ p(b)

Although we have the following consequence:

p(a) \/ p(b) |= exists x p(x)

We neither have one of the following consequences:

p(a) \/ p(b) |\= p(a)

p(a) \/ p(b) |\= p(b)

Both consequences have a countermodel. For example the first consequence doesn't hold for a model where p(a) is false and p(b) is true. In such a model the disjunction is true, but the first consequence is false. Similarly a countermodel for the second consequence can be found.


| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.