The aim of this talk is to present a semantics for proofs in classical logic.

Classical logic: We use a variant of the proof-system introduced by Tait (1968), a system which is often used for analyzing the proof-theory of classical arithmetic and its fragments. The language of this logic consists of infinitary propositional formulas, and the proof-system for this language is formulated through a sequent calculus with infinitary rules of inference.

Proofs: The target of our analysis is not the derivability predicate “the formula A is derivable”, but the more subtle relation “p is a proof of the formula A”, that we abbreviate as “p der A.” In order to define this relation, we need to formalize the concept of “formula-free proofs”, i.e, proofs that does not depend (too much) on the formulas they prove. To understand the idea behind this concept, consider the untyped λ-calculus. By the Curry-Howard correspondence, λ-terms can be seen as a “formula-free” formalization of natural deduction proofs for the implicational fragment of intuitionistic propositional logic. Hence, “p der A” can be read as “the untyped λ-term p has (simple) type A in the Curry-style type assignment.” Here we use a similar idea: we define a class of objects that we call tests which play the role of the untyped λ-terms, and in order to define p der A, we use Tait’s normal rules as type assignment.

Semantics: Our semantics is deeply inspired by Girard’s ludics (2001). As in untyped λ-calculus β-reduction can be seen as natural deduction normalization “without types”, we similarly define a “formula-free” cut-elimination procedure which works with tests, that we call interaction. By analyzing the properties of interaction, we define another relation “p int A” between tests and formulas with the following meaning: “the result of the interaction between the test p and the counter-tests for A terminates.” We finally show a soundness-and-completeness theorem: “p der A” if and only if “p int A”.