most recent 30 from http://mathoverflow.net 2013-05-18T17:30:01Z http://mathoverflow.net/feeds/question/14137 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/14137/why-are-universal-introduction-and-existential-elimination-valid-inference-rules Francesco Turco 2010-02-04T13:04:23Z 2010-02-04T13:32:20Z

<p>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]$.</p> <p>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.</p> <p>I read about some restrictions you should check before applying such rules, but they are also not so clear to me.</p> <p>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.</p> <p>Thanks.</p>

http://mathoverflow.net/questions/14137/why-are-universal-introduction-and-existential-elimination-valid-inference-rules/14140#14140 Neel Krishnaswami 2010-02-04T13:32:20Z 2010-02-04T13:32:20Z

<p>You are getting tripped up by some very traditional, yet very bad, notation. </p> <p>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.</p> <p>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.</p> <p>$$\frac{\Gamma; \Sigma \vdash \forall x.\theta(x) \qquad FV(t) \subseteq \Gamma} {\Gamma; \Sigma \vdash \theta(t)}$$</p> <p>$$\frac{\Gamma, x; \Sigma \vdash \theta \qquad \qquad x \not\in FV(\Sigma)} {\Gamma; \Sigma \vdash \forall x.\; \theta}$$</p>