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

Classical first-order logic (03B10) Decidability of theories and sets of sentences (03B25) Modal logic (including the logic of norms) (03B45) Intermediate logics (03B55)

Review text

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.

Recommendations

Cited in

(6)

This page was built for publication: A decision method for a set of first order classical formulas and its applications to decision problems for non-classical propositional logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q911574)