Re: FOL Deduction Question

From: Zarius (me_at_privacy.net)
Date: 12/23/04 

Date: Thu, 23 Dec 2004 19:58:35 +0000

A few notes to make everything clear, I'm working in the context of
automated deduction. The sequence of sequents I presented are the result of
the application of the Exists Right rule backwards (merged with duplication
as described in the given url and many other resources). Seems like the
computation would never stop so I won't ever get a counter example
deduction tree for that sequent.

Z.

> Hello,
> Suddenly I found myself confused when thinking about FOL and Gentzen
> systems. I'd appreciate some help getting my thought back on track.
>
> This sequent should be (easily) falsifiable, right?
> |- Exists x . P(x)
>
> (just consider the assignment that turns P into a function that always
> returns false)
>
> But using a standard G system for Classical FOL - with the duplication
> rules merged with Exists on right and Forall on left[1] - the computation
> would never stop. We'd get,
>
> |- Exists x . P(x)
> |- P(y1), Exists x . P(x)
> |- P(y1), P(y2), Exists x . P(x)
> |- P(y1), P(y2), P(y3), Exists x . P(x)
>
> etc.
>
> To be able to say I it's falsifiable, I'd need to get only atomic formulas
> in the sequent, but that will clearly never happen. I know I'm probably
> messing something up, though. Any comments?
>
> Thanks,
> Z
>
> [1] Like the one presented at (pag 187):
> http://www.cis.upenn.edu/~jean/gbooks/logic.html