| |
 |
|
|
Science Forum Index » Logic Forum » technical question concerning the original proof of the Gode
Page 1 of 1
|
| Author |
Message |
| mx |
 Posted: Fri Jan 09, 2004 10:09 am |
|
|
|
Guest
|
hi,
i have very technical and boring question, but may be somebody out
there read the english translation of the Godel's original paper and
could help me..
here is an attemt to formmulate my problem (under each definition i
wrote how i understood it) :
on the page 153 of the 'Collected Works' edition of 'On formally
undecidable propositions...', Godel says:
'sign of type 1' is a "combination of signs" of the form SS....Sa,
where 'S'is a successor function and 'a' is a variable of type 1
(idividual variable) or the numeral 0. If 'a' is 0, we call such sign
a numeral (Zahlzeichen).
Next Godel writes:
"for n > 1 we understand by a <i> sign of type n </i> the same thing
as by <i>variable of type n </i> " ("Fur n > 1 verstehen wir unter
einem Zeichen n-ten Typs dasselbe wie Variable n-ten Typs")
then (on the page 165 of the same "Collected Works" edition )
he then gives the following definitions:
(9) R(x) := 2^x
'R(x) corresponds to the number sequence consisting of x alone'
(16)
0 N(x) := x
(n + 1) N(x) := R(3) * n N(x)
"n N x corresponds to the operation of 'putting the sign S n times in
front of x'"
As far as variables and 'signs' are concerned:
(11) n Var(x) := \exists(z)(13 < z =< x \and Prime(z) \and x = z^n )
\and ~(n = 0)
(so, for x to be a number corresponding to the variable of non-zero
type n, x has to be a nth power of a prime number larger then 13)
however, later on, he defines the 'sign of type n' as folows:
(1 Typ'_1(x) := (\exists m,n)(m,n =< x \and [ m = 1 \or 1 Var(m)] &
x = nN[R(m)])
(x is a number corresponding to the sign of type 1, if there are
numbers n,m such that m is 1 or m is a number corresponding to a
variable of type 1, and x is the result of preceding the number
sequence consisting of m alone with with n successor signs 'S')
(19) Typ_n(x) := (n = 1 \and Typ'_1(x)) \or (n > 1 \and (\exists
v)( v =< x \and nVar(v) \and x = R(v)))
(number corresponding to the sign of nth type is a number
corresponding to the sign of type 1, if n=1, or it is such number,
that there is a number v, smaller then x , and v corresponds to the
variable of type n and x is a sequence consisting of v alone)
my question is, in what sense 'sign of type n' and 'variable of type
n' are the same ('dasselbe') , given that the sign of the type n (n >
1) would be a number corresponding to the sequence, consisting of the
number corresponding to the variable of type n (so it would be 2 to
the power of such number - 2^(p^n) & Prime(p) ), not just a number
corresponding to the nth type variable (which would be of the form z^n
& Prime(z) ) and these numbers would in general not be the same? is
he speaking about some sort of 'semantic' sameness only? what did i
misunderstand?
thank you
maxim |
|
|
| Back to top |
|
| Charlie-Boo |
| Posted: Fri Jan 09, 2004 11:26 pm |
|
|
|
Guest
|
mx@is23dt.com (mx) wrote
Quote: hi,
i have very technical and boring question, but may be somebody out
there read the english translation of the Godel's original paper and
could help me.
Boring? Quite the contrary. It is refreshing to see someone discuss
something of significance. (Too much time is spent quibbling over
exercises in elementary arithmetic!)
Quote: My question is, in what sense 'sign of type n' and 'variable of type
n' are the same ('dasselbe')?
Let <a, b, . . . > represent the sequence of numbers a, b, c, . . .
Godel's system P (PM plus Peano's Axioms) contains:
variables of type 1: X1, Y1, Z1, . . .
variables of type 2: X2, Y2, Z2, . . .
variables of type 3: X3, Y3, Z3, . . .
etc.
signs of type 1: 0, S0, SS0, . . . , X1, SX1, SSX1, . . . , Y1, SY1,
SSY1, . . . , Z1, SZ1, SSZ1, . . .
signs of type 2: <X2>, <Y2>, <Z2>, . .
signs of type 3: <X3>, <Y3>< <Z3>, . . .
etc.
As you point out, the signs of type >1 are just the variables of type
Quote: 1 seen as sequences of length 1. The reason Godel defines signs of
type >1 is so that he can juxtapose these sequences to form elementary
formulas in (20) as: sign of type n+1(sign of type n). That is:
elementary formulas: X2(0), X2(S0), X2(SS0), . . . , X2(X1), X2(SX1),
X2(SSX1), . . . , Y2(0), Y2(S0), . . ., X3(X2), X3(Y2), . . .
Elementary formulas are relation variables with arguments. Subsequent
definitions include logical operators negation, disjunction and
quantification in order to build Godel numbers for all of (higher
order) Predicate Calculus theorem proving and show that the
corresponding relationships are recursive.
BTW: In (19) Godel includes v=<x but also includes x=R(v) and by (9)
R(x)=2^x so that v=<x is v=<2^v which is always true! (This logic
also occurs in 11.) Why does he include this redundant clause? IMHO:
This shows that these functions and relations are indeed recursive
(see theorem IV.)
I use the same technique in my Program Synthesis system
(http://www.mathpreprints.com/math/Preprint/CharlieVolkstorf/20021008.1/1
section IV Proof 1 Step 2 clause ~LT(J,A) in my synthesis of programs
that determine if one number is a factor of another.) Godel is just
using Logic as a programming language, just as Peano did before him to
write a program to demonstrate that the universal set of the natural
numbers is recursively enumerable, which is axiom 1 in Section VI of
http://www.arxiv.org/html/cs.lo/0003071 .
In fact, many of Godel's axioms and definitions of recursive functions
and relations are formal rules and theorems in this paper. This is
because a computer program is simply a constructive proof that a
particular set is recursive or recursively enumerable. Mathematicians
such as Peano, Godel and Turing for generations have been showing that
various sets and functions are, or are not, recursive or recursively
enumerable by constructing programs in various bases of computing.
Today we call that process Computer Programming!
Charlie Volkstorf
Cambridge, MA
|
|
|
| Back to top |
|
| mx |
| Posted: Sat Jan 10, 2004 6:10 pm |
|
|
|
Guest
|
hi
thank you very much for your posting, but seem not to be able to find
in it the answer to my question - how they are the same 'entities' if
they are coded by different numbers?
thank you
maxim
chvol@aol.com (Charlie-Boo) wrote in message news:<3df1e59f.0401092026.72a0432a@posting.google.com>...
Quote: mx@is23dt.com (mx) wrote
hi,
i have very technical and boring question, but may be somebody out
there read the english translation of the Godel's original paper and
could help me.
Boring? Quite the contrary. It is refreshing to see someone discuss
something of significance. (Too much time is spent quibbling over
exercises in elementary arithmetic!)
My question is, in what sense 'sign of type n' and 'variable of type
n' are the same ('dasselbe')?
Let <a, b, . . . > represent the sequence of numbers a, b, c, . . .
Godel's system P (PM plus Peano's Axioms) contains:
variables of type 1: X1, Y1, Z1, . . .
variables of type 2: X2, Y2, Z2, . . .
variables of type 3: X3, Y3, Z3, . . .
etc.
signs of type 1: 0, S0, SS0, . . . , X1, SX1, SSX1, . . . , Y1, SY1,
SSY1, . . . , Z1, SZ1, SSZ1, . . .
signs of type 2: <X2>, <Y2>, <Z2>, . .
signs of type 3: <X3>, <Y3>< <Z3>, . . .
etc.
As you point out, the signs of type >1 are just the variables of type
1 seen as sequences of length 1. The reason Godel defines signs of
type >1 is so that he can juxtapose these sequences to form elementary
formulas in (20) as: sign of type n+1(sign of type n). That is:
elementary formulas: X2(0), X2(S0), X2(SS0), . . . , X2(X1), X2(SX1),
X2(SSX1), . . . , Y2(0), Y2(S0), . . ., X3(X2), X3(Y2), . . .
Elementary formulas are relation variables with arguments. Subsequent
definitions include logical operators negation, disjunction and
quantification in order to build Godel numbers for all of (higher
order) Predicate Calculus theorem proving and show that the
corresponding relationships are recursive.
BTW: In (19) Godel includes v=<x but also includes x=R(v) and by (9)
R(x)=2^x so that v=<x is v=<2^v which is always true! (This logic
also occurs in 11.) Why does he include this redundant clause? IMHO:
This shows that these functions and relations are indeed recursive
(see theorem IV.)
I use the same technique in my Program Synthesis system
(http://www.mathpreprints.com/math/Preprint/CharlieVolkstorf/20021008.1/1
section IV Proof 1 Step 2 clause ~LT(J,A) in my synthesis of programs
that determine if one number is a factor of another.) Godel is just
using Logic as a programming language, just as Peano did before him to
write a program to demonstrate that the universal set of the natural
numbers is recursively enumerable, which is axiom 1 in Section VI of
http://www.arxiv.org/html/cs.lo/0003071 .
In fact, many of Godel's axioms and definitions of recursive functions
and relations are formal rules and theorems in this paper. This is
because a computer program is simply a constructive proof that a
particular set is recursive or recursively enumerable. Mathematicians
such as Peano, Godel and Turing for generations have been showing that
various sets and functions are, or are not, recursive or recursively
enumerable by constructing programs in various bases of computing.
Today we call that process Computer Programming!
Charlie Volkstorf
Cambridge, MA
thank you
maxim |
|
|
| Back to top |
|
| Charlie-Boo |
| Posted: Sat Jan 10, 2004 9:58 pm |
|
|
|
Guest
|
mx@is23dt.com (mx) wrote
Quote: hi
thank you very much for your posting, but seem not to be able to find
in it the answer to my question - how they are the same 'entities' if
they are coded by different numbers?
thank you
maxim
They are not really the same entities. Signs of type >1 are variables
of the same type number but as a sequence of one number. Just as 0 is
not the same as {0}, the number X is not the same as <X> the sequence
containing exactly one number X. Signs of type >1 are then joined
together to form elementary formulas. Godel defines the operation of
joining sequences (such as signs) to form a new sequence. So you have
to have sequences, not individual numbers, to join them to form a new
sequence, an elementary formula, in definition (20) in his paper.
Charlie Volkstorf
Cambridge, MA
Quote: chvol@aol.com (Charlie-Boo) wrote
mx@is23dt.com (mx) wrote
hi,
i have very technical and boring question, but may be somebody out
there read the english translation of the Godel's original paper and
could help me.
Boring? Quite the contrary. It is refreshing to see someone discuss
something of significance. (Too much time is spent quibbling over
exercises in elementary arithmetic!)
My question is, in what sense 'sign of type n' and 'variable of type
n' are the same ('dasselbe')?
Let <a, b, . . . > represent the sequence of numbers a, b, c, . . .
Godel's system P (PM plus Peano's Axioms) contains:
variables of type 1: X1, Y1, Z1, . . .
variables of type 2: X2, Y2, Z2, . . .
variables of type 3: X3, Y3, Z3, . . .
etc.
signs of type 1: 0, S0, SS0, . . . , X1, SX1, SSX1, . . . , Y1, SY1,
SSY1, . . . , Z1, SZ1, SSZ1, . . .
signs of type 2: <X2>, <Y2>, <Z2>, . .
signs of type 3: <X3>, <Y3>< <Z3>, . . .
etc.
As you point out, the signs of type >1 are just the variables of type
1 seen as sequences of length 1. The reason Godel defines signs of
type >1 is so that he can juxtapose these sequences to form elementary
formulas in (20) as: sign of type n+1(sign of type n). That is:
elementary formulas: X2(0), X2(S0), X2(SS0), . . . , X2(X1), X2(SX1),
X2(SSX1), . . . , Y2(0), Y2(S0), . . ., X3(X2), X3(Y2), . . .
Elementary formulas are relation variables with arguments. Subsequent
definitions include logical operators negation, disjunction and
quantification in order to build Godel numbers for all of (higher
order) Predicate Calculus theorem proving and show that the
corresponding relationships are recursive.
BTW: In (19) Godel includes v=<x but also includes x=R(v) and by (9)
R(x)=2^x so that v=<x is v=<2^v which is always true! (This logic
also occurs in 11.) Why does he include this redundant clause? IMHO:
This shows that these functions and relations are indeed recursive
(see theorem IV.)
I use the same technique in my Program Synthesis system
(http://www.mathpreprints.com/math/Preprint/CharlieVolkstorf/20021008.1/1
section IV Proof 1 Step 2 clause ~LT(J,A) in my synthesis of programs
that determine if one number is a factor of another.) Godel is just
using Logic as a programming language, just as Peano did before him to
write a program to demonstrate that the universal set of the natural
numbers is recursively enumerable, which is axiom 1 in Section VI of
http://www.arxiv.org/html/cs.lo/0003071 .
In fact, many of Godel's axioms and definitions of recursive functions
and relations are formal rules and theorems in this paper. This is
because a computer program is simply a constructive proof that a
particular set is recursive or recursively enumerable. Mathematicians
such as Peano, Godel and Turing for generations have been showing that
various sets and functions are, or are not, recursive or recursively
enumerable by constructing programs in various bases of computing.
Today we call that process Computer Programming!
Charlie Volkstorf
Cambridge, MA
thank you
maxim |
|
|
| Back to top |
|
| mx |
| Posted: Sun Jan 11, 2004 5:14 am |
|
|
|
Guest
|
so, when he says that they are the same ("dasselbe"), he is wrong?
chvol@aol.com (Charlie-Boo) wrote in message news:<3df1e59f.0401101858.29580bf4@posting.google.com>...
Quote: mx@is23dt.com (mx) wrote
hi
thank you very much for your posting, but seem not to be able to find
in it the answer to my question - how they are the same 'entities' if
they are coded by different numbers?
thank you
maxim
They are not really the same entities. Signs of type >1 are variables
of the same type number but as a sequence of one number. Just as 0 is
not the same as {0}, the number X is not the same as <X> the sequence
containing exactly one number X. Signs of type >1 are then joined
together to form elementary formulas. Godel defines the operation of
joining sequences (such as signs) to form a new sequence. So you have
to have sequences, not individual numbers, to join them to form a new
sequence, an elementary formula, in definition (20) in his paper.
Charlie Volkstorf
Cambridge, MA
chvol@aol.com (Charlie-Boo) wrote
mx@is23dt.com (mx) wrote
hi,
i have very technical and boring question, but may be somebody out
there read the english translation of the Godel's original paper and
could help me.
Boring? Quite the contrary. It is refreshing to see someone discuss
something of significance. (Too much time is spent quibbling over
exercises in elementary arithmetic!)
My question is, in what sense 'sign of type n' and 'variable of type
n' are the same ('dasselbe')?
Let <a, b, . . . > represent the sequence of numbers a, b, c, . . .
Godel's system P (PM plus Peano's Axioms) contains:
variables of type 1: X1, Y1, Z1, . . .
variables of type 2: X2, Y2, Z2, . . .
variables of type 3: X3, Y3, Z3, . . .
etc.
signs of type 1: 0, S0, SS0, . . . , X1, SX1, SSX1, . . . , Y1, SY1,
SSY1, . . . , Z1, SZ1, SSZ1, . . .
signs of type 2: <X2>, <Y2>, <Z2>, . .
signs of type 3: <X3>, <Y3>< <Z3>, . . .
etc.
As you point out, the signs of type >1 are just the variables of type
1 seen as sequences of length 1. The reason Godel defines signs of
type >1 is so that he can juxtapose these sequences to form elementary
formulas in (20) as: sign of type n+1(sign of type n). That is:
elementary formulas: X2(0), X2(S0), X2(SS0), . . . , X2(X1), X2(SX1),
X2(SSX1), . . . , Y2(0), Y2(S0), . . ., X3(X2), X3(Y2), . . .
Elementary formulas are relation variables with arguments. Subsequent
definitions include logical operators negation, disjunction and
quantification in order to build Godel numbers for all of (higher
order) Predicate Calculus theorem proving and show that the
corresponding relationships are recursive.
BTW: In (19) Godel includes v=<x but also includes x=R(v) and by (9)
R(x)=2^x so that v=<x is v=<2^v which is always true! (This logic
also occurs in 11.) Why does he include this redundant clause? IMHO:
This shows that these functions and relations are indeed recursive
(see theorem IV.)
I use the same technique in my Program Synthesis system
(http://www.mathpreprints.com/math/Preprint/CharlieVolkstorf/20021008.1/1
section IV Proof 1 Step 2 clause ~LT(J,A) in my synthesis of programs
that determine if one number is a factor of another.) Godel is just
using Logic as a programming language, just as Peano did before him to
write a program to demonstrate that the universal set of the natural
numbers is recursively enumerable, which is axiom 1 in Section VI of
http://www.arxiv.org/html/cs.lo/0003071 .
In fact, many of Godel's axioms and definitions of recursive functions
and relations are formal rules and theorems in this paper. This is
because a computer program is simply a constructive proof that a
particular set is recursive or recursively enumerable. Mathematicians
such as Peano, Godel and Turing for generations have been showing that
various sets and functions are, or are not, recursive or recursively
enumerable by constructing programs in various bases of computing.
Today we call that process Computer Programming!
Charlie Volkstorf
Cambridge, MA
thank you
maxim |
|
|
| Back to top |
|
| Charlie-Boo |
| Posted: Mon Jan 12, 2004 1:28 pm |
|
|
|
Guest
|
mx@is23dt.com (mx) wrote
Quote: so, when he says that they are the same ("dasselbe"), he is wrong?
I have seen that passage translated as "the same as" and as "just".
Godel did have a tendency of being a bit informal in the introductory
parts of his paper. Maybe someone who speaks German can help? All I
can say is that it is a number vs. a sequence consisting of only that
number.
Charlie Volkstorf |
|
|
| Back to top |
|
| |
|
Page 1 of 1
All times are GMT - 5 Hours
The time now is Sat Oct 11, 2008 5:14 pm
|
|