Finitary logics, i.e., Tarskian consequence relations between sets of formulas and for- mulas with Hilbert-style axiomatization using rules with finitely many premises only, are the bread and butter of almost every (non-classical) logician (see e.g. [2]). However there are many interesting logics which are not finitary: e.g. certain dynamic logics, logics of common knowledge, or prominent many-valued logics such as standard Łukasiewicz logic[5,6,8,9].

We start this tutorial by introducing several interesting extensions of the class of finitary logics, present their characterizations, mutual inclusions and separations, and show that several important theorems of abstract algebraic logic can be generalized from finitary logics to some of these classes [2, 3, 7]).

Then we focus on the Lindenbaum lemma and a closely related Pair Extension Property (a ‘proper’ replacement of the Cut rule in symmetric consequence relations [4]). These crucial results (used e.g. in the completeness proofs) are usually proved for finitary logics only but are known to hold for some infinitary logics as well [5, 6, 8, 9]. We explore the mutual relationship of these two notions and present several easily check- able sufficient and/or necessary conditions for their validity outside the class of finitary logics [1, 2].

We conclude by showcasing certain applications of the presented results, remark on their relation to other notions (e.g. the Rasiowa–Sikorski lemma or expansion of a first- order theory into a Henkin one), and explore several avenues of possible generalization.

[1] M. Bílková, P. Cintula, T. Láička, Lindenbaum and pair extension lemma in infinitary logics, WoLLIC 2018, (Moss, de Queiroz, Martinez, editors), Springer, 2018, pp. 134–144.

[2] P. Cintula, C. Noguera, Logic and Implication: An Introduction to the General Algebraic Study of Non-classical Logics, Springer, 2021.

[3] P. Cintula, C. Noguera, The proof by cases property and its variants in structural consequence relations, Studia Logica vol. 101 (2013), pp. 713–747.

[4] J.M. Dunn, G.M. Hardegree Algebraic Methods in Philosophical Logic, Clarendon Press, 2001

[5] R. Goldblatt, Mathematics of Modality, CSLI Publications Stanford University, 1993.

[6] L.S. Hay; Axiomatization of the infinite-valued predicate calculus, Journal of Symbolic Logic vol. 28 (1963), pp. 77–86.

[7] T. Lávička, C. Noguera, A new hierarchy of infinitary logics in abstract algebraic logic, Studia Logica vol 105 (2017), pp. 521–551.

[8] K. Segerberg, A model existence theorem in infinitary propositional modal logic, Journal of Philosophical Logic, vol. 23 (1994), pp. 337–367.

[9] G. Sundholm, A completeness proof for an infinitary tense-logic, Theoria, vol. 43 (1977), pp. 47–51. 

“A student of mine asked me today to give him a reason for a fact which I did not know was a fact and do not yet. He says that if a figure be anyhow divided and the compartments differently coloured so that figures with any portion of common boundary line are differently coloured four colours may be wanted, but not more… If you retort with some very simple case which makes me out a stupid animal, I think I must do as the Sphynx did…” [3]

This is what the famed mathematician De Morgan wrote to his friend, Hamilton, the distinguished mathematician and physicist, in 1852. The content of this letter was the birth of the famous “four color theorem”. Over the years, several fallacious proofs were given until finally in 1977, Appel and Haken presented a correct one. The proof, however, required analyzing many (to be precise, 1936) discrete cases. Facing such a tedious case-checking work, the question arises whether there exists a shorter, more brilliant proof. Or, we may more generally wonder:

How hard is it to prove some given theorems? What are their shortest proofs? Are there such hard theorems that even their shortest proofs go beyond our physical capacities?

Even in the case that we consider the propositional level, these problems are meaningful: Let φ be a classical propositional tautology. By the so-called brute-force method, we know that φ has a proof roughly of the size 2^nn, where n is the number of the atomic variables in φ. The question is whether there exists a smarter strategy to verify the validity of φ, which does not include checking all the possible valuations.

The problems we mentioned so far focus on theorems rather than the theories in which they are proved. Looking in this direction, one can ask whether there is a theory so strong that no hard theorems exist in it. Otherwise, what happens if there exists no such theory? Then, we may wonder if there will be a significant decrease in lengths of proofs when we move to more powerful theories. If so, we can continue to advance towards stronger and stronger theories and ask: Is there a “strongest” theory, in the sense that it provides the best proofs?

These are some examples of the problems considered in proof complexity, a field whose main aim is investigating the complexity (for instance, length, i.e., number of symbols) of proofs.

In this tutorial, we begin with introducing proof systems such as Frege and extended Frege systems and resolution. We introduce Cook’s program and consider open problems and how they are related to the complexity classes P, NP, and coNP, and in general to the field of computational complexity. We will then talk about interpolation, specially feasible interpolation as one of the main methods to prove lower bounds. Finally, we will talk about the complexity of proofs in systems for non-classical logics. For more, see [1,2].

References
[1]  J. Krajíček, Proof complexity, Vol. 170. Cambridge University Press, 2019.
 

[2]  P. Pudlák, Logical foundations of mathematics and computational com- plexity: A gentle introduction, Springer, Berlin, 2013.

[3]  R. Wilson, Four Colors Suffice: How the Map Problem Was Solved - Revised Color Edition. Vol. 30. Princeton university press, 2013.

In this tutorial we concentrate on studying which truth-values are most likely to be taken on finite models by arbitrary sentences of a many-valued predicate logic. We show generalizations of Fagin’s classical zero-one law for any logic with values in a finite lattice-ordered algebra, and for some infinitely valued logics, including Łukasiewicz logic. The finitely valued case is reduced to the classical one through a uniform translation and Oberschelp’s generalization of Fagin’s result. Moreover, we show that the complexity of determining the almost sure value of a given sentence is PSPACE-complete, and for some logics we may describe completely the set of truth-values that can be taken by sentences almost surely. The presented new results have been obtained in a joint work with Guillermo Badia and Xavier Caicedo [1].

[1] Guillermo Badia, Xavier Caicedo, and Carles Noguera. Asymptotic truth-value laws in many-valued logics, arXiv:2306.13904, 2023.