Re: Existence, Self-identity and Uniqueness.

Hi

William Elliot wrote:
On Thu, 28 Dec 2006, Jan Burse wrote:
We agree that it's theorem when (E!x)F(x).
In the event ~(E!x)F(x), the premis
ixF(x) = y
is false, thus promoting again the whole statement to truthood.

Ok, thanks.

Yes, the "x=y->(A0(x)<->A0(y))" is not
the counter example. But the "forall x
A0(x)" is the counter example.

forall x A0(x) is true, but A0(the x:F0x)
is false. That violates the following
valid inference in FOL=:

G |- forall x A0(x)
--------------
G |- A0(t)

> Syntatic bothers are deciding if
> More bother ensues with quantifies, to
> show the definition is

The bothers would lead to the following
new rule in FOL= I guess:

G |- forall x A0(x)
-------------------
G, E!x1F1x1, .., E!xnFnxn |- A0(t)

Where the x1:F1x1,.., the xn:Fnxn are
the occurences of the form "the x:Fx"
in the term t.

Bye

P.S.: Here again the definition of
A0, with the typo ~x=y of my very first
post corrected to ~x=z:

x<>z :<=> ~x=z
A0(x) :<=> forall z(x<>z <-> ~x=z)

The predicate <> is new, the predicate
= is the built in of FOL=. The statement
G |- forall x A0(x) looks as follows:

forall y forall t(y<>t <-> ~y=t) |- forall x forall z(x<>z <-> ~x=z)

We have used other variables in G, so
that it is clear, that there is no direct
communication between G and forall x A0(x).

And here a repetition of the substition
of "the x:F0x", one can see that we apply
the precondition only to primeformulas:

A0(the x:F0x) == forall z(the x:F0x <> z <-> ~ the x:F0x = z)
forall z(exists y(precond(y) & y<>z) <->
~exists t(precond(t) & y=z))
== forall z(false <-> true)
== false
.

Relevant Pages

  • 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.
    ... 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)
  • 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)
  • 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 ...
    (sci.logic)