Taming the Infinity Quantifier: On Well-Behaved Fragments of First-Order Logic with the Quantifier 'There are Infinitely Many'
Thibault Rushbrooke
Abstract:
This thesis investigates a range of fragments of FOL∞, that is, first-order logic extended with a quantifier expressing ‘there are infinitely many...’ We extend several results of Bellas Acosta [1], concerning the logic ML∞ . The logic ML∞ extends the basic modal language with an infinite modality, asserting that there are infinitely many successors satisfying a certain property. We introduce logics which extend ML∞ with a backwards modality and a backwards infinite modality, with a global modality, and with both backwards modalities and the global modality. We show that each of these logics may be characterised, as fragments of FOL∞, by invariance under a suitable notion of bisimulation. On the way to obtaining these results, we prove an FOL∞ analogue of Gaifman’s theorem for first-order logic [9]. In a second line of research, we establish that the set of validities of the logic with forwards and backwards infinite modalities is decidable, and admits a finite axiomatisation. We also introduce a guarded fragment of FOL∞, and conjecture that, restricted to a certain vocabulary, this logic is also decidable.