Generalisation Rule using Hilbert's Calculus

95 Views Asked by At

One of the exercises for my logic course is to prove that given a theory T in a language $\mathcal{L}$ and a $\mathcal{L}-$formula $\varphi$, then $T\vdash_{\mathcal{L}}(\varphi\longrightarrow\exists x_{1},...,x_{n}\varphi)$ and $T\vdash_{\mathcal{L}}(\forall x_{1},...,x_{n}\varphi\longrightarrow\varphi)$, meaning there is a formal demonstration of those formulas using tautologies, sentences of T, modus ponens, $\exists-$substitution ($\varphi_{t/x}\rightarrow\exists x\varphi$ if x is free for t in $\varphi$) and $\exists-$introduction ($\exists x\varphi\rightarrow\psi$ given that $\varphi\rightarrow\psi$ and x not free in $\psi$).

Intuitively I get why both of them must be true, but I don't know where to begin (so far I've tried induction on n but that doesn't seem to get me very far and I end up splitting cases whether the variables are free in $\varphi$ or not, and then substituting $\varphi_{t/x}$ doesn't give the expected formula...). Could you give me any clues of the proof?

P.S. I don't see how to use it here, but the previous exercices consisted of proving that $\varphi\rightarrow(\neg\forall x\varphi\rightarrow\varphi)$ and $(\neg\forall x\varphi\rightarrow\forall x\varphi)\rightarrow\forall x\varphi$ are tautologies, and that if $T\vdash_{\mathcal{L}}\varphi$ then $T\vdash_{\mathcal{L}}\forall x\varphi$, maybe it's helpful

1

There are 1 best solutions below

0
On BEST ANSWER

Hint

$\varphi \to \exists x_1 \varphi$ is an axiom; re-iterate it $n$ times.

Regarding the universal quantifier, apply the previous case to $\lnot \varphi \to \exists x_1 \lnot \varphi$ abd contrapose it, to get; $\lnot \exists x_1 \lnot \varphi \to \varphi$.

Then apply the definition of $\forall$ as $\lnot \exists \lnot$.