題目：Logic as a practice
報告人：Olav Asheim （挪威奧斯陸大學哲學系教授）
主持人：張建軍（伟德betvlctor网页版哲學系教授、邏輯所所長)
時間：2014年12月4日18:30-20:00
地點：哲學系樓小報告廳314
報告人簡介：
奧拉夫·阿斯海姆（Olav Asheim），奧斯陸大學哲學系教授。1991年獲奧斯陸大學哲學博士學位，師從著名分析哲學家與現象學家達格芬·佛洛斯達爾。長期緻力于邏輯哲學、語言哲學及會通分析哲學與現象學的工作，近年從事計算機博弈哲學研究。著有《指稱與意向性》、《真理與視域》等。
Professor Olav Asheim describes the topic of his lecture as follows:
The word “logic” is on the one hand used to denote theories of reasoning and argumentation, on the other hand to denote the subject matter of these theories: the structure of reasoning and argumentation itself. In addition the word may also refer to the practice of studying logic and developing logical theory. In my lecture I will emphasize the connection between logic as a practice and logical theory as it has developed through the times. My focus will be on Gottlob Frege's all-important seminal work and how the purpose of his work connects with the theory and development of the computer leading up to present day information technology. I will start by talking briefly about the study of logic in older times, and how logical theory as developed by Aristotle, and also the parallel development of logic in China and India, served the purpose of being a tool (“organon” in Aristotle's terminology) for argumentation with rhetorics as a supplementary tool. I will then go on to talk about Frege, the founder of modern logic. His aim was different: He wanted to find a means of deciding beyond doubt if an alleged mathematical proof is valid or not, in other words to construct a proof system governed by simple and exceptionless laws. Frege found that natural languages with their vagueness and ambiguities are not suited for this task, so he constructed what he called a “concept notation”, the forerunner of modern logical notation, in which the laws of logic could be expresssed absolutely unambiguously. I shall argue that it was only natural then that those following him should get the idea of mechanizing these laws, embodying them in a machine. I shall talk briefly about Frege's logicist program: his bold attempt at reducing arithmetics to pure logic. He gave up this attempt when Bertrand Russell discovered that a contradiction follows from the very axiom he had laid down to make the connection between logic and number theory. Russell, however, followed up the logicist program, making a revision to Frege's system known as the theory of types. Together with his colleague Alfred Whitehead he presented the new system in a book called Principia Mathematica. Logicians now tried to prove that this system was complete and free of contradictions, but had to give up when Kurt Gödel proved instead that a system with the strength of the Principia Mathematica system will always contain truths that cannot be proven if the system is consistent, and that a proof of its consistency cannot be given. This bears an interesting similarity to a paradox without being one. However, his proof also led to the first precise formulation of what can be effectively done. Allan Turing showed later that what can be effectively done can be done by a machine. He then set out to build one.
The word “logic” is on the one hand used to denote theories of reasoning and argumentation, on the other hand to denote the subject matter of these theories: the structure of reasoning and argumentation itself. In addition the word may also refer to the practice of studying logic and developing logical theory. In my lecture I will emphasize the connection between logic as a practice and logical theory as it has developed through the times. My focus will be on Gottlob Frege's all-important seminal work and how the purpose of his work connects with the theory and development of the computer leading up to present day information technology. I will start by talking briefly about the study of logic in older times, and how logical theory as developed by Aristotle, and also the parallel development of logic in China and India, served the purpose of being a tool (“organon” in Aristotle's terminology) for argumentation with rhetorics as a supplementary tool. I will then go on to talk about Frege, the founder of modern logic. His aim was different: He wanted to find a means of deciding beyond doubt if an alleged mathematical proof is valid or not, in other words to construct a proof system governed by simple and exceptionless laws. Frege found that natural languages with their vagueness and ambiguities are not suited for this task, so he constructed what he called a “concept notation”, the forerunner of modern logical notation, in which the laws of logic could be expresssed absolutely unambiguously. I shall argue that it was only natural then that those following him should get the idea of mechanizing these laws, embodying them in a machine. I shall talk briefly about Frege's logicist program: his bold attempt at reducing arithmetics to pure logic. He gave up this attempt when Bertrand Russell discovered that a contradiction follows from the very axiom he had laid down to make the connection between logic and number theory. Russell, however, followed up the logicist program, making a revision to Frege's system known as the theory of types. Together with his colleague Alfred Whitehead he presented the new system in a book called Principia Mathematica. Logicians now tried to prove that this system was complete and free of contradictions, but had to give up when Kurt Gödel proved instead that a system with the strength of the Principia Mathematica system will always contain truths that cannot be proven if the system is consistent, and that a proof of its consistency cannot be given. This bears an interesting similarity to a paradox without being one. However, his proof also led to the first precise formulation of what can be effectively done. Allan Turing showed later that what can be effectively done can be done by a machine. He then set out to build one.