Efficient and Natural Proof Systems

我们都熟悉经典逻辑的语言，它通常用于数学和非形式论证，但还有其他重要和有用的逻辑。例如，一些非经典逻辑可以与编程语言相关联，以帮助控制其程序的行为，例如通过类型系统。为了定义逻辑的证明，我们需要一个由形式语言和一些推理规则组成的证明系统。我们通常按照一些已知的形式主义的规定来设计证明系统，以确保我们获得所需的数学性质。在任何情况下，我们都必须确保证明的有效性可以通过不超过一定限度的计算工作来检查。换句话说，我们希望检验正确性相对容易，这也是因为这一特性有助于设计自动发现证明的算法，然而，在检验证明的容易程度和证明的大小之间存在着一种紧张关系。如果证明太小，检查它是困难的。相反，使检查和寻找证明变得非常容易的形式主义创造了大量官僚主义的不自然的证明。所有传统的证明系统都在不同程度上受到这个问题的影响，因为所有传统的形式主义都是僵化的，它们给证明系统强加了过多的结构。我们打算设计一种形式主义，暂时称为形式主义B，在这种形式主义中，可以定义任意逻辑，并且以一种同时有效和自然的方式描述它们的证明。形式主义B在理想情况下位于证明系统类和包含原始证明的系统类之间的边界，原始证明是小而自然的，但太难检查。换句话说，我们希望通过在证明表示中保持尽可能多的效率来最大化自然性。这一努力的一个驱动力是使用现有的代数理论，这些理论似乎捕捉到了新形式主义所需要的一些结构。一个是理论上的：这个问题很有吸引力，解决这个问题很适合计算理论的研究工作，该理论试图将证明定义为更抽象的数学对象，而不仅仅是复杂的语法片段。只要说，我们目前无法用算法来决定，当同一陈述的两个看似不同的证明使用相同的思想时，它们是否等价。这是一个可以追溯到希尔伯特的问题，需要比传统语法提供的更抽象的方法来描述证明。第二个原因是实际的：我们需要形式证明来验证复杂计算机系统的正确性。计算机系统变得越强大，我们就越需要确保它们做它们应该做的事情。正式核查越来越多地被用作这方面的一个可行工具，但要使其成为日常工具，仍有许多工作要做。我们需要发明证明系统，简化与证明助手的交互，并且可以以某种规范的方式表示本质上相同的证明，以便在证明库中搜索和存储证明时不会发生重复。我们已经开发了一种新的设计方法证明系统，减少推理步骤的大小，以最小的条款，在一个理论称为“深度推理”。规则的精细尺度允许我们将证明与某些纯粹的几何对象联系起来，这些对象忠实地抽象出证明结构，并且是设计证明系统的自然指南，这些证明系统的证明不会受到几种形式的官僚主义的影响。简而言之，在十年之后，我们通过保留证明的性质，将证明分解为最小的部分，我们现正重新设计这些系统，使它们保留我们所需的一切功能，但不保留我们不需要的功能。

We are all familiar with the language of classical logic, which is normally used for both mathematical and informal arguments, but there are other important and useful logics. Some nonclassical logics, for example, can be associated with programming languages to help control the behaviour of their programs, for instance via type systems.In order to define the proofs of a logic we need a proof system consisting of a formal language and some inference rules. We normally design proof systems following the prescriptions of some known formalism that ensures that we obtain desirable mathematical properties. In any case, we must make sure that proofs can be checked for validity with a computational effort that does not exceed certain limits. In other words, we want checking correctness to be relatively easy, also because this property facilitates the design of algorithms for the automatic discovery of proofs.However, there is a tension between the ease by which proofs can be checked and their size. If a proof is too small, checking it is difficult. Conversely, formalisms that make it very easy to check and to search for proofs create big bureaucratic unnatural proofs. All traditional proof systems suffer to various extents from this problem, because of the rigidity of all traditional formalisms, which impose an excess of structure on proof systems.We intend to design a formalism, provisionally called Formalism B, in which arbitrary logics can be defined and their proofs described in a way that is at the same time efficient and natural. Formalism B will ideally lie at the boundary between the class of proof systems and that of systems containing proto-proofs that are small and natural, but are too difficult to check. In other words, we want to maximise naturality by retaining as much efficiency as possible in proof representation. A driving force in this effort will be the use of existing algebraic theories that seem to capture some of the structure needed by the new formalism.There are two main reasons for doing this. One is theoretical: the problem is compelling, and tackling it fits well into a research effort in the theory of computation that tries to define proofs as more abstract mathematical objects than just intricate pieces of syntax. Suffice to say that we are at present unable to decide by an algorithm when two seemingly different proofs of the same statement use the same ideas and so are equivalent, or not. This is a problem that dates back to Hilbert and that requires more abstract ways to describe proofs than traditional syntax provides.The second reason is practical: we need formal proofs to verify the correctness of complex computer systems. The more powerful computer systems become, the more we need to ensure that they do what they are supposed to do. Formal verification is increasingly adopted as a viable instrument for this, but still much needs to be done in order to make it an everyday tool. We need to invent proof systems that simplify the interaction with proof assistants, and that could represent in some canonical way proofs that are essentially the same, so that no duplication occurs in the search for and storing of proofs in proof libraries.This project intends to contribute by exploiting proof-theoretic advances of the past ten years. We have developed a new design method for proof systems that reduces the size of inference steps to their minimal terms, in a theory called `deep inference'. The finer scale of rules allows us to associate proofs with certain purely geometric objects that faithfully abstract away proof structure, and that are natural guides for the design of proof systems whose proofs would not suffer from several forms of bureaucracy.In short, after a decade in which we broke proofs into their smallest pieces, by retaining their properties, we are now reshaping them in such a way that they still retain all the features we need but do not keep the undesirable ones.