This article appears in the following Logic Journal of the IGPL issue: Special Issue: Logical and Semantical Frameworks with Applications [View the issue table of contents]
Natural deduction for the finite least fixed point logic with an infinitary rule
Departamento de Computação, Universidade Federal do Ceará, C.P. 12.166, Fortaleza-CE, Brasil, 60455-970.
E-mail: aldufc{at}gmail.com
Departamento de Computação, Universidade Federal do Ceará, C.P. 12.166, Fortaleza-CE, Brasil, 60455-970.
E-mail: ana{at}lia.ufc.br
 |
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 first-order classical logic (FOL) with fixed point operators, as the least fixed point logic (LFP), were proposed to deal with problems related to the expressivity of FOL. LFP captures the complexity class PTIME over the class of finite ordered structures. The descriptive characterization of computational classes is a central issue within finite model theory (FMT). Trahtenbrot's theorem 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. Motivated by Gödel incompleteness theorems, proof theory for arithmetic offer an example of a true mathematically meaningful principle non-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 
-rule, that establishes the consistency of first-order arithmetic through a proof-theoretical perspective. Inspired in this rule, here we will propose an infinitary natural deduction system, and a sequent calculus version, for FOL and LFP restricted to finite models, FOLfin and LFPfin, respectively, we will prove soundness and completeness for them and also normal form theorems for them. With this infinitary deductive system for LFPfin, we aim to present a proof theory for a logic traditionally investigated within the scope of FMT. It opens up an alternative way of proving results already obtained within FMT and also new ones through a proof-theoretical perspective.
Key Words: Least Fixed Point Logic • Finite Model Theory • Proof Theory • Infinitary Natural Deduction System • Infinitary Sequent Calculus
Received for publication 6 May 2008.
1This research is partially supported by FUNCAP.
2This research is partially supported by PROCAD/CAPES, PQ/CNPq, Universal 2008/CNPq, ‘‘Casadinho’’ 2008/CNPq.