# First Order Logic : Tableau

• Nov 4th 2012, 02:41 PM
Razoor
First Order Logic : Tableau
This formulae gives me some troubles.

Attachment 25545

Im getting this far before im in trouble:

Attachment 25546

How do I push the negation inwards ?

Appreciate all hints or solutions!

• Nov 4th 2012, 04:43 PM
Plato
Re: First Order Logic : Tableau
Quote:

Originally Posted by Razoor
This formulae gives me some troubles.
Attachment 25545[COLOR=#000000]

Lets say we are dealing with \$\displaystyle \mathbb{N}\$ and \$\displaystyle p(m,n)\$ means \$\displaystyle m\le n\$.
Then \$\displaystyle (\exists x)(\forall y)[p(x,y)]\$ says "some natural number precedes every natural number". Does that imply that "every natural is preceded by some natural number"?

Can you use IE, UI, UG & EU in a valid way to get what you need?
• Nov 5th 2012, 01:52 AM
Razoor
Re: First Order Logic : Tableau
Quote:

Originally Posted by Plato
Lets say we are dealing with \$\displaystyle \mathbb{N}\$ and \$\displaystyle p(m,n)\$ means \$\displaystyle m\le n\$.
Then \$\displaystyle (\exists x)(\forall y)[p(x,y)]\$ says "some natural number precedes every natural number". Does that imply that "every natural is preceded by some natural number"?

Can you use IE, UI, UG & EU in a valid way to get what you need?

Im not quite sure what you mean with your last question. But this is how i understand the sentence.

\$\displaystyle \exists x \forall y p(x,y) \$

"There exist an X where all Y is in the same function p(X,Y) which implies that for all Y is there an X in the same function p(X,Y)"

First of all i need to remove the imply arrow by negating the right side and split up the left and right part like this:

\$\displaystyle \exists x \forall y p(x,y) , \neg ( \forall y \exists x p(x,y) ) \$

You can then remove \$\displaystyle (\exists x)\$ by introducing a new constant for X.

\$\displaystyle \forall y p(A,y) , \neg ( \forall y \exists x p(x,y) ) \$