Advances in Mathematical Logic:

Computability Logic

(可计算性逻辑)

Graduate course taught at the Institute of Logic and Intelligence, Southwest University (西南大学 逻辑与智能研究中心) in June 2018 by

Giorgi Japaridze  (乔治。札帕日泽)

      


The professor 教授

Giorgi Japaridze holds two PhDs, one in philosophy (logic) from Moscow State University and the other in computer science from the University of Pennsylvania. Currently he works in the Computer Science Department of Villanova University, USA. The primary area of his research interests is logic and its applications in computer science. Computability logic - the subject of the present course - is an approach introduced by him.

    乔治.札帕日泽 拥有两个博士学位:逻辑学(莫斯科大学) 和 计算机科学(宾夕法尼亚大学)。现在是美国维拉诺瓦大学计算机科学系的教授。主要研究领域:逻辑学以及逻辑学在计算机科学中的应用。可计算性逻辑 (这次课程的题目)-- 是他提出来的。 


Briefly about computability logic 可计算性逻辑简介

Computability is one of the most interesting and fundamental concepts in mathematics, philosophy and computer science, and it is natural to ask what logic it induces. This is where Computability Logic (CoL) comes in. It is a formal theory of computability in the same sense as classical logic is a formal theory of truth. In a broader and more proper sense, CoL is not just a particular theory but an ambitious and challenging program for redeveloping logic following the scheme “from truth to computability”.

Under the approach of CoL, logical operators stand for operations on computational problems, formulas represent such problems, and their “truth” is seen as algorithmic solvability. In turn, computational problems --- understood in their most general, interactive sense --- are defined as games played by a machine against its environment, with “algorithmic solvability” meaning existence of a machine which wins the game against any possible behavior of the environment. With this semantics, CoL provides a systematic answer to the question “what can be computed?”, just like classical logic is a systematic tool for telling what is true. Furthermore, as it happens, in positive cases “what can be computed” always allows itself to be replaced by “how can be computed”, which makes CoL of potential interest in not only theoretical computer science, but many applied areas as well, including constructive applied theories, interactive knowledge base systems, resource oriented systems for planning and action, or declarative programming languages. On the philosophical side, CoL provides new insights into the foundations of logic and constructivism.

Currently CoL is still at an early stage of development, with open problems prevailing over answered questions. For this reason it offers plenty of research opportunities, with good chances of interesting findings, for those with interests in logic and its applications in computer science.

Literature

Computability Logic Homepage (a comprehensive online overview of the subject).

 

可计算性无疑是数学、哲学和计算机科学中最有趣的、基本的概念之一。人们自然会问它推导出来的是什么逻辑,可事实上这个问题不仅从未得到过回答,甚至在相关的广泛领域里从来还没有被提及过,这正是可计算性逻辑的起源。它是可计算性的形式理论,正如经典逻辑是真理的形式理论。更确切的说,可计算性逻辑不是一种特定的理论,而是一个充满雄心和挑战的计划 ,为在从真理到可计算性框架下重振逻辑。

 

计算和可计算问题在可计算性逻辑中被最普遍地理解为交互的,它们被当作一种博弈。博弈的一方是机器(计算机、智能体、机器人),另一方是环境(用户、自然、或者魔鬼本身 ),问题的可计算性意味着存在一个机器总能赢得这个博弈,逻辑运算表示在可计算问题上的操作,一个逻辑公式的有效性表示它存在总是可计算的问题。 由于这一语义,可计算性逻辑提供系统性的答案,什么是可以计算的的问题。就象经典逻辑是告诉我们什么是真理的系统性的工具。并且,可计算性逻辑的实例不仅是关于什么是能计算的,相同程度的也关于如何被计算。这个让可计算性逻辑不但在计算理论方面,而且许多应用领域也有潜在的优势。包括构造的应用理论、交互知识库系统、或者宣告式编程。在哲学方面,可计算性逻辑为逻辑的基础和构成主义提供新的视角。

 

可计算性逻辑目前还处于初级阶段,未解决的问题超过已解决的问题。因此,它可以为那些对逻辑感兴趣的人们提供很多研究的好机会。

 

文献

 

可计算性逻辑的网页


Syllabus 教学大纲

Meeting times and place  授课时间:周三19:00-21:00, 周四19:00-21:00. 课室: 学术报告庁

There is no textbook for this course. All written materials that you may need (including lecture notes) will be made available through this web site.

Topics: Turing machines; The Church-Turing thesis; The traditional notions of computability, decidability, recursive enumerability; The fundamental limitations of algorithmic methods; Mapping reducibility; Turing reducibility; Kolmogorov complexity; Games as universal models of an agent's interaction with the environment; Static vs. dynamic games; Interactive Turing machines; Interactive computability; Interactive version of the Church-Turing thesis; Game operations (negation; choice, parallel, blind and recurrence operations); Computational meanings of logical formulas; "Truth" as computability; Logical versus non-logical validity; Cirquent calculus; System CL4; Knowledgebase systems, planning systems and applied theories based on computability logic.

Grading: There will be a comprehensive examination at the end of the course, contributing 70% toward your final grade. The remaining 30% will come from quizzes which will be given 2 to 6 times without warning, during the first 10 minutes of the class. Homework will be posted after every meeting. It will not be collected or graded. However, the questions asked on a quiz or examination will be mostly based on (or be identical with) homework questions. Students who listen actively, participate in discussions and volunteer answering questions may receive some extra credit at the time of deriving final grades.


Lecture notes 讲稿

1.      Introduction What is computability logic. Computability logic versus classical logic. Unifying classical, “intuitionistic” and “linear” logics. The current state of development.

2.      Mathematical and computability-theoretic preliminaries Sets. Sequences. Functions. Relations. Strings. Turing machines. The traditional concepts of computability, decidability and recursive enumerability. The limitations of the power of Turing machines. The Church-Turing thesis. Mapping reducibilty. Turing reducibility. Kolmogorov complexity 

3.      Constant games Games as models of interactive computational tasks.The two players. Moves, positions and runs. Constant games defined. Prefixation. Traditional computational problems as games. Departing from functionality. Departing from the input-output scheme. Departing from the depth-2 restriction. Classical propositions as games.

4.      Not-necessarily-constant games Propositional versus first-order CoL. Constants and variables. Universes. Not-necessarily-constant games defined. Classical predicates and functions revisited. Predicates as elementary games. Unilegal runs and unistructural games. Visualizing unistructural games. Substituting functions for variables.

5.      Negation and choice operations About the operations studied in computability logic. Negation. The double negation principle. Choice conjunction and disjunction. Choice quantifiers. DeMorgan's laws for choice operations. The constructive character of choice operations. Failure of the principle of the excluded middle for choice disjunction.

6.      Parallel operations Parallel conjunction and disjunction. Free versus strict games. The law of the excluded middle for parallel disjunction. Resource-consciousness. Differences with linear logic. Parallel quantifiers. DeMorgan's laws for parallel operations. Evolution trees and evolution sequences.

7.      Reduction The operation of reduction and the relation of reducibility. Examples of reductions. The variety of reduction concepts and their systematization in computability logic. Mapping reducibility is properly stronger than (simply) reducibility.

8.      Blind quantifiers Unistructurality. The blind universal and existential quantifiers defined. DeMorgan's laws for blind quantifiers. The hierarchy of quantifiers. How blind quantification affects game trees. 

9.      Recurrence operations  What the recurrences are all about. An informal look at the main types of recurrences. Parallel recurrence versus branching recurrence. Formal definition of parallel (co)recurrence. Evolution sequences for parallel recurrences. Rimplicative reductions. Primplicatively reducing multiplication to addition. Primplicatively reducing the RELATIVES problem to the PARENTS problem. Primplicatively reducing the Kolmogorov complexity problem to the halting problem. Brimplication: the ultimate concept of algorithmic reduction. Definition of branching (co)recurrence. Evolution sequences for branching recurrences. A look at some valid and invalid principles with recurrences. Alternative definition of branching (co)recurrence.

10.  Static games  Some intuitive characterizations of static games. Dynamic games. Pure computational problems = static games. Delays. Definition of static games.

11.  Interactive computability  Hard-play machines. Easy-play machines. Definition of interactive computability. The interactive version of the Church-Turing thesis.

12.  The language and formal semantics of computability logic   The formal language. Interpretations. Validity. Logical or nonlogical validity? Computability versus “knowability”. Closure under Modus Ponens. Other closure theorems. Uniform-constructive closure.

13.  Cirquent calculus About cirquent calculus in general. The language of CL5. Cirquents. Cirquents as circuits. Formulas as cirquents. Operations on cirquents. The rules of inference of CL5. The soundness and completeness of CL5. A cirquent calculus system for classical logic. CL5 versus affine logic.

14.  Logic CL4  The language of CL4. The rules of CL4. CL4 as a conservative extension of classical logic. The soundness and completeness of CL4. The decidability of the blind-quantifier-free fragment of CL4. Other axiomatizations (affine and intuitionistic logics).

15.  Applied systems based on computability logic Computability logic as a problem-solving tool. Knowledgebase systems based on computability logic. Constructiveness, interactivity and resource-consciousness. Systems for planning and action based on computability logic. Applied theories based on computability logic. CoL-based arithmetic.


Homework 课外作业

531   66   67   613

614   620

 

 

 

 

Web Analytics