Prev: solutions manual to Algebra Baldor
Next: Equilateral Triangle Tiler Conjecture! #512 Correcting Math
From: William Elliot on 14 Mar 2010 06:42
On Sat, 13 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?

Define C# for the case when 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)?

You still haven't answer this or my previous question.

>>> 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

So you're wanting to prove (e)?

>>> K# . As you see, the book mentions
>>> the wfs used. Ocultar texto de la cita

Bah. Google's dumb and rude instance of including unwanted clutter like
"Ocultar texto de la cita" is one of the reasons why not to use google.

> I haven�t write all the paragraph. Thats why you don`t understand it.

I don't understand it because you haven't answered my questions.

> 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.
>
From: Begoña Castillo on 14 Mar 2010 18:12
> Define C# for the case when f occures in C.

When f occures in C, C# is the f-less transform of C. If C contains
the new function letter added to K in order to obtain K#, then we must
replace it by variables not in C or B. An example of f-less transform
might be:
C is: (for every x)(exists y)(A(x,y,f(x,y,...,y))--->f(y,x,...,x)=x)
C# should be: (for every x)(exists y)(B(z,x,y,...,y)&A(x,y,z))---
>(exists z)(B(z,y,x,...,x)&z=x)

> >>> 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.

No, because C=C#. This means that there is not the new function letter
present in K#. K# is an extended theory with equality that includes K.

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

Yes.

> You still haven't answer this or my previous question.
>
> >>> 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
>
> So you're wanting to prove (e)?

Yes, I am.

> >>> K# . As you see, the book mentions
> >>> the wfs used. Ocultar texto de la cita
>
> Bah.  Google's dumb and rude instance of including unwanted clutter like
> "Ocultar texto de la cita" is one of the reasons why not to use google.

Certainly, google is boring sometimes.


> > I haven´t write all the paragraph. Thats why you don`t understand it.
>
> I don't understand it because you haven't answered my questions.

Hope to have explained well. Sorry for the delay answering, there is
been a busy weekend (drinking beer!!).

From: William Elliot on 15 Mar 2010 02:00
On Sun, 14 Mar 2010, [ISO-8859-1] Bego�a Castillo wrote:

As I don't remember the problem, I can't give an intelligent reply. Please
replace the beginning portion of the problem statement so I can see the
whole problem.

>> Define C# for the case when f occures in C.
>
> When f occures in C, C# is the f-less transform of C. If C contains
> the new function letter added to K in order to obtain K#, then we must
> replace it by variables not in C or B. An example of f-less transform
> might be:
> C is: (for every x)(exists y)(A(x,y,f(x,y,...,y))--->f(y,x,...,x)=x)
> C# should be: (for every x)(exists y)(B(z,x,y,...,y)&A(x,y,z))---
>> (exists z)(B(z,y,x,...,x)&z=x)
>
>>>>> 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.
>
> No, because C=C#. This means that there is not the new function letter
> present in K#. K# is an extended theory with equality that includes K.
>
Yes, because trivially C is wff of K.

>>>>> Proof
>>
>>>> Proof of what? �Your last statement, (e) or (f)?
>
> Yes.
>
Does that mean both?

>>>>> By a simple f-term we mean an expression f(t1,...,tn) in which
>>>>> 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
>>>>> illusion. I don't know how to prove (Ev)(B(v,t1,...,tn)&C*)<-->C in
>>
>> So you're wanting to prove (e)?
>
> Yes, I am.
>
>>>>> K# . As you see, the book mentions
>>>>> the wfs used. Ocultar texto de la cita
>>
> Certainly, google is boring sometimes.
>
> Hope to have explained well. Sorry for the delay answering, there is
> been a busy weekend (drinking beer!!).
>
Riddle of the day. Which is more boring,
.. . guzzling beer or guzzling Google?
From: Begoña Castillo on 15 Mar 2010 12:08
On 12 mar, 15:58, Begoña Castillo <bego...(a)gmail.com> wrote:
> On 12 mar, 10:38, William Elliot <ma...(a)rdrop.remove.com> wrote:
>
>
> 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#). Since the f-transform C' of C
> contains one less f than C and C'<-->C in K#, if we take
> succesive f-transforms, eventually we obtain a wf C# that
> does not contain f and such that C#<-->C in K#. Call C#
> the f-less transform of C. Extend the definition to all wfs
> of K# such that (b), (c) and (d) stands. Property (e) is
> already proven. 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."
> This is the whole proposition and the proof.
> I want to prove (e).
>
>
>
>
>

From: William Elliot on 16 Mar 2010 03:08
On Mon, 15 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).(...).

[is to be removed] (is to be inserted)

Then [there is an] (we define an) effective

>> transformation mapping each wf C of K# into a wf
....
>> C# of K [such that] (recursively):
>> 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#)

(By a simple f-term we mean an expression f(t1,...,tn)
in which t1,...,tn are terms that do not contain f.)

(A- If f does occur in C and C is the atomic forumla P(u1,.. uj)
then C# is B(v,t1,.. tn) & C* where C* is the result of replacing
the left most occurance of an f-term f(t1,.. tn), with a variable v,
not occuring in C nor B.)

The resulting transformation C# has the following properties.

>> e- (C<-->C#) is provable in K#
>> f- If 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 which
>> 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. ]

Have I edited the statement of 2.28 so that it's clearer and more precise?

>> 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#). Since the f-transform C' of C
>> contains one less f than C and C'<-->C in K#, if we take
>> succesive f-transforms, eventually we obtain a wf C# that
>> does not contain f and such that C#<-->C in K#. Call C#
>> the f-less transform of C. Extend the definition to all wfs
>> of K# such that (b), (c) and (d) stands. Property (e) is
>> already proven.

He's glossed over a lot of stuff proving (e).

>> 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."

More later as needed.

>> This is the whole proposition and the proof.
>> I want to prove (e).

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.
First  |  Prev  |  Next  |  Last
Pages: 1 2 3 4 5
Prev: solutions manual to Algebra Baldor
Next: Equilateral Triangle Tiler Conjecture! #512 Correcting Math