AAL 2023


The Australasian Association for Logic will hold  its annual conference in hybrid format (using  Zoom for the online component) from  Thursday 9 November  to Friday 10 November, 2023. The physical location will be the University of Queensland  in Brisbane.

There will be three one-hour tutorials on different logic topics. The speakers will be Petr Cintula (Czech Academy of Sciences),  Raheleh Jalali (Czech Academy of Sciences),  and Carles Noguera (University of Siena)

 Session times will be 40 minutes. The scheduling is done according to Brisbane/Sydney/Canberra local time (AEST, UTC+10). Find your local time.

To register, please email australasianassoclogic2023@gmail.com. The Zoom URLs for the talks, as well as the abstracts, will be sent to registered participants.

We invite submission of abstracts in any area of logic, broadly construed. To submit, send an anonymized short abstract (at most 2 pages) and title to australasianassoclogic2023@gmail.com with the subject “AAL 2023”.  Please use the template of the ASL (https://aslonline.org/rules-for-abstracts/) in your submission as abstracts by ASL members will be published in the Bulletin of Symbolic Logic. The soft deadline for submissions is  1 September. Submissions will be accepted for consideration until the hard deadline of Saturday, 10 September. Decisions will be sent out in late September. We would like to encourage submissions from members of groups that are underrepresented in logic.

Please email australasianassoclogic2023@gmail.com if you have any questions.

Organising committee: Guillermo Badia (Queensland), Nick J.J. Smith (Sydney),   Shawn Standefer (NTU), Koji Tanaka (ANU), Zach Weber (Otago).

The book of abstracts for the conference  will be available at a suitable date.



Logics with Infinitary Rules: A Tutorial

Petr Cintula, Czech Academy of Sciences, Czech Republic


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. 

An Introduction to Proof Complexity

 Raheleh Jalali, Czech Academy of Sciences, Czech Republic


“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].

[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.

Asymptotic truth-value laws in many-valued logics

 Carles Noguera, University of Siena, Italy


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.

Contributed talks and full schedule (TBA)

The venue

The physical location of the event will be

03-309 - Steele Building, Learning Theatre.

You can get to the venue by public transport with, e.g. bus 66. You will need to purchase a go card in order to use public transport in Queensland.