Portal de Periódicos da CAPES

A decision procedure for a class of formulas of first order predicate calculus

1964; Mathematical Sciences Publishers; Volume: 14; Issue: 4 Linguagem: Inglês

10.2140/pjm.1964.14.1305

1945-5844

M. R. Krom,

Advanced Algebra and Logic

Introduction* In [4] (cf. also case V page 256 of [1]) J. Herbrand provides a decision procedure which is equivalent to a decision procedure for determining for a fixed contradiction C and for any first order prenex formula Γ whose matrix is a conjunction of signed atomic formulas, whether Γ->C is valid.In this paper we define a class a of first order formulas and then provide a decision procedure for determining for any first order prenex formula Γ whose matrix is a conjunction of signed atomic formulas and and member Δ of the class, whether Γ -> Δ is valid.Although the class of formulas Δ that we consider is rather large, it is clear that some restriction is necessary since a decision procedure for the class itself is obtained by using for Γ a single propositional parameter that does not occur in Δ.The formulas we consider are those of any system of pure first order predicate calculus without equality and without function symbols.We use V, Λ, Ί, and -> for the propositional connectives disjunction, conjunction, denial, and the conditional, respectively.The symbols Γ, Δ, Γ o , Δ o , Γ u Δ lf shall range over arbitrary formulas, P, Q, P 19 Q lf over prefixes, and M, N, M lf N lf over matrices.A propositional parameter or predicate parameter together with its attached individual variables or individual parameters will be called an atomic formula.An occurrence of an atomic formula in a formula Γ is called an atomic part of Γ.Two prenex formulas are similar if their matrices differ only in the symbols occupying individual variable places of the atomic formulas.Two prenex formulas are congruent if they differ only by equivalent replacements of bound variables.We indicate that Δ is a logical consequence of Γ by writing Γ\=4.If Γ\=A then there exists a symmetric L-deduction of Δ from Γ as described in [2].For any formulas Γ and Δ an L-deduction of A from Γ is an ordered (n + 1)tuple <(Γ 0 , , Γ n y where Γ Q = Γ and Γ n = Δ, together with a specification of how, for any m < n, Γ m+1 results from Γ m by an application of an L-rule.The reader is referred to pages 252 and 253 of [2] for the definitions of the eleven L-rules.An L-deduction is symmetric if and only if the order in which the different kinds of L-rules are applied satisfies conditions (iii) through (vi) on page 257 of [2] In addition, for convenience, we require that a symmetric L-deduction have exactly one application of the operation matrix change.