FOL Deduction Question

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

Date: Thu, 23 Dec 2004 18:48:56 +0000

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

Relevant Pages

  • FOL Deduction Question
    ... Suddenly I found myself confused when thinking about FOL and Gentzen ... This sequent should be falsifiable, ... But using a standard G system for Classical FOL - with the duplication rules ... merged with Exists on right and Forall on left- the computation would ...
    (comp.theory)
  • Re: Existence, Self-identity and Uniqueness.
    ... In FOL a definition is simply modelled ... for a predicate symbol R as follows: ... reflexivity, i.e. forall x. ... The above proof needs reflexivity, ...
    (sci.logic)
  • Re: Existence, Self-identity and Uniqueness.
    ... forall x A0is true, ... valid inference in FOL=: ... The bothers would lead to the following ... The predicate is new, ...
    (sci.logic)
  • Re: Existence, Self-identity and Uniqueness.
    ... I was on purpose using some foolishly substitutions. ... Because FOL= does not distinguish ... How do you control the following reasoning step, ... forall x A ...
    (sci.logic)
  • Re: Existence, Self-identity and Uniqueness.
    ... Because FOL= does not distinguish ... between foolishly and non foolishly substitutions. ... How do you control the following reasoning step, ... forall x A ...
    (sci.logic)