题目：Logic as a practice
报告人：Olav Asheim （挪威奥斯陆大学哲学系教授）
主持人：张建军（伟德国际1946源于英国教授、逻辑所所长)
时间：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.