《Godel, Escher, Bach》的笔记-Chapter 1: The MU-puzzle
- 章节名：Chapter 1: The MU-puzzle
- 2017-12-01 23:06:10
Formal systemsP33 Requirement of Formality: The major point, which almost doesn't need stating, is that you must not do anything which is outside the rules. We might call this restriction the “Requirement of Formality”.
Even jumping out of the system to think about the meaning.
Theorems, axioms, rulesP35 Such strings, producible by the rules, are called theorems.I gave you a theorem for free at the beginning, namely MI. Such a “free” theorem is called an axiom
Are the mathematical axioms obtained from God? At least they should be a priori.P36 A derivation of a theorem is an explicit, line-by-line demonstration of how to produce that theorem according to the rules of the formal system.
Inside and outside the systemP36 But what if you asked a friend to try to generate U? It would not surprise you if he came back after a while, complaining that he can't get rid of the initial M, and therefore it is a wild goose chase. Even if a person is not very bright, he still cannot help making some observations about what he is doing, and these observations give him good insight into the task – insight which the computer program, as we have described it, lacks.It is possible to program a machine to do a routine task in such as way that the machine will never notice even the most obvious facts about what it is doing; but it is inherent in human consciousness to notice some facts about the things one is doing.P37 a car will never pick up the idea, no matter how much or how well it is driven, that it is supposed to avoid other cars and obstacles on the road; and it will never learn even the most frequent traveled routes of its owner.
现在有了人工智能技术，自动驾驶的问题就得以解决了。当然，这里作者说得也没有错：无论人工智能算法能够把汽车开得多么好，它本身从心智上来说是无法理解这算法的——它自己只不过是“机械化”程序的执行者。The difference, then, is that it is possible for a machine to act unobservant; it is impossible for a human to act unobservant. Notice I am not saying that all machines are necessarily incapable of making sophisticated observations; just that some machines are. Nor am I saying that all people are always making sophisticated observations; people, in fact, are often very unobservant. But machines can be made to be totally unobservant; and people cannot. And in fact, most machines made so far are pretty close to being totally unobservant. Probably for this reason, the property of being unobservant seems to be the characteristic feature of machines, to most people. For example, if somebody says that some task is “mechanical”, it does not mean that people are incapable of doing the task; it implies, though, that only a machine could do it over and over without ever complaining, or feeling bored.
Jumping out of the systemP37 It is an inherent property of intelligence that it can jump out of the task which it is performing, and survey what it has done; it is always looking for, and often finding, patterns.
人工智能算法是否也可以跳出当前正在执行的任务，“回过头来”对其加以审视，并发现其中的模式呢？这种监督与审视正在执行的任务——即算法——的功能就是算法的算法。这样看来，人工智能算法在一定程度上可以说是真的拥有“智能”的。当然，这种“智能”毕竟也是部分的和有限的，因为算法毕竟无法跳出算法的算法从而形成算法的算法的算法。或者即便可以做到这一点，但也终究不能无休止地跳出——因为一个合理的、现实的算法应该是在有限的时间内能够终止的。There are cases where only a rare individual will have t he vision to perceive a system which governs many peoples' lives, a system which had never before even been recognized as a system; then such people often devote their lives to convincing other people that the system really is there, and that it ought to be exited from!
They are philosophers!P38 It is very important when studying formal systems to distinguish working within the system from making statements or observations about the system.
跳出系统看问题。I am sure that every human being is capable to some extent of working inside a system and simultaneously thinking about what he is doing.
Decision proceduresP40 If there is a test for theoremhood, a test which does always terminate in a finite amount of time, then that test is called a decision procedure for the given formal system.P41 Certainly the rules of inference and the axioms of the MIU-system do characterize implicitly, those strings that are theorems. Even more implicitly, they characterize those strings that are not theorems. But implicit characterization is not enough, for many purposes. If someone claims to have a characterization of all theorems, but it takes him infinitely long to deduce that some particular string is not a theorem, you would probably tend to say that there is something lacking in that characterization – it is not quite concrete enough. And that is why discovering means, in effect, is that you can perform a test for theoremhood of a string, and that, even if the test is complicated, it is guaranteed to terminate. In principle, the test is just as easy, just as mechanical, just as finite, just as full of certitude, as checking whether the first letter of the string is M. A decision procedure is a “litmus test” for theoremhood!
若依据康德的观点，这里说的characterization显然是属于分析的而不是综合的。然而，我们也没有必要因为它是分析的就觉得悲观，毕竟characterization本身绝不是一件轻松或微不足道的工作。人类能够做到水晶般清晰和透彻地、具体地（concrete）表征一个系统，尽管是分析地，就已实属了不起了。The set of axioms must be characterized by a decision procedure – there must be a litmus test for axiomhood.
皮波迪先生对本书的所有笔记 · · · · · ·
P3 Frederick The Great, King of Prussia, came to power in 1740. ... The celebrated math...
Chapter 1: The MU-puzzle
abolition 废除, 废止 ad infinitum 无限地；永久地；无止境地 afford vt. 给予，提供；买得...
Two-part invention P45 「 以上无穷推理的过程相当于把人看作了没有意识和逻辑从而无法跳出...
说明 · · · · · ·