Re: Existence, Self-identity and Uniqueness.

On Thu, 28 Dec 2006, Jan Burse wrote:
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 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))

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

  • Re: Philosophical question about empty set
    ... Jan Burse wrote: ... minus this Axiom are fully equipped ... so the axiom forall x(x in A iff x in B) still exists in some form? ...
    (sci.logic)
  • Re: Philosophical question about empty set
    ... Jan Burse wrote: ... the following axiom: ... A=B then forall x(x in A iff x in B) ...
    (sci.logic)
  • Making Sense of Tony
    ... exists X, forall x, Phix in X ... There is an axiom ... A set X is said to be an "initial segment" if X is ... Induction only works for internal sets. ...
    (sci.math)
  • / Class Theory.
    ... proper classes, some are named inner proper classes, others are named ... Two axiom schema applicable also to all classes in this theory are the ... forall A, Exists X, forall y (y in X Exists z (z in A and ...
    (sci.logic)
  • Re: / Class Theory.
    ... proper classes, some are named inner proper classes, others are named ... Two axiom schema applicable also to all classes in this theory are the ... forall A, Exists X, forall y (y in X Exists z (z in A and ...
    (sci.logic)