Register | Sign In


Understanding through Discussion


EvC Forum active members: 64 (9164 total)
2 online now:
Newest Member: ChatGPT
Post Volume: Total: 916,742 Year: 3,999/9,624 Month: 870/974 Week: 197/286 Day: 4/109 Hour: 0/0


Thread  Details

Email This Thread
Newer Topic | Older Topic
  
Author Topic:   "Godel, Escher, Bach" Help
JustinC
Member (Idle past 4869 days)
Posts: 624
From: Pittsburgh, PA, USA
Joined: 07-21-2003


Message 1 of 15 (306194)
04-23-2006 8:24 PM


I'm having trouble reconciling two statements in the book "Godel, Escher, Bach." I realize this is a pretty esoteric post so it may only pertain to those who've read the book or understand formal systems. Any help is appreciated though.
Towards the end of chapter three, he makes the statement
There exists recursively enumerable sets which are not recursive
Which means that if there is a way to generate a set from a given set of axioms using specific rules (a formal system for generating the set), there is not necessarily a formal system for generating the complementary set, i.e., all the numbers not in the set.
From this he claims
There exists formal systems for which there no typographical decision procedure
A decision procedure is a method that can be done in a finite amount of time that determines whether a string is a theorem (theorem= string that can be generated using the axioms and rules of the formal system).
He justifies this by stating
A typographical decision procedure is a method which tells theorems from non-theorems. The existence of such a test allows us to generate all nontheorems systematically, simply by going down a list of all strings and performing the test of them one at a time, discarding ill-formed strings and theorems along the way. this ammounts to a typographical method for generating the set of nontheorems (italics mine).
So what I got out of this is that going through the list of all strings and peforming a decision procedure on them will generate a set of theorems, and therefore the set of nontheorems, and this is a valid tyographical operation for generating nontheorems. Is this correct?
If it is, I have trouble reconciling that with a previous section where we are trying to generate the set of all primes. First he generated a formal system that gives all multiplications
Axiom Schema: xt-qx is an axiom, whenever x is a hyphen string
Rule of Inference: If x, y, and z are all hyphen strings and xtyqz is an old theorem, then xty-qzx is a new theorem
That might be hard to follow. Interpret is as: t=times, q=equals, - =1, -- =2, --- =3, etc.
Then he makes a rule which states:
Rule: If x,y, and z are hyphen-strings and if x-ty-qz is a theorom, then Cz is a theorem
This generates all composite numbers (non-primes).
Then he Proposes a rule for figuring out primes
Proposed Rule: If x is a hyphen-string and Cx is not a theorem (composite number), then Px is a theorem.
He states this is not allowed because while checking whether Cx is not a theorem we are going outside the system. What I think he means by this is that we cannot check strings which are not generated within the formal system.
But didn't he say that this is a valid method of generating a set at the top, i.e, we can look at all strings and run a decision procedure to generate set from non-set? Or is the reason this is outside the system in this case is because we don't have access to all the strings because axiom schema restricts us? Help!
Book Nook

Replies to this message:
 Message 3 by nwr, posted 04-23-2006 10:18 PM JustinC has not replied

  
AdminPD
Inactive Administrator


Message 2 of 15 (306196)
04-23-2006 8:45 PM


Thread moved here from the Proposed New Topics forum.

  
nwr
Member
Posts: 6409
From: Geneva, Illinois
Joined: 08-08-2005
Member Rating: 5.3


Message 3 of 15 (306208)
04-23-2006 10:18 PM
Reply to: Message 1 by JustinC
04-23-2006 8:24 PM


There exists recursively enumerable sets which are not recursive
Hmm. I just finished discussing the formal languages variant of this in a computer science class I am teaching.
I can't help with the specifics of GEB, since I never did finish reading that book. But I can outline the idea for the formal language variant.
The idea is that if you have a decision procedure that can tell if a word is in the language, then you can systematically generate a list of all words, test them, and put them in one list or the other.
The problem arises when you can decide if a word is in the language, but you cannot decide if a word is not in the language. A computer program might loop infinitely on words not in the language. Then generating all words and testing them will just get you into an infinite loop and won't generate the list (or set).
In the case of lists of primes, there is no problem.
I take it that the section you are looking at has to do with Goedel's incompleteness theorem. In that case the Goedel numbering is not being done within the formal system, but is instead done in the metamathematics. The metamathematical discussion maps proofs into arithmetic statements. If I recall, there is a diagonal argument that shows that there can be statements that would not be in the image of that map. However, not having read that part of GEB, I'm not sure if I am getting that right.
I'm not sure if I helped, or just further confused the issue.

This message is a reply to:
 Message 1 by JustinC, posted 04-23-2006 8:24 PM JustinC has not replied

  
JustinC
Member (Idle past 4869 days)
Posts: 624
From: Pittsburgh, PA, USA
Joined: 07-21-2003


Message 4 of 15 (306233)
04-24-2006 12:08 AM


Kindof confused me, but that's to be expected because my knowledge is very limited on this issue.
First, is a decision procedure inside the system or outside the system? Or can it be outside one system, and inside another?
Let me see if I can phrase my last post in a better way. Hofstadter states that
quote:
There exists formal systems for which there is no typographical decision procedure
He justifies this because
quote:
There are recursively enumerable sets which are not recursive.
So he's saying that if all r.e. sets had decision procedures, this would provide a typographical method for determining the negative set (all numbers not in the r.e. set), and so the r.e. set would be recursive.
But not all r.e. sets are recursive, so not all r.e. sets can have decision procedures.
Ok, so far so good (I think). But then I look at his typographical method (formal system) for determining the negative set, and it doesn't seem right.
He starts off with the set of all strings. Then he eliminates some if they are a theorem (using a decision procedure), and keeps the ones that are not theorems.
Well, how can he start off with all possible strings? I thought a formal system could only consist of a very limited amount of strings, i.e., the axioms and the theorems that follow from them.
If he starts off with the list of all possible strings then it seems that these have to be axioms, and hence theorems.
Thanks for the help.
This message has been edited by JustinC, 04-24-2006 12:12 AM

Replies to this message:
 Message 5 by nwr, posted 04-24-2006 1:07 AM JustinC has replied

  
nwr
Member
Posts: 6409
From: Geneva, Illinois
Joined: 08-08-2005
Member Rating: 5.3


Message 5 of 15 (306240)
04-24-2006 1:07 AM
Reply to: Message 4 by JustinC
04-24-2006 12:08 AM


Well, how can he start off with all possible strings?
These are strings over a finite set of characters (letters and symbols). So you can list them all in order. First list all the strings of length 1. Then list those of length 2. Then those of length 3, etc.
You never finish. But, given a string of length n, you will eventually list it.
Some of the strings might be gibberish. But they are still strings.
I thought a formal system could only consist of a very limited amount of strings, i.e., the axioms and the theorems that follow from them.
Here is where I am at a disadvantage, not having read GEB. However, I take it that he is considering all strings, not just those that are part of the formal system.
We might have a computer program. We feed in two strings. If the first string is a proof of the second string, then the program tells us it is, so the second string is a theorem. Otherwise it tells us that it is not a proof. The program doesn't care if the strings are gibberish, but of course gibberish strings won't be proofs or theorems.
Now, given a string, we want to determine if it is a theorem. So we go through the list of all possible strings to see if they are a proof of the string we are testing. If the string we are testing is a theorem, then after a finite amount of time we will come upon its proof. Unfortunately, if the string being tested is not a theorem, then this method of testing will continue infinitely and never give an answer. (Not sure if that is exactly what Hofstadter is doing).
If he starts off with the list of all possible strings then it seems that these have to be axioms, and hence theorems.
No. You have a finite set of axioms. But you can then put these axioms together to generate an inference (i.e. a proof of something). Some strings will turn out to be built out of axioms in the appropriate way to constitute an inference, or to constitute the statement of a theorem. Other strings won't (they might be gibberish).

This message is a reply to:
 Message 4 by JustinC, posted 04-24-2006 12:08 AM JustinC has replied

Replies to this message:
 Message 6 by JustinC, posted 04-24-2006 8:01 PM nwr has replied

  
JustinC
Member (Idle past 4869 days)
Posts: 624
From: Pittsburgh, PA, USA
Joined: 07-21-2003


Message 6 of 15 (306337)
04-24-2006 8:01 PM
Reply to: Message 5 by nwr
04-24-2006 1:07 AM


I think a problem is that I am misinterpreting Hofstadter. I'll just reproduce the short section verbatim. I'm having trouble understanding the last section "Illegally Characterized Primes." May be you can explain to me what exactly is talking about? Your help is greatly appreciated btw (I can't even begin to think of who I'd ask for help with this)
Starting with creating the tq-system
Axiom Schema: xt-qx is an axiom, whenever x is a hyphen string
Rule of Inference: Suppose that x, y, and z are all hyphen-strings. And suppose that xtyqz is an old theorem. Then xty-qzx is a new theorem.
Below is a derivation of the theorem --t---q------:
(1)--t-q-- (axiom)
(2)--t--q---- (by rule of inference, using line (1)
as old theorem)
(3)--t---q------ (by rule of inference, using line (2)
as old theorem)
Notice how the middle hyphen-string grows by one hyphen each time the rule of inference is applied; so it is predictable that if you want a theorem with ten hyphens in the middle, you apply the rule of inference nine times in a row
CAPTURING COMPOSITENESS
Multiplication, a slightly trickier concept than addition, has now been "captured" typographically, like the birds in Escher's Liberation. What about primeness? Here's a plan that might seem smart: using the tq-system, define a new set of theorems of the form Cx, which characterize composite numbers, as follows:
Rule: Suppose x, y, and z are hyphen strings. If x-ty-qz is a theorem, then Cz is a theorem
This works by saying that Z (the number of hyphens in z) is a composite as long as it is a product of two numbers greater than 1-namely, X +1 (the number of hyphens in x-), and Y +1 (the number of hyphens in y-). I am defending this new rule by giving you some "Intelligent mode" justifications for it. That is because you are a human being, and want to know why there is such a rule. If you were operating exclusively in "Mechanical mode", you would not need any justification, since M-mode workers just follow the rules mechanically and happily, never questioning them!
Because you work in the I-mode, you will tend to blur in your mind the distinction between strings and their interpretations. You see, things can become quite confusing as soon as you perceive "meaning" in the symbols which you are manipulating. You have to fight your own self to keep from thinking that string '---' is the number 3. The Requirement of Formality, which in Chapter I probably seemed puzzling (because it seemed so obvious), here becomes tricky, and crucial. It is the essential thing which keeps you from mixing up the I-mode with the M-mode; or said another way, it keeps from mixing up the arithmetical facts with typographical theorems.
ILLEGALLY CHARACTERIZING PRIMES
It is very tempting to jump from C-type theorems directly to P-type theorems, by proposing a rule fo the following kind:
Proposed Rule: Suppose x is a hyphen string. If Cx is not a theorem, then Px is a theorem.
The fatal flaw here is that checking whether Cx is not a theorem is not an explicitly typographical operation. To know for sure that MU is not a theorem of the MIU-system, you have to go outside the system...and so it is with the proposed rule. It is a rule with violates the whole idea of formal systems, in that it asks you to operate informally-that is, outside the system. Typographical operation (6) (keeping and using a list of previously generated theorems) allows you to look into the stockpile of previously found theorems, but this Proposed Rule is asking you to look into the hypothetical "Table of Nontheorems". But in order to generate such a table, you would have to do some reasoning outside the system- reasoning which shows why various strings cannot be generated inside the system. Now it may well be that there is another formal system which can generate the "Table of Nontheorems", by purely typographical means. In fact, our aim is to find just such a system. But the Proposed Rule is not a typographical, and must be dropped.
Could you kindly explain that last section to me?

This message is a reply to:
 Message 5 by nwr, posted 04-24-2006 1:07 AM nwr has replied

Replies to this message:
 Message 7 by nwr, posted 04-25-2006 10:56 PM JustinC has replied

  
nwr
Member
Posts: 6409
From: Geneva, Illinois
Joined: 08-08-2005
Member Rating: 5.3


Message 7 of 15 (306600)
04-25-2006 10:56 PM
Reply to: Message 6 by JustinC
04-24-2006 8:01 PM


Could you kindly explain that last section to me?
I'll give it a try.
The fatal flaw here is that checking whether Cx is not a theorem is not an explicitly typographical operation. To know for sure that MU is not a theorem of the MIU-system, you have to go outside the system...and so it is with the proposed rule.
The expression "go outside the system" is a bit confusing here.
The point is that you have some well defined inference procedures that you can use to determine that Cx is a theorem (assuming it is). Showing that Cx is a theorem would then be inside the system. But you don't have any clear procedure to determine that Cx is not a theorem. At best you could say "If have tried many ways of showing that Cx is a theorem, but they all failed." However, that doesn't show that Cx is not a theorem. There could be some other possible inference that you have not yet tried.
A platonist mathematician is quite happy to say that "Cx is not a theorem" is meaningful. That fits one's normal mathematical intuition. However there is no way to apply the rules of inference within the system so as to demonstrate that.
I hope that helps.

This message is a reply to:
 Message 6 by JustinC, posted 04-24-2006 8:01 PM JustinC has replied

Replies to this message:
 Message 8 by JustinC, posted 04-26-2006 8:07 PM nwr has replied

  
JustinC
Member (Idle past 4869 days)
Posts: 624
From: Pittsburgh, PA, USA
Joined: 07-21-2003


Message 8 of 15 (306880)
04-26-2006 8:07 PM
Reply to: Message 7 by nwr
04-25-2006 10:56 PM


quote:
The point is that you have some well defined inference procedures that you can use to determine that Cx is a theorem (assuming it is). Showing that Cx is a theorem would then be inside the system. But you don't have any clear procedure to determine that Cx is not a theorem. At best you could say "If have tried many ways of showing that Cx is a theorem, but they all failed." However, that doesn't show that Cx is not a theorem. There could be some other possible inference that you have not yet tried.
I think this helps. I think I was confusing that rule for inferring Cx with a decision procedure for determining Cx.
With just that rule of inference, there is no typographically explicit way to use that rule to determine whether a given Cx isn't a theorem.
Whereas if you have a decision procedure, you can just "run" it on a Cx and you can generate the two sets in a typographically explicit way.
But since "every r.e. set is not recursive," there can't be a decision procedure for every formal system.
Do I have the gist of it?
This message has been edited by JustinC, 04-26-2006 08:09 PM

This message is a reply to:
 Message 7 by nwr, posted 04-25-2006 10:56 PM nwr has replied

Replies to this message:
 Message 9 by nwr, posted 04-26-2006 10:32 PM JustinC has replied

  
nwr
Member
Posts: 6409
From: Geneva, Illinois
Joined: 08-08-2005
Member Rating: 5.3


Message 9 of 15 (306918)
04-26-2006 10:32 PM
Reply to: Message 8 by JustinC
04-26-2006 8:07 PM


Do I have the gist of it?
Yes.

This message is a reply to:
 Message 8 by JustinC, posted 04-26-2006 8:07 PM JustinC has replied

Replies to this message:
 Message 10 by JustinC, posted 04-26-2006 10:55 PM nwr has not replied

  
JustinC
Member (Idle past 4869 days)
Posts: 624
From: Pittsburgh, PA, USA
Joined: 07-21-2003


Message 10 of 15 (306920)
04-26-2006 10:55 PM
Reply to: Message 9 by nwr
04-26-2006 10:32 PM


Thanks for the help

This message is a reply to:
 Message 9 by nwr, posted 04-26-2006 10:32 PM nwr has not replied

  
JustinC
Member (Idle past 4869 days)
Posts: 624
From: Pittsburgh, PA, USA
Joined: 07-21-2003


Message 11 of 15 (308369)
05-02-2006 2:15 AM


Puzzle Help
I need a test for determining whether a number is a power of two, only using the expressions:
+ = addition
x = multiplication
A = For all numbers
E = There exists a number
Any thoughts?

Replies to this message:
 Message 12 by nwr, posted 05-02-2006 7:50 AM JustinC has replied

  
nwr
Member
Posts: 6409
From: Geneva, Illinois
Joined: 08-08-2005
Member Rating: 5.3


Message 12 of 15 (308421)
05-02-2006 7:50 AM
Reply to: Message 11 by JustinC
05-02-2006 2:15 AM


Re: Puzzle Help
Can it be recursive?
We can recursively define "x is a power of 2" as
x = 1, or there exists y such that y is a power of 2 and y+y=x
This message has been edited by nwr, 05-02-2006 07:15 AM

This message is a reply to:
 Message 11 by JustinC, posted 05-02-2006 2:15 AM JustinC has replied

Replies to this message:
 Message 13 by JustinC, posted 05-02-2006 6:32 PM nwr has not replied

  
JustinC
Member (Idle past 4869 days)
Posts: 624
From: Pittsburgh, PA, USA
Joined: 07-21-2003


Message 13 of 15 (308585)
05-02-2006 6:32 PM
Reply to: Message 12 by nwr
05-02-2006 7:50 AM


Re: Puzzle Help
I don't think you can use recursion because there is no way to write exponents in using the system.
But I did find the answer online:
b is a power of two.
~Ea:Ec:b=(SSS(a+a)*c)
Now, the numeral system used is:
O=0
SO=1
SSO=2
SSSO=3
etc.
So the statement, when translated is:
There do not exist numbers a and c such that the sum of 3 (SSS) plus 'a' plus 'a', multiplied by c, equals b.
Translated more, I read that as:
An odd number will never be the divisor of a power of two (besides 1. I think the (SSS) or 3 is there just in case a=o then the number will still be odd and greater than one).
Is this correct? And if so, how does one know that this is only a property of a power of two?

This message is a reply to:
 Message 12 by nwr, posted 05-02-2006 7:50 AM nwr has not replied

Replies to this message:
 Message 14 by JustinC, posted 05-02-2006 8:32 PM JustinC has not replied

  
JustinC
Member (Idle past 4869 days)
Posts: 624
From: Pittsburgh, PA, USA
Joined: 07-21-2003


Message 14 of 15 (308599)
05-02-2006 8:32 PM
Reply to: Message 13 by JustinC
05-02-2006 6:32 PM


Re: Puzzle Help
I guess I see it now.
You can't decompose 2 to anything other than 2 or 1, so you can't get an odd number greater than 1 that way.
And if you group them together its obviously always going to be even since there will always be a two in the multiplication.

This message is a reply to:
 Message 13 by JustinC, posted 05-02-2006 6:32 PM JustinC has not replied

Replies to this message:
 Message 15 by cavediver, posted 05-03-2006 5:01 AM JustinC has not replied

  
cavediver
Member (Idle past 3669 days)
Posts: 4129
From: UK
Joined: 06-16-2005


Message 15 of 15 (308689)
05-03-2006 5:01 AM
Reply to: Message 14 by JustinC
05-02-2006 8:32 PM


Re: Puzzle Help
And if so, how does one know that this is only a property of a power of two?
The other way to look at it is that under prime decomposition, all you have are 2 and the odd primes. Thus only the powers of 2 have no odd divisors.
Good thread BTW. Sorry not had time to contribute...

This message is a reply to:
 Message 14 by JustinC, posted 05-02-2006 8:32 PM JustinC has not replied

  
Newer Topic | Older Topic
Jump to:


Copyright 2001-2023 by EvC Forum, All Rights Reserved

™ Version 4.2
Innovative software from Qwixotic © 2024