Um sistema infinitário para a lógica de menor ponto fixo

Abstract

The notion of the least fixed-point of an operator is widely applied in computer science as, for instance, in the context of query languages for relational databases. Some extensions of FOL with _xed-point operators on finite structures, as the least fixed-point logic (LFP), were proposed to deal with problem problems related to the expressivity of FOL. LFP captures the complexity class PTIME over the class of _nite ordered structures. The descriptive characterization of computational classes is a central issue within _nite model theory (FMT). Trakhtenbrot's theorem, considered the starting point of FMT, states that validity over finite models is not recursively enumerable, that is, completeness fails over finite models. This result is based on an underlying assumption that any deductive system is of finite nature. However, we can relax such assumption as done in the scope of proof theory for arithmetic. Proof theory has roots in the Hilbert's programme. Proof theoretical consequences are, for instance, related to normalization theorems, consistency, decidability, and complexity results. The proof theory for arithmetic is also motivated by Godel incompleteness theorems. It aims to o_er an example of a true mathematically meaningful principle not derivable in first-order arithmetic. One way of presenting this proof is based on a definition of a proof system with an infinitary rule, the w-rule, that establishes the consistency of first-order arithmetic through a proof-theoretical perspective. Motivated by this proof, here we will propose an in_nitary proof system for LFP that will allow us to investigate proof theoretical properties. With such in_nitary deductive system, we aim to present a proof theory for a logic traditionally defined within the scope of FMT. It opens up an alternative way of proving results already obtained within FMT and also new results through a proof theoretical perspective. Moreover, we will propose a normalization procedure with some restrictions on the rules, such this deductive system can be used in a theorem prover to compute queries on relational databases.