Points, Lines and Diamonds: a Two-Sorted Modal Logic for Projective Planes
Yde Venema

Abstract:
We introduce a modal language for talking about projective planes. This 
language is two­sorted, containing formulas to be evaluated at points and 
at lines, respectively. The language has two diamonds whose intended 
accessibility relations are the two directions of the incidence relation 
between points and lines.
We provide a sound and complete axiomatization for the formulas that are 
valid in the class of projective planes. We also show that it is decidable 
whether a given formula is satisfiable in a projective plane, and we 
characterize the computational complexity of this satisfaction problem.