Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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.

Thanks.

share|improve this question
3  
Certainly 1 is not a free variable. –  Harry Gindi Feb 4 '10 at 13:20
add comment

1 Answer 1

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

share|improve this answer
    
Andrej probably just realized that the first question was about introduction, so he deleted all of his answers and comments. –  Harry Gindi Feb 4 '10 at 13:41
    
Well, that seemed like the best thing to do. Why would I spread my own confusion? –  Andrej Bauer Feb 4 '10 at 13:49
    
I wasn't faulting you for it, I was just letting Neel know where your answer went, since he noted your post in his. –  Harry Gindi Feb 4 '10 at 14:19
1  
@NeelKrishnaswami: Do you know any good book or set of notes that uses a coherent notation and deals with Skolem constants? Thanks. –  Francesco Turco Feb 4 '10 at 14:31
2  
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. –  Joel David Hamkins Feb 4 '10 at 22:00
show 4 more comments

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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