Workshop Proof Theory

May 19 and 21 - 22

Buenos Aires, Argentina

Agustina Borzi (IIF-SADAF-CONICET)

Bruno Da Ré (IIF-SADAF-CONICET)

Andrzej Indrzejczak (University of Lodz)

Nils Kürbis (Ruhr-Universität Bochum) 

João Marcos (Universidade Federal de Santa Catarina)

Alejandro Solares Rojas (UBA - CONICET)

Tuesday, May 19, Thursday, May 21 and Friday May 22 

(GMT-03, Buenos Aires Local Time)

Tuesday, May 19

11:00 - 13:00: Nils Kürbis 

11:00 - 13:00: Damian Szmuc

Thursday, May 21

15:00 - 16:00: Andrej Indrezjczak

16:00 - 16:15: Short break

16:15 - 17:15: Alejandro Solares

17:15 - 18:00: Long break

18:00 to 19:00: Joao Marcos

Friday, May 22

15:00 - 16:00: Bruno Da Ré

16:00 - 16:15: Short break

16:15 - 17:15: Agustina Borzi

17:15 - 18:00: Long break

18:00 - 19:00: Nils Kurbis

Agustina Borzi: "Sequent calculi for some containment logics"

This talk touches on the proof theory of variable inclusion (or containment) logics. In particular, it introduces new sequent calculi for right and left variable inclusion companions of Classical logic, broadly understood as proper subsystems of Classical logic in which the variables of the conclusions are contained in those of the premises, and vice versa. The starting point are sequent calculi for Paracomplete and Paraconsistent Weak Kleene, two systems closely related to containment logics in that they impose variable inclusion constraints on valid inferences, albeit only in the absence of (anti)theorems. Two strategies are then proposed to obtain subsystems of them that can be regarded as genuine containment logics: modifying the rules of negation, which yields calculi sound and complete for the pure companions of Classical logic, both paracomplete and paraconsistent logics, and restricting Weakening, which produces non-monotonic systems sound and complete for the analytic and synthetic companions of Classical logic.

Bruno Da Ré: "Metainferential tableaux for global validity"

In a recent article (Bavosa Castro, A., Borzi, A., Da Ré, B., Roffé, A. J., & Toranzo Calderón, J. S. (2026). Tableaux for metainferential logics. Journal of Applied Non-Classical Logics , 36(1), 113-146.), we have introduced a series of requisites for building sound and complete tableaux systems for inferential logics based on non-deterministic valuations and extend them with rules for metainferences, thus yielding metainferential tableaux systems capable of proving metainferences of any level n, by taking into account only the local notion of metavalidity. The aim of this talk is to generalize the previous work, by also providing a method to build sound and complete tableaux regarding the global notion of metavalidity, and possible combinations of local and global validity at different levels. (joint work with Agustina Borzi and Ariel Roffé).

Andrzej Indrzejczak: "Weak Logicism, the Logics of Classes and Sequent Calculi"

Logicism currently is not a popular approach to the foundations of mathematics. But it is still alive in the variety of neologicist positions, represented for example, by Tennant's constructive neologicism. In particular, this form of neologicism can be applied to set theory and we focus on possible ways of its formalisation in sequent calculus. 

The logic of classes, under the name the virtual theory of classes (VTC), was rst introduced by Quine as a flexible neutral tool for comparison of alternative theories of sets, like ZF, NGB or NF. It species in the safe, non-committal way the conditions for reasoning with set theoretic constructs. The main notion of a class is represented by set abstracts, and permits for investigation of the domain of classes without existential assumptions.

Quine developed VTC on the basis of classical logic but it was also dealt with by Dana Scott in the version founded on positive free logic. Independent variant of the Fregean logic of classes was proposed by Neil Tennant on the basis of negative free logic. Despite the di erences, all these approaches can be treated as forms of weak logicism reconstructing the logic of our discourse on sets but without assuming the existence of some special sets.

Neither VTC nor Scott's theory was so far explored proof-theoretically although Tennant provided natural deduction system for his Fregean logic of classes. In fact all variants can be formalised by means of sequent calculi and on the basis of different strategy of treating set abstracts. Our calculi for Quine's and Scott's logics satisfy cut elimination, generalised subformula property and are provably consistent, also in the intuitionistic variant. Sequent calculus for Tennant's logic also satises cut elimination but is not fully analytic. For the sake of illustration we show how these calculi can be extended to cover ZFC by means of (systems of) rules. This sequent formalisations of ZFC also preserve cut elimination. Moreover, some of its subsystems in free version are also provably consistent, in contrast to their classical counterparts.

Funded by the European Union (ERC, ExtenDD, project number: 101054714). Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or the European Research Council. Neither the European Union nor the granting authority can be held responsible for them.

Nils Kürbis: "Proof-theoretic logicism. Some thoughts and questions"

Logicism is the view, originally put forward and developed by Frege, that arithmetic is nothing but logic: the laws of arithmetic are analytic truths and derivable solely from the laws of logic and definitions (together with proofs that establish the legitimacy of these definitions, see Grundlagen §3).

Deductive Semantics (aka proof-theoretic semantics or inferentialism) is the view that the meanings of the logical constants are defined by the rules of inference governing them, provided they satisfy certain criteria. It originates with Gentzen and was developed by Dummett, Prawitz and Schroeder-Heister. 

Proof-theoretic Logicism combines deductive semantics and logicism. That is, according to it, some fundamental concepts of arithmetic are logical constants the meanings of which are defined by the rules of inference governing them. (Others may be defined explicitly.) This is an attractive position: deductive semantics provides a neat account of logic, which, paired with logicism, would extend to a neat account of arithmetic. 

My aim in this presentation is to assess the prospects of defending proof-theoretic logicism and to raise three questions that would need to be addressed. More precisely, my question is whether we can combine the logicism put forward by Frege in Grundlagen and modified, developed and defended by Bob Hale and Crispin Wright (and a couple of others) with (my version of) deductive semantics. 

Proof-theoretic logicism is not new. Neil Tennant has proposed precisely such a view. I do, however, have views on deductive semantics that, I think, diverge from Tennant's. My views on the matter are admittedly austere. The aim in my talk is less to assess Tennant's approach, but to see whether relative to my own views on deductive semantics, some (plausible) form of proof theoretic logicism is defensible. 

Nils Kürbis: "Proof Theory of Definite Descriptions" (Tutorial)

João Marcos: "Bivalent semantics and depth-bounded analytic proof systems for logics characterized by finite-valued nondeterministic semantics"

A classical insight, independently articulated by Roman Suszko, Dana Scott, and Newton da Costa in the 1970s, holds that the apparent multiplicity of truth values in any tarskian logic is, in a precise sense, illusory: every such logic admits a characterization using only two logical values. Building on this foundational observation, sustained research over the last couple of decades has worked toward making such bivalent presentations not merely existential but constructive and computationally tractable for progressively wider families of logics.

In this talk I will show how effective bivalent semantics and uniform classic-like analytic proof systems can be extracted for logics determined by finite-valued nondeterministic matrices. The tableau calculi so obtained are cut-based and employ only linear rules; they also polynomially simulate truth-tables, a feature not shared by their standard cut-free counterparts. I will further discuss how the framework connects with the depth-bounded approach to rationality, which offers a graded notion of inferential commitment calibrated to bounded computational resources.

(This is a report on ongoing joint work with Carlos Caleiro.)

Alejandro Solares Rojas: "Labeled KE-style systems: the case of intuitionistic modal logics"

The proof system KE is a variant of analytic tableaux, but computationally more efficient than these.  KE's hallmark is reducing the amount of branching to a minimum by making all branches mutually exclusive. Namely, it has only one branching rule that corresponds to a non-eliminable analytic-cut rule. The rest of the rules all have a non-branching format and correspond to familiar reasoning patterns, such as modus ponens and disjunctive syllogism.

In this talk, we extend KE by means of labeled signed formulas so as to mimic countermodel-search in the (bi-)relational semantics of a family of intuitionistic modal logics.  We thus obtain KE-style systems for these logics, which inherit the hallmark of reducing proof-size to a minimum. Besides this efficiency, the systems enjoy native interpretability within their underlying semantics and are modular in that they can naturally implement the "axiom-to-rule" methodology.

For the plain intuitionistic case, we detail termination via a procedure of countermodel extraction, and show some steps toward its implementation as an automated theorem prover.

Damián Szmuc: "Tutorial on metainferences"

During this talk, I'll give a short briefing on what the recent, current, and future logical and philosophical investigations of the members of the BA LOGIC group are in and around metainferences, substructural logics, peculiar-looking semantics and the like.

Eduardo Barrio  (IIF (CONICET-SADAF) & UBA)
Edson Bezerra (IIF (CONICET-SADAF) & UBA)
Camila Gallovich (IIF (CONICET-SADAF) & UBA)
Damián Szmuc (IIF (CONICET-SADAF) & UBA)
Paula Teijeiro (IIF (CONICET-SADAF) & UBA)

We are thankful for the support provided by CONICET (Consejo Nacional de Investigaciones Científicas y Técnicas, Argentina).