Let $\varphi$ be a quantifier free sentence and $T$ is a theory such that $\vec{c} \not\in T$. I am trying to see why the following is true: $T \vdash \varphi(\vec{c})$ implies $T \vdash \forall x \varphi(\vec{x})$. I am looking for a purely syntatical proof, i.e. whether the fact that there is some deduction of $\varphi(\vec{c})$ from $T$ implies that there is some deduction of $\forall x \varphi(\vec{x})$. If this is true, how can I qualify my statement so that it does become true? You can pick any deduction system and I would be grateful for your help.
Asked
Active
Viewed 78 times
0
-
1It’s not true. Maybe you mean that $\vec c$ doesn’t appear in $T$? (But then, it’s true but quantifier-free is not required.) – spaceisdarkgreen Nov 10 '23 at 02:40
-
YES! that $\vec{c}$ doesn't appear in $T$ – love and light Nov 10 '23 at 03:04
-
3In many deductive systems that’s just a rule. Universal generalization. – spaceisdarkgreen Nov 10 '23 at 03:06
-
It is called Generalization on Constants – Mauro ALLEGRANZA Nov 10 '23 at 08:32
1 Answers
0
The result is known as Generalization on constant.
The "trick" is simple: if you have a proof of $\varphi(c)$ and $c$ is not used in the set $T$ of assumptions (axioms), you can replace everywhere in the proof $c$ with a new variable $w$, where new means: nowhere occurring in the proof (the proof is a finite object and we have an unlimited supply of variables).
The result will be $T \vdash \varphi [w/c]$. The proof is by induction on the length of the derivation.
Due to the fact that $c$ does not occur in $T$, also the variable $w$ will not, and thus you can apply Generaliztion to conclude with $T \vdash \forall x \varphi$.
Mauro ALLEGRANZA
- 94,169