Related papers: What is the meaning of proofs? A Fregean distincti…

In logic there is a clear concept of what constitutes a proof and what not. A proof is essentially defined as a finite sequence of formulae which are either axioms or derived by proof rules from formulae earlier in the sequence.…

At the heart of intuitionistic type theory lies an intuitive semantics called the "meaning explanations"; crucially, when meaning explanations are taken as definitive for type theory, the core notion is no longer "proof" but "verification".…

This paper discusses proof-theoretic semantics, the project of specifying the meanings of the logical constants in terms of rules of inference governing them. I concentrate on Michael Dummett's and Dag Prawitz' philosophical motivations and…

A central problem in proof-theory is that of finding criteria for identity of proofs, that is, for when two distinct formal derivations can be taken as denoting the same logical argument. In the literature one finds criteria which are…

We define a proof system for exceptions which is close to the syntax for exceptions, in the sense that the exceptions do not appear explicitly in the type of any expression. This proof system is sound with respect to the intended…

Mathematical proofs are often said to justify their conclusions by indicating the existence of a corresponding formal derivation. We argue that this widespread view relies on an under-examined notion of correspondence, or what it means for…

A proof is one of the most important concepts of mathematics. However, there is a striking difference between how a proof is defined in theory and how it is used in practice. This puts the unique status of mathematics as exact science into…

I deal with two approaches to proof-theoretic semantics: one based on argument structures and justifications, which I call reducibility semantics, and one based on consequence among (sets of) formulas over atomic bases, called base…

We uncover a close relationship between combinatorial and syntactic proofs for first-order logic (without equality). Whereas syntactic proofs are formalized in a deductive proof system based on inference rules, a combinatorial proof is a…

It has been argued that reduction procedures are closely connected to the question about identity of proofs and that accepting certain reductions would lead to a trivialization of identity of proofs in the sense that every derivation of the…

The original idea of proof nets can be formulated by means of interaction nets syntax. Additional machinery as switching, jumps and graph connectivity is needed in order to ensure correspondence between a proof structure and a correct proof…

Wittgenstein's paradoxical theses that unproved propositions are meaningless, proofs form new concepts and rules, and contradictions are of limited concern, led to a variety of interpretations, most of them centered on the rule-following…

This is a short paper about the relationship between logic and computation. More specifically, it is about a relationship between the completeness proof for intuitionistic propositional logic within the form of proof-theoretic semantics…

The traditional view of evidence in mathematics is that evidence is just proof and proof is just derivation. There are good reasons for thinking that this view should be rejected: it misrepresents both historical and current mathematical…

Several formal systems, such as resolution and minimal model semantics, provide a framework for logic programming. In this paper, we will survey the use of structural proof theory as an alternative foundation. Researchers have been using…

Proof nets are a syntax for linear logic proofs which gives a coarser notion of proof equivalence with respect to syntactic equality together with an intuitive geometrical representation of proofs. In this paper we give an alternative…

Debates concerning philosophical grounds for the validity of classical and intuitionistic logics often have the very nature of logical proofs as one of the main points of controversy. The intuitionist advocates for a strict notion of…

We describe several views of the semantics of a simple programming language as formal documents in the calculus of inductive constructions that can be verified by the Coq proof system. Covered aspects are natural semantics, denotational…

The use of logical systems for problem-solving may be as diverse as in proving theorems in mathematics or in figuring out how to meet up with a friend. In either case, the problem solving activity is captured by the search for an…

Mathematical proofs should be paired with formal proofs, whenever feasible.