Till innehåll på sidan

Valentin Goranko: On the theories of almost sure validities in the finite in some fragments of monadic second-order logic

Tid: On 2014-10-22 kl 10.00 - 12.00

Plats: Room 16, building 5, Kräftriket, Department of mathematics, Stockholm university

Exportera till kalender

This work stems from the well-known 0-1 law for the asymptotic probabilities of first-order definable properties of finite graphs (in general, relational structures). Fagin's proof of this result is based on a transfer between almost sure properties in finite graphs and true properties of the countable random graph (aka, Rado graph). Both the transfer theorem and the 0-1 law hold in some non-trivial extensions of first-order logic (e.g., with fixed point operators) but fail in others, notably in most natural fragments of monadic second-order (MSO).

The main problem of this study is to characterise, axiomatically or model-theoretically, the set of almost surely valid in the finite formulae of MSO, i.e. those with asymptotic probability 1. The set of almost sure validities in the finite of any given logical language (where truth on finite structures is well-defined) is a well-defined logical theory, containing all logical validities of that language and closed under all sound finitary rules of inference. Beyond that, little is known about these theories in cases where the transfer theorem fails.

The talk will begin with a brief introduction to asymptotic probabilities and almost surely true properties of finite graphs, the 0-1 laws for first-order logic and in some extensions of it, and their relationship with the respective logical theories of infinite random graphs. Then I will focus on the almost sure theories in modal logic and in the \(\Sigma_1^1\) and \(\Pi_1^1\) fragments of MSO on binary relational structures, aiming at obtaining explicit logical characterisations of these theories. I will present such partial characterisations in terms of characteristic formulae stating almost sure existence (\(\Sigma_1^1\) ) or non-existence (for \(\Pi_1^1\)) of bounded morphisms to special target finite graphs. Identifying explicitly the set of target finite graphs that generate almost surely valid characteristic formulae seems a quite challenging problem, to which we so far only provide some partial answers and conjectures.