Does the following provability hold in intuitionistic logic?
- $\vdash a_0\Rightarrow(a_1\Rightarrow(\dots\Rightarrow(a_n\Rightarrow a_k)\dots))$ for $0\leq k\leq n$
- $a_0\Rightarrow (a_1\Rightarrow(\dots\Rightarrow(a_n\Rightarrow b)\dots)),\quad a_0\Rightarrow(a_1\Rightarrow(\dots\Rightarrow(a_n\Rightarrow(b\Rightarrow c))\dots))$ $\vdash a_0\Rightarrow(a_1\Rightarrow(\dots\Rightarrow(a_n\Rightarrow c)\dots))$
- $a\Rightarrow P(x)\vdash a\Rightarrow \forall x:P(x)$ [when $x$ is not in $a$]
Please note that if it holds, then any first-order predicate logic with axioms $a_1$, ..., $a_n$ proof can be rewritten as a proof in intuitionistic logic. Really:
- Replace any step $x$ in a proof by $a_0\Rightarrow(a_1\Rightarrow(\dots\Rightarrow(a_n\Rightarrow x)\dots))$. If a step in the proof is an axiom, to justify it use rule 1. If it is modus ponens then rule 2. If it is $P(x) \vdash \forall x:P(x)$, then we can by rule 3 have $a_0\Rightarrow(a_1\Rightarrow\dots\Rightarrow (a_n\Rightarrow P(x))\dots)\vdash a_0\Rightarrow(a_1\Rightarrow\dots\Rightarrow (a_n\Rightarrow \forall x:P(x))\dots)$ (when $x$ is not present in $a_0$, ..., $a_n$).
If the first 3 statements don't hold in intuitionistic logic, then it nevertheless holds in classic first-order predicate logic. Does it hold for any prominent weaker (having less axioms) axioms system? So, in any case we can limit axioms used for any system just to logic axioms. Is it a known fact? (After I discovered ordered semigroup actions, that were unknown before me, I won't wonder if the above is also first described by me).