Re: Existence, Self-identity and Uniqueness.

Jan Burse wrote:

Chris Menzel wrote:
In his original post, Owen appears simply to be introducing definite
descriptions (i.e., expressions of the form "(the x:Fx)") á la Russell
as "incomplete symbols" -- they are not genuine singular terms in the
language, but only occur as parts of convenient definitions for more
complex expressions. Hence, they not available for substitution in
inference patterns like universal instantiation. So construed, his
introduction of definite descriptions does not take him beyond the
bounds of FOL=.

Strictly speaking FOL (with or without =) does
not know about definitions. Especially not about
definitions with some "matching and expansion"
behaviour. In FOL a definition is simply modelled
as a special universally closed aequivalence.

So if you have somewhere a definition
for a predicate symbol R:

R(x1,..,xn) =_df A(x1,..,xn) or synonymously
R(x1,..,xn) :<=> A(x1,..,xn)

resp. for a function symbol f:

f(x1,..,xn) =_df G(x1,..,xn) or synonymously
f(x1,..,xn) := G(x1,..,xn)

Then this is nothing else than working
with an additional element in your
background theory. Namely an element
for a predicate symbol R as follows:

forall x1,..,forall xn(R(x1,..,xn) <-> A(x1,..,xn))

resp. for a function symbol f as follows:

forall x1,..,forall xn(f(x1,..,xn)=G(x1,..,xn))

There are many many ways to mess up with
such definitions. For example if you use
terms t1,..,tn instead of variables in
x1,..,xn in the definition. Or if you use
multiple assignments to define a predicate.

A simple already messed up example is
the peano definition of addition:

0+x:=x.
x'+y:=x+y'.

The definitions D2 and D3 are also messed
up. They step out of the language of FOL=.
What about giving it a try in ZFC? In ZFC
we could define:

Z1) forall x forall F(one_and_only_one(F) & x in F
=> the(F) = x).

Z2) forall F(one_and_only_one(F) <=>
forall x forall z (x in F & z in F -> x=z) &
exists x x in F)

We have written out the definitions explicitly
as they would be added to the background
theory. Note that Z1 is a partial definition,
that is only in case x in F, we will say
something about the(F).

Note further that in Z2 we use a variant, that
splits the definition in two parts. One part for
the existence and one part for the uniqueness.
This is motivated by the way linguistically
the predicate was introduced by Owen.

Both definitions make no use of some special
forms. They are purely FOL=. Maybe the following
hits a rephrasing in ZFC of what Owen intended:

forall x(x in y <-> x=the(F)) -> one_and_only_one(y)

We cannot apply the axiom scheme of separation,
but the left hand side is already satisfiable
due the axiom of paring. As it is equivalent
to forall x(x in y <-> x=the(F) v x=the(F)).

We have now to show the two parts of one_and_only_one.
Lets look at the extistence part. It must be that
exists x x in y, which is now equal to exists x
x = the(F), which is trivially true in FOL=
because the(F) = the(F) is an instance of
reflexivity, i.e. forall x(x=x).

The uniqueness part is also simple. It must be
that forall x forall z(x in y & z in y -> x=y),
which is now equal to forall x forall z(x=the(F) &
z=the(F) -> z=x), which is trivially true in FOL=
because (x=the(F) & z=the(F) -> z=x) can be shown
by transitive and symmetry, i.e. forall x,y,z(
(x=y & y=z -> x=z) and forall x(x=y -> y=x).

But the result is not so much due to the fact that
we used Z1), the result is rather due to the fact
that we supplied a singleton to Z2). A much more
interesting exercise would be to find out whether
the following holds:

the(F) in F ??

Bye

P.S.: The above proof needs reflexivity, transitivity
and symetry of =. The approach of Owen suggests that
only reflexivity is needed. But it turns out that
Owen's definition even does not need reflexivity. Lets
look at the alternative definition:

Z2') forall F(one_and_only_one(F) <=>
exists x forall z(z=x <-> z in F)

Again exists x forall z(z=x <-> z in y) will equal
exists x forall z(z=x <-> z=the(F)). Which holds
because forall z(z=the(F) <-> z=the(F)) holds.
No references to some property of = here!














.

Relevant Pages

  • 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: E! quantification and equivalence
    ... equality in FOL. ... Suppose P is the only predicate symbol? ...
    (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 ...
    (sci.logic)