0
$\begingroup$

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):

  1. $$\forall x (\phi(x)) \rightarrow \phi(y)$$
  2. $$\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

$\endgroup$
0
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.