Many new results and new insights about classical and non-classical logics have been obtained using the sequent calculus, e.g. Gentzen’s consistency argument; interpolation, decidability, complexity for modal and substructural logics; (what else?).
I would like to identify new results and insights about logics that were obtained using proof systems—other than the sequent calculus—that utilised some notion of analyticity / a restriction of proof space such as the subformula property. I am interested across all sorts of logics and all sorts of formalisms like hypersequent, nested, labelled, display, proof nets, deep inference based. Here I am viewing a logic as a set of formulas.
For example, hypersequent calculi were recently used to obtain new decidability and complexity upper bounds for many substructural logics extending the commutative Full Lambek calculus with weakening (FLew) and contraction (FLec). See this post for more on these logics.
[BalLanRam21] A. R. Balasubramanian, Timo Lang, RR. Decidability and Complexity in Weakening and Contraction Hypersequent Substructural Logics. LICS 2021.I would be pleased to see your thoughts and references on this below !
Hi Revantha,
Some questions:
(1) Do you want results that were *first* obtained using proof theory or at least *alternatively* obtained?
(2) Do you care whether the logic in question is primarily semantically motivated (e.g. with a formula-based model theory) or is it okay if it is proof-theoretically motivated? I suppose the former?
Cheers,
Anupam
Hi Anupam,
>(1) Do you want results that were *first* obtained using proof theory or at least *alternatively* obtained?
I am looking for results that were obtained *first* using proof theory. Alternative proofs via proof theory that yielded *new insights* are very welcome too.
>(2) Do you care whether the logic in question is primarily semantically motivated (e.g. with a formula-based >model theory) or is it okay if it is proof-theoretically motivated? I suppose the former?
I’m open to results about all logics (viewed as a set of formulas in some language). I want to exclude results like “a more refined proof system for logic L” that are ‘supplementary’ to the logic.
Dear Revantha:
I’ve been working in my Master’s with Hilbert-style systems that allow for multiple formulas in the conclusion of the rules. In case you have never heard about them, they were first studied by Shoesmith & Smiley in [1], being
referred to as symmetrical, SET-SET or multiple-conclusion systems. Informally speaking, derivations, instead of finite sequences of formulas, are bounded rooted trees labelled with sets of formulas, whose nodes are expanded by the application of rules of inference. Each formula in the conclusion of an applied rule produces a new branch. A set of formulas D follows from a set of formulas G in a SET-SET system when there is a tree built from the rules of that system, having its root labelled with G and every branch ending with at least one formula of D. In this setting, traditional Hilbert-style derivations are just linear trees, so the SET-SET formalism generalizes the traditional approach.
When you have an analytic SET-SET system, there is a simple exponential proof-search algorithm for it.
Also, in case every rule has at most one formula in its conclusion, the underlying logic is polynomial-time decidable.
There are nice applications developed recently. In particular, in [2] you may find a procedure that produces adequate and analytic (!) SET-SET calculi for a very inclusive class of partial non-deterministic
logical matrices. My current work is to generalize and implement this approach for two-dimensional partial non-deterministic matrices (see [3], a work that I will present in TABLEAUX in a few days). You may find other applications and investigations on SET-SET systems in recent works by Carlos Caleiro and Sérgio Marcelino (for example, see [4,5,6]).
I hope I have contributed in some way!
Kind regards,
Vitor Greati.
[1] Shoesmith, D.J., Smiley, T.J.: Multiple-Conclusion Logic. Cambridge UniversityPress (1978). https://doi.org/10.1017/CBO9780511565687
[2] Caleiro, C., Marcelino, S.: Analytic calculi for monadic PNmatrices. In: Iemhoff,R., Moortgat, M., Queiroz, R. (eds.) Logic, Language, Information and Com-putation (WoLLIC 2019), LNCS, vol. 11541, pp. 84–98. Springer (2019).https://doi.org/10.1007/978-3-662-59533-6
[3] Greati, V., Marcelino, S., Marcos, J: Proof Search on Bilateralist Judgments over Non-deterministic Semantics. (To be presented in the TABLEAUX21’s proceedings). Preprint: https://arxiv.org/abs/2107.08349
[4] Caleiro, C., Marcelino, S.: On Axioms and Rexpansions, pp. 39–69. Springer Inter-national Publishing, Cham (2021). https://doi.org/10.1007/978-3-030-71258-7_3
[5] Caleiro, C., Marcelino, S., Filipe, P.: Infectious semantics and analytic calculi foreven more inclusion logics. In: IEEE International Symposium on Multiple-ValuedLogic. pp. 224–229 (2020). https://doi.org/10.1109/ISMVL49045.2020.000-1
[6] Marcelino, S. An Unexpected Boolean Connective. Logica Universalis (2021). https://link.springer.com/article/10.1007/s11787-021-00280-7
This is a question of great interest to me. I have worked for at least a decade on trying to improve and apply a method of proving normalization which was invented by W. A. Howard (see his contribution to Intuitionism and Proof Theory (1970)).
I understand from looking at the list of open problems on Professor Barendregt’s web page that Gödel proposed to Professor Howard that he should try to solve the following problem: to define a function from simply typed lambda terms to natural numbers with the property that performing a reduction step on a lambda term leads to a new lambda term with a smaller number correlated than the original one. Stated like that, the problem is not exactly a problem about a logical calculus but, thanks to the correspondence between formulae and types, the problem can also be formulated as a problem about positive implicational natural deduction proofs.
Professor Howard did not quite succeed in solving Gödel’s problem although he went a long way towards it: the notion of reduction step with which he worked was slightly more restrictive than usual (without the full rule xi). I myself have tried to show that it is possible to dispense with this restriction.
Could this have been proven by sequent calculus methods? Maybe but I do not see that Howard’s actual proof has any connection with sequent calculus methods and any attempt to apply them would face certain difficulties. Given a natural deduction proof, of course there are going to be sequent proofs of the same conclusion but the difficult bit is correlating a unique sequent proof with each natural deduction proof and showing that the correlation is compatible both with standard cut-elimination methods in the sequent calculus and with the standard notion of reduction in the natural deduction calculus. That is, suppose N1 is a natural deduction proof that reduces to N2. Let f be a function which takes each natural deduction proof to a sequent proof of the same conclusion. Then one way of expressing the difficulty is to say that there may be no known notion of reduction on sequent proofs that takes f(N1) to f(N2). A perhaps sharper way of expressing the difficulty is that it may be very difficult to find a function from sequent proofs to natural numbers which has the property that f(N2) gets a smaller number than f(N1).
A project that I am interested in prosecuting is to try and extend Howard’s method to polymorphically typed lambda terms or (equivalently) to second-order logic. It seems to me that in second order logic there may even be some advantages to working with natural deduction proofs. There is an obvious way to reduce natural deduction proofs or lambda terms (so the problem is “only” to show that all reduction sequences terminate) whereas when considering sequent proofs the only notions of reduction that have been defined so far appear exceedingly unobvious and that is before you even start trying to prove that finitely many reductions will lead to a cut-free proof. You can see this very clearly by studying Takeuti’s cut-elimination proofs.
Thank you Vitor and William. I was not aware of either of these. At some point I will collect what I learn and summarise and add them to the post.
In the meantime, I look forward to hearing from all readers about other new meta-logical results obtained via analytic proof systems that extend the sequent calculus !
Just arXived: “Cirquent calculus in a nutshell”
https://arxiv.org/abs/2108.12552
Abstract: This paper is a brief and informal presentation of *cirquent calculus*, a novel proof system for resource-conscious logics. As such, it is a refinement of sequent calculus with mechanisms that allow to explicitly account for the possibility of sharing of subexpressions/subresources between different expressions/resources. This is achieved by dealing with circuit-style constructs, termed *cirquents*, instead of formulas, sequents or other tree-like structures. The approach exhibits greater expressiveness, flexibility and efficiency compared to the more traditional proof-theoretic approaches.
Dear Giorgi, if there was a new meta-logical result that was obtained using this cirquent calculus, could you concisely describe this result? From a brief look I gathered “exponential speed-up of analytic proofs over sequent calculus for computability logic” but I’m sure you can summarise it better! I would like to collect these and summarise in my posting.
In https://doi.org/10.1093/logcom/exn019 a polynomial-size cirquent-calculus proof has been constructed for the pigeonhole principle. Unlike the other known polynomial-size proofs, this proof does not have to rely on cut or extension, and can thus qualify as analytic. The legitimacy of this qualification, however, may be arguable, because “analyticity” in cirquent calculus or deep inference systems in general cannot be understood as simply having the subformula property. It permits some “recomposing” of subformulas.
Thanks for the nice explanation !
Dear Vitor and William, if there was a new meta-logical result R about a logic L that was obtained in the works you described, and obtained using an analytic proof system S that was not a sequent calculus, could you concisely and concretely describe it here (preferable with a reference) ?
As a possible template: “Result R for logic L was first established in [reference]. The proof made use of proof system S”.
I would like to collect these and summarise in my post.
Vitor has been busy working on his slides, but should respond to you after his talk at TABLEAUX tomorrow! It is curious to observe, anyway, that our joint contribution was scheduled for a session called “Sequent Calculi”. 😉
https://tableaux2021.org/#program
Dear Revantha,
Here are three results related to the analytic Hilbert-style systems I have mentioned:
1) The 4-valued “logic of information sources” specified via non-deterministic semantics in [1]
is polynomial-time decidable. This follows from the axiomatization procedure and the proof-search algorithm
we have provided in [2]. The latter reference deals with this logic in
a two-dimensional setting, but the result also holds for the one-dimensional version, as it was
originally presented. The analytic calculus, in this case, was given in [3, Ex. 3.10].
2) The Logic of Formal Inconsistency called mCi is finitely axiomatizable by
an analytic finitary Hilbert-style system when inhabiting the t-aspect of the B-consequence
relation induced by a two-dimensional version of the 5-valued non-deterministic matrix
for this logic presented by Avron in [4]. The one-dimensional Hilbert-style axiomatization that we
know for mCi is not finite. The present result follows again from the procedures
presented in [2]. The calculus was not given in that paper, but it can be produced
using the implementation available at https://github.com/greati/logicantsy.
3) Considering again the one-dimensional versions of the results in [2]
(described in [3]), we have that, if co-NP \neq PSPACE, intuitionistic logic (IL)
cannot be axiomatized by a Set-Set Theta-analytic finite and finitary Hilbert-style axiomatization (for Theta a finite set of one-variable formulas) — as deciding IL is PSPACE-complete.
🙂
[1] Arnon Avron, Jonathan Ben-Naim, and Beata Konikowska. “Cut-free ordinarysequent calculi for logics having generalized finite-valued semantics”.
In:LogicaUniversalis1 (2007), pp. 41–70. DOI:10.1007/s11787-006-0003-6
[2] Greati V., Marcelino S., Marcos J. (2021) Proof Search on Bilateralist Judgments over Non-deterministic Semantics. In: Das A., Negri S. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2021. Lecture Notes in Computer Science, vol 12842. Springer, Cham. https://doi.org/10.1007/978-3-030-86059-2_8
[3] S. Marcelino and C. Caleiro. “Axiomatizing non-deterministic many-valued gen-eralized consequence relations”. In:Synthese(2019). DOI: 10.1007/s11229-019-02142-8
[4] Arnon Avron. “5-valued non-deterministic semantics for the basic paraconsistentlogicmCi”. In:Studies in Logic, Grammar and Rhetoric(2008), pp. 127–136.
Dear Revantha, Further to your post of 1 September, I may have misunderstood the question or just couldn’t resist the temptation to talk about W. A. Howard’s methods. My answer drew attention to a theorem about a specific kind of logical calculus (natural deduction), not just a logic. I am starting to suspect that by “a logic” you mean something calculus-invariant, perhaps a collection of inferences taken to be valid. Am I suspecting rightly?
Having thought a bit further about the matter, I would say one can distinguish three questions:
(1) Are there important theorems of proof theory that were achieved using methods other than cut-elimination?
(2) Are there theorems of the kind mentioned in (1) which are moreover theorems about purely logical, rather than logico-mathematical systems?
(3) Are there theorems of the kind mentioned in (2) which can be formulated without reference to a specific kind of logical calculus, e.g. natural deduction or sequent calculi?
Question (1) is the question of most interest to me, though of course answers to (2) are an important subset of answers to (1). I suspect though that what you had in mind is (3). Am I suspecting rightly? William