Consiglio Nazionale delle Ricerche

Via De Marini 6, I-16149 Genova, Italy

forcheri@ima.ge.cnr.it, gentilini@ima.ge.cnr.it, molfino@ima.ge.cnr.it

Mathematical logic helps to form the rational basis of common sense
and, at the same time, it clashes with it. This conflict can be
explained by observing that results sistematically obtained by formal
logic alter deeply the *rationality categories* socially
accepted; in this respect, it is worthwhile to note that these results
often express innovations of natural science, already recognized by
technology, that people uses without awareness. Thus, logic is a
powerful educational tool to up-to-date common sense rationality, that
is to transfer new paradigms of thinking.

Notwithstanding this fact, mathematical logic was not given a central role in the Italian high school curriculum till few time ago. At present, the situation is changing, as the diffusion of computer science and its technology is leading to the renewal of high school curricula. This renewal recognizes the increasing importance of logic in various scientific and humanistic fields and takes into account its influence on recent orientations of computer science and artificial intelligence research. Accordingly, logic elements have been introduced in both mathematics and computer science teaching at high school level. However, it must be noted that in-service teachers do not have, usually, a deep preparation in logic. This situation requires a deep analysis of the new competencies that are required to teachers, and the design and realization of a training program aimed at providing in-service teachers with a logic background that allow them to become operatively aware of the influence of logic on common sense reasoning (which is a historical category). Our work is carried on within this framework. In particular, we designed a training course devoted to teachers of the Ligurian region. In the following, we shall describe the epistemological approach we followed in the design; on this basis, we shall discuss the content we propose and the pedagogical problems we took in account.

On the basis of our educational experience and referring to the west European culture, we think that several steps in human thinking have been determined by concepts and results of mathematical logic. In our opinion, awareness of this fact can be better acquired by analysing the influence of logic on common sense reasoning in the current historical context. Accordingly, content and method of our training program in logic have been devised on the basis of:

- the basic concepts of logic which mark the cultural transition from the last century to the present one (past phase);
- the current research direction which indicates the evolving trend (present phase).

1. As to the the concepts that deeply influenced, sometimes implicitly, common rationality evolution from the last century to the first half of the present one, we include:

- The "control" of infinite introduced by set theory [10,22], that is the capability of formally speaking about different types of infinite. Besides, the possibility of describing all mathematics by means of the set theory, using the concept of function. The expressive power reached by mathematics by means of both set theory and the general concept of function.
- The axiomatic view of both mathematical and scientific theories,
comprising:
- the view of theories as formal axiom systems and inference rules [24,30]}, that renders theories and proofs objects of mathematical exploration;
- the distinction between the concepts of provability and truth [24], both provided with definitions which can be technically handled within a syntax and a semantics of theories;
- the definition of consistency of a theory, and the possibility of proving this consistency only by referring to more powerful theories [16,28,29,14,5]: the consistency of a theory including Arithmetic cannot be proved using constructive methods. In addition, the realization of two facts: the metatheory on a theory T can be formalized using the language of T; it can be formally discussed what parts of the metatheory of T can be proved in T.

- The loss of both mutual consistency and determinism of scientific theories that takes place when these theories are examined as formal objects. For example, Newtonian, quantum, and relativity mechanics are not compatible each other and propose conflicting images of the world. Notwithstanding this fact, existing technology testifies that each of them can be applied in the real world.

We note that people of the past century, even cultured, could not make out these ideas: an example is constituted by Hilbert, who was convinced that Arithmetic could prove its consistency by itself.

2. The orientations, sometimes in dialectic position with the previous ones, that we think will characterize common rationality evolution from the second half of the present century to the first half of the next one, are:

Set Theory lost [10,22] the preminent position taken in the past phase of logic. The relevance of the uncountable infinite seems to be decreasing with respect to the centrality of the numerable infinite N. This centrality is suggested by several facts: the formal definition, within Arithmetic, of important questions about complexity theory [7]; the relevance of N in the description of computational processes [6,18,23,4]; the confirmation of the importance of fragments of Arithmetic for Proof Theory [25,5]. On the contrary, results of research on uncountable infinites regard internal aspects of Set Theory [25,5]; moreover, the work focuses more on the concept of self-reference, intrinsic to the notion of inaccessible cardinal [10], rather than on that of infinite.

A totally new approach to logic (in the first phase essentially cartesian) has been given by the introduction of paraconsistent logics [9]. These logics aim at formally including, even if locally, contradictions. Moreover, they are applied to quantum physics by means of quantum paraconsistent logics [8,12].

The importance of logics that formalize uncertainty (i.e. probabilistic, possibilistic, fuzzy logic) is increasing, from both a general and an effective point of view [19,11,13]. These logics allow a logical treatment of uncertainity, totally absent from logic of the past phase. In fact, the past phase regarded reasoning with uncertainity as an informal concept.

The stimulus of artificial intelligence induces formal logic to tackle fragments of knowledge till now considered as non admitting formalization [26]. Formal ontologies for representing knowledge is a new idea that realizes a compromise between mathematical logic and philosophy topics which are traditionally disjoint from it.

The number of formal semantics, in alternative or opposition against classical semantics, is increasing. In particular, we recall semantics based on the category theory [2,21]: these semantics seem especially powerful for formalisms representing computational processes (for example lamba calculus [27,3,1,17]).

Furthermore, logical calculi for deduction, alternative to the classical ones, are proposed [15,13]. The main observation deriving from this situation is the strong orientation, totally new with regards to the past phase of mathematical logic, towards a

*pluralism of possible rationalities that are all equally formal*.Through Lambek Calculi, proof theory has entered into linguistic [20]; this, in addition to formal semantics for natural language [31], introduces new aspects in the logical study of the language.

- to render teachers aware of the two phases of the previous section
- to help them to stress the dialectic relationship between the two phases.\\

As to the content, the program of the course is the following:

- Language, axiomatic system, proof: formal notions.
- Predicative calculus.
- Set theory and formalization of the concept of infinite.
- True and provable statements: Godel’s theorems.
- Recursive function and computation.
- Classical deduction schemes.
- Logics and artificial intelligence.
- Logics and computer science.
- Modal Logics
- Non classical semantics
- Non classical and alternative deduction schemes
- Formalized paraconsistency
- Formalized uncertainty

The total amount of time of the course is of 32 hours, subdivided in 16 modules. Each topic is developed into 2 modules, each one of 2 hours.

As to the pedagogical design, due to the interdisciplinary nature of logic, we decided to devote the course to teachers with different preparations and interests; consequently, we introduce topics of various nature and emphasize different views of the topics at hand. For example, we insert formalization of syntax and semantics oriented towards philosophy of the language, to capture the interest of teachers of humanities; to render the course appealing for teachers of scientific subjects, we emphasize topics such as: axiomatic view of scientific theories; consistency and completeness of a theory; independence of a statement on an axiom system. Finally, we take into account the attitude of the teachers of philosophy by adopting a historical point of view in the presentation of concepts. In general, we intend to focus attention of concepts and cultural ideas that are relevant in the teaching activity independently of the specific field of interest; for example: the notion of proof; the difference between provability and truth; the steps of the axiomatization of set theory; infinite sets. In order to take into account the specific professional needs of the various teacher's -categories, we decide of subdividing the presentation of each subject into two different modules: introductory and deepening. The deepening module aims at giving a formal treatment of the topic at hand, possibly including hints on research in the field. Moreover, we intend to complete the presentation of each theme with an educational analysis regarding the transfer of the theme itself to students, the possible levels of formalization, and the study of the related cognitive difficulties.

- H. P. Barendregt.
*The Lambda Calculus*. North Holland, Amsterdam, 1984. - J. I. Bell.
*Toposes and Local Set Theories*. Clarendon Press, 1988. - J. Van Benthem.
*Language in Action: Categories, Lambdas and Dynamic Logic*. North Holland, Amsterdam, 1991. - P. Van Emde Boas.
Machine models and simulations.
*Handbook of Theoretical Computer Science*(Van Leeuwen J., ed.), Elsevier, Amsterdam, 1990, p. 3-61. - G. Boolos.
*The Logic of Provability*Cambridge University Press, Cambridge, 1993. - E. Borger.
*Computability, Complexity and Logic*. North Holland, Amsterdam, 1989. - S. Buss.
*Bounded Arithmetic*. Bibliopolis, Napoli, 1986. - M. I. Dalla Chiara. Quantum logic.
In:
*Handbook of Philosophical Logic*(D. Gabbay and F. Guenthner, eds.), Kluwer Academic Publishing, 1989. - N. C. Da Costa. On Jackowski discussive logic.
In:
*Non classical Logics, Model Theory and Computability*(Arruda, Da Costa, and Choaqui, eds.), North Holland, Amsterdam, 1977. - K. J. Devlin.
*Fundamentals of Contemporany Set Theory*. Springer-Verlag, 1979. - D. Dubois, J. Lang, and H. Prade. Possibilistic logic.
In:
*Handbook of Logic in AI and Logic Programming*(Dov M. Gabbay, C. J. Hogger, J. A. Robinson, eds.), Clarendon Press, Oxford, 1994. - M. I. Dalla Chiara et al. Logic of unsharp quantum mechanics. 1995}
- P. Forcheri, P. Gentilini, and M. T. Molfino.
Research in automated deduction as a basis for a probabilistic proof-theory.
In:
*Logic and Algebra*. (P. Agliano' and A. Ursini, eds.), Dekker, New York, 1996, pp. 491-528. - P. Gentilini.
Provability logic in the Gentzen formulation of arithmetic.
*Z. Math. Log. Grundlagen. Math. 38*(1992), 536-550. - J.Y. Girard.
*Linear Logic*.*TCS 50*(1987), 1-102. - K. Godel. Uber Formal Unentscheidbar Satze der
Principia Mathematica und Verwander Systeme I.
*Monatshefte fur Mathematik und Physik 38*(1931), 173-198. - C. A. Gunter and D. S. Scott. Semantic domains.
In:
*Handbook of Theoretical Computer Science*(J. Van Leeuwen, ed.), Elsevier, Amsterdam, 1990. - D. S. Johnson. A catalog of complexity classes.
In:
*Handbook of Theoretical Computer Science*(J. Van Leeuwen, ed.), Elsevier, Amsterdam, 1990. - H. E. Kyburg. Uncertainty logics.
In:
*Handbook of Logic in AI and Logic Programming 3*(Dov M. Gabbay, C. J. Hogger, and J. A. Robinson, eds.), Clarendon Press, Oxford, 1994. - J. Lambek. Categorial and categorical grammars.
In:
*Categorial Grammars and Natural Language Structures*(Oehrle, ed.), 1987. - J. Lambek and P. J. Scott.
*Introduction to Higher Order Categorial Logic*. Cambridge University Press, 1986. - A. Levy.
*Basic Set Theory*. Springer-Verlag, 1979. - M. Li and P.B.M. Vitanyi.
Kolmogorov complexity and its applications.
*Handbook of Theoretical Computer Science*(J. Van Leeuwen, ed.), Elsevier, Amsterdam, 1990. - D. Monk.
*Mathematical Logic*. Springer Verlag, Berlin, 1976. - E. Nelson.
*Predicative Arithmetic*. Princenton University Press, 1986. - D. Perlis and V. S. Subrahmanian.
Meta-languages, reflection principles and self-reference.
In:
*Handbook of Logic in AI and Logic Programming 2*(Dov M. Gabbay, C. J. Hogger, J. A. Robinson, eds.), Clarendon Press, Oxford. - D. S. Scott. Lambda calculus: some models, some philosophy.
In:
*The Kleene symposium*(J. Barwise, ed.), North Holland, 1980. - C. Smorynski. The incompleteness theorems.
In:
*Handbook of Mathematical Logic*(Barwise, ed.), North Holland, Amsterdam, 1977. - C. Smorynski.
*Self-Reference And Modal Logic*. Springer-Verlag, Berlin, 1985. - G. Takeuti.
*Proof Theory*. North-Holland, Amsterdam, 1987. - D. Westerstahl.
Quantifiers in formal and natural languages.
*Handbook of Philosophical Logic*(D. Gabbay and F. Guenthner, eds.), Kluwer Academic Publishing, 1979.