Functions and Induction

Abstract

The “core business” of the LINCOS system in the context of astrolinguistics discussed in the present treatise, is the construction of entities (i.e., types). This aspect is inherited from CC, the calculus of constructions, the base of the linguistic system, as mentioned in Chap. 1. In the present chapter a review is presented of various ways of achieving such constructions. For reasons of perspicuity, we use first a simple example in real life: the static situation of a book lying on a shelf. Any other comparable situation will do equally well. Evident “real” relations for this case are expressed in the system in an understandable way. En passant the basic logical operators from classical propositional logic are reviewed also in the formalism of functions and induction: conjunction, disjunction, negation, and implication. In this natural way the powerful and useful concept of induction, in which entities are defined in terms of themselves, appears on the scene. In this way the realm of CCI, the calculus of constructions including induction, is easily entered. We conclude with reviewing existence and equality considered to be functions as well.