Re: FOL Deduction Question

From: Jose Juan Mendoza Rodriguez (me_at_privacy.net)
Date: 12/23/04 

Date: Thu, 23 Dec 2004 16:51:36 +0000

Hello,

I haven't read that book, but it seems to me that you are applying
rule Exists-right (on page 188) from bottom to top, and rules are
supposed to be applied only from top to bottom.

I'm not acquainted with System G, but I'm pretty sure that you cannot
draw this sequent:

  |- P(y1), Exists x . P(x)

from this one:

  |- Exists x . P(x)

Since "P(y1)" is almost the same as "Forall y. P(y)" ("y" being
a new variable).

If by falsifying you mean deriving the empty sequent, then this
is impossible since the system is sound (Lemma 5.4.3).

All you can do is deriving a formula starting from an axiom (read the
definition of axiom on page 188). That axiom will 'encode' the
interpretation you have in mind:

   --------------- Axiom
   P(y1) --> P(y1)
   -------------------- Not-Left
   P(y1), ¬P(y1) -->
   ----------------------------- Exists-left
   Exists x . P(x), ¬P(y1) -->
   ----------------------------- Not-right
   ¬P(y1) --> ¬Exists x . P(x)

You arrange things so that the predicates that 'encode' your
interpretation get placed on the left side of the sequent, and you
will get conclusions on the right side.

I hope I haven't confused you. If this is the first time you meet
predicate logic, then you should look for another introductory text,
since Gallier's book seems rather sophisticated.

Regards.
José Juan Mendoza Rodríguez

Relevant Pages

  • Is there a way to limit the numbers of most recently used programs on the start menu
    ... I have an Axiom 30 with Mobile Windows 2003 and have an enormous list of ... programs I have opened recently that drops to the very bottom. ... Toshiba with Pocket PC 2002 and could limit the MRU list to a few programs ...
    (microsoft.public.pocketpc)
  • Re: FOL Deduction Question
    ... > supposed to be applied only from top to bottom. ... In the context of automated deduction you begin with the sequent you want to ... we apply the rules backwards but we're not drawing the ...
    (comp.theory)