A formalization of logic in diagonal-free cylindric algebras
Is Version Of
We exhibit a quasi-projectional relation algebra reduct of any diagonal-free cylindric algebra of dimension 3 having sufficiently strong projection and equality parameters. We also offer a complete proof that full first-order logic can be formalized in the calculus of binary relations (a result due to Maddux and Tarski). Finally, we use these constructions to recursively define a translation function from the sentences of first-order logic to the equational theory of diagonal-free cylindric algebras of dimension 3 which preserves validity.