Can we have another set of inference rule which is simplier and equivalent (in the sense that they prove the same formulas)?

Question

I have some questions on inference rules in model theory.

Question 1) In (some books of) model theory, $(\psi \rightarrow \phi, \psi \rightarrow \forall x \phi)$ where $x$ is not free in $\psi$ is taken as an inference rule. I think that to take $(\phi,\forall x \phi)$ is much simplier than the one above. I intuitively see that they are equivalent. However, I could only prove that if we assume $\phi$, we can deduce $\forall x \phi$ using the first inference rule. Here is my work:

$\phi $ (just start with this)

$\phi \rightarrow (y=y \rightarrow \phi)$

$y=y \rightarrow \phi $

$y=y \rightarrow \forall x\phi $

$y=y$

$\forall x\phi $

However, I couldn’t prove the the other direction. So, is my claim false?

Question 2) If we have $(A,B)$ as an inference rule, can’t we prove $A\rightarrow B$ in general? Note: I know that for logical inference rules, if we have $(A,B)$ then $A\rightarrow B$ is a tautology and we have $(\emptyset , A\rightarrow B)$ as an inference rule. But I want to “prove” $A\rightarrow B$ using other inference rules (except rules of types $(\emptyset , tautology)$.

Answer 1

Short answer: Whether these two rules are equivalent depends (of course) on what other rules you have available. So Question 1 can't be answered unless you specify the other rules in your system.

However, I think the answer to Question 2 may shed some light on Question 1.

You ask "If we have $(A,B)$ as an inference rule, can’t we prove $A\rightarrow B$ in general?" No - as a trivial kind of example, if you have no rules or axioms that introduce sentences of the form $\varphi\to \psi$, then you have no hope of proving $A\to B$. But if you want your logic to capture the idea of implication (and in particular if you want your proof system to be complete), you must have this property.

More generally, we say that a logic satisfies the Deduction Theorem if: For a set of sentences $\Gamma$, and sentences $\varphi$ and $\psi$, if $\Gamma\cup \{\varphi\}\vdash \psi$, then $\Gamma\vdash \varphi\rightarrow \psi$. That is, whenever we have a proof of $\psi$ from hypotheses $\Gamma$ and $\varphi$, we also have a proof of $\varphi\rightarrow \psi$ from hypotheses $\Gamma$.

Now some logical systems (such as, typically, those called "natural deduction") have the deduction theorem built in, as the "$\rightarrow$ Introduction" rule. For others (such as, typically, those called "Hilbert systems") we must prove the deduction theorem by induction on the structure of the proof $\Gamma\cup \{\varphi\}\vdash \psi$.

The strategy for such an inductive proof is to go through the proof of $\Gamma\cup \{\varphi\}\vdash \psi$ line-by-line and "relativize" by adding "$\varphi\rightarrow$" everywhere. This is exactly where your rule $(\varphi\rightarrow \psi,\varphi\rightarrow \forall x\psi)$ comes from: it's the universal generalization rule $(\psi,\forall x\psi)$ relativized to $\varphi$.

Incidentally, this is also where the bizarre-looking Hilbert system axiom $(P\to (Q\to R))\to ((P\to Q)\to (P\to R))$ comes from: It's the instance of Modus Ponens "from $Q\to R$ and $Q$, conclude $R$" relativized to $P$.

So in conclusion: I suspect that in the context of your other rules, $(\psi,\forall x\psi)$ really is strictly weaker than $(\varphi\rightarrow \psi,\varphi\rightarrow \forall x\psi)$. The reason you need to assume the stronger rule is that it is used in the proof of the Deduction Theorem. If you were working with a natural deduction system which had the Deduction Theorem built in, then your two rules would be equivalent.

Answer 2

Regarding your question 1 (really 2 questions I saw), your concerned simplified inference rule (universal generalization) is a special case of the generalization theorem in most Hilbert systems and please note most use turnstile $\vdash$ symbol instead of your implication. So strictly speaking it's used as a theorem, not an inference rule, and your $\psi$ is generally taken to be a set of propositions instead of a single proposition. Since you're allowed to let your $\psi$ to be empty on the left side of the $\vdash$, then you get your simpler version automatically. As for your concerned other direction assuming your $\phi$ has only possible free occurrences of $x$, then normally you need to invoke something called substitution theorem such as on page 32 of Shoenfield's Mathematical Logic.

Regarding your question 2, obviously basic inference rules such as modus ponens in Hilbert Systems cannot be proved in the system itself (otherwise isn't your proof system circular?). But there're usually additional derivable and admissible rules introduced in various natural deduction systems to make proof much easier (and this is one of the reasons why ND systems are natural than Hilbert systems). In some ND systems the inference rule equivalent to deduction theorem called $\to$ introduction rule is a derivable and admissible rule, not one of the basic rules. And in some logic system like relevance logic, this rule doesn't even hold...