基于计算 ludics 的和谐性

Prawitz 将所谓的反演原则表述为根岑直觉主义自然演绎的特征之一。在证明论语义的文献中，这一原则常与另一称为恢复原则的原则相配对。通过采用计算 Ludics 框架，我们将这些原则重新表述为同一个条件，我们称之为和谐条件。我们展示这一重新表述使我们能够揭示立于这些原则背后的两种直观观念：反演原则中存在的‘包含’观念，以及恢复原则是反演原则的‘逆’这一观念。我们还在计算 Ludics 框架中表述了另外两个条件，并展示它们各自等价于和谐条件。