Higher-Order Logic

Jan Burse, created Feb 08. 2010 Now that we have put all the pieces together, the sales system, the client installer and the product, it comes to the point where we have to write documentation for our product. User manuals, reference documents, data sheets and professional articles are on the plan. This means taking a closer look, to the foundations of the product, to the context of the product and to the aims of the product. This time I trapped myself in taking a too close a look. The idea was simple to give a fresh foundation to the workings of a Prolog interpreter. The outcome was fatal. It resulted in many months’ non accountable hours. As a rule I do not pay myself for basic research. What was this voice I was hearing that was calling me? It was the temptation of product improvements and new directions of product development. So I stepped into the dark of non-classical logic and higher order logics. Mental reservations that nothing can be drawn from such logics were there. What can there be that cannot already be accomplished by first order logics? But we wanted to get a deeper insight on one hand into para-consistency and on the other hand into alternatives to set theory. Hence we could not overcome the temptation. Slowly the mental reservation gave way to dealing with non-classical and higher order logic. We can view these non-standard logics as weaker forms of the corresponding standard logic or even standard theory. Typically this means that the non-standard has a broader set of models. Now because validity means that a formula is satisfied by every model, we can readily draw the following conclusion. When working with validity we can safely go from non-standard logic to standard logic and/or theory, but not necessarily vice versa. This means that a conservative formula valid in non-standard logic will also be valid in standard logic and/or theory. But we must avoid the fallacy to expect a formula valid in standard logic and/or theory to be also valid in non-standard logic. So we started to run, by first completing a paper we had already started some three years ago. This paper was about non-classical predicate logic, and it was a nice framework to investigate different logics based on minimal logic. We were already able to put into relationship a para-consistent logic, a para-complete logic and classical logic. Unfortunately the used fragment was very poor in terms of connectives and quantifiers. Only implication and forall was available. So we spent some time adding a fusion and an existential type. Every Prolog query is an existential type question on a fusion of goals. So we had to investigate. Next we started experimenting with enhancing the notion of a Prolog term. Why not allow variables in the position of functors? The answer came very quickly, we have to be careful in forming for example terms such as F(F), Russell’s paradox is lurking. So we needed to extend our framework towards type theory, by introducing kinds that will denote families of formulas. Appropriate formation rules can then exclude Russell’s paradox. If we further allow lamda expression and new inference rules we even get comprehension for free. This was a good point to stop and relate our results to something we had already explored some 15 years ago. At that time we showed that hierarchical logic programs have a model. Our result made freely use of set theory without any consideration what sub theory has exactly been used and whether it is consistent. This time we can say for sure that hierarchical logic programs are consistent and we also know that a crucial notion is comprehension. And this notion is even available for some non-classical and higher order logics. Unfortunately we will have to run again and again since hierarchical logic programs are only the beginning.