# Thread: derivations in predicate calculus

1. ## derivations in predicate calculus

The problems:

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

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

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

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

c) $\displaystyle \vdash \exists x (x = \tau)$ for any term $\displaystyle \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: $\displaystyle (\phi \rightarrow (\psi \rightarrow \phi))$
2: $\displaystyle ((\phi \rightarrow (\psi \rightarrow \theta)) \rightarrow ((\phi \rightarrow \psi) \rightarrow (\phi \rightarrow \theta)))$
3: $\displaystyle ((\neg\phi\rightarrow\neg\psi)\rightarrow(\psi\rig htarrow\phi))$
4: $\displaystyle (\forall x \phi(x) \rightarrow \phi (\tau))$ ($\displaystyle \tau$ is a term freely substitutable for x in $\displaystyle \phi$)
5: $\displaystyle (\forall x (\phi \rightarrow \psi) \rightarrow (\phi \rightarrow \forall x \psi))$ (where x is not free in $\displaystyle \phi$)
6: $\displaystyle \forall x (x=x)$
7: $\displaystyle (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!

2. None of the axioms say anything about $\displaystyle \exists$. Is it considered an abbreviation for $\displaystyle \neg\forall\neg$?

3. Originally Posted by emakarov
None of the axioms say anything about $\displaystyle \exists$. Is it considered an abbreviation for $\displaystyle \neg\forall\neg$?
Yes, it is, do you think I should just immediately go through and change all the $\displaystyle \exists$ to $\displaystyle \neg\forall\neg$?

4. Originally Posted by logicloser
The problems:

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

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

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

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

c) $\displaystyle \vdash \exists x (x = \tau)$ for any term $\displaystyle \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: $\displaystyle (\phi \rightarrow (\psi \rightarrow \phi))$
2: $\displaystyle ((\phi \rightarrow (\psi \rightarrow \theta)) \rightarrow ((\phi \rightarrow \psi) \rightarrow (\phi \rightarrow \theta)))$
3: $\displaystyle ((\neg\phi\rightarrow\neg\psi)\rightarrow(\psi\rig htarrow\phi))$
4: $\displaystyle (\forall x \phi(x) \rightarrow \phi (\tau))$ ($\displaystyle \tau$ is a term freely substitutable for x in $\displaystyle \phi$)
5: $\displaystyle (\forall x (\phi \rightarrow \psi) \rightarrow (\phi \rightarrow \forall x \psi))$ (where x is not free in $\displaystyle \phi$)
6: $\displaystyle \forall x (x=x)$
7: $\displaystyle (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?

5. a) for any

(1) by assumption
(2) by assuming the negation of where is also written as
Not yet. You need remove the $\displaystyle \forall$ by applying axiom (4) with an arbitrary term, such as an unrelated variable $\displaystyle y$. Then you'll have $\displaystyle \phi(y)$ and $\displaystyle \neg\phi(y)$, i.e., \bot (contradiction, which is what you need.
Note, by the way, that this law: $\displaystyle \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 $\displaystyle y$. If all variables are strictly accounted for -- as in branch of proof theory called type theory -- such shenanigans are not possible.
Here it becomes a little involved are would probably require a lot of intermediate helper theorems. Assume $\displaystyle \forall x.\,\phi(x)\to\psi$ and $\displaystyle \neg\forall x.\,\neg\phi(x)$. We'll prove $\displaystyle \psi$ by contradiction, so assume $\displaystyle \neg\psi$. But first we will prove $\displaystyle \forall x.\,\neg\phi(x)$; together with $\displaystyle \neg\forall x.\,\neg\phi(x)$ this will give us the needed contradiction.
To prove $\displaystyle \forall x.\,\neg\phi(x)$, fix some $\displaystyle x_0$ and assume $\displaystyle \phi(x_0)$; we need to obtain a contradiction. Plug $\displaystyle x_0$ into $\displaystyle \forall x.\,\phi(x)\to\psi$ to get $\displaystyle \phi(x_0)\to\psi$. By MP, we get $\displaystyle \psi$, but earlier we assumed $\displaystyle \neg\psi$.