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.