FOL Deduction Question
From: Zarius (me_at_privacy.net)
Date: 12/23/04
- Next message: Jose Juan Mendoza Rodriguez: "Re: FOL Deduction Question"
- Previous message: Nameless: "Re: Version 2.5 of the GOLD Parser Builder was just released"
- Next in thread: Jose Juan Mendoza Rodriguez: "Re: FOL Deduction Question"
- Reply: Jose Juan Mendoza Rodriguez: "Re: FOL Deduction Question"
- Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
Date: Thu, 23 Dec 2004 01:53:42 +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
- Next message: Jose Juan Mendoza Rodriguez: "Re: FOL Deduction Question"
- Previous message: Nameless: "Re: Version 2.5 of the GOLD Parser Builder was just released"
- Next in thread: Jose Juan Mendoza Rodriguez: "Re: FOL Deduction Question"
- Reply: Jose Juan Mendoza Rodriguez: "Re: FOL Deduction Question"
- Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
Relevant Pages
|
