题目：Logic as a practice
报告人：Olav Asheim （挪威奥斯陆大学哲学系教授）
主持人：张建军（南京大学哲学系教授、逻辑所所长)
时间：2014年12月4日18:30-20:00
地点：哲学系楼小报告厅316
欢迎各位师生参加!
南京大学哲学系/现代逻辑与逻辑应用研究所
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.