Axiomatization via translation: Hiz's warning for predicate logic

TL;DR

This paper discusses the challenges and pitfalls in translating axiomatizations of predicate logic, highlighting how overlooking translation issues can lead to incorrect claims of completeness in logical systems.

Contribution

It demonstrates that translating axiomatizations between different primitive operators can cause incompleteness, providing specific examples and clarifying common misconceptions.

Findings

Translation issues can lead to incomplete axiomatizations.

Certain schemas are not provable after translation, causing incompleteness.

Misinterpretation of primitive operators affects logical completeness.

Abstract

The problems of logical translation of axiomatizations and the choice of primitive operators have surfaced several times over the years. An early issue was raised by H. Hi{\. z} in the 1950s on the incompleteness of translated calculi. Further pertinent work, some of it touched on here, was done in the 1970s by W. Frank and S. Shapiro, as well as by others in subsequent decades. As we shall see, overlooking such possibilities has led to incorrect claims of completeness being made (e.g. by J. L. Bell and A. B. Slomson as well as J. N. Crossley) for axiomatizations of classical predicate logic obtained by translation from axiomatizations suited to differently chosen logical primitives. In this note we begin by discussing some problematic aspects of an early article by W. Frank on the difficulties of obtaining completeness theorems for translated calculi. Shapiro had established the incompleteness of Crossley's axiomatization by exhibiting a propositional tautology that was not provable. In contrast, to deal with Bell and Slomson's system which is complete for propositional tautologies, we go on to show that taking a formal system for classical predicate calculus with the primitive $ \exists$, setting $\forall x \phi(x) \stackrel{\text{def}}{=}\neg \exists x \neg \phi(x)$, and writing down a set of axioms and rules complete for the calculus with $\forall $ instead of $ \exists$ as primitive, does not guarantee completeness of the resulting system. In particular, instances of the valid schema $\exists x \phi (x) \rightarrow \exists x \neg \neg\phi (x)$ are not provable, which is analogous to what occurs in modal logic with $\Box$ and $\Diamond$.