## 1. Background


### 1.1 General proof theory: consequence vs. proofs



The term "general proof theory" was coined by Prawitz. In
general proof theory, "proofs are studied in their own right in
the hope of understanding their nature", in contradistinction to
Hilbert-style "reductive proof theory", which is the
"attempt to analyze the proofs of mathematical theories with the
intention of reducing them to some more elementary part of mathematics
such as finitistic or constructive mathematics" (Prawitz, 1972,
p. 123). In a similar way, Kreisel (1971) asks for a re-orientation of
proof theory. He wants to explain "recent work in proof theory
from a neglected point of view. Proofs and their representations by
formal derivations are treated as principal objects of study, not as
mere tools for analyzing the consequence relation." (Kreisel,
1971, p. 109) Whereas Kreisel focuses on the dichotomy between a
theory of proofs and a theory of provability, Prawitz concentrates on
the different goals proof theory may pursue. However, both stress the
necessity of studying proofs as fundamental entities by means of which
we acquire demonstrative (especially mathematical) knowledge. This
means in particular that proofs are epistemic entities which should
not be conflated with formal proofs or derivations. They are rather
what derivations denote when they are considered to be representations
of arguments. (However, in the following we often use
"proof" synonymously with "derivation",
leaving it to the reader to determine whether formal proofs or proofs
as epistemic entities are meant.) In discussing Prawitz's (1971)
survey, Kreisel (1971, p. 111) explicitly speaks of a
"mapping" between derivations and mental acts, and
considers it a task of proof theory to elucidate this mapping,
including the investigation of the identity of proofs, a topic that
Prawitz and Martin-Lof had put on the proof-theoretic agenda.



This means that in general proof theory we are not solely interested
in whether \(B\) follows from \(A\), but in the way by means of which
we arrive at \(B\) starting from \(A\). In this sense general proof
theory is intensional and epistemological in character, whereas model
theory, which is interested in the consequence relation and not in the
way of establishing it, is extensional and metaphysical.


### 1.2 Inferentialism, intuitionism, anti-realism



Proof-theoretic semantics is inherently inferential, as it is
inferential activity which manifests itself in proofs. It thus belongs
to *inferentialism* (a term coined by Brandom, see his 1994;
2000) according to which inferences and the rules of inference
establish the meaning of expressions, in contradistinction to
*denotationalism*, according to which denotations are the
primary sort of meaning. Inferentialism and the
'meaning-as-use' view of semantics is the broad
philosophical framework of proof-theoretic semantics. This general
philosophical and semantical perspective merged with constructive
views which originated in the philosophy of mathematics, especially in
mathematical intuitionism. Most forms of proof-theoretic semantics are
intuitionistic in spirit, which means in particular that principles of
classical logic such as the law of excluded middle or the double
negation law are rejected or at least considered problematic. This is
partly due to the fact that the main tool of proof-theoretic
semantics, the calculus of natural deduction, is biased towards
intuitionistic logic, in the sense that the straightforward
formulation of its elimination rules is the intuitionistic one. There
classical logic is only available by means of some rule of indirect
proof, which, at least to some extent, destroys the symmetry of the
reasoning principles (see section
 3.5).
 If one adopts the standpoint of natural deduction, then
intuitionistic logic is a natural logical system. Also the BHK
(Brouwer-Heyting-Kolmogorov) interpretation of the logical signs plays
a significant role. This interpretation is not a unique approach to
semantics, but comprises various ideas which are often more informally
than formally described. Of particular importance is its functional
view of implication, according to which a proof of \(A \rightarrow B\)
is a constructive function which, when applied to a proof of \(A\)
yields a proof of \(B\). This functional perspective underlies many
conceptions of proof-theoretic semantics, in particular those of
Lorenzen, Prawitz and Martin Lof (see sections
 2.1.1,
 2.2.2,
 2.2.3).



According to Dummett (1975), the logical position of intuitionism
corresponds to the philosophical position of anti-realism. The realist
view of a recognition-independent reality is the metaphysical
counterpart of the view that all sentences are either true or false
independent of our means of recognizing it. Major parts of
proof-theoretic semantics follow Dummett and his association with
anti-realism.


### 1.3 Gentzen-style proof theory: Reduction, normalization, cut elimination



Gentzen's calculus of natural deduction and its rendering by
Prawitz is the background to most approaches to proof-theoretic
semantics. Natural deduction is based on at least three central
ideas:


* *Discharge of assumptions*: Assumptions can be
"discharged" or "eliminated" in the course of
a derivation, so the central notion of natural deduction is that of a
derivation *depending on assumptions*.
* *Separation*: Each primitive rule schema
contains only a single logical constant.
* *Introductions and eliminations*: The rules for
logical constants come in pairs. The introduction rule(s) allow(s) one
to infer a formula with the constant in question as its main operator,
the elimination rule(s) permit(s) to draw consequences from such a
formula.



In Gentzen's natural deduction system for first-order logic
derivations are written in tree form and based on the well-known
rules. For example, implication has the following introduction and
elimination rules

 
\[
\begin{prooftree}
\AxiomC{$[A]$}
\noLine
\UnaryInfC{$B$}
\RightLabel{$\,\to$I}
\UnaryInfC{$A\to B$}
\end{prooftree}

\hspace{6em}

\begin{prooftree}
\AxiomC{$A\to B$}
\AxiomC{$A$}
\RightLabel{$\,\to$E}
\BinaryInfC{$B$}
\end{prooftree}
\]


where the brackets indicate the possibility to discharge occurrences
of the assumption \(A\). The *open assumptions* of a derivation
are those assumptions on which the end-formula depends. A derivation
is called *closed*, if it has no open assumption, otherwise it
is called *open*. If we deal with quantifiers, we have to
consider open individual variables (sometimes called
"parameters"), too. Metalogical features crucial for
proof-theoretic semantics and for the first time systematically
investigated and published by Prawitz (1965) include:



*Reduction*: For every detour consisting of an introduction
immediately followed by an elimination there is a reduction step
removing this detour.



*Normalization*: By successive applications of reductions,
derivations can be transformed into normal forms which contain no
detours.



For implication the standard reduction step removing detours is the
following:

 
\[
\begin{prooftree}
\AxiomC{$[A]$}
\noLine\UnaryInfC{$\vdots$}
\noLine\UnaryInfC{$B$}
\UnaryInfC{$A\to B$}
\AxiomC{$|$}
\noLine\UnaryInfC{$A$}
\BinaryInfC{$B$}
\end{prooftree}
\hspace{1em}
\text{reduces to}
\hspace{1em}
\begin{prooftree}
\AxiomC{$|$}
\noLine\UnaryInfC{$A$}
\noLine\UnaryInfC{$\vdots$}
\noLine\UnaryInfC{$B$}
\end{prooftree}
\]


A simple, but very important corollary of normalization is the
following: *Every closed derivation in intuitionistic logic can be
reduced to a derivation using an introduction rule in the last
step.* We also say that intuitionistic natural deduction satisfies
the "*introduction form property*". In
proof-theoretic semantics this result figures prominently under the
heading "fundamental assumption" (Dummett, 1991, p. 254).
The "fundamental assumption" is a typical example of a
philosophical re-interpretation of a technical proof-theoretic
result.



*Further Reading:*



For the general orientation of *proof-theoretic semantics*, see
the special issue of *Synthese* edited by Kahle and
Schroeder-Heister (2006), the reader edited by Piecha and
Schroeder-Heister (2016b), the textbook by Francez (2015), and the
surveys by Wansing (2000) and by Schroeder-Heister (2016).



For the philosophical position and development of *proof
theory*, see the entry on
 Hilbert's program,
 the entry on the
 development of proof theory
 as well as Prawitz (1971).



For *intuitionism*, see the entry on
 intuitionistic logic,
 the entry on
 intuitionism in the philosophy of mathematics
 and the entry on the
 development of intuitionistic logic.



For *anti-realism*, see the entry on
 challenges to metaphysical realism
 as well as Tennant (1987; 1997) and Tranchini (2010; 2012a).



For *Gentzen-style proof-theory and the theory of natural
deduction*, see the entry on
 natural deduction systems in logic
 as well as, in addition to Gentzen's (1934/35) original
presentation, Jaskowski's (1934) theory of suppositions,
Prawitz's (1965) classical monograph, Tennant (1978; 2017),
Troelstra and Schwichtenberg (2000), Negri and von Plato (2001),
Mancosu, Galvan and Zach (2021), and Andrzej Indrzejczak's entry
on
 natural deduction in the *Internet Encyclopedia of Philosophy*. 



## 2. Some versions of proof-theoretic semantics


### 2.1 The semantics of implication: Admissibility, derivability, rules



The semantics of implication lies at the heart of proof-theoretic
semantics. In contradistinction to classical truth-condition
semantics, implication is a logical constant in its own right. It has
also the characteristic feature that it is tied to the concept of
consequence. It can be viewed as expressing consequence at the
sentential level due to modus ponens and to what in Hilbert-style
systems is called the deduction theorem, i.e. the equivalence of
\(\Gamma ,A \vdash B\) and \(\Gamma \vdash A \rightarrow B\).



A very natural understanding of an implication \(A \rightarrow B\) is
reading it as expressing the inference rule which allows one to pass
over from \(A\) to \(B\). Licensing the step from \(A\) to \(B\) on
the basis of \(A \rightarrow B\) is exactly, what modus ponens says.
And the deduction theorem can be viewed as the means of establishing a
rule: Having shown that \(B\) can be deduced from \(A\) justifies the
rule that from \(A\) we may pass over to \(B\). A rule-based semantics
of implication along such lines underlies several conceptions of
proof-theoretic semantics, notably those by Lorenzen, von Kutschera
and Schroeder-Heister.


#### 2.1.1 Operative logic



Lorenzen, in his *Introduction to Operative Logics and
Mathematics* (1955) starts with logic-free (atomic) calculi, which
correspond to production systems or grammars. He calls a rule
*admissible* in such a system if it can be added to it without
enlarging the set of its derivable atoms. The implication arrow
\(\rightarrow\) is interpreted as expressing admissibility. An
implication \(A \rightarrow B\) is considered to be valid, if, when
read as a rule, it is admissible (with respect to the underlying
calculus). For iterated implications \((=\) rules) Lorenzen develops a
theory of admissibility statements of higher levels. Certain
statements such as

 
\[A \rightarrow A \quad\text{ or }\quad ((A \rightarrow B), (B \rightarrow C)) \rightarrow(A \rightarrow C)
\]


hold independently of the underlying calculus. They are called
*universally admissible*
["allgemeinzulassig"]), and constitute a system of
positive implicational logic. In a related way, laws for universal
quantification \(\forall\) are justified using admissibility
statements for rules with schematic variables.



For the justification of the laws for the logical constants \(\land ,
\lor , \exists\) and \(\bot\), Lorenzen uses an *inversion
principle* (a term he coined). In a very simplified form, without
taking variables in rules into account, the inversion principle says
that everything that can be obtained from every defining condition of
\(A\) can be obtained from \(A\) itself. For example, in the case of
*disjunction*, let \(A\) and \(B\) each be a defining condition
of \(A\lor B\) as expressed by the primitive rules \(A \rightarrow
A\lor B\) and \(B \rightarrow A\lor B\). Then the inversion principle
says that \(A\lor B \rightarrow C\) is admissible assuming \(A
\rightarrow C\) and \(B \rightarrow C\), which justifies the
elimination rule for disjunction. The remaining connectives are dealt
with in a similar way. In the case of \(\bot\), the absurdity rule
\(\bot \rightarrow A\) is obtained from the fact that there is no
defining condition for \(\bot\).


#### 2.1.2 Gentzen semantics



In what he calls "Gentzen semantics", von Kutschera (1968)
gives, as Lorenzen, a semantics of logically complex implication-like
statements \(A\_1,\ldots,A\_n \rightarrow B\) with respect to calculi
\(K\) which govern the reasoning with atomic sentences. The
fundamental difference to Lorenzen is the fact that \(A\_1,\ldots,A\_n
\rightarrow B\) now expresses a *derivability* rather than an
*admissibility* statement.



In order to turn this into a semantics of the logical constants of
propositional logic, von Kutschera argues as follows: When giving up
bivalence, we can no longer use classical truth-value assignments to
atomic formulas. Instead we can use calculi which prove or refute
atomic sentences. Moreover, since calculi not only generate proofs or
refutations but arbitrary derivability relations, the idea is to start
directly with derivability in an atomic system and extend it with
rules that characterize the logical connectives. For that von
Kutschera gives a sequent calculus with rules for the introduction of
\(n\)-ary propositional connectives in the succedent and antecedent,
yielding a sequent system for generalized propositional connectives.
Von Kutschera then goes on to show that the generalized connectives so
defined can all be expressed by the standard connectives of
intuitionistic logic (conjunction, disjunction, implication,
absurdity).



*Further Reading:*



For extensions of expressive completeness in the style of von
Kutschera: Wansing (1993a).


#### 2.1.3 Natural deduction with higher-level rules



When developing a general schema for inference rules for arbitrary
logical constants, Schroeder-Heister (1984) proposed, as a semantical
requirement, that a logically complex formula expresses the content or
*common content* of *systems of rules*. A rule \(R\) is
either a formula \(A\) or has the form \(R\_1,\ldots,R\_n \Rightarrow
A\), where \(R\_1,\ldots,R\_n\) are rules. These so-called
"higher-level rules" generalize the idea that rules may
discharge assumption formulas to the case where they may discharge
assumption rules (i.e., rules used as assumptions). For the standard
connectives this means that \(A\land B\) expresses the content of the
pair \((A,B)\); \(A \rightarrow B\) expresses the content of the rule
\(A \Rightarrow B\); \(A\lor B\) expresses the common content of \(A\)
and \(B\); and absurdity \(\bot\) expresses the common content of the
empty family of rule systems. For arbitrary \(n\)-ary propositional
connectives this leads to a natural deduction system with generalized
introduction and elimination rules. These general connectives are
shown to be definable in terms of the standard ones, which establishes
the expressive completeness of the standard intuitionistic
connectives.


### 2.2 The Semantics of derivations as based on introduction rules


#### 2.2.1 Inversion principles and harmony



In his *Investigations into Logical Deduction*, Gentzen makes
some (frequently quoted) programmatic remarks on the semantic
relationship between introduction and elimination inferences in
natural deduction.



> 
> The introductions represent, as it were, the 'definitions'
> of the symbols concerned, and the eliminations are no more, in the
> final analysis, than the consequences of these definitions. This fact
> may be expressed as follows: In eliminating a symbol, we may use the
> formula with whose terminal symbol we are dealing only 'in the
> sense afforded it by the introduction of that symbol'. (Gentzen,
> 1934/35, p. 80)
> 



This cannot mean, of course, that the elimination rules are
*deducible* from the introduction rules in the literal sense of
the word; in fact, they are not. It can only mean that they can be
*justified* by them in some way.



> 
> By making these ideas more precise it should be possible to display
> the E-inferences as unique functions of their corresponding
> I-inferences, on the basis of certain requirements. (ibid., p. 81)
> 



So the idea underlying Gentzen's programme is that we have
"definitions" in the form of introduction rules and some
sort of semantic reasoning which, by using "certain
requirements", validate the elimination rules.



By adopting Lorenzen's term and adapting its underlying idea
(see section
 2.1.1)
 to the context of natural deduction, Prawitz (1965) formulated an
"inversion principle" to make Gentzen's remarks more
precise:



> 
> Let \(\alpha\) be an application of an elimination rule that has \(B\)
> as consequence. Then, deductions that satisfy the sufficient condition
> [...] for deriving the major premiss of \(\alpha\), when combined
> with deductions of the minor premisses of \(\alpha\) (if any), already
> "contain" a deduction of \(B\); the deduction of \(B\) is
> thus obtainable directly from the given deductions without the
> addition of \(\alpha\). (p. 33)
> 



Here the sufficient conditions are given by the premisses of the
corresponding introduction rules. Thus the inversion principle says
that a derivation of the conclusion of an elimination rule can be
obtained without an application of the elimination rule if its major
premiss has been derived using an introduction rule in the last step,
which means that a combination

 
\[\begin{prooftree}
\AxiomC{$\vdots$}
\RightLabel{I-inference}
\UnaryInfC{$A$}
\AxiomC{$\{\mathcal{D}\_i\}$}
\RightLabel{E-inference}
\BinaryInfC{$B$}
\end{prooftree}\]


of steps, where \(\{\mathcal{D}\_i\}\) stands for a (possibly empty)
list of deductions of minor premisses, can be avoided.



The relationship between introduction and elimination rules is often
described as "harmony" (Dummett 1973, pp. 396-397),
or as governed by a "principle of harmony" (Tennant, 1978,
p. 74). This terminology is not uniform and sometimes not even fully
clear. It essentially expresses what is also meant by
"inversion". Even if "harmony" is a term which
suggests a symmetric relationship, it is frequently understood as
expressing a conception based on introduction rules as, e.g., in
Read's (2010) "general elimination harmony"
(although occasionally one includes elimination-based conceptions as
well). Sometimes harmony is supposed to mean that connectives are
strongest or weakest in a certain sense given their introduction or
their elimination rules. This idea underlies Tennant's (1978)
harmony principle, and also Popper's and Koslow's
structural characterizations (see section
 2.4).
 The specific relationship between introduction and elimination rules
as formulated in an inversion principle excludes alleged inferential
definitions such as that of the connective *tonk*, which
combines an introduction rule for disjunction with an elimination rule
for conjunction, and which has given rise to a still ongoing debate on
the format of inferential definitions. Formal characterizations of
harmony have used the translation of inference rules into second-order
propositional logic (Girard's system F) and have become a
central topic of intensional proof-theoretic semantics (Tranchini,
2023).



*Further Reading:*



For *logical connectives* in general, see the entry on
 sentence connectives in formal logic.



For *inversion principles*, see Schroeder-Heister (2007).



For *variants of proof-theoretic harmony*, see Francez (2015),
Schroeder-Heister (2016) and Tranchini (2023).


#### 2.2.2 Proof-theoretic validity



Proof-theoretic validity is the leading approach in proof-theoretic
semantics. As a technical concept it was developed by Prawitz (1971;
1973; 1974), by turning a proof-theoretic validity notion based on
ideas by Tait (1967) and originally used to prove strong
normalization, into a semantical concept. Dummett provided much
philosophical underpinning to this notion (see Dummett, 1991). The
objects which are primarily valid are proofs as representations of
arguments. In a secondary sense, single rules can be valid if they
lead from valid proofs to valid proofs. In this sense, validity is a
global rather than a local notion. It applies to arbitrary derivations
over a given atomic system, which defines derivability for atoms.
Calling a proof *canonical*, if it uses an introduction rule in
the last step, proof-theoretic validity is based on the following
three ideas:


1. The priority of closed canonical proofs.
2. The reduction of closed non-canonical proofs to canonical
ones.
3. The substitutional view of open proofs.



*Ad 1:* The definition of validity is based on Gentzen's
idea that introduction rules are 'self-justifying' and
give the logical constants their meaning. This self-justifying feature
is only used for closed proofs, which are considered primary over open
ones.



*Ad 2:* Noncanonical proofs are justified by reducing them to
canonical ones. Thus reduction procedures (detour reductions) as used
in normalization proofs play a crucial role. As they justify
arguments, they are also called "justifications" by
Prawitz. This definition again only applies to closed proofs,
corresponding to the introduction form property of closed normal
derivations in natural deduction (see section
 1.3).



*Ad 3:* Open proofs are justified by considering their closed
instances. These closed instances are obtained by replacing their open
assumptions with closed proofs of them, and their open variables with
closed terms. For example, a proof of \(B\) from \(A\) is considered
valid, if every closed proof, which is obtained by replacing the open
assumption \(A\) with a closed valid proof of \(A\), is valid. In this
way, open assumptions are considered to be placeholders for closed
proofs, which is why we may speak of a substitutional interpretation
of open proofs.



This yields the following definition of proof-theoretic validity:


1. Every closed proof in the underlying atomic system is valid.
2. A closed canonical proof is considered valid, if its immediate
subproofs are valid.
3. A closed noncanonical proof is considered valid, if it reduces to
a valid closed canonical proof or to a closed proof in the atomic
system.
4. An open proof is considered valid, if every closed proof obtained
by replacing its open assumptions with closed valid proofs and its
open variables with closed terms is valid.



Formally, this definition has to be relativized to the atomic system
considered (see section
 2.6),
 and to a set of available justifications (proof reductions).
Furthermore, *proofs* are here understood as
*candidates* of valid proofs ("arguments" in
Prawitz's terminology), which means that the rules from which
they are composed are not fixed. They look like proof trees, but their
individual steps can have an arbitrary (finite) number of premisses
and can eliminate arbitrary assumptions. The definition of validity
singles out those proof structures which are 'real' proofs
on the basis of the given reduction procedures.



Validity with respect to every choice of an atomic system can be
viewed as a generalized notion of logical validity. In fact, if we
consider the standard reductions of intuitionistic logic, then all
derivations in intuitionistic logic are valid independent of the
atomic system considered. This is semantical *correctness*. We
may ask if the converse holds, viz. whether for any proof that is
valid for every atomic system, there is a corresponding derivation in
intuitionistic logic. That intuitionistic logic is complete in this
sense is known as Prawitz's conjecture (see Prawitz, 1973;
2013). There are certain doubts concerning the validity of this
conjecture for systems that go beyond implicational logic. In any case
it will depend on the precise formulation of the notion of validity,
in particular on its handling of atomic systems (see section
 2.8).



For a more formal definition and detailed examples demonstrating
validity, as well as some remarks on Prawitz's conjecture see
the



> 
> Supplement on Examples of Proof-theoretic Validity.
>  



*Further Reading:*



For a detailed exposition of further developments of
*Prawitz's theory of proof-theoretic validity*, in
particular his theory of grounds, see Piccolomini d'Aragona
(2023).



For a *computational interpretation of proof-theoretic
validity* as a method for tactical proof see Gheorghiu and Pym
(2022, other internet resources).


#### 2.2.3 Constructive type theory



Martin-Lof's type theory (Martin-Lof, 1984) is a
leading approach in constructive logic and mathematics.
Philosophically, it shares with Prawitz the three fundamental
assumptions of standard proof-theoretic semantics, mentioned in
section
 2.2.2:
 the priority of closed canonical proofs, the reduction of closed
non-canonical proofs to canonical ones and the substitutional view of
open proofs. However, Martin-Lof's type theory has at least
two characteristic features which go beyond other approaches in
proof-theoretic semantics:


1. The consideration of proof objects and the corresponding
distinction between proofs-as-objects and
proofs-as-demonstrations.
2. The view of formation rules as intrinsic to the proof system
rather than as external rules.



The first idea goes back to the Curry-Howard correspondence (see de
Groote, 1995; Sorensen and Urzyczyn, 2006), according to which
the fact that a formula \(A\) has a certain proof can be codified as
the fact that a certain term \(t\) is of type \(A\), whereby the
formula \(A\) is identified with the type \(A\). This can be
formalized in a calculus for type assignment, whose statements are of
the form \(t {:} A\). A proof of \(t {:} A\) in this system can be
read as showing that \(t\) is a proof of \(A\). Martin-Lof (1995;
1998) has put this into a philosophical perspective by distinguishing
this two-fold sense of proof in the following way. First we have
proofs of statements of the form \(t {:} A\). These statements are
called *judgements*, their proofs are called
*demonstrations*. *Within* such judgements the term
\(t\) represents a *proof* of the *proposition* \(A\). A
proof in the latter sense is also called a *proof object*. When
demonstrating a judgement \(t {:} A\), we demonstrate that \(t\) is a
proof (object) for the proposition \(A\). Within this two-layer system
the *demonstration* layer is the layer of argumentation. Unlike
proof objects, demonstrations have epistemic significance; their
judgements carry assertoric force. The proof layer is the layer at
which meanings are explained: The meaning of a proposition \(A\) is
explained by telling what counts as a proof (object) for \(A\). The
distinction made between canonical and non-canonical proofs is a
distinction at the propositional and not at the judgemental layer.
This implies a certain explicitness requirement. When I have proved
something, I must not only have a justification for my proof *at my
disposal* as in Prawitz's notion of validity, but at the
same time have to be *certain* that this justification fulfills
its purpose. This certainty is guaranteed by a demonstration.
Mathematically, this two-fold sense of proof develops its real power
only when types may depend on terms. Dependent types are a basic
ingredient of of Martin-Lof's type theory and related
approaches.



The second idea makes Martin-Lof's approach strongly differ
from all other definitions of proof-theoretic validity. The crucial
difference, for example, to Prawitz's procedure is that it is
not *metalinguistic* in character, where
"metalinguistic" means that propositions and candidates of
proofs are specified first and then, by means of a definition in the
metalanguage, it is fixed which of them are valid and which are not.
Rather, propositions and proofs come into play only in the context of
demonstrations. For example, if we assume that something is a proof of
an implication \(A \rightarrow B\), we need not necessarily show that
both \(A\) and \(B\) are well-formed propositions outright, but, in
addition to knowing that \(A\) is a proposition, we only need to know
that \(B\) is a proposition *provided that* \(A\) *has been
proved*. Being a proposition is expressed by a specific form of
judgement, which is established in the same system of demonstration
which is used to establish that a proof of a proposition has been
achieved.



In Martin-Lof's theory, proof-theoretic semantics receives
a strongly ontological component. A recent debate deals with the
question of whether proof objects have a purely ontological status or
whether they codify knowledge, even if they are not epistemic acts
themselves. More recently, Martin-Lof has embedded his approach
into a theory of interaction between assertions, challenges and
obligations (Martin-Lof 2019) which gives his proof-theoretic
semantics a pragmatic aspect and also relates it to dialogical
semantics (see section
 3.9).



Martin-Lof's type theory has found its most significant
mathematical application in homotopy theory, leading to homotopy type
theory (HoTT) and the univalent foundations programme (The Univalent
Foundations Program 2013). The latter is often (sometimes
controversially) considered a novel foundational approach to
mathematics in the intuitionistic spirit, as an alternative to
classical set-theoretic approaches.



*Further Reading:*



For the history and philosophy of *Martin-Lof*'*s
type theory* see Sommaruga (2000). For *type theory* in
general, for *homotopy type theory*, and for the *univalent
foundations* programme, see the entry on
 intuitionistic type theory
 and the entry on
 type theory.
 


### 2.3 Clausal definitions and definitional reasoning



Proof-theoretic semantics normally focuses on logical constants. This
focus is practically never questioned, apparently because it is
considered so obvious. In proof theory, little attention has been paid
to atomic systems, although there has been Lorenzen's early work
(see section
 2.1.1),
 where the justification of logical rules is embedded in a theory of
arbitrary rules, and Martin-Lof's (1971) theory of iterated
inductive definitions where introduction and elimination rules for
atomic formulas are proposed. The rise of logic programming has
widened this perspective. From the proof-theoretic point of view,
logic programming is a theory of atomic reasoning with respect to
clausal definitions of atoms. Definitional reflection is an approach
to proof-theoretic semantics that takes up this challenge and attempts
to build a theory whose range of application goes beyond logical
constants.


#### 2.3.1 The challenge from logic programming



In logic programming we are dealing with program clauses of the
form

 
\[
A \Leftarrow B\_1 , \ldots ,B\_m
\]


which *define* atomic formulas. Such clauses can naturally be
interpreted as describing introduction rules for atoms. From the point
of view of proof-theoretic semantics the following two points are
essential:



(1) Introduction rules (clauses) for logically compound formulas are
not distinguished in principle from introduction rules (clauses) for
atoms. Interpreting logic programming proof-theoretically motivates an
extension of proof-theoretic semantics to arbitrary atoms, which
yields a semantics with a much wider realm of applications.



(2) Program clauses are not necessarily well-founded. For example, the
head of a clause may occur in its body. Well-founded programs are just
a particular sort of programs. The use of arbitrary clauses without
further requirements in logic programming is a motivation to pursue
the same idea in proof-theoretic semantics. One would admit any sort
of introduction rules and not just those of a special form, and in
particular not necessarily ones which are well-founded. This carries
the idea of definitional freedom, which is a cornerstone of logic
programming, over to semantics, again widening the realm of
application of proof-theoretic semantics.



The idea of considering introduction rules as meaning-giving rules for
atoms is closely related to the theory of inductive definitions in its
general form, according to which inductive definitions are systems of
rules (see Aczel, 1977).


#### 2.3.2 Definitional reflection



The theory of definitional reflection (Hallnas, 1991; 2006;
Hallnas and Schroeder-Heister, 1990/91; Schroeder-Heister, 1993)
takes up the challenge from logic programming and gives a
proof-theoretic semantics not just for logical constants but for
arbitrary expressions, for which a clausal definition can be given.
Formally, this approach starts with a list of clauses which is the
*definition* considered. Each clause has the form



\[
A \Leftarrow \Delta
\]


where the head \(A\) is an atomic formula (atom). In the simplest
case, the body \(\Delta\) is a list of atoms \(B\_1,\ldots,B\_m\), in
which case a definition looks like a definite logic program. We often
consider an extended case where \(\Delta\) may also contain some
structural implication '\(\Rightarrow\)', and sometimes
even some structural universal quantification, which essentially is
handled by restricting substitution. If the definition of \(A\) has
the form

 
\[ \mathbb{D}\_A\ \left\{ 
\begin{array}{rcl} 
A & \Leftarrow & \Delta\_1 \\ 
 & \vdots & \\ 
A & \Leftarrow & \Delta\_n 
\end{array} \right. \]


then \(A\) has the following introduction and elimination rules



\[
\begin{prooftree}
\AxiomC{$\Delta\_1$}
\UnaryInfC{$A$}
\end{prooftree}
\;\cdots\;
\begin{prooftree}
\AxiomC{$\Delta\_n$}
\UnaryInfC{$A$}
\end{prooftree}
\]
 
\[
\begin{prooftree}
\AxiomC{$A$}
\AxiomC{$[\Delta\_1]$}
\noLine\UnaryInfC{$C$}
\AxiomC{$\cdots$}
\AxiomC{$[\Delta\_n]$}
\noLine\UnaryInfC{$C$}
\QuaternaryInfC{$C$}
\end{prooftree}
\]


The introduction rules, also called rules of *definitional
closure*, express reasoning 'along' the clauses. The
elimination rule is called the *principle of definitional
reflection*, as it reflects upon the definition as a whole. If
\(\Delta\_1,\ldots,\Delta\_n\) exhaust *all possible conditions*
to generate \(A\) according to the given definition, and if each of
these conditions entails the very same conclusion \(C\), then \(A\)
itself entails this conclusion. If the clausal definition is viewed as
an inductive definition, this principle can be viewed as expressing
the extremal clause in inductive definitions: Nothing else beyond the
clauses given defines \(A\). Obviously, definitional reflection is a
generalized form of the inversion principles discussed. It develops
its genuine power in definitional contexts with free variables that go
beyond purely propositional reasoning, and in contexts which are not
well-founded. An example of a non-wellfounded definition is the
definition of an atom \(R\) by its own negation:

 
\[
\mathbb{D}\_R \;\{\; R \Leftarrow (R \Rightarrow \bot)
\]


Defining an atom by its negation is a standard example in logic
programming. In the context of definitional reflection it was
suggested by Hallnas. It is here discussed in detail in the



> 
> Supplement on Definitional Reflection and Paradoxes.
>  



*Further Reading:*



For *non-wellfoundedness* and *paradoxes* see the entry
on
 self-reference
 and the entry on
 Russell's paradox.


### 2.4 Structural characterization of logical constants



There is a large field of ideas and results concerning what might be
called the "structural characterization" of logical
constants, where "structural" is here meant both in the
proof-theoretic sense of "structural rules" and in the
sense of a framework that bears a certain structure, where this
framework is again proof-theoretically described. Some of its authors
use a semantical vocabulary and at least implicitly suggest that their
topic belongs to proof-theoretic semantics. Others explicitly deny
these connotations, emphasizing that they are interested in a
characterization which establishes the logicality of a constant. The
question "What is a logical constant?" can be answered in
proof-theoretic terms, even if the semantics of the constants
themselves is truth-conditional: Namely by requiring that the (perhaps
truth-conditionally defined) constants show a certain inferential
behaviour that can be described in proof-theoretic terms. However, as
some of the authors consider their characterization at the same time
as a semantics, it is appropriate that we mention some of these
approaches here.



The most outspoken structuralist with respect to logical constants,
who explicitly understands himself as such, is Koslow. In his
*Structuralist Theory of Logic* (1992) he develops a theory of
logical constants, in which he characterizes them by certain
"implication relations", where an implication relation
roughly corresponds to a finite consequence relation in Tarski's
sense (which again can be described by certain structural rules of a
sequent-style system). Koslow develops a structural theory in the
precise metamathematical sense, which does not specify the domain of
objects in any way beyond the axioms given. If a language or any other
domain of objects equipped with an implication relation is given, the
structural approach can be used to single out logical compounds by
checking their implicational properties.



In his early papers on the foundations of logic, Popper (1947a; 1947b;
Binder et al., eds., 2022) gives inferential characterizations of
logical constants in proof-theoretic terms. He uses a calculus of
sequents and characterizes logical constants by certain derivability
conditions for such sequents. His terminology clearly suggests that he
intends a proof-theoretic semantics of logical constants, as he speaks
of "inferential definitions" and the "trivialization
of mathematical logic" achieved by defining constants in the way
described. Although his presentation is not free from conceptual
imprecision and error, he anticipated many ideas now common in
proof-theoretic semantics, such as the delineation of logical
constants by means of certain minimality or maximality conditions with
respect to introduction or elimination rules.



Important contributions to the logicality debate that characterize
logical constants inferentially in terms of sequent calculus rules are
those by Kneale (1956) and Hacking (1979). A thorough account of
logicality is proposed by Dosen (1980; 1989) in his theory of
logical constants as "punctuation marks", expressing
structural features at the logical level. He understands logical
constants as following certain double-line rules for sequents which
can be read in both directions. For example, conjunction and
disjunction obey (in classical logic, with multiple-formulae
succedents) the double-line rules

 
\[
\xlongequal[{\Large \Gamma \,\vdash\, A \,\land\, B,\, \Delta}]
{{\Large \Gamma \,\vdash\, A,\, \Delta\quad \Gamma \,\vdash\, B,\, \Delta}}
\hspace{2em}
\xlongequal[{\Large \Gamma,\, A \,\lor\, B \,\vdash\, \Delta}]
{{\Large \Gamma,\, A \,\vdash\, \Delta\quad \Gamma,\, B \,\vdash\, \Delta}}
\]


Dosen is able to give characterizations which include systems
of modal logic. He explicitly considers his work as a contribution to
the logicality debate and not to any conception of proof-theoretic
semantics. Sambin et al., in their Basic Logic (Sambin, Battilotti,
and Faggian, 2000), explicitly understand what Dosen calls
double-line rules as fundamental meaning giving rules. The double-line
rules for conjunction and disjunction are read as implicit definitions
of these constants, which by some procedure can be turned into the
explicit sequent-style rules we are used to. So Sambin et al. use the
same starting point as Dosen, but interpret it not as a
structural description of the behaviour of constants, but semantically
as their implicit definition.



There are several other approaches to a uniform proof-theoretic
characterization of logical constants, all of which at least touch
upon issues of proof-theoretic semantics. Such theories are
Belnap's Display Logic (Belnap, 1982), Wansing's Logic of
Information Structures (Wansing, 1993b), generic proof editing systems
and their implementations such as the Edinburgh Logical Framework
(Harper, Honsell, and Plotkin, 1987) and many successors which allow
the specification of a variety of logical systems. Since the rise of
linear and, more generally, substructural logics there are various
approaches dealing with logics that differ with respect to
restrictions on their structural rules (see section
 3.10).
 A recent movement away from singling out a particular logic as the
true one towards a more pluralist stance (see, e.g., Beall and
Restall, 2006), which is interested in what different logics have in
common without any preference for a particular logic, can be seen as a
shift away from semantical justification towards structural
characterization.



*Further Reading:*



For *Popper's theory of logical constants* see Binder et
al. (2022), Piecha (2023).



For *logical constants* and their *logicality* see the
entry on
 logical constants.



For *linear* and *substructural logics* see the entry on
 linear logic,
 and the entry on
 substructural logics.



For *pluralism in logic*, see the entry on on
 logical pluralism.


### 2.5 Categorial proof theory



There is a considerable literature on category theory in relation to
proof theory, and, following seminal work by Lawvere, Lambek and
others (see Lambek and Scott, 1986), category theory itself can be
viewed as a kind of abstract proof theory. If one looks at an arrow
\(A \rightarrow B\) in a category as a kind of abstract proof of \(B\)
from \(A\), we have a representation which goes beyond pure
derivability of \(B\) from \(A\) (as the arrow has its individuality),
but does not deal with the particular syntactic structure of this
proof. For intuitionistic systems, proof-theoretic semantics in
categorial form comes probably closest to what denotational semantics
is in the classical case.



One of the most highly developed approaches to categorial proof theory
is due to Dosen. He has not only advanced the application of
categorial methods in proof theory (e.g., Dosen and
Petric, 2004), but also shown how proof-theoretic methods can be
used in category theory itself (Dosen, 2000). Most important
for categorial logic in relation to proof-theoretic semantics is that
in categorial logic, arrows always come together with an identity
relation, which in proof-theory corresponds to the identity of proofs.
In this way, ideas and results of categorial proof theory pertain to
what may be called intensional proof-theoretic semantics (see section
 3.7),
 that is, the study of proofs as entities in their own right, not just
as vehicles to establish consequences (Dosen, 2006; 2016).



As there is the strong relationship between arrows in the categorial
sense and proofs in the sense of deductive reasoning, there are
categorial analogues to practically all concepts dealt with in the
deductive realm, often with novel methods, ideas and results that
supplement deductive approaches in a very productive way. Categorial
proof-theoretic semantics is a very broad research area that runs in
parallel to the deductive perspective adopted in this entry --
the deductive perspective is by far more common in philosophy. In the
field of intuitionistic logic, categorial logic covers highly advanced
topics: beyond standard quantifier logic dependent type theories in
the tradition of Martin-Lof (see section
 2.2.3)
 including homotopy type theory. For many other logical systems
categorial semantics have been developed, including classical logic
and various substructural logics such as linear logic.



A philosophically highly significant general feature of categorial
proof-theory is its inherently hypothetical character. This is due to
the fact that it starts from hypothetical statements \(A \rightarrow
B\) (arrows) rather than categorical statements \(A\)
("categorical" as opposed to "hypothetical",
not "categorial" which is used here for "pertaining
to category theory"). It this way it overcomes a paradigm of
standard, in particular validity-based, proof-theoretic semantics (see
section
 3.6).



*Further Reading:*



For *categorial approaches* in general see the entry on
 category theory
 and the entry on
 structuralism in the philosophy of mathematics.



For *categorial proof-theoretic semantics* see Pym, Ritter, and
Robinson (2023, other internet resources).


### 2.6 Atomic systems



Proof-theoretic semantics is predominantly concerned with logical
constants. Even if one agrees with this orientation -- the theory
of definitional reflection (see section
 2.3.2)
 is an exception to it -- we must nonetheless fix the status of
atomic sentences and their proofs. In model-theoretic semantics the
truth of a logically complex sentence is defined with respect to a
structure, which is called a "model" of this sentence.
This structure determines, which atomic sentences are true and which
are not. Whether a complex sentence is true hinges on its atomic
constituents. This is quite analogous in proof-theoretic semantics.
Whether a proof of a complex sentence is valid depends on the atomic
base of the system under consideration. Here an atomic base is
normally considered a calculus for the generation of atomic sentences:
Proofs of atomic sentences in the atomic base are per se valid.
Similar to the model-theoretic definition of logical truth as truth
with respect to all structures, in proof-theoretic semantics one would
define logically valid proofs as proofs which are valid with respect
to all atomic bases.



There are various options which atomic systems should be considered to
be candidates for atomic bases. (1) The simplest would be Herbrand
models as used in the theory of logic programming, which are just
collections of atomic sentences. Proof-theoretically, these would be
calculi consisting of axioms only, without proper rules of inference.
(2) In the writings of Lorenzen (see section
 2.1.1)
 and Prawitz (see section
 2.2.2)
 atomic systems are considered lists of production rules, that is,
calculi with axioms and rules of the form \(A\_1,\ldots,A\_n \Rightarrow
B\) allowing one to generate \(B\) from \(A\_1,\ldots,A\_n\). (3) More
involved systems may contain atomic rules that allow one to discharge
assumptions, quite in analogy to logical rules such as implication
introduction. (4) Generalizing this idea one may admit rules for atoms
that discharge rules themselves, that is, rules of higher levels (see
section
 2.1.3).
 (5) Even further advanced would be atomic systems that incorporate
rules of definitional reflection (see section
 2.3.2).
 -- Many other sorts of rules for atoms constituting atomic
systems may be imagined.



For proof-theoretic semantics, the critical point here is that certain
formal results depend on which types of atomic systems are admitted.
This holds in particular for the issue of semantical completeness (see
section
 2.8).
 The investigation of which atomic systems, when taken as atomic bases
of proof-theoretic semantics, lead to which formal system at the
logical level, has just begun (see Sandqvist 2015b; Piecha and
Schroeder-Heister, 2016a; Stafford 2023, other internet resources). It
should be noted that this is an intensional feature of proof-theoretic
semantics: We are not just interested in which atoms are generated by
the various forms of atomic systems, but how this is done, that is, by
which type of rules this is achieved. This is a crucial difference to
model-theoretic semantics, which is purely extensional in this
respect. For further intensional features of proof-theoretic semantics
see section
 3.7.


### 2.7 Sentence-based semantics



Instead of defining the validity of proofs of sentences, one can
define the proof-theoretic validity of sentences directly. In the
definition of validity of logically complex sentences one would then
discard the reference to proofs of these sentences. This does not mean
that one is giving up the proof-theoretic approach, as one would still
refer to proofs in the atomic base. Proofs come in at the atomic
level, but not at the logical level. This approach is technically much
simpler to elaborate than the one based on the validity of proofs (see
section
 2.2.2),
 but still sufficient to discuss basic topics such as semantical
completeness (see section
 2.8).
 In fact, from a proof of a sentence \(A\) which is valid in the sense
of section
 2.2.2,
 the validity of \(A\) in the sense of sentence-based semantics can be
inferred; and conversely, from the validity of \(A\) in sentence-based
semantics a (though degenerate) valid proof of \(A\) can be
constructed. In a sense, sentence-based semantics is related to the
proof-theoretic semantics inherent in Martin-Lof's system
(see section
 2.2.3),
 where in the case of elementary logic (where dependent types do not
play any role), the proof information \(t\) of a judgement \(t{:}A\)
can be discarded in favour of the simplified judgement \(A\
\textit{true}\).



One possible definition of the validity of sentences in minimal
propositional logic with respect to an atomic system \(S\) as its
atomic base in propositional logic would be the following:


1. An atomic formula \(A\) is \(S\)-valid, if it is derivable in
\(S\).
2. A conjunction \(A\land B\) is \(S\)-valid, if both \(A\) and \(B\)
are \(S\)-valid.
3. A disjunction \(A\lor B\) is \(S\)-valid, if either \(A\) or \(B\)
is \(S\)-valid.
4. An implication \(A \rightarrow B\) is \(S\) valid, if for every
extension \(S'\) of \(S\), if \(A\) if \(S'\)-valid then \(B\) is
\(S'\)-valid.



Note that in the statement of hypothetical validity reference is made
to arbitrary extensions of the atomic base considered. As in the
formal definition of the validity of proofs, considering
base-extensions is used to ensure monotonicity and to avoid vacuous
validity. In the literature, following Sandqvist (2015a), the term
"base-extension semantics" is often used in a more
specific sense: namely for a special form of sentence-based semantics,
in which disjunction receives a deviant interpretation.



Validity in sentence-based semantics depends on the choice of atomic
systems. This choice is what makes sentence-based semantics
proof-theoretic. As indicated in section
 2.6,
 the type of atomic system counts, as does the extension relation
considered for implications and consequence statements.


### 2.8 Semantical completeness



Proof-theoretic semantics is intuitionistic in spirit, at least by its
origin. Correspondingly, Prawitz (1971) conjectured that those
consequence statements \(\Gamma \vDash A\), which are justified by
proofs valid with respect to any atomic base, are exactly the
derivability statements \(\Gamma \vdash A\) of the formal system of
intuitionistic logic. Within the framework of sentence semantics,
which for the issue of validity in relation to semantical completeness
is easier to handle than the framework of valid proofs, this
conjecture turned out to be false. Harrop's rule



\[
\begin{prooftree}
\AxiomC{$\neg A \to (B \lor C)$}
\UnaryInfC{$(\neg A \to B) \lor (\neg A \to C)$}
\end{prooftree}
\]


which is not derivable (but only admissible) in intuitionistic logic
can be validated in this framework (Piecha and Schroeder-Heister,
2019). However, when the extension structure of atomic bases is
modified beyond the set-theoretical superset relation, the picture
changes and Kripke's completeness proof for intuitionistic logic
becomes applicable to the proof-theoretic framework (Goldfarb 2016;
Stafford and Nascimento 2023). Another way to avoid incompleteness is
to give disjunction a non-standard interpretation, for example by
requiring that the minor premisses and conclusion of the rule of
\(\lor\)-elimination can always be considered atomic (see Sandqvist,
2015a).



*Further Reading:*



For Prawitz's completeness conjecture see the
 Supplement on Examples of Proof-theoretic Validity.



For the role of Harrop's rule in the context of admissibility
statements for intuitionistic logic, see the entry on
 intuitionistic logic.


## 3. Extensions and alternatives to standard proof-theoretic semantics


### 3.1 Elimination rules as basic



Most approaches to proof-theoretic semantics consider introduction
rules as basic, meaning giving, or self-justifying, whereas the
elimination inferences are justified as valid with respect to the
given introduction rules. This conception has at least three roots:
The first is a verificationist theory of meaning according to which
the assertibility conditions of a sentence constitute its meaning. The
second is the idea that we must distinguish between what gives the
meaning and what are the consequences of this meaning, as not all
inferential knowledge can consist of applications of definitions. The
third one is the primacy of assertion over other speech acts such as
assuming or denying, which is implicit in all approaches considered so
far.



One might investigate how far one gets by considering elimination
rules rather than introduction rules as a basis of proof-theoretic
semantics. Some ideas towards a proof-theoretic semantics based on
elimination rather than introduction rules have been sketched by
Dummett (1991, Ch. 13), albeit in a very rudimentary form. A more
precise definition of validity based on elimination inferences is due
to Prawitz (1971; 2007; see also Schroeder-Heister 2015). Its
essential idea is that a closed proof is considered valid, if the
result of applying an elimination rule to its end formula is a valid
proof or reduces to one. For example, a closed proof of an implication
\(A \rightarrow B\) is valid, if, for any given closed valid proof of
\(A\), the result of applying modus ponens

 
\[\begin{prooftree}
\AxiomC{$A \to B$}
\AxiomC{$A$}
\BinaryInfC{$B$}
\end{prooftree}\]


to these two proofs is a valid proof of \(B\), or reduces to such a
proof. This conception keeps two of the three basic ingredients of
Prawitz-style proof-theoretic semantics (see section
 2.2.2):
 the role of proof reduction and the substitutional view of
assumptions. Only the canonicity of proofs ending with introductions
is turned into the canonicity of proofs ending with eliminations.


### 3.2 Negation and denial



Standard proof-theoretic semantics is assertion-centred in that
assertibility conditions determine the meaning of logical constants.
Corresponding to the intuitionistic way of proceeding, the negation
\(\neg A\) of a formula \(A\) is normally understood as implying
absurdity \(A \rightarrow \bot\), where \(\bot\) is a constant which
cannot be asserted, i.e., for which no assertibility condition is
defined. This is an 'indirect' way of understanding
negation. In the literature there has been the discussion of what,
following von Kutschera (1969), might be called 'direct'
negation. By that one understands a one-place primitive operator of
negation, which cannot be, or at least is not, reduced to implying
absurdity. It is not classical negation either. It rather obeys rules
which dualize the usual rules for the logical constants. Sometimes it
is called the "denial" of a sentence, sometimes also
"strong negation" (see Odintsov, 2008). Typical rules for
the denial \({\sim}A\) of \(A\) are

 
\[
\begin{prooftree}
\AxiomC{${\sim}A$}
\AxiomC{${\sim}B$}
\BinaryInfC{${\sim}(A \lor B)$}
\end{prooftree}
\hspace{1.5em}
\begin{prooftree}
\AxiomC{${\sim}A$}
\UnaryInfC{${\sim}(A \land B)$}
\end{prooftree}
\hspace{1.5em}
\begin{prooftree}
\AxiomC{${\sim}B$}
\UnaryInfC{${\sim}(A \land B)$}
\end{prooftree}
\]


Essentially, the denial rules for an operator correspond to the
assertion rules for the dual operator. Several logics of denial have
been investigated, in particular Nelson's (1949) logics of
"constructible falsity" motivated by Nelson with respect
to a certain realizability semantics. The main focus has been on his
systems later called N3 and N4 which differ with respect to the
treatment of contradiction (N4 is N3 without *ex contradictione
quodlibet*). Using denial any approach to proof-theoretic
semantics can be dualized by just exchanging assertion and denial and
turning from logical constants to their duals. In doing so, one
obtains a system based on refutation \((=\) proof of denial) rather
than proof. It can be understood as applying a Popperian view to
proof-theoretic semantics by keeping its intuitionistic spirit.
Formally, it leads to systems such as dual intuitionistic logic by
giving them a proof-theoretic semantics.



Another approach would be to not just dualize assertion-centered
proof-theoretic semantics in favour of a denial-centered
refutation-theoretic semantics, but to see the relation between rules
for assertion and for denial as governed by an inversion principle or
principle of definitional reflection of its own. This would be a
principle of what might be called
"assertion-denial-harmony". Whereas in standard
proof-theoretic semantics, inversion principles control the
relationship between assertions and assumptions (or consequences),
such a principle would now regulate the relationship between assertion
and denial. Given certain defining conditions of \(A\), it would say
that the denial of every defining condition of \(A\) leads to the
denial of \(A\) itself. For conjunction and disjunction this leads to
the common pairs of assertion and denial rules

 
\[
\begin{prooftree}
\AxiomC{$A$}
\UnaryInfC{$A \lor B$}
\end{prooftree}
\hspace{1.5em}
\begin{prooftree}
\AxiomC{$B$}
\UnaryInfC{$A \lor B$}
\end{prooftree}
\hspace{1.5em}
\begin{prooftree}
\AxiomC{${\sim}A$}
\AxiomC{${\sim}B$}
\BinaryInfC{${\sim}(A \lor B)$}
\end{prooftree}
\]

\[
\begin{prooftree}
\AxiomC{$A$}
\AxiomC{$B$}
\BinaryInfC{$A \land B$}
\end{prooftree}
\hspace{1.5em}
\begin{prooftree}
\AxiomC{${\sim}A$}
\UnaryInfC{${\sim}(A \land B)$}
\end{prooftree}
\hspace{1.5em}
\begin{prooftree}
\AxiomC{${\sim}B$}
\UnaryInfC{${\sim}(A \land B)$}
\end{prooftree}
\]


This idea can easily be generalized to definitional reflection,
yielding a reasoning system in which assertion and denial are
intertwined. It has parallels to the deductive relations between the
forms of judgement studied in the traditional square of opposition
(Schroeder-Heister, 2012a; Zeilberger, 2008). It should be emphasized
that the denial operator is here an external sign indicating a form of
judgement and not a logical operator. This means in particular that it
cannot be iterated.



The idea that both assertion and denial conditions give meaning to a
sentence and thus to logical operations also figures under the term
"bilateralism", a term coined by Rumfitt.



*Further Reading*



For the proof-theoretic semantics of *negation and denial* see
Tranchini (2012b), Wansing (2001; 2017), as well as the special issue
on *assertion and denial* edited by Carrara, Chiffi and De
Florio (2017) and the entry on
 negation,
 the entry on
 connexive logic
 and the entry on
 contradiction.



For the idea of bilateralism see Rumfitt (2000), Kurbis (2016;
2019), Drobyshevich (2021) and the special issue on *bilateralism
and proof-theoretic semantics* edited by Sara Ayhan (2023).



For Popperianism and proof theoretic semantics see Binder et al.
(2022), Kapsner (2014).


### 3.3 Harmony and reflection in the sequent calculus



Gentzen's sequent calculus exhibits a symmetry between right and
left introduction rules which suggest to look for a harmony principle
that makes this symmetry significant for proof-theoretic semantics. At
least three lines have been pursued to deal with this phenomenon. (i)
Either the right-introduction or or the left-introduction rules are
considered to be introduction rules. The opposite rules
(left-introductions and right-introductions, respectively) are then
justified using the corresponding elimination rules. This means that
the methods discussed before are applied to whole sequents rather than
formulas within sequents. Unlike these formulas, the sequents are not
logically structured. This approach builds on definitional reflection,
which applies harmony and inversion to rules for arbitrarily
structured entities rather than for logical compounds only. It has
been pursued by de Campos Sanz and Piecha (2009). (ii) The right- and
left-introduction rules are derived from a characterization in the
sense of Dosen's double line rules (section
 2.4),
 which is then read as a definition of some sort. The top-down
direction of a double-line rule is already a right- or a
left-introduction rule. The other one can be derived from the
bottom-up direction by means of certain principles. This is the basic
meaning-theoretic ingredient of Sambin et al.'s *Basic
Logic* (Sambin, Battilotti, and Faggian, 2000). (iii) The right-
and left-introduction rules are seen as expressing an interaction
between sequents using the rule of cut. Given either the right- or the
left-rules, the complementary rules express that everything that
interacts with its premisses in a certain way so does with its
conclusion. This idea of interaction is a generalized symmetric
principle of definitional reflection. It can be considered to be a
generalization of the inversion principle, using the notion of
interaction rather than the derivability of consequences (see
Schroeder-Heister, 2013). All three approaches apply to the sequent
calculus in its classical form, with possibly more than one formula in
the succedent of a sequent, including structurally restricted versions
as investigated in linear and other logics. Therefore this topic
touches very much the issue of substructural logic and of
substructural approaches to proof-theoretic semantics (see section
 3.10).


### 3.4 Subatomic structure and natural language



Even if, as in definitional reflection, we are considering
definitional rules for atoms, their defining conditions do not
normally decompose these atoms. A proof-theoretic approach that takes
the internal structure of atomic sentences into account, has been
proposed by Wieckowski (2008; 2011; 2016; 2021). He uses
introduction and elimination rules for atomic sentences, where these
atomic sentences are not just reduced to other atomic sentences, but
to subatomic expressions representing the meaning of predicates and
individual names. Apart from its foundational significance, this can
be seen as a first step towards natural language applications of
proof-theoretic semantics. A further step in this direction has been
undertaken by Francez, who developed a proof-theoretic semantics for
several fragments of English (see Francez, Dyckhoff, and Ben-Avi,
2010; Francez and Dyckhoff, 2010; Francez and Ben-Avi, 2015; Francez,
2022). Specifically, Francez is able to use the proof-theoretic
approach to deal with scope ambiguity and many other issues of
semantic meaning variation. Besides computer science, natural language
grammar and natural language semantics will play a key role in the
practical application of proof-theoretic semantics.



*Further Reading*



For the proof-theoretic semantics of *natural language* see
Francez (2015, Part II).


### 3.5 Classical logic



Proof-theoretic semantics is intuitionistically biased. This is due to
the fact that natural deduction as its preferred framework has certain
features which make it particularly suited for intuitionistic logic.
In classical natural deduction the *ex falso quodlibet*



\[\begin{prooftree}
\AxiomC{$\bot$}
\UnaryInfC{$A$}
\end{prooftree}\]


is replaced with the rule of *classical reductio ad
absurdum*

 
\[\begin{prooftree}
\AxiomC{$[A\to \bot]$}
\noLine\UnaryInfC{$\bot$}
\UnaryInfC{$A$}
\end{prooftree}\]


In allowing to discharge \(A \rightarrow \bot\) in order to infer
\(A\), this rule undermines the *subformula principle*.
Furthermore, in containing both \(\bot\) and \(A \rightarrow \bot\),
it refers to two different logical constants in a single rule, so
there is no *separation* of logical constants any more.
Finally, as an elimination rule for \(\bot\) it does not follow the
general pattern of introductions and eliminations. As a consequence,
it destroys the *introduction form property* that every closed
derivation can be reduced to one which uses an introduction rule in
the last step.



Classical logic fits very well with the multiple-succedent sequent
calculus. There we do not need any additional principles beyond those
assumed in the intuitionistic case. Just the structural feature of
admitting more than one formula in the succedent suffices to obtain
classical logic. As there are plausible approaches to establish a
harmony between right-introduction and left-introduction in the
sequent calculus (see section
 3.3),
 classical logic appears to be perfectly justified. However, this is
only convincing if reasoning is appropriately framed as a
multiple-conclusion process, even though this does not correspond to
our standard practice where we focus on single conclusions. One could
try to develop an appropriate intuition by arguing that reasoning
towards multiple conclusions delineates the area in which truth lies
rather than establishing a single proposition as true. However, this
intuition is hard to maintain and cannot be formally captured without
serious difficulties. Philosophical approaches such as those by
Shoesmith and Smiley (1978) and proof-theoretic approaches such as
proof-nets (see Girard, 1987; the entry on
 linear logic)
 are attempts in this direction.



A fundamental reason for the failure of the introduction form property
in classical logic is the indeterminism inherent in the laws for
disjunction. \(A\lor B\) can be inferred from \(A\) as well as from
\(B\). Therefore, if the disjunction laws were the only way of
inferring \(A\lor B\), the derivability of \(A\lor \neg A\), which is
a key principle of classical logic, would entail that of either \(A\)
or of \(\neg A\), which is absurd. A way out of this difficulty is to
abolish indeterministic disjunction and use instead its classical de
Morgan equivalent \(\neg(\neg A \land \neg B)\). This leads
essentially to a logic without proper disjunction. In the quantifier
case, there would be no proper existential quantifier either, as
\(\exists xA\) would be understood in the sense of \(\neg \forall
x\neg A\). If one is prepared to accept this restriction, then certain
harmony principles can be formulated for classical logic.



As Karl Popper was the first to observe (see Binder et al., 2022), the
simple combination of rules for classical and intuitionistic
connectives collapses into the classical system. More sophisticated
theories that combine classical and intuitionistic systems in a
faithful way are found in *ecumenical systems* (see Pimentel
and Pereira 2021). Approaches to classical logic originally developed
in computer science by algorithmic considerations, in particular in
the context of proof search, are Michel Parigot's \(\lambda
\mu\)-calculus (Parigot 1992) and the application of the focusing
method to classical logic (Liang and Miller, 2009; 2023). Both
approaches rest on the idea that by certain indexing techniques a
single formula in the multiple-formula succedent of a classical
sequent can be distinguished and dealt with individually.



*Further Reading*



For *classical logic* in general see the entry on
 classical logic.


### 3.6 Hypothetical reasoning



Standard approaches to proof-theoretic semantics, especially
Prawitz's validity-based approach (section
 2.2.2),
 take closed derivations as basic. The validity of open derivations is
defined as the transmission of validity from closed derivations of the
assumptions to a closed derivation of the assertion, where the latter
is obtained by substituting a closed derivation for an open
assumption. Therefore, if one calls closed derivations
'categorical' and open derivations
'hypothetical', one may characterize this approach as
following two fundamental ideas: (I) The primacy of the categorical
over the hypothetical, (II) the transmission view of consequence.
These two assumptions (I) and (II) may be viewed as *dogmas of
standard semantics*. "Standard semantics" here not
only means standard proof-theoretic semantics, but also classical
model-theoretic semantics, where these dogmas are assumed as well.
There one starts with the definition of truth, which is the
categorical concept, and defines consequence, the hypothetical
concept, as the transmission of truth from conditions to consequent.
From this point of view, constructive semantics, including
proof-theoretic semantics, exchange the concept of truth with a
concept of construction or proof, and interpret
"transmission" in terms of a constructive function or
procedure, but otherwise leave the framework untouched.



There is nothing wrong in principle with these dogmas. However, there
are phenomena that are difficult to deal with in the standard
framework. Such a phenomenon is non-wellfoundedness, especially
circularity, where we may have consequences without transmission of
truth and provability (see section
 3.8).
 Another phenomenon are substructural distinctions, where it is
crucial to include the structuring of assumptions from the very
beginning (see section
 3.10).
 Moreover, and this is most crucial, we might define things in a
certain way without knowing in advance of whether our definition or
chain of definitions is well-founded or not. We do not first involve
ourselves into the metalinguistic study of the definition we start
with, but would like to start to reason immediately. This problem does
not obtain if we restrict ourselves to the case of logical constants,
where the defining rules are trivially well-founded. But the problem
arises immediately, when we consider more complicated cases that go
beyond logical constants.



This makes it worthwhile to proceed in the other direction and start
with the hypothetical concept of consequence, i.e., characterize
consequence directly without reducing it to the categorical case.
Philosophically this means that the categorical concept is a limiting
concept of the hypothetical one. In the classical case, truth would be
a limiting case of consequence, namely consequence without hypotheses.
This program is closely related to the approach of categorial proof
theory (see section
 2.5),
 which is based on the primacy of hypothetical entities
("arrows"). Formally, it would give preference to the
sequent calculus over natural deduction, since the sequent calculus
allows the manipulation of the assumption side of a sequence by means
of left-introduction rules. In a term-annotated system, we would not
annotate formulas, but hypothetical statements by terms. If a
hypothetical statement is expressed by a sequent in the form \(A
\vdash B\), we would not annotate it as \(x{:}A \vdash t(x){:}B\) as
in the Curry-Howard correspondence, but in a way like \(f{:}(A \vdash
B)\). That is, the full hypothetical statement would be annotated,
which makes the parallel to the categorial approach, where \(f\) would
be the arrow \(f : A \rightarrow B\), obvious.



*Further Reading*



For *hypothetical reasoning* and *intensional proof
theoretic semantics* see Dosen (2003; 2016) and
Schroeder-Heister (2012c, 2016).


### 3.7 Intensional proof-theoretic semantics



As mentioned in the first section
 (1.1),
 proof-theoretic semantics is intensional in spirit, as it is
interested in proofs and not just provability. For proof-theoretic
semantics it is not only relevant, whether \(B\) follows from \(A\),
but also, in which way we can establish that \(B\) follows from \(A\).
In other words, the identity of proofs is an important issue. However,
though this is prima facie obvious and proof-theoretic semanticists
would normally agree with this abstract claim, the practice in
proof-theoretic semantics is often different, and the topic of the
identity of proofs is much neglected. It very frequently happens that
rules which are equally powerful are identified. For example, when
principles of harmony are discussed, and one considers the standard
introduction rule for conjunction 
\[\begin{prooftree}
\AxiomC{$A$}
\AxiomC{$B$}
\BinaryInfC{$A\land B$}
\end{prooftree}\]




many proof-theoretic semanticists would consider it irrelevant whether
one chooses the pair of projections

 
\[
\begin{prooftree}
\AxiomC{$A \land B$}
\UnaryInfC{$A$}
\end{prooftree}
\hspace{1.5em}

\begin{prooftree}
\AxiomC{$A\land B$}
\UnaryInfC{$B$}
\end{prooftree}
\]


or the pair

 
\[
\begin{prooftree}
\AxiomC{$A \land B$}
\UnaryInfC{$A$}
\end{prooftree}
\hspace{1.5em}

\begin{prooftree}
\AxiomC{$A\land B$}
\AxiomC{$A$}
\BinaryInfC{$B$}
\end{prooftree}
\]


as the elimination rules for conjunction. The second pair of rules
would often be considered to be just a more complicated variant of the
pair of projections. However, from an intensional point of view, these
two pairs of rules are not identical. Identifying them corresponds to
identifying \(A \land B\) and \(A \land (A \rightarrow B)\), which is
only extensionally, but not intensionally correct. As Dosen has
frequently argued (e.g., Dosen 1997; 2006), formulas such as
\(A \land B\) and \(A \land(A \rightarrow B)\) are equivalent, but not
isomorphic. Here "isomorphic" means that when proving one
formula from the other and vice versa, we obtain, by combining these
two proofs, the identity proof. This is not the case in this
example.



Pursuing this idea leads to principles of harmony and inversion which
are different from the the standard ones. As harmony and inversion lie
at the heart of proof-theoretic semantics, many of its issues are
touched. Taking the topic of intensionality seriously means reshaping
many fields of proof-theoretic semantics (see Schroeder-Heister,
2022). This has repercussions in various neighbouring fields such as
the treatment of paradoxes. The first monograph on intensional
proof-theoretic semantics, with particular emphasis on the topic of
paradoxes, has been written by Tranchini (2023).



Since the identity of proofs is a basic topic of categorial proof
theory (see section
 2.5),
 the latter will require more attention in proof-theoretic semantics
than is currently the case.


### 3.8. Paradoxes



The logical, mathematical and semantical paradoxes, which play a
crucial role in logic and the philosophy of mathematics, receive a
novel rendering in the framework of proof-theoretic semantics. If one
formulates paradoxes in the context of introduction and elimination
rules, one can apply to them the proof-theoretic machinery of
proof-reduction. Suppose introduction and elimination rules for set
terms are given as follows (in a kind of naive set theory):



\[
\begin{prooftree}
\AxiomC{$A(t)$}
\UnaryInfC{$t \in \{x:A(x)\}$}
\end{prooftree}
\hspace{1.5em}

\begin{prooftree}
\AxiomC{$t \in \{x:A(x)\}$}
\UnaryInfC{$A(t)$}
\end{prooftree}
\]


Then, for \(r\) as \(\{x: x \not\in x\}\), we can infer \(r \in r\)
from \(r \not\in r\) and vice versa, which is a natural deduction
variant of Russell's paradox. Now Prawitz (1965, Appendix B)
observed that the derivation of absurdity arising from Russell's
paradox is non-normalizable, a feature that Tennant (1982) was able to
demonstrate for a vast range of paradoxes. From the standpoint of
proof-theoretic semantics, a non-normalizable proof may well be
considered invalid, at least not valid in the sense in which a
normalizable proof is valid. This means that we obtain a
proof-theoretic criterion to tell whether we have a meaningful proof
or not, and proofs of the paradoxes would not be meaningful in this
sense. The Prawitz-Tennant analysis of paradoxes has opened up the
field of the proof-theory of paradoxes, which goes way beyond
proof-theoretic semantics in the narrower sense. It is closely related
to the aspect of intensionality (see section
 3.7)
 and also to the idea of definitional reflection (see section
 2.3.2
 and the
 Supplement on Definitional Reflection and Paradoxes).



A particularly interesting paradox from the point of view of
proof-theoretic semantics is Ekman's paradox. It results from
codifying an implicational variant of Russell's paradox in
minimal propositional logic. It turns out that, depending on how
reductions of detour derivations are formulated, certain derivations
in minimal propositional logic are not normalizable. This sheds a
strong light on the concept of proof reduction, which is absolutely
essential in natural-deduction style proof-theoretic semantics: much
depends on its careful definition. In fact, the concept of proof
reduction constitutes the concept of proof identity and goes way
beyond the extensional idea that "detours" in proofs are
removed.



*Further Reading*



For *Russell's paradox in general* see the entry on
 Russell's paradox.



For the treatment of *paradoxes in proof-theoretic semantics*,
including Ekman's paradox see Tranchini (2023).


### 3.9 Reduction, game theory and dialogues



While deduction is forward-directed, passing from sentences already
established to further sentences by means of justified rules,
reduction proceeds backwards, trying to find an argument for a given
claim. It thus belongs to proof search. Various methods of proof
search have been discovered and discussed in computer science:
resolution and tableau systems are prominent examples. However, from a
semantical perspective, reductive approaches are not conceptually
secondary to deduction but are theories in their own right. One might
even suggest that reductive methods are primary from the semantical
point of view, as the search for an argument, or the possible ways of
searching for it, constitute the meaning of a given claim. This idea
has been adopted, for example, in dialogical or game-theoretical
semantics, but can and should be incorporated in proof-theoretic
semantics in general. This is a major desideratum of proof-theoretic
semantics, which so far is predominantly based on deduction rather
than reduction.



*Further Reading*



For the idea of *reductive logic* and its semantics see the
monograph by David Pym and Eike Ritter (2004).



For *dialogical logic* see the entry on
 dialogical logic
 as well as Thomas Piecha's entry on
 dialogical logic
 the *Internet Encyclopedia of Philosophy*.



For game-theoretical approaches in logic see the entry on
 logic and games.


### 3.10 Substructural approaches



As soon as one treats proof-theoretic semantics in the framework of
the sequent calculus and thus focuses on hypothetical rather than
categorical claims, the area of logics with restricted structural
rules, called "substructural logics", demands semantical
consideration. Here the way assumptions are introduced and kept in
one's discourse represents a much more fine-grained structure
than assumptions in natural deduction, where they are normally
considered to be sets of statements. Due to the possibility of
structuring the succedent of a sequent in an analogous way,
proof-theoretic semantics looses its intuitionistic bias without
necessarily becoming classical. Within the framework of substructural
logic, deviant logical systems such as relevant logic or
resource-sensitive logics can easily be modelled. A particularly
interesting topic is the logic of bunched implications, which
distinguishes different, but co-existing ways of structuring
assumptions and conclusions (see Pym, 2002). Substructural logic is
well-established as a general tool to *describe* logical
systems within a single emcompassing structural framework. Whether
substructural logic *eo ipso* represents a semantical
framework, is still an open question.



*Further Reading*



For *substructural logic* in general see the entry on
 substructural logics.


## 4. Conclusion and outlook



Standard proof-theoretic semantics has practically exclusively been
occupied with logical constants. Logical constants play a central role
in reasoning and inference, but are definitely not the exclusive, and
perhaps not even the most typical sort of entities that can be defined
inferentially. A framework is needed that deals with inferential
definitions in a wider sense and covers both logical and extra-logical
inferential definitions alike. The idea of definitional reflection
with respect to arbitrary definitional rules (see section
 2.3.2)
 and also natural language applications (see secton
 3.4)
 point in this direction, but farther reaching conceptions can be
imagined. Furthermore, the concentration on harmony, inversion
principles, definitional reflection and the like is somewhat
misleading, as it might suggest that proof-theoretic semantics
consists of only that. It should be emphasized that already when it
comes to arithmetic, stronger principles are needed in addition to
inversion. However, in spite of these limitations, proof-theoretic
semantics has already gained very substantial achievements that can
compete with more widespread approaches to semantics.



*Further Reading*



For contributions on a variety of aspects of proof-theoretic semantics
see the reader edited by Piecha and Wehmeier (2023, open access).