Second doubt
in [Logic]
|
Prev: Finite Variants upon Peano's Axioms
Next: Luminet-Poincare-Dodecahedral Space is empowering the "new math" #493 Correcting Math
From: marcos on 4 Mar 2010 12:47 Hello everybody. In Mendelson's "Introduction to mathematical logic" I've found a proposition very hard to understand. I will write it: "Definition 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 property B(u,y1,...yn), we often introduce a new funtion letter f(y1,...,yn) such that B(f(y1,...,yn),y1,...,yn) holds for all y1,...,yn. In cases where we have proved the existence of a unique object u that satisfies a wf B(u) and B(u) contains u as its only free variable, then we introduce a new individual constant b such that B(b) holds. (...) This can be made precise in the following manner: Proposition 2.28 Let K be a theory with equality. Assume that in K exists one and only one u such that 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) as well as all instances of axioms (A1)-(A7) that involve f. 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 deducible in K# f- If C is deducible in K#, then C# is deducible in K Hence, if C does not contain f and C is deducible in K#, then C is deducible in K Proof: By a simple 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) and C*) the f-transform of C. If C does not contain f, then let C be its own f-transfom. Clearly, (Exists v such that)(B(v,t1,...,tn) and C*)<-->C in K#. (Here, we use (There exists one and only one u such that) B(u, y1,...yn), deducible in K, and the axiom B(f(y1,...,yn),y1,...,yn) of K#)..." I don't write anymore because here stands my doubt. I don't understand this last mentioned step: How do we obtain the wf (Exists v such that)(B(v,t1,...,tn) and C*)<-- >C?. I've tried to write the proposition as clear as possible. Anyway, you can find this proposition in internet(page number 104). Thanks.
From: William Elliot on 5 Mar 2010 02:26 On Thu, 4 Mar 2010, marcos wrote: > "Definition 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 property B(u,y1,...yn), we often > introduce a new funtion letter f(y1,...,yn) such that > B(f(y1,...,yn),y1,...,yn) holds for all y1,...,yn. In cases where we > have proved the existence of a unique object u that satisfies a wf > B(u) and B(u) contains u as its only free variable, then we introduce > a new individual constant b such that B(b) holds. (...) This can be > made precise in the following manner: > Proposition 2.28 > Let K be a theory with equality. Assume that in K exists one and only > one u such that > 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) as well as all instances of axioms > (A1)-(A7) that involve f. 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 deducible in K# > f- If C is deducible in K#, then C# is deducible in K > Hence, if C does not contain f and C is deducible in K#, then C is > deducible in K > Proof: > By a simple 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) and C*) the f-transform of C. If C > does not contain f, then let C be its own f-transfom. Clearly, (Exists > v such that)(B(v,t1,...,tn) and C*)<-->C in K#. (Here, we use > (There exists one and only one u such that) B(u, y1,...yn), deducible in > K, and the axiom B(f(y1,...,yn),y1,...,yn) of K#)..." > I don't write anymore because here stands my doubt. I don't understand > this last mentioned step: > How do we obtain the wf (Exists v such that)(B(v,t1,...,tn) and C*)<-- >> C?. If C is P(f(x1,..xj)), then C* is P(v).
From: marcos on 5 Mar 2010 03:56 On 5 mar, 08:26, William Elliot <ma...(a)rdrop.remove.com> wrote: > On Thu, 4 Mar 2010, marcos wrote: > > "Definition 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 property B(u,y1,...yn), we often > > introduce a new funtion letter f(y1,...,yn) such that > > B(f(y1,...,yn),y1,...,yn) holds for all y1,...,yn. In cases where we > > have proved the existence of a unique object u that satisfies a wf > > B(u) and B(u) contains u as its only free variable, then we introduce > > a new individual constant b such that B(b) holds. (...) This can be > > made precise in the following manner: > > Proposition 2.28 > > Let K be a theory with equality. Assume that in K exists one and only > > one u such that > > 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) as well as all instances of axioms > > (A1)-(A7) that involve f. 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 deducible in K# > > f- If C is deducible in K#, then C# is deducible in K > > Hence, if C does not contain f and C is deducible in K#, then C is > > deducible in K > > Proof: > > By a simple 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) and C*) the f-transform of C. If C > > does not contain f, then let C be its own f-transfom. Clearly, (Exists > > v such that)(B(v,t1,...,tn) and C*)<-->C in K#. (Here, we use > > (There exists one and only one u such that) B(u, y1,...yn), deducible in > > K, and the axiom B(f(y1,...,yn),y1,...,yn) of K#)..." > > I don't write anymore because here stands my doubt. I don't understand > > this last mentioned step: > > How do we obtain the wf (Exists v such that)(B(v,t1,...,tn) and C*)<-- > >> C?. > > If C is P(f(x1,..xj)), then C* is P(v).- Ocultar texto de la cita - > > - Mostrar texto de la cita - Hello, William Elliot. My doubt remains the same. I know where does C* come from, but the last written wf (Exists v such that)(B(v,t1,...,tn) and C*)<-->C is still difficult to me.
From: William Elliot on 5 Mar 2010 08:23 On Fri, 5 Mar 2010, marcos wrote: > On 5 mar, 08:26, William Elliot <ma...(a)rdrop.remove.com> wrote: >> On Thu, 4 Mar 2010, marcos wrote: >>> "Definition 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 property B(u,y1,...yn), we often >>> introduce a new funtion letter f(y1,...,yn) such that >>> B(f(y1,...,yn),y1,...,yn) holds for all y1,...,yn. In cases where we >>> have proved the existence of a unique object u that satisfies a wf >>> B(u) and B(u) contains u as its only free variable, then we introduce >>> a new individual constant b such that B(b) holds. (...) This can be >>> made precise in the following manner: >>> Proposition 2.28 >>> Let K be a theory with equality. Assume that in K exists one and only >>> one u such that >>> 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) as well as all instances of axioms >>> (A1)-(A7) that involve f. 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 deducible in K# >>> f- If C is deducible in K#, then C# is deducible in K >>> Hence, if C does not contain f and C is deducible in K#, then C is >>> deducible in K >>> Proof: >>> By a simple 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) and C*) the f-transform of C. If C >>> does not contain f, then let C be its own f-transfom. Clearly, (Exists >>> v such that)(B(v,t1,...,tn) and C*)<-->C in K#. (Here, we use >>> (There exists one and only one u such that) B(u, y1,...yn), deducible in >>> K, and the axiom B(f(y1,...,yn),y1,...,yn) of K#)..." >>> I don't write anymore because here stands my doubt. I don't understand >>> this last mentioned step: >>> How do we obtain the wf (Exists v such that)(B(v,t1,...,tn) and C*)<-- >>>> C?. >> >> If C is P(f(x1,..xj)), then C* is P(v).- Ocultar texto de la cita - > My doubt remains the same. I know where does C* > come from, but the last written wf > (Exists v such that)(B(v,t1,...,tn) and C*)<-->C is still difficult to > me. > For <- use P(t) -> some x with P(x). For ->, from B(f(t1,.. tn), t1,.. tn) and uniqueness comes v = f(t1,.. tn). Thus substitue v in C* with f(t1,.. tn) to get C.
From: marcos on 6 Mar 2010 03:55
On 5 mar, 14:23, William Elliot <ma...(a)rdrop.remove.com> wrote: > On Fri, 5 Mar 2010, marcos wrote: > > On 5 mar, 08:26, William Elliot <ma...(a)rdrop.remove.com> wrote: > >> On Thu, 4 Mar 2010, marcos wrote: > >>> "Definition 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 property B(u,y1,...yn), we often > >>> introduce a new funtion letter f(y1,...,yn) such that > >>> B(f(y1,...,yn),y1,...,yn) holds for all y1,...,yn. In cases where we > >>> have proved the existence of a unique object u that satisfies a wf > >>> B(u) and B(u) contains u as its only free variable, then we introduce > >>> a new individual constant b such that B(b) holds. (...) This can be > >>> made precise in the following manner: > >>> Proposition 2.28 > >>> Let K be a theory with equality. Assume that in K exists one and only > >>> one u such that > >>> 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) as well as all instances of axioms > >>> (A1)-(A7) that involve f. 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 deducible in K# > >>> f- If C is deducible in K#, then C# is deducible in K > >>> Hence, if C does not contain f and C is deducible in K#, then C is > >>> deducible in K > >>> Proof: > >>> By a simple 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) and C*) the f-transform of C. If C > >>> does not contain f, then let C be its own f-transfom. Clearly, (Exists > >>> v such that)(B(v,t1,...,tn) and C*)<-->C in K#. (Here, we use > >>> (There exists one and only one u such that) B(u, y1,...yn), deducible in > >>> K, and the axiom B(f(y1,...,yn),y1,...,yn) of K#)..." > >>> I don't write anymore because here stands my doubt. I don't understand > >>> this last mentioned step: > >>> How do we obtain the wf (Exists v such that)(B(v,t1,...,tn) and C*)<-- > >>>> C?. > > >> If C is P(f(x1,..xj)), then C* is P(v).- Ocultar texto de la cita - > > My doubt remains the same. I know where does C* > > come from, but the last written wf > > (Exists v such that)(B(v,t1,...,tn) and C*)<-->C is still difficult to > > me. > > For <- use > P(t) -> some x with P(x). > > For ->, from B(f(t1,.. tn), t1,.. tn) > and uniqueness comes v = f(t1,.. tn). > > Thus substitue v in C* with f(t1,.. tn) to get C. > Thank you very much, William Elliot. |