I am in need of some clarification relating to the rules mentioned. I am doing two different courses on Logic (Philosophy / Computer Science departments) and unforunately they use slightly different vocab for different words.

I was working on the proof for $\exists x\,(x=b\;\land\; P(x))\vdash P(b)$, where $b$ is understood to be some term and $x$ is some "variable". I first wrote the following proof

$\begin{array}{ccc} 1 & &\exists x\,(x=b\;\land\; P(x)) &\text{Premise}\\ 2 &|& b=b\land P(b) &\text{Assumption}\\ 3 &|& P(b) &\land\text{-elimination (2)}\\ 4&&P(b) &\exists\text{-elimination (2-3)} \end{array}$

I understand the $\exists$-elimination rule comes with the side condition that the variable you "assume" exists must be free - but I'm not sure the precise condition. The definitions for this course are:

A variable $x$ is free in $\phi$ if it is not within the scope of a quantifier.

A term $t$ is free for $x$ in $\phi$ if nowhere in $\phi$ does an $x$ variable occur within the scope of any variable that occurs in $t$.

$$ \frac{\begin{array}{ccc} &&\phi[x_0/x]\\ &&\vdots\\ \exists x\phi&&\psi \end{array}}{\psi}\exists\text{-elim} $$ I thought the condition was that we needed $b$ to be free for $x$ in $\phi$, but this seems too easy? The philosophy department only put requirements on $x$ not being a free variable in $\psi$ and the assumptions needed "along the way" in the $\vdots$-bit, and even says that $x$ can be a free variable in $\phi$, totally contradictory to the computer science department...!

My questions are

  1. Is my deduction valid as it is?

  2. What are the precise side conditions of the $\exists$-elim and $\forall$-intro rules, using the definitions I mention?

  3. Are there any side conditions on the $=$ rules? My lecture notes don't mention any but I thought they did? Specifically this one:

    $$\frac{t_1=t_2\quad \phi[t_1/x]}{\phi[t_2/x]}=\text{-elim}$$ for $t_1,t_2$ terms, $x$ a variable.


(edit, I meant to say: the Term* you "assume" exists [...])



Term is a more general syntactical object than variable : a term is a variable or a constant or a "complex" term built-up from "simpler" terms with a function symbol, like $x+1$ in arithmetic, where $x$ is a variable, $1$ is a constant and $+$ is a (binary) fucntion symbol.

Free and free for are two different concepts :

  • an occurrence of a variable is free in a formula if it is not in the scope of a quantifier : in the formula $\exists y(y=x+1)$ we have that the occurrence of $y$ into $(y=x+1)$ is bounded by the leading quantifier $\exists y$ while the occurrence of $x$ is free;

  • a variable $z$ (or a term $t$) is free for $x$ in $\phi$ if there are free occurrences of $x$ in $\phi$ and if the replacement of all occurrences of $x$ in $\phi$ with $z$ (or with $t$) will cause no "capturing" of $z$ (or of variables occurring in $t$) by some quantifier already present into $\phi$. I.e. if we consider again the formula $\exists y(y=x+1)$, we have that $z$ is free for $x$ in it, because the result of the replacement is $\exists y(y=z+1)$ and we have no "capturing", but the $y$ is not for $x$ in it, because the result will be : $\exists y(y=y+1)$ that does not have the same "meaning".

In the $\exists$-elimination rule :

$$ \frac{\begin{array}{ccc} &&\phi[x_0/x]\\ &&\vdots\\ \exists x\phi&&\psi \end{array}}{\psi}\exists\text{-elim} $$

the proviso is :

$x_0$ does not occur in $\psi$, $\phi$ or any undischarged assumption of the subderivation of $\psi$, except $\phi[x_0/x]$.

Of course, if you use a constant $c$ in place of $x_0$, the proviso is the same.

In the $\forall$-introduction rule :

$$ \frac{\phi(x)}{\forall x\phi(x)}\forall\text{-intro} $$

the proviso is :

the variable $x$ may not occur free in any hypothesis on which $\phi(x)$ depends.

Here is an example showing the need for the proviso :

1) $x=0$ --- assumed

2) $\forall x(x=0)$ --- $\forall$-intro : illegal !

3) $x=0 \to \forall x(x=0)$ --- $\to$-intro, discharging 1)

4) $\forall x[x=0 \to \forall x(x=0)]$ --- $\forall$-intro : correct ! there are no assumptions left

5) $0=0 \to \forall x(x=0)$ --- $\forall$-elim.

The conclusion is clearly false in $\mathbb N$.

Here is an example showing the need for the proviso in the $\exists$-elim rule :

1) $\exists x(x=0)$ --- assumed

2) $(x=0)$ --- assumed for $\exists$-elim

3) $x=0$ --- from 2) and 1) by $\exists$-elim, discharging 2) : illegal ! $x=0$ is "the $\psi$" and we have the variable $x$ used in the $\exists$-elim application free in it

4) $\forall x(x=0)$ --- $\forall$-intro : correct ; there are no free occurrence of $x$ in the only assumption left, i.e. into 1)

5) $\exists x(x=0) \to \forall x(x=0)$ --- $\to$-intro.

The conclusion is clearly false in $\mathbb N$.

Regarding your proof, it can be easily "restored" :

$\begin{array}{ccc} 1 & &\exists x\,(x=b\;\land\; P(x)) &\text{Premise}\\ 2 &|& y=b\land P(y) &\text{Assumption for } \exists\text{-elimination : y new}\\ 3 &|& P(y) &\land\text{-elimination (2)}\\ 4 &|& y=b &\land\text{-elimination (2)}\\ 5&&P(b) &=\text{-elimination (3-4)}\\ 6&&P(b) &\exists\text{-elimination (2-5) : y not occurring in it} \end{array}$

  • 1
    $\begingroup$ In $\exists$-elimination you need to assume additionally that $x_0$ is not free in $\phi$ either. $\endgroup$ – Henning Makholm Jun 5 '15 at 15:04
  1. No, that is not valid. In the $\exists$-elimination rule, $x_0$ cannot be an arbitrary term, but must be a new variable that is not free in $\psi$. That means you cannot use $b$ as $x_0$ -- first, $b$ might not even be a variable (it could be a constant symbol or even a term containing function symbol); second, even if $b$ is a variable it is not free in $\psi$ which is $P(b)$ in your attempted application.

  2. You need side conditions that prevent $x_0$ from occurring free in either $\phi$ or $\psi$. If you allow $\phi$ to contain $x_0$ you can derive nonsense by first proving (from whatever set of axioms you're using) that $\exists x.x\ne x_0$, then use $\exists$-elimination to assume $x_0\ne x_0$, derive a contradiction and hence any nonsense you want as $\psi$.

    On the other hand it is right that $x$ (but not $x_0$) can be free in $\phi$ (if it didn't the rule would not be much fun at all).

  3. The $=$ rule you show does not need any side conditions.

  • $\begingroup$ Do you mean to say $b$ is free in $P(b)$, and this is why we can't use it? I will edit in the = rule I had in mind $\endgroup$ – Szmagpie Jun 5 '15 at 14:49
  • $\begingroup$ @Jonas: Well, yes and no. I'm saying that (1) $b$ is not necessarily a variable symbol, but (2) even when it is (for example when $b\equiv y$), this variable symbol would not be free in $P(b)$. $\endgroup$ – Henning Makholm Jun 5 '15 at 14:51
  • $\begingroup$ @Jonas: Note that my first answer to question 2 was horribly wrong. Now fixed. $\endgroup$ – Henning Makholm Jun 5 '15 at 15:01

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.