Abstract

A given 1-order formula with n variables is valid if it is deducible in logic with n + 2 variables and two new binary predicates P and Q from one simple axiom expressing that P and Q are Tarski's conjugated quasi-projections. This can be addressed as the affirmative quasi-solution to Open problem posed in [7]. This Special Axiom can be dropped in the context of arithmetical and/or set theoretical validity explored in [13]. On the other hand, the proof also allows us to deduce negative solution to the original formalization of Henkin's problem in question from a footnote in [13]. The quasi-solution in question provides us with useful refinements in computer theorem-proving via Herbrand-style formula-rewriting systems