3
$\begingroup$

I'm reading Mathematical Logic by Stephen Cole Kleene and I am stuck trying to understand the logic behind his rule of universal quantifier introduction.

In the text, for propositional and first-order logic, the author provides first a Hilbert-type system for deduction and then a Gentzen-type system. In the Hilbert-type system for first-order logic, he posits a universal quantifier rule, which is formulated as such:

If $C \to A(x)$
then $C \to \forall(x)A(x)$

where $C$ is a 0-place predicate/propositional variable/formula with no free variables
$A(x)$ is a unary predicate taking $x$/a formula with $x$ free

This rule is re-branded as universal quantifier introduction in the Gentzen-type system with syntax modified thus:

If $G \vdash A(x) $
then $G \vdash \forall(x)A(x)$

where $G$ is the set of assumptions with the requirement that $G$ does not contain $x$ free
and $A$ is as it was in the previous formulation

I can't seem to grasp the logic behind either formulation of this rule. It doesn't follow that $[C \to A(x)] \to [C \to \forall(x)A(x)]$ since $C$ could be true and $A$ could hold for $x$ but not for all $x$s, rendering the former implication true and the latter false which would immediately make the whole implication false. If any light could be shed on why this rule holds and maintains the soundness of the deduction, it would be much appreciated.

  • 4
    "A could hold for 'x' but not for all 'x's" is not possible. The point is x is a name for an arbitrary value; if you've proved something about x without making any assumption about the value denoted by the symbol x, then it must be true for all instances for x.2012-08-27
  • 0
    The "where" part below each rule gets rid of the possibilities that $C$ holds for some $x$ and $A(x)$ holds for not all $x$ where the symbol $x$ refers to the same thing. The first rule says that $C$ has no free variables. That means even if $x$ appears in $C$, it must be bound, and has no relation with the same symbol $x$ that appears in $A(x)$. The same is true for the second rule.2012-08-27

2 Answers 2

6

Note that neither of the two rules you quote are formulated as "$(C\to A(x))\to(C\to\forall x.A(x))$". The middle $\to$ there is not in any of the rules -- they carefully use "if ... then" rather than a symbolic "$\to$", which means that the implication they express is at the level of logic-as-a-formal-game rather than at the level of truth in a particular interpretation. By reading it as $\to$ you have inadvertently made the rules into nonsense.

What the rule tells you is that if the string of symbols $$C\to A(x)$$ is valid in the interpretation you speak about, then the string of symbols $$ C\to\forall x.A(x)$$ is also valid. This is something that holds about particular strings of symbols, some of which symbols happen to be $x$, but it's not something that holds for any particular value of $x$ -- at the levels the rules work at, $x$ is just chalk and it does not have values.

To say that $C\to A(x)$ is valid means that it evaluates to true under every assignment of its free variables. Therefore the claim "$C\to A(x)$ is valid in such-and-such interpretation" does not itself have $x$ as a free variable; it is not a claim that can even in principle be true for some but not all values of $x$ any more than it can be true for some but not all values of $q$.

  • 0
    Just to add a little - the "deduction theorem" gives a link between the metatheoretic if/then and the $\to$ connective. It says that if $P \vdash Q$, where $P$ is a sentence, then $\vdash P \to Q$. The example in the question shows why the restriction on $P$ is necessary. http://en.wikipedia.org/wiki/Deduction_theorem2012-08-28
  • 0
    It is, however, correct to say $\forall x.(C \to A(x)) \to (C \to \forall x.A(x))$. I think the issue isn't that $\to$ differs from $\vdash$, but rather an issue of how free variables scope relate to either of them.2016-09-27
0

In case of many logical systems the following metatheorem can be proved:

"if the formula $A$ is a theorem and a variable $x$ is not a constant (i.e. it does not occur freely in any of our axioms), then $\forall x A$ is also a theorem".

If, in addition, you have at your disposal the deduction theorem:

"if $C$ is a theorem in a system with axiom set enlarged by $B$ then $B\rightarrow C$ is a theorem"

then your universal quantifier rule is a simple consequence.

To be precise: suppose that $C\rightarrow A$ is a theorem in our logical system. We woud like to prove that $C\rightarrow\forall x A$ is also a theorem. Adjoin $C$ to the set of our axioms.. Then, by modus ponens, $A$ is also a theorem. Since $x$ is not a constant in our logical system we have also that $\forall x A$ is a theorem by the virtue of the metatheorem mentioned at the beggining of my answer. Hence $C\rightarrow\forall x A$ is a theorem of our logical system, thanks to the deduction metatheorem.

As you can see in order to prove that metatheorem you mentioned all you need is the deduction theorem and that simple metatheorem I beggined with.

Those metatheorems can be proved in case of Hilbert and Gentzen type systems using metareasonining about the structure of assemblies but the details of proof depend on the particular formalism chosen to encode those systems.

  • 0
    This argument confuses truth and provability: _"Assume that C is true. Then, by modus ponens, A is also a theorem"_ is nonsense -- being true does not make something a _theorem_. And the reason why $C\to\forall x A$ is a _theorem_ is that there the very rule in question allows us to construct a proof of it.2012-08-28
  • 0
    Thank you for your kind remark Mr. @Makholm. Of course I used both expressions ("true formula" and "theorem") as synonyms of a "provable formula". I edited my post and now everything is clear.2012-08-28
  • 0
    But your reasoning still doesn't work -- it seems to assume that the meaning (and/or theoremhood) of $\phi\to\psi$ is concerned with the case that $\phi$ itself is a _theorem_ (rather than merely being true in some particular situation). (...)2012-08-28
  • 0
    By the same kind of reasoning I would be able to "prove" that $xx=1\to xx\neq 1$ ought to be a theorem in the basic theory of groups: Because I _know_ that $xx=1$ is not a theorem (there are groups it is not valid for, so it cannot be a theorem), if I assume that $xx=1$ is a theorem, I immediately hit a contradiction which allows me to conclude anything at all -- in particular I can conclude $xx\ne 1$. So $xx=1\to xx\ne 1$ must be a theorem ?!?2012-08-28
  • 0
    I don't understand your last comments.2012-08-28
  • 0
    My point is that it is **does not work** to argue that $\phi\to\psi$ is a theorem by following in the scheme "Assume that $\phi$ is a theorem. Then (bla bla bla) and therefore $\psi$ is a theorem. So $\phi\to\psi$ must be a theorem too". That's not how the deduction theorem works -- it allows you to make use of $\phi$ as an assumption _within the formal proof_, not to assume at the metalevel that $\phi$ is a theorem.2012-08-28
  • 0
    First of all let's stay away from the semantic notions and concentrate on the syntactic, proof theoretic reasoning. In this setting your arguments does not make any sense: in proof theoretic, syntactic setting it does make sense to say that some formula is a theorem, it simply means that it has a proof. But in this setting it does not make any sense to say that something is not a theorem. What would it mean?2012-08-28
  • 0
    You mixed two levels: a contradiction arises if a formula $R$ has a proof and a formula $not\ R$ has a proof but in your argument you do not adjoin a formula $xx=1$ to the set of axioms but you make metalogical assumption that $xx=1$ has a prove: that is not how the deduction theorem works!2012-08-28
  • 0
    Saying that something is not a theorem means that it doesn't have a proof. What's wrong about that? Further, if you want to stay with syntactic reasoning, then you cannot hope to find an argument that justifies the OP's proof rules, because the proof rules available to us are a matter of choice! The rule takes theorems to theorems because we choose to adopt is as a proof rule, and for no other reasons. (On the other hand, if you allow semantics, then proof rules can be justified by arguing that the set of semantic truths are closed under them).2012-08-28
  • 0
    Exactly: **that is not how the deduction theorem works**, but it _is_ how you attempt use the deduction theorem in your answer. I deliberately constructed an absurd argument as a demonstration that the way you try to apply the deduction theorem is not valid.2012-08-28
  • 0
    Well then your metareasoning is contradictory: you assert that something is a theorem (it has a proof) and then you use your knowledge that it is not a theorem (so it has no proof). No wonder that in a contardictory metalogic you see all formulas as theorems.2012-08-28
  • 0
    Mr. @Makholm thanks for your comments. Now i see that I have mixed up levels of reasoning myself and thus my reasoning in my answer is not correct. Thanks for pointing that out.2012-08-28
  • 0
    But if we replace "Assume that $C$ is a theorem" by "Adjoin $C$ to the set of our axioms" my arguments seems to be correct.2012-08-28
  • 0
    Yes, more or less. Then you just need to be sure that the deduction theorem still holds for the formal system in the presence of generalization. And it seems to me that the DT requires the very rule you're trying to justify (or something essentially equivalent to it) in order to go through.2012-08-28