Go up to TopGo forward to 2 The Language of Logic

# 1 Introduction

AGEOMETRETOS MEDEIS EISITO
Let no one without skill in geometry enter.
(Inscription over the portal of Plato's Academy
in the sense of "Study mathematics first")

We introduce in this report basic mathematical domains and techniques as a foundation for the formal treatment of many concepts in computer science and engineering. The relationship between computer science and mathematics is still a subject of debate. Nevertheless it is clear that the mathematical way of problem solving is at the core of every scientific and technical activity whose goal is to describe phenomena of the real world and to influence these, e.g. by a computer program that fulfills a particular purpose.

The key idea in this process is abstraction (see Figure The Mathematical Process): we construct a simplified image (model, theory, domain) of the real world that captures all those aspects that we consider of relevance for our problem but neglects those facets that seem without influence. While being not a duplicate of the real world, this domain has the advantage that it can be unambiguously described and that we can operate in it (ask questions, derive knowledge, define new concepts) without resorting to the objects of the real world. An interpretation of the solution developed in this domain yields real world effects that (provided that our abstraction has been faithful and that our operations have been correct) meet our expectations.

The Mathematical Process

While the real world has all kinds of different objects and phenomena, their mathematical images are ultimately described in terms of a relatively small number of notions, such as numbers, functions, and relations which in turn can be all reduced to the fundamental concept of sets. The constructions of these domains, their resulting inner structures, and their consequent properties reveal much of how mathematics works; we will elaborate them in this report in detail.

For understanding the constructions in a deeper sense it is important to learn not only mathematical contents but also mathematical techniques, in particular the language and the reasoning rules provided by mathematical logic. If these are mastered, we read and understand definitions and statements in any scientific area and judge whether a given argument is complete and correct. We therefore put in this report much emphasis on formally correct definitions and propositions in addition to the semi-formal ones that can be usually found in a textbook. Likewise we give proofs in a greater degree of formality and detail as is common practice; our goal is to enable the reader to check and to understand statements and claims, not to learn them by heart.

This report is therefore not only a collection of mathematical "cookbook recipes" that can be applied without any deeper insight (although it contains a lot of definitions and propositions); it is intended to make the reader understand "how things work" in order to enable her to operate in all formal domains that she will encounter in the future.

To emphasize this "no magic" approach, we use a small piece of software, the Logic Evaluator, a Java applet/application whose source can be found at

`http://www.risc.uni-linz.ac.at/software/formal`.
This interpreter allows to write function and predicate definitions in an executable subset of first order predicate logic with set theory and to evaluate terms and propositions. Many of the concepts introduced in this paper are implemented in this way; demonstration examples as the basis of own experiments can be found throughout the electronic version of this document (with screenshots in the hardcopy). The Java classes for formulas and terms are listed to illustrate the operational interpretation of logic formulas.

Much inspiration and some of the contents of this report have been derived from the textbook

B. Buchberger, F. Lichtenberger
Mathematik für Informatik I -- Die Methode der Mathematik
Zweite, korrigierte Auflage, Springer, Berlin, 1981
as well as from the lecture notes
F. Lichtenberger
Mathematik für Informatiker 2
Johannes Kepler Universität, Sommersemester 1999
based on material from former courses of Bruno Buchberger. A subset of the Theorema software
`http://www.theorema.org`
being developed by Bruno Buchberger and his working group has been a source of inspiration for the Logic Evaluator. Many thanks to Werner Danielczyk-Landerl, Peter Kulczycki, Michael Petz, and Wolfgang Windsteiger for discussions on and/or corrections of this report.

This document contains two parts, the main body oriented towards mathematical domains (Chapters 2-7) and an appendix oriented towards mathematical techniques (Appendices A and B). We recommend to study the material in the order

2 -> A -> 3 -> 4 -> 5 -> B -> 6 -> 7
skipping the details of the proofs in Chapters 3 and 4 on first reading and studying them again after having read Appendix B.
Author: Wolfgang Schreiner
Last Modification: October 4, 1999