I'm trying to prove: $$\forall x (\phi \rightarrow \psi) \rightarrow (\forall x (\phi) \rightarrow \forall x (\psi))$$ and $$\forall x \forall y (\phi) \rightarrow \forall y \forall x (\phi) $$
using the traditional axioms of predicate logic (and whatever standard theorems from propositional logic necessary):
- $$\forall x (\phi(x)) \rightarrow \phi(y)$$
- $$\forall x (\phi \rightarrow \psi) \rightarrow (\phi \rightarrow \forall x (\psi))$$
and generalization as the inference rule: $$\vdash \phi \rightarrow \space \vdash \forall x(\phi) $$
Just to be explicit I am using the following axioms for propositional logic: $$\phi \rightarrow ( \psi \rightarrow \phi )$$ $$(\phi \rightarrow (\psi \rightarrow \theta) ) \rightarrow ((\phi \rightarrow \psi)\rightarrow (\phi \rightarrow \theta)) $$ $$(\lnot\phi \rightarrow \lnot \psi) \rightarrow (\psi \rightarrow \phi) $$ and modus ponens as the inference rule.
I know how to prove these propositions using the deduction theorem, but I would like to prove them without invoking it (or any other metatheorem for that matter) .
I tried but I can't use generalization to conclude $$ \psi \rightarrow \space \forall x(\psi) $$ and use hypothetical syllogism (the closed form) to get to the proposition - that is:
I get $$(\forall x (\phi \rightarrow \psi) \space \land \space \forall x (\phi)) \space \rightarrow \space (\phi \rightarrow \psi) $$ by 1. and some theorems of propositional logic, also: $$(\forall x (\phi \rightarrow \psi) \space \land \space \forall x (\phi) ) \space \rightarrow \space \phi $$ so I conclude $$(\forall x (\phi \rightarrow \psi) \space \land \space \forall x (\phi)) \rightarrow (\phi \land (\phi \rightarrow \psi)$$ that is: $$(\forall x (\phi \rightarrow \psi) \space \land \space \forall x (\phi)) \rightarrow \psi$$
Is there a way to continue from here...or am I way off
I'm sorry - I should have thought more before posting this...guess I was tired and frustrated last night. Anyway:
$$(\phi \rightarrow \psi) \vdash \forall x (\phi \rightarrow \psi) $$
if x is bounded in $$\phi$$ we get $$(\phi \rightarrow \psi) \vdash ( \phi \rightarrow \forall x ( \psi) ) $$ but x is bounded in the antecedent in the last line (of the post) from which the proposition follows