Prev: Finite Variants upon Peano's Axioms
Next: Luminet-Poincare-Dodecahedral Space is empowering the "new math" #493 Correcting Math
From: marcos on 11 Mar 2010 04:46
On 4 mar, 18:47, marcos <mar...(a)tomasacarolina.e.telefonica.net>
wrote:
> 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?..
>
Hello William Elliot and everybodi else. I still don't understand the
presence of the formula B(v,t1,...,tn) in the wf
(Exist v such that)(B(v,t1,...,tn)&C*)<-->C.

First  |  Prev  | 
Pages: 1 2
Prev: Finite Variants upon Peano's Axioms
Next: Luminet-Poincare-Dodecahedral Space is empowering the "new math" #493 Correcting Math