Consider the following system for Hilbert-style deduction:
Axioms:
- $A \rightarrow (B \rightarrow A)$
- $(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))$
- $(A \rightarrow (B \rightarrow A\land B)) $
- $A \land B \rightarrow A$
- $A \land B \rightarrow B$
- $(A \rightarrow B) \rightarrow((C \rightarrow B)\rightarrow(A\lor C \rightarrow B))$
- $A \rightarrow A\lor B$
- $B \rightarrow A\lor B$
- $\neg \neg A \rightarrow A$
- $\neg A \leftrightarrow (A \rightarrow \bot)$
- $\forall x A(x) \rightarrow A(t)$ where $t$ is free for $x$ in $A(x)$
- $ \forall x(A \rightarrow B(x)) \rightarrow (A \rightarrow \forall x B(x))$
where $x$ is not a free variable of $A$
- $A(t) \rightarrow \exists x A(x)$ where $t$ is free for $x$ in $A(x)$
- $\forall x (A(x)\rightarrow B) \rightarrow(\exists x A(x) \rightarrow B)$ where $x$ is not a free variable of $B$ (I)
Rules of inference:
- $\dfrac {A \qquad A \rightarrow B} B$
- $\dfrac {A(x)}{\forall x A(x)}$ where $x$ is not free in the formulas used to deduce $A(x)$
$A \leftrightarrow B$ is an abbreviation for $(A \rightarrow B) \land (B \rightarrow A)$.
I can prove (I) semantically. This is a complete system, so one expects removing it will damage the system, since then there will be valid formulas not provable in the remaining system, leaving it incomplete, unless (I) was redundant in the original system.
However, I was curious with the difference the axiom has with this one:
$\forall x (A(x)\rightarrow B) \rightarrow(\forall x A(x) \rightarrow B)$ where $x$ is not a free variable of $B$. (II)
I'll try to explain what I think of their difference. I'll translate (I) and (II) to a small example in propositional logic, using the fact that $\forall$ behaves like $\land$ and $\exists$ like $\lor$:
(I)': $(A_1\rightarrow B) \land (A_2 \rightarrow B)\rightarrow (A_1 \lor A_2\rightarrow B)$
(II)': $(A_1\rightarrow B) \land (A_2 \rightarrow B)\rightarrow (A_1 \land A_2\rightarrow B)$
Using the fact that $A_1 \rightarrow B$ is equivalent to $\neg A_1 \lor B$ the LHS of (I)' is equivalent to $(\neg A_1 \land \neg A_2)\lor B$ which is $\neg (A_1\lor A_2)\lor B$ which is RHS. But the similar argument does not hold for (II)', meaning the implication in (I)' can be reversed, but not in (II)'. Does this actually mean (I)' is a "stronger" formula?
My main question is that does replacing (II) with (I) damage the Hilbert system? By damaging I mean will then there exist some formula so that the original system could prove it but the new system cannot? I think if we can somehow show that having (I) as an axiom we can derive (II) in the system, but not vice-versa, which means the original system is stronger. But how can we show something is not derivable?
First, note that (II) is redundant since it's a theorem of the system (without using (I)). Here's a proof:
Now, the question is wether we can deduce (I) from the other axioms or not. If it is a theorem, you should give a proof in the system, but if it's not a theorem (as I believe so), the problem is not quite easy! To show that (I) is not a theorem, you can have model-theoretic approaches and proof-theoretic approaches.
In a model-theoretic approach, you may introduce a new semantics for which your deduction system (without (I)) is sound but there's a counter-model for (I). Note that for the standard semantics we have the soundness theorem, but (I) is also valid; so the standard semantics doesn't work.
In a proof-theoretic approach, you may find some structural properties of your deduction system which shows that every theorem has a special property, which (I) doesn't have. Usually, we don't have this kind of structural properties for Hilbert-style systems. So you may find a natural deduction system, a tableau system or a Gentzen-style system which is equivalent to your system (without (I)) and try to prove theorems like normalization or cut-elimination.