A decision method for a set of first order classical formulas and its applications to decision problems for non-classical propositional logics (Q911574)

The set of R-formulas is defined inductively as an extension of the set of all first order predicate formulas generated by a finite set P of unary predicate symbols (as the only set of non-logical constant symbols) over the usual classical propositional connectives and quantifiers, by the following formation rule: if A(x) is an R-formula and x is a free variable not occurring in A(y), then \(\forall y(R(x,y)\to A(y))\), \(\forall y(R(y,x)\to A(y))\), \(\exists y(r(x,y)\wedge A(y))\) and \(\exists y(R(y,x)\wedge A(y))\) are all R-formulas, where R is a new fixed binary predicate symbol. R-positive formulas are the formulas over \(P\cup R\) in which R has no negative occurrences. If we denote by F the set of all finite conjunctions of R-sentences, R-positive sentences and the sentences expressing symmetry and transitivity of R, then we can formulate the main result of the paper: the set F is decidable. This statement can be used, as demonstrated in the paper, to solve the decidability problem of some non-classical propositional and modal logics.