Normalization Procedures for the Strongest Syllogistic Natural Deduction Systems

Abstract

This paper deals with the natural deduction systems R^∗†, R^∗†_trans, and RCA^†(opp) for the relational syllogistics R^∗†, R^∗†_trans, and
RCA^†(opp), respectively, studied by L.S. Moss and his coauthors. Characteristic features of R^∗†—the weakest of these syllogistics—are two-place relations only expressed with transitive verbs or comparative adjectives, such as ‘like’ or ‘happier than’, which, together with quantifiers, could form a nested relative clause—set terms—such as ‘a thing that likes some women, who is happier than all men’. R^∗†_trans extends R^∗† with the transitivity property of the comparative adjectives,
and RCA^†(opp)—the strongest of these syllogistics—extends R^∗†_trans with the Boolean conjunction applied inside the set terms, such as ‘a thing that likes and sees some women’, and converse relations, such as ‘is liked by’. Each of the syllogistics allows set term negation, such as ‘non-woman’, ‘dislike’, or ‘unhappier than’, and this negation enjoys the bar notation consisting of the (standard) equivalences that hold true on the level of the set terms. Being propositional connective-free,
the syllogistic languages employ atomic sentences only, which are composed of the set terms and constants, such as ‘Angelina likes some women who do not know any puppy’, with the bar notation holding true for them as well. Another specific of RCA^†(opp) is that its formulation demands extending its language with individual variables to compose general sentences, such as ‘x likes some women’.

The main result of this paper is the normalization theorems for the systems under consideration: each derivation in any of them is converted to a normal one via detour, permutation, and simplification conversions, where the normal derivation is efficient in the sense that it does not contain detours, hidden detours, or vacuous applications of rules canceling assumptions, respectively. The important corollary of these theorems is that each system has a syllogistic analog of the subformula property in the case of propositional logics—the so-called sub-set-term-property, i.e., in a normal derivation of ϕ from Γ, each set term is a subterm of d, where d is a term in ϕ and/or Γ, and each constant is a constant in ϕ and/or Γ. An overview of future plans, a conclusion, and a reference to some previous work are at the end of this paper.