The four authors present their speculations about the future developments of mathematical logic in the twenty-first century. The areas of recursion theory, proof theory and logic for computer science, model theory, and set theory are discussed independently.

Temporal Type Theory (TTT) has been recently introduced as a topos-theoretic approach to understanding the behaviour of systems over time. A truly innovative point of TTT is that it makes truth inherently dependent on time; this is to be contrasted with the classical approach in which past, present and future are related via logical operators. Further on this line of research, the notion of truth is substituted by the ‘time duration’ over which a proposition is true, giving rise to the (...) logic of temporal landscapes. In this paper, we embed the main notions of the Calendar and Time Type System (a framework that was built for reasoning about calendric notions in the context of the Web and is centred around the notion of time granularity) in Temporal Type Theory, attempting to address a common requirement in the practical use of temporal formalisms: the ability to speak about certain time moments and appropriate time windows in (past and future) time, in the form of hours, dates, holidays, etc. With a view to concrete applications, we provide examples on how calendar types can be combined with temporal operators of TTT to augment the expressive power of this framework. In that respect, the addition of calendar types genuinely adds to the range of Temporal Type Theory as a powerful specification language. (shrink)

In this paper we define and examine frame constructions for the family of manyvalued modal logics introduced by M. Fitting in the '90s. Every language of this family is built on an underlying space of truth values, a Heyting algebra H. We generalize Fitting's original work by considering complete Heyting algebras as truth spaces and proceed to define a suitable notion of H-indexed families of generated subframes, disjoint unions and bounded morphisms. Then, we provide an algebraic generalization of the canonical (...) extension of a frame and model, and prove a preservation result inspired from Fitting's canonical model argument in [FIT 92a]. The analog of a complex algebra and of a principal ultrafilter is defined and the embedding of a frame into its canonical extension is presented. (shrink)

Students often study logic on the assumption that it provides a normative guide to reasoning in English. In particular, they are taught to associate connectives like “and” with counterparts in Sentential Logic. English conditionals go over to formulas with → as principal connective. The well-known difficulties that arise from such translation are not emphasized. The result is the conviction that ordinary reasoning is faulty when discordant with the usual representation in standard logic. Psychologists are particularly susceptible to this attitude.

In the four papers available on our web site (of which this is the first), we propose to develop an inductive logic. By “inductive logic” we mean a set of principles that distinguish between successful and unsuccessful strategies for scientific inquiry. Our logic will have a technical character, since it is built from the concepts and terminology of (elementary) model theory. The reader may therefore wish to know something about the kind of results on offer before investing time in definitions (...) and notation. Providing such an informal overview is the purpose of the present essay. We begin with discussion of the central concept under investigation, namely, theory acceptance. (shrink)

The topics of structural proof theory and logic programming have influenced each other for more than three decades. Proof theory has contributed the notion of sequent calculus, linear logic, and higher-order quantification. Logic programming has introduced new normal forms of proofs and forced the examination of logic-based approaches to the treatment of bindings. As a result, proof theory has responded by developing an approach to proof search based on focused proof systems in which introduction rules are organized into two alternating (...) phases of rule application. Since the logic programming community can generate many examples and many design goals, the close connections with proof theory have helped to keep proof theory relevant to the general topic of computational logic. (shrink)

Intelligence can be understood as a form of rationality, in the sense that an intelligent system does its best when its knowledge and resources are insufficient with respect to the problems to be solved. The traditional models of rationality typically assume some form of sufficiency of knowledge and resources, so cannot solve many theoretical and practical problems in Artificial Intelligence (AI). New models based on the Assumption of Insufficient Knowledge and Resources (AIKR) cannot be obtained by minor revisions or extensions (...) of the traditional models, and have to be established fully according to the restrictions and freedoms provided by AIKR. The practice of NARS, an AI project, shows that such new models are feasible and promising in providing a new theoretical foundation for the study of rationality, intelligence, consciousness, and mind. (shrink)