# derivations in predicate calculus

• Apr 22nd 2010, 04:00 PM
logicloser
derivations in predicate calculus
The problems:

a) $\vdash (\forall x \phi \rightarrow \exists x \phi)$ for any $\phi$

(1) $\forall x \phi$ by assumption
(2) $\forall x \neg\phi$ by assuming the negation of $\exists x \phi$ where $\exists x$ is also written as $\neg \forall x \neg$

b) $\forall x(\phi \rightarrow \psi) \vdash (\exists x \phi \rightarrow \psi)$where x is not free in $\psi$

This one I think it must involve axioms 4 and 5 somehow, but I guess that's obvious

c) $\vdash \exists x (x = \tau)$ for any term $\tau$ not involving x

And this one must involve axioms 4 and 6

Derive them using these (for your convenience and my LaTeX practice):
Axioms:
1: $(\phi \rightarrow (\psi \rightarrow \phi))$
2: $((\phi \rightarrow (\psi \rightarrow \theta)) \rightarrow ((\phi \rightarrow \psi) \rightarrow (\phi \rightarrow \theta)))$
3: $((\neg\phi\rightarrow\neg\psi)\rightarrow(\psi\rig htarrow\phi))$
4: $(\forall x \phi(x) \rightarrow \phi (\tau))$ ( $\tau$ is a term freely substitutable for x in $\phi$)
5: $(\forall x (\phi \rightarrow \psi) \rightarrow (\phi \rightarrow \forall x \psi))$ (where x is not free in $\phi$)
6: $\forall x (x=x)$
7: $(x = y \rightarrow (\phi(x,x) \rightarrow \phi(x,y)))$

As well as Modus Ponens, Generalization, and the Deduction theorem

Any help would be really appreciated!
• Apr 23rd 2010, 04:22 AM
emakarov
None of the axioms say anything about $\exists$. Is it considered an abbreviation for $\neg\forall\neg$?
• Apr 23rd 2010, 07:44 AM
logicloser
Quote:

Originally Posted by emakarov
None of the axioms say anything about $\exists$. Is it considered an abbreviation for $\neg\forall\neg$?

Yes, it is, do you think I should just immediately go through and change all the $\exists$ to $\neg\forall\neg$?
• Apr 23rd 2010, 08:26 AM
PiperAlpha167
Quote:

Originally Posted by logicloser
The problems:

a) $\vdash (\forall x \phi \rightarrow \exists x \phi)$ for any $\phi$

(1) $\forall x \phi$ by assumption
(2) $\forall x \neg\phi$ by assuming the negation of $\exists x \phi$ where $\exists x$ is also written as $\neg \forall x \neg$

b) $\forall x(\phi \rightarrow \psi) \vdash (\exists x \phi \rightarrow \psi)$where x is not free in $\psi$

This one I think it must involve axioms 4 and 5 somehow, but I guess that's obvious

c) $\vdash \exists x (x = \tau)$ for any term $\tau$ not involving x

And this one must involve axioms 4 and 6

Derive them using these (for your convenience and my LaTeX practice):
Axioms:
1: $(\phi \rightarrow (\psi \rightarrow \phi))$
2: $((\phi \rightarrow (\psi \rightarrow \theta)) \rightarrow ((\phi \rightarrow \psi) \rightarrow (\phi \rightarrow \theta)))$
3: $((\neg\phi\rightarrow\neg\psi)\rightarrow(\psi\rig htarrow\phi))$
4: $(\forall x \phi(x) \rightarrow \phi (\tau))$ ( $\tau$ is a term freely substitutable for x in $\phi$)
5: $(\forall x (\phi \rightarrow \psi) \rightarrow (\phi \rightarrow \forall x \psi))$ (where x is not free in $\phi$)
6: $\forall x (x=x)$
7: $(x = y \rightarrow (\phi(x,x) \rightarrow \phi(x,y)))$

As well as Modus Ponens, Generalization, and the Deduction theorem

Any help would be really appreciated!

How much has been laid down prior to these exercises i.e., much support do you have at your disposal?

On the one hand, as you've written it, it appears you've been asked to prove these claims with just the seven axiom schemes, two rules and Dth.
But this is at odds with what you comtemplate for a proof of a). Apparently, you're going to attempt a proof by contradiction.
So apparently, at least one version of this proof method has already been introduced.
This is what I mean by support. How much support do you have to work with in addition to the bare-bones deductive apparatus
you describe at the bottom?

You can also indicate what (conservative) definitional extensions to the system have been carried out.
Certainly, the existential quantifier is one.

You know, if you're working from a textbook, why not provide the pertinent information about it?
• Apr 23rd 2010, 08:44 AM
emakarov
Not yet. You need remove the $\forall$ by applying axiom (4) with an arbitrary term, such as an unrelated variable $y$. Then you'll have $\phi(y)$ and $\neg\phi(y)$, i.e., \bot (contradiction, which is what you need.

Note, by the way, that this law: $\forall x.\,\phi\to\exists x.\,\phi$ is not so good after all because it is false in the interpretation with an empty domain. Proving it is possible because of the bad accounting of free variables -- here we picked a stray variable $y$. If all variables are strictly accounted for -- as in branch of proof theory called type theory -- such shenanigans are not possible.

Quote:
Here it becomes a little involved are would probably require a lot of intermediate helper theorems. Assume $\forall x.\,\phi(x)\to\psi$ and $\neg\forall x.\,\neg\phi(x)$. We'll prove $\psi$ by contradiction, so assume $\neg\psi$. But first we will prove $\forall x.\,\neg\phi(x)$; together with $\neg\forall x.\,\neg\phi(x)$ this will give us the needed contradiction.

To prove $\forall x.\,\neg\phi(x)$, fix some $x_0$ and assume $\phi(x_0)$; we need to obtain a contradiction. Plug $x_0$ into $\forall x.\,\phi(x)\to\psi$ to get $\phi(x_0)\to\psi$. By MP, we get $\psi$, but earlier we assumed $\neg\psi$.

Now there is a task to translate this into using your axioms...