0
$\begingroup$

Assume $\Gamma$ is a set of formulas, $P$ a formula, and $\Gamma\vdash P(c)$ has been derived.

The generalization rule states that $\Gamma \vdash \forall x\,P (x)$ can be derived if $c$ does not occur in $\Gamma$.

This is an intuitive rule, since if we can deduce $P(c)$ having no information about the constant $c$, that means $c$ could have any value, and therefore P would be true for any interpretation, that is $\forall x\,P (x)$.

However, I have tried to demonstrate this rule using first order logic, but I think it is impossible since there is no way to directly translate "c does not occur in $\Gamma$" in FOL as far as I know.

What logic system do I need to use in order to demonstrate this?

Where can I find a formal proof for this rule?

$\endgroup$
2
  • 2
    $\begingroup$ In some proof system, like Natural Deduction it is a basic rule. $\endgroup$ – Mauro ALLEGRANZA Apr 12 '20 at 17:20
  • 2
    $\begingroup$ In different proof systems (the so-called Hilbert-style) it is proved using quantifiers axioms. See e.g Enderton, page 117. $\endgroup$ – Mauro ALLEGRANZA Apr 12 '20 at 17:22
1
$\begingroup$

I don't know exactly what it should mean to 'demonstrate this rule using first order logic'. This is a rule of inference... it is part of the metatheory... it is a statement about first order logic, not in it.

There are a couple adjacent things that make sense.

  1. One could prove that it is an admissible inference rule in a given system of first order logic. This would consist of proving that if a deduction of $P(c)$ exists from a $\Gamma$ where $c$ doesn't appear, then a deduction of $\forall x P(x)$ exists. Oftentimes universal generalization taken as a primitive rule, so this is trivial, but sometimes it is not. In any case one would need to know what the rules and axioms of the system are in order to produce such an argument.
  2. One could prove that the rule is sound semantically, i.e. if $P(c)$ is a logical consequence of $\Gamma$, then $\forall xP(x)$ is as well. So let $M$ be an interpretation where $\Gamma$ holds and $y$ in the domain of $M.$ We will show $P(y)$ holds in $M.$ Consider the interpretation $M'$ which is the same as $M$ except $c$ is interpreted as $y$ instead of whatever $M$ had it as. Since $c$ does not appear in $\Gamma,$ $M'$ still satisfies $\Gamma,$ and so by assumption, $P(c)$ holds in $M',$ and thus so does $P(y).$ And $P(y)$ does not contain $c,$ so $P(y)$ holds in $M.$
$\endgroup$
11
  • 1
    $\begingroup$ @mateleco It's a proof that if $\Gamma\models P(c)$ then $\Gamma\models \forall x P(x).$ $\endgroup$ – spaceisdarkgreen Apr 12 '20 at 21:29
  • 1
    $\begingroup$ @mateleco I was thinking of $c$ as a constant, not a variable. But I think you have the right idea (it should just be the intuitive argument, but with attention to the precise definition of satisfaction). $\endgroup$ – spaceisdarkgreen Apr 13 '20 at 14:08
  • 1
    $\begingroup$ @mateleco No, $\Gamma \models P(c)$ would not hold here. For that to be the case, $P(c)$ would need to be true for any interpretation that satisfies $\Gamma,$ not just the one you selected where $P(c)$ is true but $P(k)$ (for some other constant symbol $k$) is false. In particular you could choose an interpretation where $c$ is interpreted as whatever $k$ was interpreted as and $P(c)$ would be false there (and it'd still satisfy $\Gamma$ since $c$ doesn't appear so the change has no impact on $\Gamma$). $\endgroup$ – spaceisdarkgreen Apr 13 '20 at 14:34
  • 1
    $\begingroup$ @mateleco It varies from treatment to treatment. Way I learned it (and what I think is fairly typical nowadays) is that interpretation and variable assignment are kept separate. There are constant, function, and relation symbols in your language whose meaning is defined by the interpretation. This decides the truth value of any sentence (i.e. something without free variables). Satisfaction/validity of a formula with free variables is not defined. But you can add a variable assignment and talk about satisfaction of a formula in reference to a particular variable assignment. $\endgroup$ – spaceisdarkgreen Apr 13 '20 at 16:01
  • 1
    $\begingroup$ @mateleco Now, this doesn't quite play nicely with proof systems that let you derive formulas as well as sentences. But restricted to sentences, the proof system agrees with validity. $\endgroup$ – spaceisdarkgreen Apr 13 '20 at 16:05
2
$\begingroup$

If we are talking about Hilbert-style proof system, this rule is not an inference rule within the theory. A proof of "if $\Gamma \vdash P(c)$ then $\Gamma \vdash (\forall x)P(x)$" would be a meta-proof, i.e. a proof of the sentence about the first-order theory, but not a sentence in the theory.

So an informal proof is as follows. Since $\Gamma \vdash P(c)$, there exists a proof, i.e. a finite sequence of sentences each of which is either an axiom, or a sentence of $\Gamma$, or a sentence derived by inference rule of the theory. Now we pick a new variabe $y$ such that $y$ does not appear in the proof. This is possible because (1) the proof must be of a finite sequence, hence contains a finite number of variables; (2) in a first-order theory, there are infinitely (though countable) many variables. After we pick such a $y$, we replace $c$ by $y$ in the proof, yielding a new finite sequence of sentences. It is not difficult to verify that this new sequence is indeed a proof in the theory. That is, one has to verify that every sentence in this new sequence is either an axiom, or a sentence of $\Gamma$, or dervied by inference rules. Note $\Gamma$ does not contain the constant symbol $c$. So the above verification is possible. Finally, in this new proof, the last sentence must be $P(y)$. Now applying Gen rule, we can obtain $(\forall y)P(y)$. Deriving $(\forall x)P(x)$ from $(\forall y)P(y)$ is straightforward.

The above meta-proof is "informal" because it is stated in English. I think it is possible to formulate the above proof in a first-order set theory, although I'm not certeain. Nevertheless, I think it suffices to accept such an informal proof, just like other meta-proofs and meta-statements that discuss various properties about the subject-matter first-order theory, such as models, consistency, completeness, etc.

$\endgroup$

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.