Why is this sequent generalization valid?

46 Views Asked by At

In Takeuti's Proof Theory, he has a sequent rule that from $\Gamma \rightarrow \Delta, F(a)$ where $a$ is a free variable, one can infer $\Gamma\rightarrow \Delta, (\forall x)F(x)$. This seems like it should be invalid. For instance, $\{F(a_1)\} \rightarrow \{F(a_2)\}, F(a_3)$ under the model $F^\mathcal{M}=\{1,3\}$ and assignment $s=(1,2,3)$ comes out true, yet this model and assignment does not satisfy $\{F(a_1)\}\rightarrow \{F(a_2)\},(\forall x)F(x)$.

1

There are 1 best solutions below

0
On

See Theorem 8.2 (completeness and soundness), page 41 :

A formula is provable in LK iff it is valid.

And see page 40 : an interpretation is a structure with domain $D$ and a mapping $\phi_0$ from variables into $D$.

Finally :

A sequent is valid if it is satisfied in very interpretation.

Conclusion: your consideration is correct, and the lower sequent is not valid. But neither the upper sequent is.