Skip Navigation


Journal of Logic and Computation Advance Access originally published online on November 22, 2007
Journal of Logic and Computation 2008 18(4):521-562; doi:10.1093/logcom/exm064
This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Similar articles in ISI Web of Science
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Gabbay, M. J.
Right arrow Articles by Mathijssen, A.
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

© The Author, 2007. Published by Oxford University Press. All rights reserved. For Permissions, please email: journals.permissions@oxfordjournals.org

Original Articles

One-and-a-halfth-order Logic

Murdoch J. Gabbay

Department of Computer Science, Heriot-Watt University, Riccarton, Edinburgh EH14 4AS, UK. E-mail: murdoch.gabbay{at}gmail.com

Aad Mathijssen

Department of Mathematics and Computer Science, Technische Universiteit Eindhoven, P.O. Box 513, 5600 MB Eindhoven, The Netherlands.

E-mail: aad.mathijssen{at}gmail.com

The practice of first-order logic is replete with meta-level concepts. Most notably there are meta-variables ranging over formulae, variables, and terms, and properties of syntax such as alpha-equivalence, capture-avoiding substitution and assumptions about freshness of variables with respect to meta-variables. We present one-and-a-halfth-order logic, in which these concepts are made explicit. We exhibit both sequent and algebraic specifications of one-and-a-halfth-order logic derivability, show them equivalent, show that the derivations satisfy cut-elimination, and prove correctness of an interpretation of first-order logic within it. We discuss the technicalities in a wider context as a case-study for nominal algebra, as a logic in its own right, as an algebraisation of logic, as an example of how other systems might be treated, and also as a theoretical foundation for future implementation.

Keywords: first-order logic; nominal techniques; substitution; {alpha}-conversion; meta-variables



References

  1. Andréka H, Németi, Sain I. Algebraic logic. In: Handbook of Philosophical Logic—Gabbay D, Guenthner F, eds. (2001) vol. 2, 2nd Edition. Dordrecht: Kluwer Academic. 133–249.
  2. Barwise J. Perspectives in Mathematical Logic. In: Admissible Sets and Structures: An Approach to Definability Theory (1975) Berlin: Springer.
  3. Barwise J. An introduction to first-order logic. In: Handbook of Mathematical Logic—Barwise J, ed. (1977) North Holland, Amsterdam. 5–46.
  4. Beeson M. Lambda logic. In: IJCAR 2004: The 2nd International Joint Conference on Automated Reasoning. Vol. 3097 of LNCS (2004) Berlin: Springer. 460–474.
  5. Bell J, Machover M. A Course in Mathematical Logic (1977) North-Holland, Amsterdam.
  6. Brunner N. 75 years of independence proofs by Fraenkel-Mostowski permutation models. In: Mathematica Japonica (1996) 43:177–199.
  7. Burris S, Sankappanavar H. A Course in Universal Algebra (1981) Berlin: Springer.
  8. Courcelle B. The expression of graph properties in some fragments of monadic second-order logic. In: Handbook of Graph Grammars and Computing by Graph Transformations—Rozenberg G, ed. (1997) vol. 1. London: World Scientific. 313–400.
  9. Degtyarev A, Voronkov A. Equality reasoning in sequent-based calculi. In: Handbook of Automated Reasoning—Robinson JA, Voronkov A, eds. (2001) Cambridge, USA: Elsevier, Amsterdam, MIT Press. 611–706.
  10. Dowek G, Hardin T, Kirchner C. Binding logic: Proofs and models. In: LPAR'02: 9th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, Vol. 2514 of LNCS (2002) Berlin: Springer. 130–144.
  11. Dunn M, Restall G. Relevance logic. In: Handbook of Philosophical Logic—Gabbay D, Guenthner F, eds. (2002) vol. 6, 2nd Edition. Dordrecht: Kluwer Academic. 1–128.
  12. Farmer WM. The seven virtues of simple type theory. Technical Report 18, McMaster University, SQRL, 2003 (revised 2006).
  13. Fernández M, Gabbay MJ. Nominal rewriting. In: Information and Computation (2007) 205:917–965.[CrossRef][ISI]
  14. Gabbay D, Malod G. Naming worlds in modal and temporal logic. In: Journal of Logic, Language and Information (2002) 11:29–65.[CrossRef]
  15. Gabbay MJ. A Theory of Inductive Definitions with alpha-Equivalence. In: PhD thesis (2000) Cambridge, UK.
  16. Gabbay MJ. Hierarchical nominal terms and their theory of rewriting. In: ENTCS (2007) 174:37–52.
  17. Gabbay MJ, Lengrand S. The lambda-context calculus. In: LFMTP'07: International Workshop on Logical Frameworks and Meta-Languages. to be published in ENTCS.
  18. Gabbay MJ, Mathijssen A. Capture-avoiding substitution as a nominal algebra. In: Theoretical Aspects of Computing ICTAC 2006. Vol. 4281 of LNCS. Berlin: Springer. 198–212.
  19. Gabbay MJ, Mathijssen A. Nominal algebra. In: Technical Report HW-MACS-TR-0045, Heriot-Watt (2006).
  20. Gabbay MJ, Mathijssen A. Capture-avoiding substitution as a nominal algebra. In: Technical Report HW-MACS-TR-0053 (2007) Heriot-Watt.
  21. Gabbay MJ, Mathijssen A. A formal calculus for informal equality with binding. In: WoLLIC'07: 14th Workshop on Logic, Language, Information and Computation. Vol. 4576 of LNCS (2007) Berlin: Springer. 162–176.
  22. Gabbay MJ, Pitts AM. A new approach to abstract syntax with variable binding. In: Formal Aspects of Computing (2002) 13:341–363.[CrossRef]
  23. Gentzen G. Untersuchungen über das logische schließen [Investigations into logical deduction]. In: Mathematische Zeitschrift 39. 176–210. 405–431, 1935. Translated in [43], 68–131.
  24. Girard J-Y. Linear logic. In: Theoretical Computer Science (1987) 50:1–102.[CrossRef][ISI]
  25. Halmos P. Algebraic logic, ii. homogeneous locally finite polyadic boolean algebras of infinite degree. In: Fundamenta Mathematicae (1956) 43:255–325.
  26. Henkin L, Monk J, Tarski A. Cylindric Algebras (1971 and 1985) North Holland, Amsterdam: Parts I and II.
  27. Hodges W. Elementary predicate logic. In: Handbook of Philosophical Logic—Gabbay D, Guenthner F, eds. (2001) vol. 1, 2nd Edition. Dordrecht: Kluwer Academic. 1–131.
  28. Huet G, Kahn G, Paulin-Mohring C. The Coq proof assistant, a tutorial. http://coq.inria.fr/V8.1/tutorial.html.
  29. Johnstone P. Notes on logic and set theory (1987) Cambridge: Cambridge University Press.
  30. Leivant D. Higher order logic. In: Handbook of Logic in Artificial Intelligence and Logic Programming—Gabbay D, Hogger C, Robinson J, eds. (1994) vol. 2. Oxford: Oxford University Press. 229–322.
  31. McCune W, Veroff R, Fitelson B, Harris K, Feist A, Wos L. Short single axioms for boolean algebra. In: Journal of Automated Reasoning (2002) 29:1–16.[CrossRef][ISI]
  32. Meredith C. Single axioms for the systems (C,N), (C,O) and (A,N) of the two-valued propositional calculus. In: The Journal of Computing Systems (1953) 3:155–164.
  33. Metamath.org. Derivation of classical propositional logic from Meredith's axiom. http://us.metamath.org/mpegif/meredith.html.
  34. Miculan M. Developing (meta)theory of lambda-calculus in the theory of contexts. In: ENTCS (2001) 58:37–58.
  35. Miller D. A logic programming language with lambda-abstraction, function variables, and simple unification. In: Extensions of Logic Programming (1991) 475:253–281.[CrossRef]
  36. O'Hearn PW, Pym DJ. The logic of bunched implications. In: Bulletin of Symbolic Logic (1999) 5:215–244.[CrossRef][ISI]
  37. Paulson LC. The foundation of a generic theorem prover. In: Journal of Automated Reasoning (1989) 5:363–397.[CrossRef]
  38. Paulson LC. Isabelle: the next 700 theorem provers. In: Logic and Computer Science—Odifreddi P, ed. (1990) London: Academic Press. 361–386.
  39. Pfenning F, Elliot C. Higher-order abstract syntax. In: PLDI '88: Proceedings of the ACM SIGPLAN 1988 conference on Programming Language design and Implementation (1988) New York: ACM Press. 199–208.
  40. Pinter C. A simple algebra of first-order logic. In: Notre Dame Journal of Formal Logic (1973) 14:361–366.[CrossRef]
  41. Prawitz D. Natural Deduction: A Proof Theoretical Study (1965) Stockholm: Almqvist and Wiksell.
  42. Shapiro S. Systems between first-order and second-order logics. In: Handbook of Philosophical Logic—Gabbay D, Guenthner F, eds. (2001) vol. 1, 2nd Edition. Dordrecht: Kluwer Academic. 131–188.
  43. Szabo M, ed. Collected Papers of Gerhard Gentzen (1969) North Holland, Amsterdam.
  44. Urban C, Pitts AM, Gabbay MJ. Nominal unification. In: Theoretical Computer Science (2004) 323:473–497.[CrossRef][ISI]
  45. van Benthem J. Higher-order logic. In: Handbook of Philosophical Logic—Gabbay D, Guenthner F, eds. (2001) vol. 1, 2nd Edition. Dordrecht: Kluwer Academic. 189–244.
  46. van Dalen D. Intuitionistic logic. In: Handbook of Philosophical Logic—Gabbay D, Guenthner F, eds. (2002) vol. 5, 2nd Edition. Dordrecht: Kluwer Academic. 1–114.

Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?



This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Similar articles in ISI Web of Science
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Gabbay, M. J.
Right arrow Articles by Mathijssen, A.
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?