5
$\begingroup$

I'm following this online guide to quantifier inference rules for natural deduction [pdf].

Question: I need help as I don't understand two of the rules, $\forall$-intro and $\exists$-elim. I discuss each below.

Attached below is a screenshot of the relevant section of the guide.

$\forall$-intro Rule

The $\forall$-elim rule makes sense. If a property $\varphi$ holds for all $x$ (in a given set) then of course it holds for a particular $x = t$, that is, $\varphi(t)$.

However, my reading of the $\forall$-intro is that if a property $\varphi$ holds for a particular constant $a$, then it holds for all $x$ in the relevant set, $\forall x \varphi(x)$. This does not make intuitive sense to me.

A counter-example is $\varphi \equiv \text{is identically 3}$. So $\varphi(a=3)$ is true, but $\varphi(x=4)$ is false.

$\exists$-elim Rule

The $\exists$-intro rule makes sense to me. If a property $\varphi$ holds for a particular $t$ in a given set, then of course there exists an $x$ such that $\varphi(x)$ holds, namely $x=t$.

However, my reading of the $\exists$-elim rule is that

if

  1. there exists an $x$ such that $\varphi(x)$ holds, and
  2. an assumption of $varphi(a)$ being true (for any $a$ from the relevant set) leads to $\chi$

then $\chi$ holds.

This makes no sense to me. For a counter example, we again use $\varphi \equiv \text{is identically 3}$. The first premise is that there exists an $x$ such that $\varphi(x)$. This a true premise as it holds for $x=3$. The second premise $\chi$ is derived from an assumption that $\varphi(a=4)$ which is not true. Which leads us to prove anything...

What am I misunderstanding?

The guide introduces terminology "Eigenvariable condition" but does not explain it well enough for me to understand.

enter image description here

Improve this question
$\endgroup$

1 Answer 1

Reset to default
8
$\begingroup$

The key is in the side condition that the constant symbol does not appear in any undischarged hypotheses to the proof of $\varphi(a)$: $a$ must be a generic constant that you don't know anything about. In your example, you cannot prove that $a = 3$ without assuming something about $a$. In terms of sequent calculus, the $\forall$-introduction rule says that, if you know $a \mid \psi \vdash \varphi$ and $\psi$ does not mention $a$, then you can conclude $\cdot\mid \psi \vdash \forall a. \psi$. It is more accurate to think of $a$ as a variable, rather than a constant.

Improve this answer
$\endgroup$
3
  • 1
    $\begingroup$ This is helpful. Thank you. Just to check: if $a$ is mentioned in $\psi$ then it is not unconstrained, and therefore $a$ cannot represent any element of the set to which $x$ also belongs, and this in turn prevents us from jumping to "for all $x$". $\endgroup$ Commented Sep 21 at 18:27
  • $\begingroup$ Yes, that is right. $\endgroup$ Commented Sep 21 at 18:51
  • 3
    $\begingroup$ It might be helpful to think of the new constants as temporarily naming an instance of something. E.g., the $\exists$ elimination rule formalizes the following proof idiom: “Since we know there exists an object satisfying $\varphi$, let us fix one such object and call it $a$. ... (proceed to derive $\chi$)”. Or for $\forall$ introduction: “In order to show that all objects satisfy $\varphi$, let us fix an arbitrary object, say $a$, and ... (proceed to derive $\varphi(a)$)”. For that to make sense, we better choose a name $a$ that does not already denote something else in the context. $\endgroup$ Commented Sep 22 at 14:12

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.