Information Technology Reference
In-Depth Information
Ontology can be informal of formal, and our approach is that ontology must be
nothing but formal and mathematically unambiguous. To be more precise concern-
ing
logic
, let us describe
what
logic is and
how
logic is defined.
Firstly, there is not a single logic for everything. Secondly, we need to distinguish
logic as the basis for mathematical reasoning from logic as dedicated to theory de-
velopment and programming of rule bases. In all this, it is important to understand
what is the object language for logic, and what is the metalanguage supporting that
object language.
The logic for mathematical reasoning goes back to Aristotle and even before
those times to pre-Socratic times when e.g. reductio ad absurdum was used by Zeno.
Mathematicians, like Szabó [22], say Aristotle didn't say all that much that influ-
enced modern developments of logic, whereas philosophers, like Hintikka, read
lots between the lines and provide far going interpretation about what Aristotle said
e.g. about deictics (syntactic, roughly speaking) and apodeictics (semantics, roughly
speaking). Our take on logic must be the mathematical one, since the philosophical
approach doesn't primarily support formalism and ontology based strict representa-
tions. Logic becomes formal logic during late nineteen century when Frege [12] de-
fines what we now call
first-order logic
. This logic was originally intended as logic
only for mathematical reasoning, i.e. logic for mathematics. At the change of the
century, Hilbert pointed out the difficulties concerning natural numbers and logic,
and the question was “Which comes first?”. The metalanguage for this first-order
logic is not existing
per se
, but we rather have a situation where the non-meta based
object language for logic is constructed, and leading to formal difficulties and even
paradoxes, which are then rendered, and the formal basis for the object language is
reiterated to avoid these difficulties. This process of finding difficulties followed by
rendering these difficulties continued for decades, and when Hilbert some fifty years
later (with Bernays) was finishing work on set theory and foundations of mathemat-
ics [13, 14], the question remained still unanswered. Between Frege's
Begriffsschrift
and Hilbert-Bernays'
Grundlagen
, lots of things happen in the discussion on logic.
Peano [17] did his axioms for natural numbers, Russell entered the debate through
paradoxes and many others contributed to these discussions. Some computation-
ally interesting things happen also late at those times, e.g. by Schönfinkel [20], a
frequent visitor to Hilbert in Göttingen, and his work on combinatory logic, later
transformed by Curry in his thesis [5] (supervised by Hilbert and Bernays) provid-
ing groundwork for
-calculus, using only a subset of Schönfinkel's combinators,
and thereby type theory was born. Curry together with Howard later showed how
propositions can be interpreted as types, an observation that has seduced computer
scientist almost a century now.
Logic as dedicated to theory development
builds upon a very precise meaning of
what logic really is. Formally (and computationally) speaking, logic consists of
λ
•
its signature with sorts (types) and operators,
•
algebras providing the meaning of the signature,
•
all terms constructed (syntactically) using operators in the signature, and the
resulting algebraic interpretations (semantics) of these terms,
