Prev: solutions manual to Algebra Baldor
Next: Equilateral Triangle Tiler Conjecture! #512 Correcting Math
From: Begoña Castillo on 16 Mar 2010 05:00
On 16 mar, 08:08, William Elliot <ma...(a)rdrop.remove.com> wrote:
> On Mon, 15 Mar 2010, [ISO-8859-1] Begoña Castillo wrote:
I give up trying to understand this proposition. I will follow
reading
the book, and when I finish, I will read some other one more
comprehensive than this ( for example, Enderton's books of logic
and set theory). Set theory and Cantor's conclusions about the
infinite are amazing.
Thanks for trying to help an amateur like me, William Elliot,

From: Aatu Koskensilta on 16 Mar 2010 06:33
William Elliot <marsh(a)rdrop.remove.com> writes:

> His presentation is sloopy. He should first have defined C# and then
> proven (e) and (f). Instead he attempts to give the proof and the
> construction of C# when f occures in C simultaneously, letting the
> reader to compensate for his cheap explaination.

Mendelson's exposition is less than optimal in certain regards but your
complaint about the structure of the proof seems to be based on some
misunderstanding. Mendelson first defines a transformation taking atomic
formulas in the extended language to formulas in the original language,
and shows conditions a and e hold for this transformation. The
transformation is then extended to a more comprehensive transformation
taking arbitrarily complex formulas in the extended language to formulas
in the original language. It is clear from the construction that
conditions a - e hold for this extended transformation. So to finish the
proof it suffices to prove that f holds, which is relatively
straightforward if we avail ourselves to a bit of elementary model
theory, as Mendelson (quite sensibly) does. Whatever fault we find in
Mendelson's execution, there's nothing sloppy in this way of proving the
theorem.

--
Aatu Koskensilta (aatu.koskensilta(a)uta.fi)

"Wovon man nicht sprechan kann, dar�ber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: Aatu Koskensilta on 16 Mar 2010 09:38
Bego�a Castillo <begona3(a)gmail.com> writes:

> I give up trying to understand this proposition.

Let's consider the case where the defined function f is unary, with the
defining formula B(x,y) having two free variables. We have

1) T |- (x)(Ey)B(x,y)
2) T |- (x)(y)(z)(B(x,y) and B(x,z) --> z = y)

and we introduce a theory T' by setting

o the language of T' is that of T extended with a unary function letter
f

o the axioms of T' are those of T plus

(x)B(x, f(x))

Since all the axioms of T are also axioms of T' we obviously have: for
all formulas P in the language of T, if T |- P then T' |- P. It follows
that 2) in particular is provable in T' and hence

(*) T' |- (x)(y)(B(x, f(x)) and B(x, y) --> y = f(x))

that is, it is provable in T' that f(x) is the only y such that
B(x,y). In the portion of proof that troubles you we wish to construct,
for any atomic formula P in the language of T', a formula P' in the
language of T such that

T' |- P <--> P'

If we succeed in this it is a simply matter to extend the transformation
to all formulas in the language of T': given a formula P in the extended
language we just disassemble it to its atomic constituents, transform
those, and reassemble the result back into a formula in the language of
T, that is, into a formula in which f does not occur.

For simplicity, we'll consider formulas of the form R(t) for some
predicate letter R and term t. (The general case follows just by some
additional notational bookkeeping.) So let P = R(t) be an atomic formula
in the language of T'. If t doesn't contain f we don't need to do
anything, we can simply set P' = P. If f occurs in t pick the leftmost
subterm q of t of form f(r) where r is a term not containing f. (The
term q might be t itself.) Let Q be the result of replacing q in P with
a fresh free variable u, and let P* be:

(Eu)(B(x,u) & Q)

Now, P* is provably equivalent to P in T', by invoking (*). There are
fewer occurrences of f in P* than in P, so iterating the procedure,
yielding P**, P***, ... terminates at some point with a formula P' not
containing f, and hence in the language of T, provable equivalent in T'
to P.

> I will follow reading the book, and when I finish, I will read some
> other one more comprehensive than this ( for example, Enderton's books
> of logic and set theory).

Enderton presents essentially the same proof as Mendelson, but in a much
more readable manner, in Section 2.7 of his _A Mathematical Introduction
to Logic_.

--
Aatu Koskensilta (aatu.koskensilta(a)uta.fi)

"Wovon man nicht sprechan kann, dar�ber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: marcos on 16 Mar 2010 15:07
On 16 mar, 14:38, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote:
> Bego a Castillo <bego...(a)gmail.com> writes:
> > I give up trying to understand this proposition.
>
> Let's consider the case where the defined function f is unary, with the
> defining formula B(x,y) having two free variables. We have
>
>  1) T |- (x)(Ey)B(x,y)
>  2) T |- (x)(y)(z)(B(x,y) and B(x,z) --> z = y)
>
> and we introduce a theory T' by setting
>
>  o the language of T' is that of T extended with a unary function letter
>    f
>
>  o the axioms of T' are those of T plus
>
>       (x)B(x, f(x))
>
> Since all the axioms of T are also axioms of T' we obviously have: for
> all formulas P in the language of T, if T |- P then T' |- P. It follows
> that 2) in particular is provable in T' and hence
>
>  (*) T' |- (x)(y)(B(x, f(x)) and B(x, y) --> y = f(x))
>
> that is, it is provable in T' that f(x) is the only y such that
> B(x,y). In the portion of proof that troubles you we wish to construct,
> for any atomic formula P in the language of T', a formula P' in the
> language of T such that
>
>  T' |- P <--> P'
>
> If we succeed in this it is a simply matter to extend the transformation
> to all formulas in the language of T': given a formula P in the extended
> language we just disassemble it to its atomic constituents, transform
> those, and reassemble the result back into a formula in the language of
> T, that is, into a formula in which f does not occur.
>
> For simplicity, we'll consider formulas of the form R(t) for some
> predicate letter R and term t. (The general case follows just by some
> additional notational bookkeeping.) So let P = R(t) be an atomic formula
> in the language of T'. If t doesn't contain f we don't need to do
> anything, we can simply set P' = P. If f occurs in t pick the leftmost
> subterm q of t of form f(r) where r is a term not containing f. (The
> term q might be t itself.)  Let Q be the result of replacing q in P with
> a fresh free variable u, and let P* be:
>
>  (Eu)(B(x,u) & Q)
>
> Now, P* is provably equivalent to P in T', by invoking (*). There are
> fewer occurrences of f in P* than in P, so iterating the procedure,
> yielding P**, P***, ... terminates at some point with a formula P' not
> containing f, and hence in the language of T, provable equivalent in T'
> to P.
>
> > I will follow reading the book, and when I finish, I will read some
> > other one more comprehensive than this ( for example, Enderton's books
> > of logic and set theory).
>
> Enderton presents essentially the same proof as Mendelson, but in a much
> more readable manner, in Section 2.7 of his _A Mathematical Introduction
> to Logic_.
>
> --
> Aatu Koskensilta (aatu.koskensi...(a)uta.fi)
>
> "Wovon man nicht sprechan kann, dar ber muss man schweigen"
>  - Ludwig Wittgenstein, Tractatus Logico-Philosophicus

Only one question: you invoke (*) (T'I-(x)(y)(B(x,f(x))andB(x,y)--
>y=f(x)
to prove (Eu)B(x,u)&Q<-->R(t). Please, explain me the steps.
Thanks.

Marcos Castillo.

"No man is an Island, entire of itself;(...)"
John Donne, Meditation XVII
From: William Elliot on 17 Mar 2010 03:40
On Tue, 16 Mar 2010, Aatu Koskensilta wrote:
> William Elliot <marsh(a)rdrop.remove.com> writes:
>
>> His presentation is slopy. He should first have defined C# and then
>> proven (e) and (f). Instead he attempts to give the proof and the
>> construction of C# when f occurs in C simultaneously, letting the
>> reader to compensate for his cheap explanation.
>
> Mendelson's exposition is less than optimal in certain regards but your
> complaint about the structure of the proof seems to be based on some
> misunderstanding. Mendelson first defines a transformation taking atomic
> formulas in the extended language to formulas in the original language,
> and shows conditions a and e hold for this transformation.

I don't have the book. He didn't include an essential part,
namely the construction of C#.

> The transformation is then extended to a more comprehensive
> transformation taking arbitrarily complex formulas in the extended
> language to formulas in the original language. It is clear from the
> construction that conditions a - e hold for this extended
> transformation. So to finish the proof it suffices to prove that f
> holds, which is relatively straightforward if we avail ourselves to a
> bit of elementary model theory, as Mendelson (quite sensibly) does.

I was beginning to see that.

> Whatever fault we find in Mendelson's execution, there's nothing sloppy
> in this way of proving the theorem.

Taken out of context where I'm required to reconstruct the recursion
for defining C#, it did indeed, come across as sloppy and demandingly
hard to follow.
First  |  Prev  |  Next  |  Last
Pages: 1 2 3 4 5
Prev: solutions manual to Algebra Baldor
Next: Equilateral Triangle Tiler Conjecture! #512 Correcting Math