Finite axiomatizability in Łukasiewicz logic (Q716501)

Using the deep relationship between Łukasiewicz logic, MV-algebras, and piecewise linear geometry, the main result the paper proves is a classification of (equivalent classes of) finitely axiomatisable theories in Łukasiewicz propositional logic by means of weighted abstract simplicial complexes. Recall that an abstract simplicial complex is a pair \((V,\Sigma)\) where \(V\) is a finite nonempty set and \(\Sigma\) is a set of subsets of \(V\) whose union is \(V\) and such that every subset of an element of \(\Sigma\) is again in \(\Sigma\). A \textit{weighted abstract simplical complex} \((V,\Sigma,\omega)\) is an abstract simplicial complex \((V,\Sigma)\) together with a function \(\omega\) mapping \(V\) to the positive integers. The main steps of the proofs are: 1) The fact that the Lindenbaum algebra of every (theory consisting of a) \(1\)-satisfiable formula \(\theta\) in \(n\) propositional variables is the algebra of \(n\)-variate McNaughton functions restricted to \(\mathrm{Mod}(\theta) = \{v \in [0,1]^n \mid v(\theta) = 1\}\), where truth-assignments have been identified with points in the unit hypercube. 2) The fact that for each nonempty subset \(X \subseteq [0,1]^n\), \(X\) is a rational polyhedron (i.e., a finite union of compact convex polyhedra with rational vertices) iff \(X = \mathrm{Mod}(\psi)\) for some formula \(\psi\). 3) The lemma that proves that a theory \(\Theta\) is finitely axiomatisable iff \(\Theta = \mathrm{Th}(P) = \{\psi \mid v(\psi) = 1, \forall v \in P\}\), for \(P\) some rational polyhedron. 4) The theorem that proves that the map \(P \mapsto \mathrm{Th}(P)\) determines a bijective correspondence between \(\mathbb{Z}\)-homeomorphism classes of rational polyhedra in some \(n\)-cube, and equivalence classes of finitely axiomatisable theories (where two polyhedra \(P\), \(Q\) are said to be \(\mathbb{Z}\)-homeomorphic if there is a piecewise linear homeomoprhism \(\eta : P \to Q\) that is onto and such that each linear piece of both \(\eta\) and its inverse has integer coefficients). 5) The theorem proving that two weighted abstract simplicial complexes \(K\), \(K'\) are equivalent iff \(\mathrm{Th}(|\Delta_K|)\) is equivalent to \(\mathrm{Th}(|\Delta_{K'}|)\) (where \(|\Delta_K|\) is the geometric realisation, as a rational polyhedron in \([0,1]^n\), of \(K\), and where two weighted abstract complexes are equivalent if they can be connected by a finite sequence of simple stellar subdivisions and their inverses). 6) The proposition proving that for every finitely axiomatisable theory \(\Theta\) there is a weighted abstract simplicial complex \(H\) such that \(\Theta\) is equivalent to \(\mathrm{Th}(|\Delta_H|)\). The main theorem is then proved in the following form: The map \(K \mapsto \mathrm{Th}(|\Delta_K|)\) determines a bijective correspondence between equivalence classes of weighted abstract simplicial complexes and equivalence classes of finitely axiomatisable theories in Łukasiewicz propositional logic. The author then proves that the equivalence problem for weighted abstract simplicial complexes is decidable iff so is the equivalence problem for finitely axiomatisable theories. It must be stressed that the decidability status of these problems is still open, while Markov's result cited in the bibliography implies that the equivalence problem for abstract simplicial complexes is undecidable. The paper is completed with a brief survey of recent related results, showing that the field has been attracting increasing attention in the last few years.