Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Constructive proofs for the standard translation of many-sorted to unsorted predicate logic

Hrafn Valtýr Oddsson

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 two constructive proofs. The first repairs a known gap in Herbrand's original proof for the equality-free case from his 1930 dissertation. This results in a proof that is conceptually simpler than the later proofs by Schmidt and Wang. The second proof establishes the same result, but also applies to languages with equality and can handle relation and function symbols that allow more than one combination of sorts in their argument places. Both proofs work for both classical and intuitionistic logic. As an application, we use the second proof to give a fully syntactic justification of van Dalen's translation of second-order logic into unsorted first-order logic.

Constructive proofs for the standard translation of many-sorted to unsorted predicate logic

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 two constructive proofs. The first repairs a known gap in Herbrand's original proof for the equality-free case from his 1930 dissertation. This results in a proof that is conceptually simpler than the later proofs by Schmidt and Wang. The second proof establishes the same result, but also applies to languages with equality and can handle relation and function symbols that allow more than one combination of sorts in their argument places. Both proofs work for both classical and intuitionistic logic. As an application, we use the second proof to give a fully syntactic justification of van Dalen's translation of second-order logic into unsorted first-order logic.
Paper Structure (13 sections, 16 theorems, 62 equations, 3 tables)

This paper contains 13 sections, 16 theorems, 62 equations, 3 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. $\mathrm{FOL}$
  4. $\mathrm{MSL}$
  5. Signature extensions
  6. Liberal equality
  7. The standard translation from $\mathrm{MSL}$ to $\mathrm{FOL}$
  8. Repairing Herbrand's proof
  9. The general case
  10. Optional sort axioms
  11. Second-order logic
  12. The forward direction
  13. Proof of Proposition \ref{['LibeqExt']}

Key Result

Proposition 6

Theorems & Definitions (54)

  • Definition 1
  • Remark
  • Remark
  • Definition 2
  • Definition 3
  • Definition 4
  • Definition 5
  • Proposition 6
  • Definition 7
  • Proposition 8
  • ...and 44 more