The syntactic nature of logic and computation separates them from other fields of mathematics. Nevertheless, syntax has been the only way to adequately capture the dynamics of proofs and programs such as cut-elimination, and the finiteness and the atomicity of syntax are preferable for foundational aims as seen in Hilbert's program. Another issue is that a uniform basis for logic and computation has been missing, and this problem hampers a coherent view on them. For instance, formal proofs in proof theory are far from (ordinary) proofs of the validity of a formula in model theory. Our goal is to solve these fundamental problems by rebuilding central concepts in logic and computation such as formal systems, validity (in such a way that it coincides with the existence of proofs), cut-elimination and computability uniformly in terms of finite graphs based on game semantics. Unlike game semantics, however, we do not rely on anything infinite or extrinsic to the graphs. A key idea that enables our finitary, autonomous approach is the shift from graphs in game semantics to dynamic ones. The resulting combinatorics establishes a single, syntax-free, finitary framework that recasts formal systems admitting proofs with cuts, validity, the finest computational steps of cut-elimination and higher-order computability. This subsumes fully complete semantics of intuitionistic linear logic, which solves a problem open for thirty years, and even extends the full completeness to proofs with cuts. As a byproduct, our dynamic graphs give rise to Hopf algebras, which opens up new applications of algebras to logic and computation.

翻译：逻辑与计算的句法本质使它们与其他数学领域区分开来。然而，句法一直是对证明与程序（如消割）的动态过程进行充分捕获的唯一方式，且句法的有限性与原子性符合基础性目标，如希尔伯特纲领所示。另一个问题是，逻辑与计算缺乏统一的基础，这阻碍了对其形成连贯的视角。例如，证明论中的形式证明远非模型论中公式有效性的（普通）证明。我们的目标是通过基于博弈语义的有限图重新构建逻辑与计算中的核心概念（如形式系统、有效性（使其与证明存在性一致）、消割与可计算性）来解决这些基本问题。但与博弈语义不同，我们并不依赖于任何无限或图外部的内容。实现这一有限自治方法的关键思想是将博弈语义中的图转变为动态图。由此产生的组合学建立了一个单一、无句法、有限的框架，该框架重新诠释了允许带割证明的形式系统、有效性、消割的最精细计算步骤以及高阶可计算性。这涵盖了直觉线性逻辑的完全完备语义——解决了一个三十年悬而未决的问题——甚至将完全完备性扩展到了带割的证明。作为副产品，我们的动态图产生了Hopf代数，这为代数在逻辑与计算中的新应用开辟了道路。