Prev: solutions manual to Algebra Baldor
Next: Equilateral Triangle Tiler Conjecture! #512 Correcting Math
From: marcos on 12 Mar 2010 03:58
Hello everybody. Some days ago I wrote to this group to solve one
doubt, and William Elliot tried to explain me. But the doubt remains.
Please can't anybody read the first message written with the title
"Second doubt" in this group?. Thanks in advance.
From: William Elliot on 12 Mar 2010 04:38
On Fri, 12 Mar 2010, marcos wrote:

> Hello everybody. Some days ago I wrote to this group to solve one
> doubt, and William Elliot tried to explain me. But the doubt remains.
> Please can't anybody read the first message written with the title
> "Second doubt" in this group?. Thanks in advance.
>
No. I delete inactive threads after two days
and I'm not going to search newsgroup archives
looking for it. Restate your question in as
streamlined of a fashion as possible.
From: Begoña Castillo on 12 Mar 2010 09:58
On 12 mar, 10:38, William Elliot <ma...(a)rdrop.remove.com> wrote:
> On Fri, 12 Mar 2010, marcos wrote:
> > Hello everybody. Some days ago I wrote to this group to solve one
> > doubt, and William Elliot tried to explain me. But the doubt remains.
> > Please can't anybody read the first message written with the title
> > "Second doubt" in this group?. Thanks in advance.
>
> No.  I delete inactive threads after two days
> and I'm not going to search newsgroup archives
> looking for it.  Restate your question in as
> streamlined of a fashion as possible.

I will write it entirely.
"Definitions of new function letters and individual constants:
In mathematics, once we have proved, for any y1,...,yn, the existence
of a unique object u that has a propety
B(u,y1,...,yn), we often introduce a new function letter f(y1,...,yn)
such that B(f(y1,...,yn),y1,...,yn) holds for all
y1,...,yn.(...). This can be made precise in the following manner.
Proposition 2.28
Let K be a theory with equality. Assume that is provable in K this
wf:exists one and only one u such that B(u,y1,...,yn)(I will write it
(E1u)B(u,y1,...,yn). Let K# be the theory with equality obtained by
adding to K a new function letter f of n arguments and the proper
axiom B(f(y1,...,yn),y1,...,yn).(...). Then there is an effective
transformation mapping each wf C of K# into a wf
C# of K such that:
a- If f does not occur in C, then C# is C
b- (¬C)# is ¬(C#)
c- (C-->D)# is C#-->D#
d- ((for every x)C)# is (for every x)(C#)
e- (C<-->C#) is provable in K#
f- If C is provable in K#, then C# is provable in K
Hence, if C does not contain f and C is provable in K#, then C is
provable in K
Proof
By a simple f-term we mean an expression f(t1,...,tn) in wich
t1,...,tn are terms that do not contain f. Given an atomic wf C of K#,
let C* be the result of replacing the leftmost occurrence of a simple
term f(t1,...,tn) in C by the first variable v not in C or B. Call the
wf (exists v such that)(B(v,t1,...,tn)&C*)(I will write it (Ev)
(B(v,t1,...,tn)&C*), the f-transform of C. If C does not contain f,
then let C be its own f-transform.
Clearly, (Ev)(B(v,t1,...,tn)&C*)<--->C in K#. (Here, we use
(E1u)B(u,y1,...,yn), provable in K, and the axiom
B(f(y1,...,yn),y1,...,yn) of K#).(...)"

I have tried several times to understand it, and for a moment I
thought so when you answered my question the last time, but it was an
ilusion. I don't know how to prove (Ev)(B(v,t1,...,tn)&C*)<-->C in
K# . As you see, the book mentions the wfs used.
Thanks, William Elliot.

From: William Elliot on 13 Mar 2010 02:34
On Fri, 12 Mar 2010, [ISO-8859-1] Bego�a Castillo wrote:

> "Definitions of new function letters and individual constants:
> In mathematics, once we have proved, for any y1,...,yn, the existence
> of a unique object u that has a propety
> B(u,y1,...,yn), we often introduce a new function letter f(y1,...,yn)
> such that B(f(y1,...,yn),y1,...,yn) holds for all
> y1,...,yn.(...). This can be made precise in the following manner.

> Proposition 2.28
> Let K be a theory with equality. Assume that is provable in K this
> wf:exists one and only one u such that B(u,y1,...,yn)(I will write it
> (E1u)B(u,y1,...,yn).

> Let K# be the theory with equality obtained by adding to K a new
> function letter f of n arguments and the proper axiom
> B(f(y1,...,yn),y1,...,yn).(...). Then there is an effective
> transformation mapping each wf C of K# into a wf C# of K such that:

> a- If f does not occur in C, then C# is C
> b- (�C)# is �(C#)
> c- (C-->D)# is C#-->D#
> d- ((for every x)C)# is (for every x)(C#)

What if f occures in C?

> e- (C<-->C#) is provable in K#
> f- If C is provable in K#, then C# is provable in K

> Hence, if C does not contain f and C is provable in K#, then C is
> provable in K

First you'd have to show that C is a wff of K.

> Proof

Proof of what? Your last statment, (e) or (f)?

> By a simple f-term we mean an expression f(t1,...,tn) in wich
> t1,...,tn are terms that do not contain f. Given an atomic wf C of K#,
> let C* be the result of replacing the leftmost occurrence of a simple
> term f(t1,...,tn) in C by the first variable v not in C or B. Call the
> wf (exists v such that)(B(v,t1,...,tn)&C*)(I will write it (Ev)
> (B(v,t1,...,tn)&C*), the f-transform of C. If C does not contain f,
> then let C be its own f-transform.

> Clearly, (Ev)(B(v,t1,...,tn)&C*)<--->C in K#. (Here, we use
> (E1u)B(u,y1,...,yn), provable in K, and the axiom
> B(f(y1,...,yn),y1,...,yn) of K#).(...)"
>
> I have tried several times to understand it, and for a moment I
> thought so when you answered my question the last time, but it was an
> ilusion. I don't know how to prove (Ev)(B(v,t1,...,tn)&C*)<-->C in
> K# . As you see, the book mentions the wfs used.
From: Begoña Castillo on 13 Mar 2010 04:19
On 13 mar, 08:34, William Elliot <ma...(a)rdrop.remove.com> wrote:
> On Fri, 12 Mar 2010, [ISO-8859-1] Begoña Castillo wrote:
> > "Definitions of new function letters and individual constants:
> > In mathematics, once we have proved, for any y1,...,yn, the existence
> > of a unique object u that has a propety
> > B(u,y1,...,yn), we often introduce a new function letter f(y1,...,yn)
> > such that B(f(y1,...,yn),y1,...,yn) holds for all
> > y1,...,yn.(...). This can be made precise in the following manner.
> > Proposition 2.28
> > Let K be a theory with equality. Assume that is provable in K this
> > wf:exists one and only one u such that B(u,y1,...,yn)(I will write it
> > (E1u)B(u,y1,...,yn).
> > Let K# be the theory with equality obtained by adding to K a new
> > function letter f of n arguments and the proper axiom
> > B(f(y1,...,yn),y1,...,yn).(...). Then there is an effective
> > transformation mapping each wf C of K# into a wf C# of K such that:
> > a- If f does not occur in C, then C# is C
> > b- (¬C)# is ¬(C#)
> > c- (C-->D)# is C#-->D#
> > d- ((for every x)C)# is (for every x)(C#)
>
> What if f occures in C?
>
> > e- (C<-->C#) is provable in K#
> > f- If C is provable in K#, then C# is provable in K
> > Hence, if C does not contain f and C is provable in K#, then C is
> > provable in K
>
> First you'd have to show that C is a wff of K.
>
> > Proof
>
> Proof of what?  Your last statment, (e) or (f)?
>
>
>
> > By a simple f-term we mean an expression f(t1,...,tn) in wich
> > t1,...,tn are terms that do not contain f. Given an atomic wf C of K#,
> > let C* be the result of replacing the leftmost occurrence of a simple
> > term f(t1,...,tn) in C by the first variable v not in C or B. Call the
> > wf (exists v such that)(B(v,t1,...,tn)&C*)(I will write it (Ev)
> > (B(v,t1,...,tn)&C*), the f-transform of C. If C does not contain f,
> > then let C be its own f-transform.
> > Clearly, (Ev)(B(v,t1,...,tn)&C*)<--->C in K#. (Here, we use
> > (E1u)B(u,y1,...,yn), provable in K, and the axiom
> > B(f(y1,...,yn),y1,...,yn) of K#).(...)"
>
> > I have tried several times to understand it, and for a moment I
> > thought so when you answered my question the last time, but it was an
> > ilusion. I don't know how to prove (Ev)(B(v,t1,...,tn)&C*)<-->C in
> > K# . As you see, the book mentions the wfs used.- Ocultar texto de la cita -
>
> - Mostrar texto de la cita -- Ocultar texto de la cita -
>
> - Mostrar texto de la cita -
I haven´t write all the paragraph. Thats why you don`t understand it.
I will write it:
"(...)Since the f-transform C' of C contains one less f than C and
C'<-->C is provable in K#, if we take succesive
f-transforms, eventually we obtain a wf C# that does not contain f and
such that C#<-->C is provable in K#. Call
C# the f-less transform of C. Extend the definition to all wfs of K#
by letting (¬D)# be ¬(D#), (D-->E)#
be D#-->E#, and ((every x)D)# be (every x)D#. Properties (a)-(e) of
proposition 2.28 are then obvious. To prove property
(f), it suffices, by property (e), to show that, if C does not contain
f and C is provable in K#, then C is provable in K. We may assume that
C is a closed wf, since a wf and its closure are deducible from each
other."
Sorry. I thought that it was enough to show until my doubt stood.

 |  Next  |  Last
Pages: 1 2 3 4 5
Prev: solutions manual to Algebra Baldor
Next: Equilateral Triangle Tiler Conjecture! #512 Correcting Math