Go up to Top
Go forward to 2 The Language of Logic
|
Go up to Top Go forward to 2 The Language of Logic |
|
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. Lichtenbergeras well as from the lecture notes
Mathematik für Informatik I -- Die Methode der Mathematik
Zweite, korrigierte Auflage, Springer, Berlin, 1981
F. Lichtenbergerbased on material from former courses of Bruno Buchberger. A subset of the Theorema software
Mathematik für Informatiker 2
Johannes Kepler Universität, Sommersemester 1999
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 -> 7skipping the details of the proofs in Chapters 3 and 4 on first reading and studying them again after having read Appendix B.