[Search for users] [Overall Top Noters] [List of all Conferences] [Download this site]

Conference rusure::math

Title:Mathematics at DEC
Moderator:RUSURE::EDP
Created:Mon Feb 03 1986
Last Modified:Fri Jun 06 1997
Last Successful Update:Fri Jun 06 1997
Number of topics:2083
Total number of notes:14613

295.0. "Godel, Escher, Bach Problem" by BEING::POSTPISCHIL () Thu May 30 1985 19:19

There is a problem in Godel, Escher, Bach which I can not answer.  It is:

	Write "b is a power of 10" in Typographical Number Theory.

Help!

For those who have not read the book recently, a quick description of
Typographical Number Theory follows the form feed. 



				-- edp

Numerals.
	0 is a numeral.
	A numeral preceded by S is also a numeral.
	Examples:	0	S0	SS0	SSS0

Variables.
	a, b, c, d, and e are variables.
	A variable followed by a prime is also a variable.
	Examples:	a	c'	b''	e'''

Terms.
	All numerals and variables are terms.
	A term preceded by S is also a term.
	If s and t are terms, then so are (s+t) and (s*t).
	Examples:	0	b	SSa'	(S0*(SS0+c))
			S(Sa*(Sb*Sc))

Any of the following are well-formed formulas.

Atoms.
	If s and t are terms, then s=t is an atom.
	Examples:	S0=0	S(b+c)=((c*d)*e)
	If an atom contains a variable u, then u is free in it.

Negations.
	A well-formed formula preceded by a tilde is a well-formed formula.
	Examples:	~S0=0	~<0=0->S0=0>	~b=S0
	The quantification status of a variable (which says whether the
		variable is free or quantified) does not change under
		negation.

Compounds.
	If x and y are well-formed formulas, and provided that no variable
		which is free in one is quantified in the other, then the
		following are all well-formed formulas:
		<x&y>	<x|y>	<x->y>
	Examples:	<0=0^~0=0>	<b=b|~Ec:c=b>
	The quantification status of a variable does not change here.

Quantifications.
	If u is a variable, and x is a well-formed formula in which u is free,
		then the following strings are well-formed formulas:
		Eu:x and Au:x
	Examples:	Ab:<b=b|~Ec:c=b>


The interpretations of the above are fairly standard, although I have had
to substitute for some characters.  & and | are "and" and "or".  -> means
"implies".  "A" and "E" are substituted for the same letters, upside-down,
meaning "for all" and "there exists".

Example exercises:

	"All natural numbers are equal to 4" is expressed in Typographical
	Number Theory as Aa:a=4

	"There is no natural number which equals its own square" is
		~Ea:a=(a*a)

	"Different natural numbers have different successors" is
		Aa:Ab:<~a=b->~Sa=Sb>

	"If 1 equals 0, then every number is odd" is
		<S0=0->Aa:Eb:a=S(SS0*b)>

	"b is a power of 2" is
		Ac:<<Ed:b=(c*d)&Ae:<Ea:c=SSe*a->c=SSe>>->c=SS0>
T.RTitleUserPersonal
Name
DateLines
295.1BEING::POSTPISCHILTue Jun 11 1985 14:3821
Let me explain my TNT statement of "b is a power of 2".  It was

	Ac:<<Ed:b=(c*d)&Ae:<Ea:c=SSe*a->c=SSe>>->c=SS0>

This can be read as "Every prime number, c, which divides b is 2".  To say
"c is a prime number", I say "If 2+e divides c, then 2+e is c."

However, Stan suggested a simpler statement:  "Every number greater than 1
which divides b is divisible by 2".  In TNT, this is 

	Ac:<Ed:b=(SSc*d)->Ee:c=(e*SS0)>

Note that instead of saying "c is greater than 1", I just say "c+2 divides b".
Since c is "any number", c+2 is "any number greater than 1".

For the problem of expressing "b is a power of 10", it is simple to say "b
is a product of a power of 2 and a power of 5", but it is also necessary to
say the the power of 2 is the same as the power of 5.  Any ideas?


				-- edp
295.2BEING::POSTPISCHILThu Jun 20 1985 13:3563
If anyone is deterred from working on this problem because of the awkwardness
of translating to and from the symbols, feel free to use more normal language.
As an example, I have a moderately promising lead (best in a few years), which
I will discuss below in English (sort of).

It is fairly simple to say "b is the product of a power of 2 (c) and a power
of 5 (d).".  What is necessary then is to say that the two powers are the same,
that is, if c = 2^m and d = 5^n, then m = n.

The Goldbach Conjecture says every even number can be expressed as the sum
of not more than two primes ("number", herein, means "non-negative integer").
Although this has not been proven, I believe there is another theorem in which
the number of primes is greater, but still finite.  Suppose it is three.

If m and n are both odd (c and d do not have square roots), let c' = 2*c and
d' = 5*d.  If they are both even, let c' = c and d' = d.  (If they are not
both odd or both even, they are not equal, so no further work is necessary.)
The problem is now to show that the even powers of c' and d' are equal.

If it could be stated that there are three primes, p, q, and r, such that
2^p*2^q*2^r = c', then it would have to be true that 5^p*5^q*5^r = d', if
b is to be a power of 10.  There are three problems with this.

The first problem is the above-mentioned theorem.  This is not a serious
problem, as I believe the theorem exists.  The number of necessary primes may
not be three, but as long as it is finite, this method may work.

The second problem is stating that 2^p*2^q*2^r = c'.  Specifically, it is
necessary to say there exists a number x such that x = 2^p, a number y such
that y = 2^q, and a number z such that z = 2^r.  (Since it is also necessary
to do this with 5 substituted for 2, I will use "a" to denote the base.)  One
approach is to use Fermat's Theorem, which tells us a^p = a, mod p (because
p is prime and a is relatively prime to p).  Saying "x is the smallest number
greater than a such that x = a mod p" is almost the same as saying x = a^p. 
Unfortunately, if a is not equal to p-1 and a divides p-1, there may be a
number greater than a and less than a^p which satisfies the property
x = a, mod p.

The third problem is that it may be necessary for p, q, or r to be 2 or 5.
However, this is easily solved by dividing the problem into cases:

	None of p, q, and r are 2 or 5.
	Neither p nor q is 2 or 5, but r is 2.  Then just examine the numbers
		c'' and d'' such that c' = 4*c'' and d' = 25*d''.
	Neither p nor q is 2 or 5, but r is 5.  Then just examine the numbers
		c'' and d'' such that c' = 32*c'' and d' = 3125*d''.
	p is not 2 or 5, but q is 2 and r is 5.  Then just examine the numbers
		c'' and d'' such that c' = 128*c'' and d' = 78125*d''.

Three problems need to be resolved:

	What is the theorem which states every even number can be expressed
		as the sum of some finite number of primes?
	Under what conditions does some number satisfy a < x < a^p and
		x = a, mod p?
	How can the previous case be eliminated?

Note:  Differences of primes would serve as well as sums.  Is there a theorem
which states every even number can be expressed as the difference of two
primes?


				-- edp
295.3ALIEN::POSTPISCHILThu Jun 20 1985 16:598
My condition for the possibility of a number satisfying a < x < a^p and
x = a, mod p, is incorrect.  I will have to check, but a correct condition may
be: 

	a is not relatively prime to p-1.


				-- edp
295.4TURTLE::GILBERTThu Jun 20 1985 17:103
I've been detered from working on the problem, but not because of any
problems with the actual notation....  It's just difficult to find a
solution that's non-recursive, doesn't use sets, or introduce functions.
295.5ALIEN::POSTPISCHILThu Jun 20 1985 17:184
The condition posed in .3 is also incorrect.


				-- edp
295.6TOOLS::STANSat Jan 25 1986 17:0292
Newsgroups: net.math
Path: decwrl!pyramid!hplabs!hp-pcd!uoregon!luks
Subject: Godel-Escher-Bach ans. + new problem
Posted: 22 Jan 86 05:33:00 GMT
Organization: Univ of Oregon - Eugene, OR
Nf-ID: #N:uoregon:139800001:000:3261
Nf-From: uoregon!luks    Jan 21 21:33:00 1986
 
This is in response to following request from Eric Postpischil:
 
>In Godel, Escher, Bach, Douglas Hofstadter poses the problem of expressing "b
>is a power of 10" in Typographical Number Theory.  Does anybody have a solution
>for this?
 
I offer an outline of my solution to this, but I follow with an even more
intriguing version of the problem suggested by
Steve Becker, Physics Dept, Bucknell University, Lewisburg, PA 17837
(BITNET:  sbecker@bucknell ).
 
Solution to problem as stated:
 
Since the TNT formula is tedious to type or read, an outline of the
idea is best.
 
I assume it is clear how to express such assertions as
    "a > b", "a = b modulo (m)"    ("=" used for "is congruent to")
Hofstadter indicated how to express:  "p  is prime"
It is easy, for  p  prime, to express:  "n  is a power of  p"
(e.g., by asserting that  n  is divisible by no primes other than  p").
 
Now, "b  is a power of 10"  iff
 
   "b = rs  and  there exist  x  and  y such that
                     r = 2**x   and   s = 5**y   AND  x = y"
 
(We write it in this peculiar form to isolate the last conjunct "x = y",
which is the real hangup.)
 
Suppose that  r = 2**x, and  p  is any prime > r+1.  Observe that
the SMALLEST  t  such that  t  is a power of  p  and  t = r modulo (p-2)
is precisely  p**x .
 
(Proof:  For any  z,   p**z = 2**z modulo (p-2)
and so, if   p**z = r modulo (p-2)  with  z<x
then modulo (p-2):  2**x =  p**z = 2**z
so that   2**(x-z) = 1 modulo (p-2)
which implies  p-2 =< 2**(x-z) -1 =< 2**x -1
so that  p =< r+1, a contradiction.)
 
We can exploit this to express a predicate for the assertion
 
  A:  "p>r+1  and  p is prime  and
         there exists  x  such that  r = 2**x  and  t = p**x"
 
(for the last, by asserting  t = r modulo (p-2)  and there is
no  u<t  such that  u  is a power of  p  and   u = r modulo (p-2) ).
 
Similarly, if  s = 5**y, and  p  is any prime >s+4, the smallest  t
such that  t  is a power of  p  and   t = s modulo (p-5)
is  p**y.  So this gives us a handle on a predicate that asserts
 
  B:   "p>s+4  and  p is prime  and
          there exists  y  such that  s = 5**y  and  t = p**y"
 
What we want, finally, is
 
  "there exist  r and s  such that
     ( b = rs  and  there exist  p  and  t  such that  A and B)"
 
(eliminating one redundant "p is prime" if you like).
 
Note that, contrary (I think) to Hofstadter's warning that this may require
"quite a bit of number theory", we only seem to need Euclid's observation
that there are an infinite number of primes (so that  p  always exists).
 
====================
 
Now for Steve Becker's problem:
 
Express in Hofstadter's Typographical Number Theory:
 
   " b = 10**x "
 
The difference here, if it is not obvious, is that he wants you to identify
the exponent  x.  I found it hard to believe that this was possible in TNT.
However, it, and a lot more, can be so expressed.  Unless someone else comes
up with the answer, I shall post Steve's solution in about 10 days.
Meanwhile, those who wish to see the solution WITH ALL THE GORY TNT DETAILS
may write to him at the above address.
 
                      
		                      - Gene Luks,  University of Oregon
295.7BEING::POSTPISCHILWed Jan 29 1986 13:4738
To complete the original problem, I have written Gene Luks' solution in TNT.  It
is surprisingly short.  Note that the statements which assert modular
congruence, (e.g. a = b mod c) are not quite complete.  They say a = b+k*c,
where k is some non-negative integer instead of any integer.  However, this does
not matter because in each of these statements, b is known to be less than c, so
there is no a less than b which is congruent to b mod c. 

Ee:Ee':Ed:Ed':
 <b=(e*e')&
  <~Ea:Ec:d=(SSa*SSc)&				{ d is prime. }
   <Ec:d=(SSe+c)&				{ d >= e+2. }
    <Ec:d=(SSSSSe'+c)&				{ d >= e'+5. }
     <Aa:<Ec:d'=(SSa*c)->Ec:SSa=(d*c)>&		{ d' is a power of d. }
      <Aa:<Ec:e=(SSa*c)->Ec:a=(c+c)>&		{ e is a power of 2. }
       <Aa:<Ec:e'=(SSa*c)->Ec:a=(SSSSS0*c)>&	{ e' is a power of 5. }
        <Ec:(d'+(c+c))=(e+(c*d))&		{ d'=e mod d-2 (also d'>=e). }
         <Ec:(d'+(SSSSS0*c))=(e'+(c*d))&	{ d'=e' mod d-5 (also d'>=e'). }
          Aa':<<Aa:<Ec:a'=(SSa*c)->Ec:SSa=(d*c)>&
		Ec:<(a'+(c+c))=(e+(c*d))|(a'+(SSSSS0*c))=(e'+(c*d))>
	       >->
	       <Ec:a'=(d'+c)>
	       { (a' is a power of d and (a' = e mod d-2 or
		 a' = e' mod d-5)) implies a' >= d'.  In other
		 words, d' is the least number with these
		 properties. }
	      >
         >
        >
       >
      >
     >
    >
   >
  >
 >                            


				-- edp
295.8Solution to New ProblemALIEN::POSTPISCHILAlways mount a scratch monkey.Wed Feb 05 1986 18:3661
Network Mail received on 02-Feb-86 at 18:21

From: RHEA::DECWRL::"pyramid!hplabs!hp-pcd!uoregon!luks" "Eugene Luks"
To:   hp-pcd!hplabs!pyramid!decwrl!dec-rhea!dec-castor!postpischil
Subject: RE: Godel, Escher, Bach problem

. . .

This is another follow-up to the request from Eric Postpischil:

>In Godel, Escher, Bach, Douglas Hofstadter poses the problem of expressing "b
>is a power of 10" in Typographical Number Theory.  Does anybody have a solution
>for this?

In responding to Eric's request, I posted a solution that I had
worked out while reading that section of GEB.  It is both simple
and elementary but clearly ad-hoc.  As indicated, it answered
Hofstadter's specific challenge:

   "Express `b is a power of 10' in Typographical Number Theory"

but not a broader one (proposed by Steve Becker, BITNET: sbecker@bucknell):

   "Express `b = 10**x' in Typographical Number Theory"

In fact, Steve's problem is based upon the sources that Hofstadter
undoubtedly had in mind.  A significant result of mathematical logic
is the observation that a first-order theory based only upon Peano's
Postulates seems to incorporate all the basic statements and proofs
of elementary number theory.  See, for example, Chapter 3 of
[Introduction to Mathematical Logic, by Elliott Mendelson,
Van Nostrand, 1964], especially pp 131-134 where a technique is
developed for expressing any recursive function.  Steve followed
the recipe to obtain a solution to the second problem.

-----

Outline of solution:

It is easy to see that  "y = mod(n,m)"  is expressible in  TNT,
where  mod(n,m)  refers to the residue of  n modulo m, i.e., the
remainder when  n  is divided by  m.

Claim: the following statement (easy to convert to TNT) asserts "b = 10**x"

  "there exist  c  and  d  such that
          mod(c,1+d) = 1
      and
          mod(c,1+(1+x)d) = b
      and
          for all  v<x:   mod(c,1+(2+v)d) = 10*mod(c,1+(1+v)d)"

The proof of the claim is left as a nice exercise for the reader.
Hint: the Chinese Remainder Theorem is essential.

-----

Perhaps the above remarks will be deemed worthwhile by the respondents
to Eric's request who commented that the problem has "limited scope and
interest"  and that  "nobody cares about TNT"  and  "I couldn't imagine
duller problems than DHs".   Then again, perhaps not.
295.9Proof AvailableALIEN::POSTPISCHILAlways mount a scratch monkey.Thu Feb 06 1986 21:178
    I forgot to mention I have a proof for the claim made in the previous
    response.  It's obvious, almost trivial -- once you see it.  Really, if
    you've been following this problem, you'll kick yourself when you
    finally understand the statement made in the previous response.  If
    nobody posts an explanation/proof, I'll do it in a week or two. 
    
    
    				-- edp 
295.10ExplanationBEING::POSTPISCHILAlways mount a scratch monkey.Thu Feb 13 1986 20:2865
I am contemplating writing a program to write a Godel string for TNT.  Is
anybody interested?  Would anybody care to guess or estimate the length the
string will be? 

Here is the explanation for the statement in .8:

> Claim: the following statement (easy to convert to TNT) asserts "b = 10**x"
>
>   "there exist  c  and  d  such that
>           mod(c,1+d) = 1
>       and
>           mod(c,1+(1+x)d) = b
>       and
>           for all  v<x:   mod(c,1+(2+v)d) = 10*mod(c,1+(1+v)d)"

First, consider the sequence of numbers 1+d, 1+2d, 1+3d, . . . 1+(1+x)d.  I
will denote these with f(n), so f(n) = 1+d+nd, and the sequence runs from
f(0) to f(x).

Next, let g(n) = mod(c,f(n)).  (Recall that mod(a,b) is used here to indicate
the remainder when a is divided by b.  In the range of non-negative integers,
it is equivalent to the C function a%b.)

Observe that the above statements say:

	g(0) = 1,
	g(i+1) = 10*g(i) for 0 <= i < x, and
	g(x) = b,

so

	b = g(x)
	    g(x) = 10*g(x-1)
	           10*g(x-1) = 10*(10*g(x-1))
	. . .
				= 10^(x-1)*g(1) = 10^x*g(0)
						  10^x*g(0) = 10^x*1
							      10^x*1 = 10^x.

In the reverse direction, assume b = 10^x.  There are arbitrarily long
sequences of numbers which are relatively prime in pairs and which all exceed
an arbitrary value.  For example, consider the sequence 1+(1+i)*(2^m*n!), for
0 <= i <= n.  The smallest number in this sequence is 1+2^m*n!.  For a given
n, this can be made as large as desired by increasing m.  And the sequence can
be made as long as desired by increasing n.  I leave it as an exercise to show
that each pair of numbers in such a sequence is relatively prime.

Getting back to b = 10^x, let's make the smallest number in our sequence
greater than 10^x, and let's make the sequence at least x+1 numbers long.
Let d = 2^m*n! for whatever m and n are necessary to make such a sequence. 
Also, let's again denote the sequence with f(i).  Now we want a number c such
that: 

	mod(c,f(0)) = 1,
	mod(c,f(1)) = 10,
	. . .
	mod(c,f(x)) = 10^x.

Since all of the f's are greater than 10^x and they are all relatively
prime, the Chinese Remainder Theorem says there is such a c.  Thus we have a
c and a d that meet the necessary conditions, so b = 10^x implies the TNT
statement put forth.


				-- edp
295.11CLT::GILBERTJuggler of NoterdomThu Feb 13 1986 22:135
Nice work!

It appears that you've found a way to create recursive functions, right?
If so, asserting that 'x is a Fibonacci number' should be easy, and a
cogent description of how to define a recursive function would be useful.
295.12Fibonacci ExampleBEING::POSTPISCHILAlways mount a scratch monkey.Fri Feb 14 1986 15:3123
Re .11:

"x is a Fibonacci number" is equivalent to:

	There exist a c, a d, and an e such that

		c % (1+d) = 1,
		c % (1+2d) = 1,
		For all v < e,
			c % (1+(2+v)d) = (c % (1+(1+v)d)) + (c % (1+vd)),
		    and
		c % (1+(1+e)d) = x.

Isn't that simple!  For any recursive function, you just define the first terms,
then write the general rule, then say the last term equals the variable you are
describing. 

Basically, we've now got arrays in TNT.  c is an array, and d is used to
retrieve any element of the array.  c % (1+id) is the i-th element of the array,
where 0 < i <= size of the array.


				-- edp
295.13BEING::POSTPISCHILAlways mount a scratch monkey.Thu Feb 27 1986 20:1715
    There is a preliminary version of the program to compute a Godel-string
    for TNT in BEING""::USER:[POSTPISCHIL.PUB].  The source is in G.C,
    and the task image is in G.EXE.  Currently, it just writes a=10^a'
    and the conjunction of the axioms of TNT, but the source contains
    other routines, including a routine that asserts a relationship
    between four numbers, a, b, c, and d:
    
    	When a, b, c, and d are considered as encodings of strings,
    	and every occurrence of the variable 'c' in 'a' is replaced
    	with 'd', the result is 'b'.
    
    (That routine is isub.)
    
    
    				-- edp
295.14AITG::DERAMODaniel V. {AITG,ZFC}:: D'EramoSun Dec 04 1988 16:145
     What is the status of your attempt to compute a Godel-string
     for TNT (Typographical Number Theory).  Do you have any
     bounds (lower or upper) on its length?
     
     Dan
295.15BEING::POSTPISCHILAlways mount a scratch monkey.Mon Dec 05 1988 12:2412
    Re .14:
    
    It's within reach, but I stopped.  I was writing this as a set of
    routines to call other routines, each returning a statement or formula.
    Instead, I thought it might be better to write a little language in
    which I could describe statements or formulas, and write a parser for
    this language.  I believe that would be less cumbersome.
    
    I may take a look at what I have and report on it or start up again. 
    
    
    				-- edp 
295.16BEING::POSTPISCHILAlways mount a scratch monkey.Mon Dec 05 1988 13:4229
    Re .14:
    
    I've taken a cursory look at what I have.  Saying "this statement" is
    relatively easy and is largely done.  One messy part involved the
    statement that one string was identical to another when all occurrences
    of a certain variable were substituted with another expression, but
    that's done.  Statements like that only need to be written once, since
    I simply asserted that there existed a set of arrays in which
    corresponding members of each array had that property.  Later, you just
    write that numbers are corresponding elements of those arrays.  That in
    itself is relatively easy; you just say a number is the remainder when
    the number encoding the array is divided by (index+1)*key+1.
    
    The routines that represent these statements get fairly complex, and
    they are written in Polish Notation, with the function name followed by
    its arguments.
    
    But, as I recall, the hard part was writing the statements that assert
    a sequence of statements is a proof of a statement.  Previous
    assertions, such as that a variable is substituted throughout an
    expression, were fairly easy, since they only involved one
    substitution.  But the rules about proofs are more complex; they are
    interwoven and require referring to varying parts of the proof.  Just
    for starters, I need to express the rule saying you can copy a
    statement from above -- as long as it is not in a fantasy (the scope of
    an assumption) unless it is a fantasy you are already in. 
    
    
    				-- edp 
295.17AITG::DERAMODaniel V. {AITG,ZFC}:: D'EramoWed Dec 07 1988 01:1325
295.18BEING::POSTPISCHILAlways mount a scratch monkey.Wed Dec 07 1988 14:3243
    Re .17:
    
    I've already written the part about the substitution.  The variables
    involved are dst, src, ori, and rep, which are the complete destination
    string, the complete source string, the variable being substituted, and
    the expression replacing it.  These are C variables representing TNT
    variables whose numeric values represent TNT strings. 
    
    To say dst is the result of substiting rep for ori in src, I assert dst
    and src are the result of a step-wise process. 
    
    The step-wise process is:
    	Set srcx and dstx to null.
    	Concatenate s on the right of srcx and d on the right of dstx,
    		where s does not begin with a prime and s does not
    		contain any variable or s is completely a variable.
    		And if s is equal to ori, then d is equal to rep.
    	Repeat the previous step.
    	There exists a stopping point where srcx and dstx equal src
    		and dst.
    
    I don't need to worry about explaining how to break up src and dst; I
    can just say bunches of s's and d's exist, so all the steps exist, so
    you can get to dst from src somehow.  In that respect, writing this is
    a bit different from writing algorithms. 
    
    On the other hand, if I can avoid fantasies, that would be nice.  A
    major task at this point is to say something like "This string is the
    result of this other string and this statement, where this statement is
    a TNT axiom or is derived from one or more of the statements in the
    other string by valid TNT rules . . .".  If I did not have to quality
    which statements in the other string could and could not be used, that
    would mean I could say a and b were statements in the other string and
    c is the result of one of the following TNT rules applied to a and b: .
    . . . 
         
    That's one reason I was thinking of writing a language to describe this
    in.  There's also the matter of managing the allocation of TNT
    variables as they are needed, and so on.  That could all be eliminated
    from the language; it is currently visible in the code I have written. 
    
    
    				-- edp 
295.19tricky functionAITG::DERAMODaniel V. {AITG,ZFC}:: D'EramoWed Dec 07 1988 18:427
     Are you taking care to rename bound variables during a
     substitution if the term being spliced in has that variable
     free?  Or are you only handling substitution of "closed"
     terms (i.e. terms without variables, built up using 0 and
     the functions)?
     
     Dan
295.20BEING::POSTPISCHILAlways mount a scratch monkey.Wed Dec 07 1988 19:1715
    Re .19:
    
    The problem hasn't arisen.  I just have a way of saying "This string is
    the result of substituting this for that in the other string.".  There
    won't be any need to rename bound variables; one of the rules of proof
    construction will be that such substitutions are not allowed.  In other
    words, the author of the proof must have previously made whatever
    substitutions are necessary to make the current substition legal.
    
    And, of course, since we're only go to say that there is (or is not) a
    number that codes for such a proof, all the work of authorship is done
    for us.
    
    
    				-- edp 
295.21AITG::DERAMODaniel V. {AITG,ZFC}:: D'EramoThu Dec 08 1988 22:1624
     re .20
     
>>    And, of course, since we're only go to say that there is (or is not) a
>>    number that codes for such a proof, all the work of authorship is done
>>    for us.
     
     That "there exists" sure comes in handy!  
     
     But it also shows why you do have to avoid allowing the
     illegal substitution, because otherwise you can go from
     
          Aa:Eb:~a=b               ! provable from the arithmetic axioms
     
     to
     
          Eb:~b=b                  ! illegally substitute b for a
     
     ~Eb:~b=b is also provable, and using this contradiction a
     [number encoding a] proof will exist for every [number
     encoding a] formula.

     So be careful. :-)
     
     Dan
295.22another form (even harder to write out)AITG::DERAMODaniel V. {AITG,ZFC}:: D'EramoFri Jan 27 1989 01:5238
     Another deep and difficult to prove result here is that any
     recursively enumerable predicate P(x1,...,xn) over the
     nonnegative integers can be captured by a formula [in the
     sense described below] A(a ,...,a ) of the form
        1      n
     
          Eb :Eb :...Eb <s=t>
            1   2      m
     
     where s and t are terms in the variables a  and b
                                               i      j
     
     [I am using numerical subscripts instead of a,a',a'',...
     here.]
     
     By "captured by a formula" I mean for example if say
     P(3,7,5) is true, then the corresponding formula
     A(SSS0,SSSSSSS0,SSSSS5) is a theorem of TNT.
       3 S's   7 S's   5 S's
     
     The proof of true A(SSS0,SSSSSSS0,SSSSS5) is very simple; you
     just explicitly give the required numbers b  through b
                                                1          m
     and show that s=t when you plug all of the numbers in for
     the variables.  However, if P(2,0,1) is false, then proving
     ~A(SS0,0,S0) may be much more difficult, because it involves
     showing that no combination of b 's yields s=t.
                                     j
     
     In fact, true (in the standard model) but unprovable (from
     the axioms of TNT) sentences of the form
     
          ~Eb :Eb :...:Eb :<s=t>
             1   2       m
     
     where s and t are terms over the variables b  can be constructed.
                                                 m
     Dan
295.23those were subscriptsGUESS::DERAMODan D'EramoSat Nov 17 1990 21:5211
        re .-1
        
>>   sense described below] A(a ,...,a ) of the form
>>      1      n
        
        is supposed to read ...
        
>>   sense described below] A(a ,...,a ) of the form
>>        		       1      n
        
	Dan
295.24ZFC::deramoDan D'EramoTue Nov 19 1991 17:5413
Somewhere on usenet a while back I saw this...

Dan

>	A Goedel sentence was constructed by G.J. Chaitin at IBM Watson
>	research lab (Algorithmic Information Theory, Cambridge University
>	Press, ISBN 0-521-34306-2); it had about 900000 characters.  As well
>	as a simplified proof of Goedel's theorem, his book has a very pretty
>	theory analyzing complexity via the size of programs.
> 
>	-- 
>	David L. Rector				drector@orion.oac.uci.edu
>	Dept. of Math.				U. C. Irvine, Irvine CA 92717
295.25Yes but...CADSYS::COOPERTopher CooperTue Nov 19 1991 18:085