Computability Logic
可计算性逻辑
Graduate course taught at the Institute of Artificial Intelligence of Xiamen University in June-July 2007 by
Giorgi Japaridze
乔治 札帕日泽
（名） （姓）
Giorgi Japaridze was born in Georgia, former Soviet Union. He received two PhDs, one from Moscow State University (in logic) and the other from the University of Pennsylvania (in computer science). 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 recently introduced by him.
乔治.札帕日泽，生于前苏联格鲁吉亚共和国，拥有两个博士学位：莫斯科大学的（逻辑学）和 宾夕法尼亚大学的（计算机科学）。现在是美国维拉诺瓦大学计算机科学系的教授。主要研究领域：逻辑学以及逻辑学在计算机科学中的应用。可计算性逻辑 （这次课程的题目）-- 是他近年提出来的。这是第一次对中国进行学术访问.
Briefly about computability logic
Computability is certainly one of the most interesting and fundamental concepts in mathematics, philosophy and computer science, and it would be more than natural to ask what logic it induces. Let us face it: this question has not only never been answered, but never even been asked within a reasonably coherent and comprehensive formal framework. This is where Computability Logic (CL) 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, computability logic is not just a particular theory but an ambitious and challenging program for redeveloping logic following the scheme "from truth to computability". It was introduced by Japaridze in 2003 and, at present, still remains in its infancy stage, with open problems prevailing over answered questions. It is largely a virgin soil offering plenty of research opportunities, with good chances of interesting findings, for those with interests in logic and its applications in computer science, including theory of computation and artificial intelligence.
Computation and computational problems in CL are understood in their most general, interactive sense, and are precisely seen as games played by a machine (computer, agent, robot) against its environment (user, nature, or the devil himself). Computability of such problems means existence of a machine that always wins the game. Logical operators stand for operations on computational problems, and validity of a logical formula means being a scheme of "always computable" problems.
Remarkably, classical, intuitionistic and linear (in a broad sense) logics turn out to be three natural fragments of CL. This is no accident. The classical concept of truth is nothing but a special case of computability -- computability restricted to problems of zero interactivity degree. Correspondingly, classical logic is nothing but a special fragment of CL. One of the main -- so far rather abstract -- intuitions associated with intuitionistic logic is that it must be a logic of problems (Kolmogorov 1932); this is exactly what CL is, only in a much more expressive language than intuitionistic logic. And one of the main -- again, so far rather abstract -- claims of linear logic is that it is a logic of resources. Reversing of the roles of the machine and its environment turns computational problems into computational resources, which makes CL a logic of resources, only, again, in a more expressive language than that of linear logic, and based on an intuitively convincing and mathematically strict resource semantics rather than some naive philosophy and unreliable syntactic arguments. For more about CL vs. linear logic, visit Game Semantics or Linear Logic?.
The CL paradigm is not only about "what can be computed", but equally about "how can be computed". This opens potential application areas far beyond pure computation theory, such as:
The primary online source of on the subject is maintained at the Computability Logic Homepage.
可计算性无疑是数学、哲学和计算机科学中最有趣的、基本的概念之一。人们自然会问它推导出来的是什么逻辑，可事实上这个问题不仅从未得到过回答，甚至在相关的广泛领域里从来还没有 被提及过，这正是可计算性逻辑的起源。它是可计算性的形式理论，正如经典逻辑是真理的形式理论。更确切的说，可计算性逻辑不是一种特定的理论，而是一个充满雄心和挑战的计划 ，为在“从真理到可计算性”框架下重振逻辑。可计算性逻辑是Japaridze在2003年提出来的，目前还处于初级阶段，需解决的问题超过已解决的问题。这是一片还未开垦的领域，为那些对逻辑和逻辑在计算机方面的应用，以及对计算人工智能理论感兴趣的人们提供了很多研究和有趣发现的好机会。
计算和可计算问题在可计算性逻辑中被最普遍地理解为交互的， 它们被当作一种博弈。博弈的一方是机器（计算机、智能体、机器人），另一方是环境（用户、自然、或者魔鬼本身 ），问题的可计算性意味着存在一个机器总能赢得这个博弈，逻辑运算表示在可计算问题上的操作，一个逻辑公式的有效性表示它存在“总是可计算的”问题。
值得一提的是，经典的、直觉的和线性的（广义上）逻辑成为可计算性逻辑的三部分。真理的经典概念只是可计算性的特例----零交互问题的可计算性，相应的，经典逻辑只是可计算 性逻辑的特殊部分。和直觉逻辑相关联的（至今颇抽象的）主义是它应该是一种问题的逻辑，这也就是可计算性逻辑，只不过采用了比直觉逻辑更富表达能力的构造语言。 线性逻辑最重要的（又一颇抽象的）声称是它是一种资源逻辑，把机器和环境的角色换一下，计算问题就变成计算资源，这使得可计算性逻辑成为资源逻辑，同样也只是采用了比线性逻辑更富表达能力的构造语 言，并且是基于令人信服的直觉和严格数学语义,而非一些幼稚的哲学和不可信的依据句法构造推论的资源语义。要更详细地了解可计算性逻辑和线性逻辑的比较，可以访问网站博弈语义还是线性逻辑 ？
可计算性逻辑的实例不仅是关于“什么是能计算的”，相同程度的也关于“如何被计算”。这开放了远不止单纯计算理论的潜在应用领域，比如：
l 知识库系统 可计算性逻辑对于传统的知识库，知识表示和查询逻辑是个有吸引力的选择，它的优势包括：
Ø 可计算性逻辑是交互的，这是好的知识库逻辑需要具备的，毕竟现实中多数的知识库和信息系统是交互的。
Ø 可计算性逻辑是有资源意识的：一次性的验孕设备提供的潜在信息只是一个（即使任意一个）妇女的怀孕情况，而不是两个。可计算性逻辑自然地捕捉到了这种极微小的区别，但传统的系统无法说明这些。
Ø 可计算性逻辑很容易区分真理和一个主体发现/计算/认知什么是正确的实际能力。为达到相似的效果，传统的知识库逻辑必须借助有争议的、混乱的和惹麻烦的认知构造。
l 规划和行为系统 可计算性逻辑可能是传统人工智能规划逻辑的合理替代， 它的优点如下：
Ø 可计算性逻辑是交互的，规划系统应该能很好的解决一个主体和环境的交互。
Ø 一个良好的规划逻辑应该能够容易的说明这样的情况，即同一个弹道导弹可摧毁只有一个(即使任意一)目标,而不是两个，有资源意识的可计算性逻辑正好符合要求。
Ø 可计算性逻辑是知识和信息资源的逻辑，它能自动地处理知识前条件(knowledge preconditions)问题。
Ø 基于可计算性逻辑的规划系统似乎能避免臭名昭著的框架(frame)问题。
l 构造的应用理论 可计算性逻辑是经典逻辑的保守扩展，这使得可计算性逻辑在多数传统和没挑战性的应用领域里取代经典逻辑，尤其是很值得让可计算性逻辑代替经典逻辑作为应用理论（比如皮埃诺算术）的基础。这么做的好处包括基于可计算性逻辑的应用理论 比较基于经典逻辑的相应部分有下面的优点：
Ø 富有表达力：经典逻辑的语言只是可计算性逻辑语言的一小部分。
Ø 可计算的意义：基于可计算性逻辑的理论代表了可计算的问题而不仅是真语句。
Ø 建设性的：基于可计算性逻辑理论中的公式F的任何证据都可以有效地编码成由F代表的可计算问题的解答。
最主要的可计算性逻辑的网页
Selected papers on computability logic
关于可计算性逻辑选择的论文
The official journal versions of the following papers may be slightly different from the corresponding online preprints. It is recommended that you try to use the journal version first. Access to some journals may be restricted though, in which case you may download the online preprint.
以下论文在官方杂志上的版本可能跟网上的preprint稍微有一点不同。建议先尝试使用官方的杂志，除非它不能打开，再用preprint。
Precursors of computability logic
(most relevant pre-2003 papers)
可计算性逻辑的“先驱” （2003年以前最有关系的论文）
Some related papers by Chinese authors
一些中国作者的有关论文
The following papers are primarily or partially devoted to the logic of tasks (任务逻辑), introduced in item [7] (2002) of the previous list. The logic of tasks is essentially nothing but a special, relatively simple fragment of computability logic in a somewhat naive form. The author treats it as an "experimental stage" on the way leading to developing computability logic. The latter is a generalization and substantial refinement of the former, but otherwise the two are fully consistent, and results concerning the logic of tasks would typically automatically extend to computability logic as well.
Syllabus
Meeting times: Tuesdays and Thursdays 4:30-6:10.
授课时间：星期二和星期四 4:30-6:10.
课室 (Classroom): 教学楼 202
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.
这门课程没有课本。 所有的资料（包括演讲稿）可以在这个网页上得到。
Below is a tentative list of topics. Each topic is expected to take one or two lectures.
Overview of the theory of
computation:
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.
Overview of classical logic:
Propositional logic; Predicate (first-order)
logic; The classical concepts of truth and validity; Hilbert- and Gentzen-style axiomatizations;
The deduction theorem; Gödel's completeness theorem; Peano arithmetic; Gödel's
incompleteness theorems.
Games:
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 operations; Blind operations;
Parallel operations; Recurrence operations; Sequential operations.
Computability and validity:
The computational meanings of logical formulas;
"Truth" as computability; Validity versus uniform validity.
Deductive systems for computability logic:
The propositional logics CL1 and CL2; The
first-order logics CL3 and CL4; Affine logic; Intuitionistic logic.
Applied theories based on computability logic:
The advantages of such theories; The
philosophy of constructivism;
Computability-logic-based arithmetic.
Knowledge base systems based on computability logic:
Computability logic as a logic of knowledge;
Computability logic as a declarative programming language;
Resource-consciousness and constructiveness; Computability logic vs.
epistemic logics.
Systems for planning and action based on computability logic:
The logic of tasks; Reflections on the frame and
knowledge preconditions problems.
Cirquent calculus:
Linear logic;
Shallow cirquent calculus; Abstract resource semantics; Deep cirquent
calculus.
Open problems and future directions:
The need for developing better and richer syntax; Thoughts
about a to-be-developed theory of interactive complexity;
Potential applications in artificial intelligence - from theory to practice; A
hot list of
specific open problems.
Grading: A term paper should be submitted at the end of the semester, whose topic can be chosen by a student and approved by the instructor. Alternatively, a student may opt for taking a final examination instead of writing a term paper. The term paper or examination will contribute 50% toward your final grade. The remaining 50% will come from quizzes that will be given 5 to 10 times without warning, during the first 10-15 minutes of the class. Homework will be assigned after every meeting. It will not be collected or graded. However, the questions asked on a quiz will be typically based on (or be identical with) some questions from the latest 2 homework assignments. Students who listen actively, participate in discussions and volunteer answering questions may receive some extra credit at the time of deriving final grades.
评分标准： 学生在学期结束以前必须交一篇学期论文。题目可以由学生自己选择，再经过老师同意确定下来。另外，学生可以 选择参加学期考试代替学期论文。学期论文或者学期考试算学期分数的50%，其他的50%将由5-10次突然的小测试得到。这些小测试将在上课开始的10-15分钟进行。课外作业将在每次授课后布置，不需要上交，也不会评分，但是通常小测试中的问题会在前两次作业中出现。学生在课堂上积极讨论、主动回答问题的，可以在学期末的评分中得到额外的分数。
NOTE: The following lecture notes are NOT copyrighted. Anyone in the world is permitted to copy and use them with or without modifications, and with or without acknowledging the source.
Introduction [6月19日]: What is computability logic. Computability logic versus classical logic. The current state of developement.
Mathematical preliminaries [6月19日]: Sets. Sequences. Functions. Relations. Strings.
Overview of the theory of computation [6月19日 - 6月21日]: Turing machines. The traditional concepts of computability, decidability and recursive enumerability. The limitations of the power of Turing machines. The Church-Turing thesis. Mapping reducibility. Turing reducibility. Kolmogorov complexity.
Classical propositional logic (quick review) [6月21日 - 6月26日]: What logic is or should be. Propositions. Boolean operations. The language of classical propositional logic. Interpretation and truth. Validity (tautologicity). Truth tables. The NP-completeness of the nontautologicity problem. Gentzen-style axiomatizations (sequent calculus systems).
Classical first-order logic (quick review) [6月26日 - 6月28日]: Propositional logic versus first-order (predicate) logic. The universe of discourse. Constants, variables, terms and valuations. Predicates as generalized propositions. Boolean operations as operations on predicates. Substitution of variables. Quantifiers. The language of first-order logic. Interpretation, truth and validity. The undecidability of the validity problem. A Gentzen-style deductive system. Soundness and Gödel's completeness.
Games [6月28日 - 7月3日]: Games as models of interactive computational tasks. Constant games. Prefixation. Traditional computational problems as games. Departing from functionality. Departing from the input-output scheme. Departing from the depth-2 restriction. Propositions as games. Not-necessarily-constant games. Games as generalized predicates. Substitution of variables in games.
Negation and choice operations [7月3日]: 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.
Parallel operations [7月3日 - 7月5日]: 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.
Reduction [7月5日 - 7月10日]: 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.
Blind quantifiers [7月10日]: Unistructurality. The blind universal and existential quantifiers. DeMorgan's laws for blind quantifiers. The hierarchy of quantifiers. How blind quantification affects game trees.
Recurrence operations [7月12日 - 7月17日]: What the recurrences are all about. An informal look at the main types of recurrences. The parallel versus branching recurrences. Formal definition of the parallel recurrence and corecurrence. Evolution sequences for parallel recurrences. Weak reductions. Weakly reducing multiplication to addition. Weakly reducing the RELATIVES problem to the PARENTS problem. Weakly reducing the Kolmogorov complexity problem to the halting problem. The ultimate concept of algorithmic reduction. Definition of the branching recurrence and corecurrence. Evolution sequences for branching recurrences. A look at some valid and invalid principles with recurrences.
Static games [7月17日]: Some intuitive characterizations of static games. Dynamic games. Pure computational problems = static games. Delays. Definition of static games.
Interactive computability [7月17日]: Hard-play machines. Easy-play machines. Definition of interactive computability. The interactive version of the Church-Turing thesis.
The language and formal semantics of computability logic [7月19日]: The formal language. Interpretations. Definitions of validity and uniform validity. Validity or uniform validity? The extensional equivalence between validity and uniform validity. Computability versus "knowability". Closure under Modus Ponens. Other closure theorems. Uniform-constructive closure.
Cirquent calculus [7月19日]: 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.
Logic CL4 [7月24日]: 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).
Applied systems based on computability logic [7月26日]: 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. Computability-logic-based arithmetic.
Homework assignments
星期二 |
||||||
星期四 |
7月 26日 |