3
$\begingroup$

within the following axiomatic system I've beeb trying to proof the formulas (1) $\forall x \exists y R(x,y) \rightarrow \forall y \exists x R(y,x) \\$ and (2) $\\ \exists x (\exists y P(y) \rightarrow P(x))$.

The axioms are:

1) tautology axioms: every tautology is an axiom (where tautologies are the formulas for which exists a homomorphism from a tautology in propositional logic)

2) distributivity axioms: all formulas of the form $\forall x (\phi \rightarrow \psi) \rightarrow (\forall x \phi \rightarrow \forall x \psi)$

3) existence axioms: $\exists x \phi(x) \rightarrow \neg \forall x \neg \phi(x)$ and $\neg \forall x \neg \phi(x) \rightarrow \exists x \phi(x)$ for every formula $\phi$

4) generality axiom: all formulas of the form $\phi \rightarrow \forall x \phi$, whereby $\phi$ is a formula in which x isn't present

5) equality axioms: all formulas that have one of the forms $u=v, u=v \rightarrow u = u, (u=v \wedge v = w) \rightarrow u=w$, wherby u,v,w are any variables

6) Leibniz-axioms: all formulas of the form $(u_1 = v_1 \wedge \cdots \wedge u_n = v_n) \rightarrow f(u_1, \cdots, u_n) = f(v_1, \cdots, v_n)$ where f is a function symbol and axioms of the form $(u_1 = v_1 \wedge \cdots \wedge u_n = v_n) \rightarrow (R(u_1, \cdots u_n) \leftrightarrow (R(v_1, \cdots, v_n)) $ where R is a relation symbol.

7) substitution axioms: for a variable x, formula $\phi$, term t that is allowed to be substituted for x in $\phi$: $(\forall x \phi) \rightarrow \phi(x/t)$

With these axioms and Modus ponens I've been trying to derive the formulas mentioned above.

Here are my solutions so far:

(1) I've derived a formula of the form $\forall z \exists y R(z,y) \rightarrow \forall z \neg \forall y \neg R(z,y)$ and now I'm trying to bring the x in the second part instead of the y. So is $\forall z \neg \forall y \neg R(z,y) \rightarrow \forall z \neg \forall x \neg R(z,x)$ correct due to the substitution axiom or is it wrong to apply the substitution axiom because of the $\forall z \neg$ before the $\forall y$? (And if the latter is the case, how can the $\forall x$ be brought in?

(2) I've tried to derive the formula a couple of times, but I alway run into problems with the $\exists$. How can it be placed at the beginning of the whole formula?

$\endgroup$
7
  • $\begingroup$ I just corrected two typos I hade made with the axioms. Maybe it is clearer now? $\endgroup$
    – Studentu
    Nov 10, 2018 at 15:55
  • 1
    $\begingroup$ The first amounts to a change of index variable. Is there an axiom or tautology like $\forall x \in \mathbb{D} \phi(x) \rightarrow \forall y\in\mathbb{D}\phi(y)$? If yes, the 1st problem is solved. Does $\phi(t)\rightarrow \exists x\phi(x)$? If yes, the 2nd problem is solved. $\endgroup$
    – Lance
    Nov 10, 2018 at 16:57
  • $\begingroup$ @Lance: Thanks for your reply. Unfortunately, there can't be such tautologies (since there are no homomorph tautologies in prop. logic). 1) Yes, I'd say we can achieve this with axiom 7, but my problem is that we have $\forall z \neg \forall x \in \mathbb{D}\phi(x)$ and not simply $\forall x \in \mathbb{D}\phi(x)$. So there's the disturbing $\forall z \neg$ which - as I understand it - hinders us to do the change? 2) No, we have no such axiom. $\endgroup$
    – Studentu
    Nov 10, 2018 at 17:21
  • $\begingroup$ I have no experience with first order logic, but I don't think as a branch of math, it will ever treat the name of a index variable as significant. Anyways, like I said, I don't know :( $\endgroup$
    – Lance
    Nov 10, 2018 at 17:26
  • $\begingroup$ Okay, no problem, thanks for your input, Lance! $\endgroup$
    – Studentu
    Nov 10, 2018 at 17:48

0

Reset to default

You must log in to answer this question.