[For the entire collection see Zbl 0547.00036.]
First-order logic (FO) possesses an important property: every first-order global predicate is PTIME computable. This means that for every first- order sentence \(\phi\) there is an algorithm that, given a presentation of a structure S of the vocabulary of \(\phi\), computes the truth-value of \(\phi\) on S within time bounded by a polynomial in the cardinality of S. However, the inverse does not hold. Therefore, there arises the problem of extending first-order logic by adding different operators in such a way that exactly PTIME computable predicates are expressible in the extended logic. This problem was considered also by other authors. In the paper formation rules are presented for a least fixed point operator (LFP) and an iterative fixed point operator (IFP), and it is shown that a global prepredicate is PTIME computable iff it is expressible in \(FO+LFP\) with order, or iff it is expressible in \(FO+IFP\) with order. These two last logics will be called the polynomial time logics (PTL).
Of course, the considered problem concerns the logic with finite structures. And therefore, the paper gives also an overview on first- order logic with finite structures. First, ”the failure” of first-order logic in the case of finite structures is presented by showing that famous theorems for first-order logic (soundness and completeness theorem, compactness theorem, Craig interpolation theorem, Beth definability theorem, weak definability theorem, and substructure preservation theorem) do not hold in the case of finite structures. Then, it is shown that, in some sense, the theorems of interpolation, of definability, and of substructure preservation are not effective.
Another problem arises: Do the analogues of the above mentioned famous theorems hold in the case of polynomial time logic? It is shown that this problem, for the interpolation theorem and definability theorem, is equivalent to such problems as \(NP\cap co\)-NP\(=P?\) or \(UNAMBIGIOUS=P?\).