The $\forall I$ rule (forall introduction) in Dirk van Dalen's Logic and Structure (4th ed) is:

$${\forall I}\, \frac{\varphi}{\forall x\, \varphi} $$

where the intended restriction is: the variable $x$ may not occur free in any hypothesis on which $\varphi$ depends, i.e. an uncancelled hypothesis in the derivation of $\varphi$.

I have two question concerning this:

  1. ¿ Can we derive $P(x) \vdash \forall x\, P(x)$ ?

    If i write the following derivation: $${\forall I}\, \frac{P(x)}{\forall x\, P(x)} $$ then im not sure if the restriction is fulfilled. Considering that $P(x)$ by itself does not depend on any hypothesis (and it is a premise), im tempted to say yes...

    But, from the defined semantics of the same author (which admits free variables, see Definition 2.8.1 (ii)), we have:

    $$P(x) \not\vDash \forall x\, P(x)$$

    In the same book soundness & completeness is proved, in the general form:

    $$\Gamma \vdash \varphi \ \ \text{ iff } \ \ \Gamma \vDash\varphi $$

    So i think my first derivation can't be right. A related topic of discussion could be what is the meaning of free variables on premises?. At least from the semantical point of view, i think of free variables as arbitrary individuals (some authors like Enderton define a kind of "context" formalized as a valuation function). Anyway, i don't see Van Dalen rejecting the occurrence of free variables in premises of natural deduction (as others do).

  2. Lets compare Van Dalen's $\forall I$ rule with the following more (i think...) frecuently seen variant:

    $${\forall I}\, \frac{\varphi[t/x]}{\forall x\, \varphi(x)} $$

    where $t$ is allowed to be a variable (or even a constant?) with no free occurrence in $\varphi$ or any hypothesis on which $\varphi$ depends (again, this really means uncancelled hypothesis in the derivation of $\varphi$), AND provided that $t$ is substitutable for $x$ in $\varphi$.

    I can see this variant have two restrictions, not only one as in Van Dalen's version. But this rule not forces you to use the same variable as the bounded/quantified and also as the arbitrary individual (sometimes called "parameter") in the derivation. I say this because is common reasoning practice that to prove $\varphi$ is true for every element $x$, we write: Let $c$ be an element...

    Also, this rule subsumes Van Dalen's if im not mistaken, just take $t=x$ and then we have $[x/x]=x$.

    An similar situation occurs for the $\exists E$ rule, we could introduce another variable (or constant) as an unknown individual. But also for this rule in the mentioned book we cant.

    So the second question is, what is the rationale to reuse the same var in the $\forall I$ rule as given in Van Dalen's book?. I don't really care conventions, im more interested in what is more general in some way.

  1. No, because $x$ is free in assumption $P(x)$ and we have that it depends on itself.

See counter-example page 87 : without proviso, we can derive the invalid : $x=0 \to \forall x (x=0)$.

We can check it with the formal definition of derivation [page 33] : a derivation is a tree where the root is the conclusion and the Leaves are the assumptions :

Definition 2.4.1 The set of derivations is the smallest set $X$ such that

(1) The one-element tree $\varphi$ belongs to $X$ for all $\varphi \in \text {PROP}$. [...]

Thus, a single node tree is a derivation where the formula is both the conclusion and the (undischarged) assumption of the derivation.

Compare with : Sara Negri & Jan von Plato, Structural Proof Theory (Cambridge UP, 2001), page 64 :

Usually rule $\forall \text I$ is written as $\frac{A}{\forall x A}$ and the restriction is that $x$ is not free in any of the assumptions that $A$ depends on, where one must keep in mind that if $A$ is an assumption it depends on itself.

About free variables :

what is the meaning of free variables on premises? At least from the semantical point of view, i think of free variables as arbitrary individuals (some authors like Enderton define a kind of "context" formalized as a valuation function).

A free variable acts as a pronoun in natural Language; compare "$x$ is red" with "it is red". Its meaning (and truth value) depends on the context where we assert it.

(One of) The way to formalize a "semantical context" is through a variable assignment function.

  1. In the alternative formulation, we have the same proviso :

$t$ does not have free occurrences in $\varphi$ or any hypothesis on which $\varphi$ depends.

$t$ is a term and thus, as you say, it may be also a variable. But, being not free in $\varphi$, it cannot be $x$ itself, if $x$ occur free in $\varphi$.

  • $\begingroup$ 1. How exactly is that something wich is a premise depends on itself... is it really ovbious? 2. You are right, we cant take $t=x$, because $x$ should not be free in $\varphi$. That means it does not subsumes van Dalen's rule, but then the two are different. $\endgroup$ – fulem Jun 7 at 7:03
  • $\begingroup$ @fulem - no, it is not obvious. See expanded answer. $\endgroup$ – Mauro ALLEGRANZA Jun 7 at 8:12
  • $\begingroup$ Thanks. This is now a very clear answer. Altough, concerning 2, i would appreciate at least a comment or opinion of what you think about the distinct possible formulations of the rule $\forall I$, on one side Van Dalen's rule seems to reuse the same bound variable name as the individual, but on other formulations of the same rule new symbols (not necesary of different syntactic category) are introduced. Have you some opinion on that matter? $\endgroup$ – fulem Jun 7 at 23:10
  • $\begingroup$ @fulem - IMO, Negri-von Plato explanation is a good one. The formulation with $\varphi [t/x]$ is explicitly stated in order to prevent that $x$ is free in the premise of the rule (because - if originally present - we have replaced it with $t$ new). The "simplified" version (used by van Dalen) avoids the substitution but it needs the additional proviso about the "self-dependency", which is not very intuitive. $\endgroup$ – Mauro ALLEGRANZA Jun 10 at 15:21

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.