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
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.
References
-
[1] Compton KJ. A Deductive System for Existential Least Fixpoint Logic. Journal of Logic and Computation (1993) 3(2):197–213.
[2] Ebbinghaus HD, Flum J. Finite Model Theory (1995) New York: Springer.
[3] Ebbinghaus HD, Flum J, Thomas W. Mathematical Logic (1994) 2nd Edition. Springer, New York: Undergraduate Texts in Mathematics.
[4] Fagin R. Generalized First-order Spectra and Polynomial-time Recognizable Sets. In: Complexity of Computation—Karp R, ed. (1974) 7. SIAM-MAS Proceedings. 43–73.
[5] Fraïssé R. Sur Quelques Classifications des Systèmes de Relations. Université d'Alger, Publications Scientifiques, Série A (1954) 1:35–182.
[6] Gentzen G. Die Widerspruchsfreiheit der reinen Zahlentheorie, Mathematische Annalen, 112, 493–565. In: The Collected Papers of Gerhard Gentzen—Szabo ME, ed. (1969) Amsterdam: North-Holland. 132–170.
[7] Gentzen G. Beweisbarkeit und Unbeweisbarkeit von Anfangsfällen der Transfiniten Induktion in der reinen Zahlentheorie, Mathematische Annalen, 119, 140–161. In: The Collected Papers of Gerhard Gentzen—Szabo ME, ed. (1969) Amsterdam: North-Holland. 287–311.
[8] Girard J-Y, Lafont Y, Taylor P. Proofs and Types (1989) Cambridge: Cambridge.
[9] Henkin L. The Completeness of the First-Order Functional Calculus. Journal of Symbolic Logic (1949) 14.
[10] Immerman N. Descriptive Complexity (1999) New York: Springer.
[11] Immerman N. Upper and Lower Bounds for First Order Expressibility. Journal of Computer and System Sciences (1982) 25:76–98.[CrossRef][Web of Science]
[12] Immerman N. Relational Queries Computable in Polynomial Time (extended abstract). In: ACM Symposium on Theory of Computation (1982) ACM Press. 147–152.
[13] Kleene S. On notations for ordinal numbers. Journal of Symbolic Logic (1938) 3(4):150–5.[CrossRef]
[14] Knaster B. Un Théorème sur les Fonctions d'Ensembles. Annales Soc. Polonaise (1928) 6:133–134.
[15] Libkin L. Elements of Finite Model Theory (2004) Berlin: Springer.
[16] Mendelson E. Introduction to Mathematical Logic (1964) Princeton: D. Van Nostrand Company, INC.
[17] Pereira LC, Massi CDB. Normalização para a Lógica Clássica (1990) 2. O que nos faz pensar, Cadernos de Filosofia da PUC-RJ. 49–53.
[18] Prawitz D. Natural Deduction: A Proof-Theoretical Study. In: Stockholm Studies in Philosophy 3 (1965) Stockholm: Almqvist and Wiksell. Acta Universitatis Stockholmiensis.
[19] Schütte K. Beweistheoretische Erfassung der Unendliche Induktion in der Zahlentheorie. Mathemastiche Annalen (1951) 122:369–389.
[20] Schmidt DA. Denotational Semantics: a Methodology for Language Development (1986) Boston: Allyn and Bacon, INC.
[21] Scott D. Domains for Denotational Semantics (1982) Berlin: Springer. 577–613. LNCS 140: Proc. 9th ICALP.
[22] Tarski A. A Lattice-Theoretical Fixpoint Theorem and its Applications. Pacific J. Math. (1955) 55:285–309.
[23] Trahtenbrot BA. The Impossibility of an Algorithm for the Decision Problem for Finite Models. Doklady Academii Nauk SSSR (1950) 70:569–572.
[24] Troelstra AS, Schwichtenberg H. Proof Theory (1996) Cambridge: Cambridge University Press.
[25] Van Dalen D. Logic and Structure (1989) 2nd Edition. Berlin: Springer Verlag.
[26] Vardi MY. The complexity of relational query languages. In Proc. ACM Symp. on Theory of Computing (1982) 137–146.
CiteULike 
Connotea 
Del.icio.us What's this?
| ||||||||||||||||||||||||||||||||||||||||||||||||