The Intermediate Logic of Convex Polyhedra

TL;DR

This paper presents a finite axiomatisation of the intermediate logic of convex polyhedra, linking geometric properties of polytopes with logical formulas, and establishing completeness via geometric realisations.

Contribution

It introduces a novel finite axiomatisation of the logic of convex polyhedra and connects geometric constraints with logical semantics using polyhedral geometry.

Findings

Finite axiomatisation of the logic of convex polyhedra (PL).

Geometric realisation of frames into convex polyhedra.

Completeness established via sawed tree structures.

Abstract

We investigate a recent semantics for intermediate (and modal) logics in terms of polyhedra. The main result is a finite axiomatisation of the intermediate logic of the class of all polytopes -- i.e., compact convex polyhedra -- denoted PL. This logic is defined in terms of the Jankov-Fine formulas of two simple frames. Soundness of this axiomatisation requires extracting the geometric constraints imposed on polyhedra by the two formulas, and then using substantial classical results from polyhedral geometry to show that convex polyhedra satisfy those constraints. To establish completeness of the axiomatisation, we first define the notion of the geometric realisation of a frame into a polyhedron. We then show that any PL frame is a p-morphic image of one which has a special form: it is a 'sawed tree'. Any sawed tree has a geometric realisation into a convex polyhedron, which completes the proof.