Constructive proofs for the standard translation of many-sorted to unsorted predicate logic
Pith reviewed 2026-05-21 10:06 UTC · model grok-4.3
The pith
An effective procedure shows the standard translation from many-sorted logic to unsorted logic remains correct when equality is present.
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
Core claim
We give an elementary proof in the form of an effective procedure that shows the correctness of the standard translation of many-sorted logic to unsorted logic, including when equality is present. As an application, this provides a fully syntactic justification of van Dalen's translation of second-order logic into unsorted first-order logic. We also give a new proof for Herbrand's claim that, without equality, a sentence is derivable in many-sorted logic if and only if it is derivable in unsorted logic.
What carries the argument
The standard translation, which adds a predicate for each sort, relativizes quantifiers to these predicates, and includes axioms governing the predicates' behavior.
Load-bearing premise
That the effective procedure correctly maps any derivation in the many-sorted system to a valid derivation in the unsorted system under the given translation definitions.
What would settle it
A specific many-sorted sentence or derivation with equality such that the procedure either fails to produce a valid unsorted derivation or the translated sentence is provable in one system but not the other.
read the original abstract
It is well known that many-sorted logic can be reduced to unsorted first-order logic by adding predicates for each sort, relativizing quantifiers to these predicates, and adding appropriate axioms governing their behavior. Existing constructive proofs for the correctness of this translation break down when the many-sorted language includes equality and the unsorted target calculus includes the usual rules/axioms for equality. We give an elementary proof in the form of an effective procedure that closes this gap. As an application, we give a fully syntactic justification of van Dalen's translation of second-order logic into unsorted first-order logic. We also give a new proof for a claim made by Herbrand in his 1930 dissertation that, in the equality-free case, a sentence is derivable in many-sorted logic iff it is derivable in unsorted logic. Our proof avoids the heavy machinery of later proofs by Schmidt and Wang.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper claims to close a known gap in constructive proofs for the standard translation from many-sorted predicate logic (with equality) to unsorted first-order logic by supplying an elementary effective syntactic procedure that maps derivations while preserving validity under the relativizing translation with sort predicates and axioms. It applies the procedure to give a fully syntactic justification of van Dalen's translation of second-order logic into unsorted first-order logic and supplies a new elementary proof of Herbrand's 1930 claim that, in the equality-free case, derivability in many-sorted logic is equivalent to derivability in unsorted logic, avoiding the later machinery of Schmidt and Wang.
Significance. If the effective procedure is correctly defined and shown to handle equality rules without semantic detours, the result strengthens the syntactic foundations for standard reductions between many-sorted and unsorted logics. The elementary character of the proof and its application to second-order logic constitute a genuine advance over existing non-constructive or heavy-machinery arguments; the new proof of Herbrand's claim is particularly valuable for its directness and avoidance of later technical overhead.
major comments (1)
- [Description of the effective procedure (around the main theorem)] The central claim rests on the effective procedure correctly transforming derivations that involve equality axioms and sort-relativized quantifiers. The manuscript presents this as a direct step-by-step mapping, but without an explicit verification on a small concrete derivation (e.g., a simple equality axiom instance together with a relativized quantifier), it remains unclear whether the interaction between the unsorted equality rules and the added sort predicates is fully covered in all cases.
minor comments (2)
- [Introduction] The abstract and introduction would benefit from a brief, self-contained statement of the precise form of the standard translation (sort predicates, relativization, and the added axioms) before describing the procedure.
- [Preliminaries] Notation for the many-sorted and unsorted languages could be made more uniform across sections to ease comparison of the source and target derivations.
Simulated Author's Rebuttal
We thank the referee for the careful reading of the manuscript and for the positive recommendation of minor revision. The suggestion to include a concrete example is helpful for clarifying the interaction between equality rules and the relativizing translation. We address the point below.
read point-by-point responses
-
Referee: The central claim rests on the effective procedure correctly transforming derivations that involve equality axioms and sort-relativized quantifiers. The manuscript presents this as a direct step-by-step mapping, but without an explicit verification on a small concrete derivation (e.g., a simple equality axiom instance together with a relativized quantifier), it remains unclear whether the interaction between the unsorted equality rules and the added sort predicates is fully covered in all cases.
Authors: We agree that an explicit small-scale example would make the coverage of equality axioms and sort predicates more transparent. In the revised version we will insert a short, fully worked derivation that begins with a many-sorted equality axiom instance, applies a relativized universal quantifier, and shows the step-by-step image under the effective procedure in the unsorted calculus. This addition will be placed immediately after the statement of the main theorem and will not alter the existing proof. revision: yes
Circularity Check
No significant circularity; constructive procedure is self-contained
full rationale
The paper supplies an explicit effective syntactic procedure that maps many-sorted derivations (including equality) to unsorted derivations while preserving the standard relativizing translation. This mapping is presented as a direct, step-by-step translation of proof rules that handles sort predicates and equality axioms without invoking semantic completeness or external fitted parameters. The new proof for Herbrand’s equality-free claim is likewise given directly and is stated to avoid the machinery of Schmidt and Wang. No equation or definition reduces to its own output by construction, no load-bearing premise rests on a self-citation chain, and the central claim remains independent of the inputs it translates. The derivation is therefore self-contained against external benchmarks.
Axiom & Free-Parameter Ledger
axioms (2)
- standard math Usual rules and axioms for equality in the unsorted first-order target calculus.
- domain assumption Definition of the standard translation via sort predicates, relativization of quantifiers, and governing axioms for the predicates.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.