Proof-Theoretic Semantics and Truth

I present two theories of truth formulated in Nelson Logic N3 and determine their proof-theoretic strength. The first theory NFS resembles the classical theory FS, yet in contrast to FS, NFS is omega-consistent. The second theory NKF can be viewed as arising from an internalization of the sequent arrow of PKF. NKF, in contrast to PKF, has the same proof-theoretic strength as the classical theory KF. 

From a bilateralist point of view in PTS it seems reasonable to consider bilateral derivability relations, one for proving and one for refuting. In a sequent calculus system this does not seem trivially realizable, though. After all, we have two relations to consider: the derivability relation expressed within a sequent and the one expressed between the sequents. So, it seems that if we are serious about having a bilateral sequent calculus, then we must implement the bilaterality in both these relations.

I will show, however, that this leads to the opposite of our aim, namely an apparent asymmetry between the notions of proof and refutation becoming visible in such a setting. This seems to be related to more profound issues that we need to think about, such as our notion of refutation and our understanding of the horizontal lines in natural deduction and in sequent calculus. Therefore, I will argue, there are limits as to how bilateral we can design our sequent calculus.

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 constructive proof, while the classical logician advocates for a notion which allows non-constructive proofs through reductio ad absurdum. A great deal of controversy still subsists to this day on the matter, as there is no agreement between disputants on the precise standing of non-constructive methods.

Two very distinct approaches to logic are currently providing interesting contributions to this debate. The first, oftentimes called logical ecumenism, aims to provide a unified framework in which two "rival" logics may peacefully coexist, thus providing some sort of neutral ground for the contestants. The second, proof-theoretic semantics, aims not only to elucidate the meaning of a logical proof, but also to provide means for its use as a basic concept of semantic analysis. Logical ecumenism thus provides a medium in which meaningful interactions may occur between classical and intuitionistic logic, whilst proof-theoretic semantics provides a way of clarifying what is at stake when one accepts or denies reductio ad absurdum as a meaningful proof method.

In this talk we show how to coherently combine both approaches by providing not only a medium in which classical and intuitionistic logics may coexist, but also one in which classical and intuitionistic  notions of proof may coexist.

PTS stems from Prawitz’s normalisation theorems for Gentzen’s Natural Deduction. In the original formulation, due to Prawitz himself, proofs are conceived of in terms of inferential structures equipped with reduction functions for removing maximal steps of generalised elimination rules. I shall indicate this variant with the expression reducibility semantics. In the more recent mainstream approach, inferential structures are left aside, and PTS is understood as a theory of consequence for formulas over atomic bases. This variant of PTS is nowadays referred to as base(-extension) semantics. The latter in turn splits into two (sub-)versions: the standard approach, and the Sandqvist approach. Both reducibility semantics and base-semantics are expected to be semantics for intuitionistic, or at least constructive logics, and many completeness or incompleteness results for these logics have been obtained so far. In my talk, I discuss some general results on the relation between reducibility semantics and base-semantics which, when suitable conditions are met, permit one to shift from one approach to the other. From these results I then draw some consequences, relative to the issue of completeness of (recursive) logical systems.

The talk consists of two parts, from concrete to abstract. First, we give a first exploration of proof-theoretic semantics for a substructural logic. We work out a base-extension semantics (B-eS) for a minimal substructural logic -- intuitionistic multiplicative linear logic (IMLL). We begin by reviewing Sandqvist’s B-eS for intuitionistic propositional logic (IPL), and propose an alternative treatment of conjunction that takes the form of the generalized elimination rule for the connective. This motivates a sound and complete B-eS for IMLL, in which the definitions of the logical constants all take the form of their elimination rule. Second, we justify that this approach of defining semantics in the form of the elimination rules is principled. For arbitrary natural deduction systems where the elimination rules are defined by the introduction rules using definitional reflection (DR), one can define a B-eS and prove soundness and completeness uniformly. The B-eS for IPL, IMLL, and IMALL are all instances of this general result.

I present a theory of abstraction and extensionality based on the logic HYPE, called HBST (HYPE Basic Set Theory). HYPE has been suggested as a promising logic to formulate strong theories of truth and abstraction in virtue of its classical recapture properties: in fact, it can be shown that a theory of Kripkean truth over HYPE, KFL, is as strong as the classical theory KF. Furthermore, HYPE can be seen as a logic adequate to deal with intensionally defined sets obeying some form of extensionality. Set identity criteria in theories with abstraction principles resemble criteria of property identity, and thus hyperintensional frameworks are particularly suited to deal with them. I develop a consistency proof for the theory HBST, and show some of its features. I note an interesting interplay between the axiomatic and semantic treatment of the theory, and note that, compared to the case of truth, the theory we obtain is exceptionally weak. Some remarks and diagnosis are offered for this phenomenon.

Deductive logic infers conclusions from established premisses by deduction. By contrast, reductive logic seeks to find premisses that are sufficient to establish a putative conclusion. In reductive logic, proof-search — by which the space of possible ‘reductions’ is explored — is an essential component. I will explore connections between reductive logic, proof-search, and proof-theoretic semantics, and consider a possible role for coalgebra in providing a unifying framework.

We present incompleteness results for intuitionistic propositional logic (IPC) with respect to some standard notions of proof-theoretic validity. The validity of atomic formulas is given by their derivability in atomic systems, that is, in systems of rules which contain only atomic formulas. These systems are usually interpreted as knowledge bases. Considering completeness results for IPC with respect to notions of proof-theoretic validity that handle atomic systems in different ways, one can ask about the correct interpretation of atomic systems. We discuss a view of atomic systems as definitions and point out its problems.

In (Dummett 1976), it is posited that for a statement to be true, there must exist something in virtue of which it is true (Regulative Principle C). Neil Tennant (2018) interprets this principle as a truthmaking axiom, asserting that the entity in virtue of which a statement is true is, indeed, a truthmaker. To dispel potential confusion, Tennant clarifies that Dummettian anti-realists find no issue with this truthmaker axiom, given their conception of truth as contingent upon the existence of a truthmaker—albeit one that is, in principle, surveyable or epistemically accessible. In (Tennant 2018), a reconstruction of these ideas is proposed in the form of "a logical theory of truthmakers and falsitymakers", wheras truthmaker (and falsitymakers) are conceived as potentially infinitary proofs (or refutations) of sentences of a first-order language L within a suitably rich metatheory. While the proposal is intriguing, I believe some of its aspects call for further examination.

Firstly, as Milne argues in (Milne 2005), it should be considered a «conceptual truth» of the notion of truthmaking that, if a statement possesses a truthmaker, then it is true. However, if this is indeed a conceptual truth, it is easy to see how Milne's principle and Regulative Principle C could easily lead to paradoxes reminiscent of the liar paradox (Milne 2005) – just consider the statement "This statement doesn't have any truthmakers". Secondly, in what sense can we conceive of Tennant's infinitary proofs as being "epistemically accessible" or "surveyable"?

In this presentation, I aim to tackle both of these concerns by proposing two predicative theories of truthmaking tailored for a first-order language that is sufficiently expressive to talk about its own truthmaking. Drawing inspiration from the influential work of Glanzberg (2004) and using resources thoroughly described in the seminal (Barwise 1975), I'll put forth two predicative theories of self-applicable truthmaking capable of avoiding truthmaking paradoxes:

1. The first theory, building on the philosophical picture recently presented by Fine (2017), regards truthmakers as modeled by sets of literals of a specified language, aligning with established practices in truth-conditional or model-theoretic theories of truthmaking.

2. The second theory envisions truthmakers as infinitary proofs in an infinitary proof system resembling the system presented in Tennant (2018). However, my theory allows for an infinite set of proofs to serve as a premise of an infinitary rule only if the set is predicatively definable using specified mathematical resources.

(Barwise 1975): Barwise, J. (1975). Admissible sets and structures. Cambridge University Press.

(Dummett 1976): Dummett, M. "What is a Theory of Meaning? II", in G. Evans and J. McDowell, eds., Truth and Meaning, OUP, 1976

(Fine 2017): Fine, K. (2017). Truthmaker semantics. A Companion to the Philosophy of Language, 556-577.

(Glanzberg 2004): Glanzberg, M. (2004). A contextual-hierarchical approach to truth and the liar paradox. Journal of Philosophical Logic, 33(1), 27-88.

(Milne 2005): Milne, P. "Not every truth has a truthmaker." Analysis 65.3 (2005): 221-224.

(Tennant 2018):  Tennant, N. "A logical theory of truthmakers and falsitymakers", in M. Glanzberg, ed., The Oxford Handbook of Truth (2018)

The proof-theoretic semantics for IPL is subtle. The range of incompleteness results relative to simple and sensible presumptions --- particularly, by Piecha et al. ---  cause concern. Nonetheless, a semantics was eventually given by Sandqvist that works only relative to, perhaps, unusual design choices. We investigate its correctness from the native perspective, the categorical perspective, the logic programming perspective, and its relationship to earlier ideas by Dummett and Prawitz.

The aim of this talk will be to present two extensions to the atomic system presented by Gheorghiu, Gu, and Pym for IMLL, giving rise to an atomic system for a B-eS for Intuitinistic Linear Logic. The first such extension is that of the notion of additive regions; regions in an atomic rule which allow the rule to express additive, or “resource sharing”, derivations. The second, and much more interesting extension, is that which allows for expressing formulas marked by the modality ! in ILL. Formulas marked by such modalities are not subject to the structural constraints placed on other formulas in ILL, and the B-eS for IMLL (and IMALL) reflect these structural constraints well, making it particularly hard to express behaviour that does not conform to these constraints. Finding a way around this problem is not easy and, in this talk, we present one such solution which does gives rise to a sound and complete semantics for ILL.