Re: Existence, Self-identity and Uniqueness.

On Thu, 28 Dec 2006, William Elliot wrote:
On Thu, 28 Dec 2006, Jan Burse wrote:
William Elliot wrote:
On Thu, 28 Dec 2006, Jan Burse wrote:

Correction at ** below.

We agree that it's theorem when (E!x)F(x).
In the event ~(E!x)F(x), the premise
ixF(x) = y
is false, thus promoting again the whole statement to truthood.

Ok, thanks.

What's the theorem that's part of this comment?
Please don't over clip, it derails continuity of thought.

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)

Derived rules of inference, bah.
The axiom
(Ax)G(x) -> G(t)
for any term t, you claim, cannot be used willy nilly with ixF(x).

Case (Ax)F(x)
case (Ax,y) x = y
(Ax)G(x) -> G(ixF(x))
case (Ex,y) x /= y
~G(ixF(x))
~[(Ax)G(x) -> G(ixF(x))]
Case ~(Ax)F(x)
(Ax)F(x) -> G(ixF(x))

** (Ax)G(x) -> G(ixF(x))

That is true, the axiom is for terms of the language,
not for syntactic term constructs, synthetic terms.

Moral of the story: don't use ixF(x) without (E!x)F(x).

.

Relevant Pages