scientific
landscape
| modeling |
(models, semantics)
| semiotics |
reasoning
of
relations
| categories |
| relations |
| objects |
| wholes & levels |
| meta |
glossary
|
formalization & symbol manipulation |
| ontology |
| truth & reality |
|
the scientific landscape |
| representation (models, semantics) |
| logic & reasoning | complexity & metrics | category of relations | |||||||||
|
| meaning
| linguistic glossary |
| components & datatypes | |||||||||||
|
| |||||||||||||||
|
Location: http://www.cs.mun.ca/~ulf/gloss/symani.html.
By Ulf Schünemann since 2003.
Please email me your comments.
| ||||||||||||||||
| Formalization is too weak to fully express / replace intuition (private) and informal conventions (public). |
1. Limits of Defining Formalism's Meaning: The Symbol Grounding Problem.
Searle's Chinese Room «has provoked an enormous variety of responses
... Stevan Harnad, for example, ... [emphasizes]
the importance of infusing otherwise purely syntactic strings with semantic content,
if they are to be meaningful symbols rather than meaningless marks ...
The necessity to locate a suitable mechnism for imparting meaning to symbols
he calls the symbol grounding problem.
... [A] Chinese-Chinese disctionary may succeed in relating some Chinese
symbols to other Chinese symbols, but ... such a resource is woefully inadequate
for anyone who actually wanted to learn Chinese. ...
... [M]ore generally for any language whatever ...
the ords that occur in that language are either defined or undefined ("primitive").»
In princple, the defined words could be recursively expanded
to those words which define them,
until «nothing but string of proimitives specifying the meaning of
non-primitive symbols should remain. If we cannot understand primitive
symbols, surely we cannot understand symbols defined by means of them» [Fetzer:6].
Two explanations:
2. Limits of Expressing Meaning: The Unformalizable Residue.
[Cf. expressability in programming language design.]
«To put thoughts in words or to describe a particular experience involves
formalization of intuition. It has been contended that no finite number of
propositions could describe exhaustively all that is involved in a
particular experience. In other words, it is impossible to formalize
without residue the complete intuition at the moment.
The matter of approximating intuition by formalization is clearer with
regard to mathematics. For example, we know intuitively many things about
integers. ...
Peano's axioms are thought to be capable of characterizing completely our
notion of positive integers. Yet, as Russell observed long ago, Peano's
axioms are satisfied by all progressions such as the odd positive integers,
the negative integers. ...
In fact ... there are important results which indicate unmistakably
that we can formalize without residue neither the fundamental intuitive
notion of positive integers nor the basic notion of sets or classes.
... It also follows [from Gödel's theorem] that no ordinary axiom
system can preclude the interpretation that besides the ordinary 1, 2, ...
the set of positive integers also contains certain other queer things;
there is no way to formalize in an ordinary logistic system our intuition
that 1, 2, ... are the only integers.
On the other hand, there is no axiom system in which we can get
all the real numbers or the classes of positive integers. This
follows easily from Cantor's famous argument for non-denumerability. Thus,
given any axiom system, we can enumerat all the classes of positive
integers which can be proven to exist in the system, either by
applying Löwenheim's theorem or by reflecting on the fact that the
theorems of existence in the system can enumerated. Hence, if we define
with Cantor a class K of positive integers such that for ecach n,
n belongs to K if and only if n does not belong to the
nth class in the enumeration, then the existence of K cannot be
proven in the system. In other words, although in the system we can also
speak of all the classes of positive integers, we cannot really formalize
without rediue the intuitive notion of "all" with regard to classes of
positive integers; in each formalized axiom system, there is always some
class of positive integers that is left out» [Wang 33ff].
3. The Puzzle of the Löwehnheim-Skolem Theorem (model theory).
«The [Löwenheim-Skolem theorem] states that every formal system
expressed in the first order functional calculus has a denumerable model.
In particular the general theory of sets as axiomatized e.g., by von
Neumann and Gödel has a denumerable model; yet this theory was
designed in part in order to formalize in a consistent and rigorous manner
the arguments of Cantor's theory of infinite cardinals» [Myhill 43].
«[T]he continuum is according to formalized set-theory non-denumerable;
i.e., its non-denumerability is a thesis of that theory. ... On the other
hand, since formalized set-theory possesses a denumerable model, it
possesses a model in the integers; and so there is a one-to-one
correlation between all the sets of formalized set-theory and integers,
namely the correlation which correlates each set with the integer
representing it in the model. A fortiori there is a correlation between
those particular sets in the formal system which constitute the continuum
and a subset of the integers. It appears to follow» [Myhill 43]
But what the Löwehnheim-Skolem theorem really means is that
«there exist relations having all the formal properites assigned to
class-membership by the axioms of (any consistent) set-theory, and also
having denumerable fields. But none of these relations is
class-membership; for class-membership certainly has a vastly
non-denumerable field. Hence all the Löwehnheim-Skolem models of
set-theory are non-standard, relative to the given interpretation. Indeed,
there is evidently only one standard model of set-theory, because the
predicate-letter epislon, the only one which appears, is already
preassigned on interpretation.
...
[I]f we fix the interpretation of epsilon, the set-theory has but
one model, namely the one which interprets epsilon in the way we fixed it,
and U as the field of epsilon thus interpreted; and that this model is
indenumberable. But then it seems after all that the indenumerability arose
in the (informal, external) interpretation and not in the formalism itself;
so that after all there is a good sense in which formalism is inadequate to
express indenumerability [underlining added].
This difficulty can I think be resolved by distinguishing a private and
a public aspect of formalism» [Myhill 49f].
A. Private: Formalism is too weak to replace intuition of the standard model. «Formalism in its private aspect is a computational device for avoiding `raw thought' .. All real mathematics is made with ideas, but formalism is always ready in case we grow afraid of the shifting vastness of our creations. ... The Skolem `paradox' thus proclaims our need never to forget completely our intuitions. We could shift to a formalism indistinguishable from set-theory and it could be something other than set-theory. It only remains set-theory as long as the intuition of membership has not slipped away from us. It could be formally the same and have a grotesquely different meaning. ... At least, even if our intuition of membership perishes entirely, we can rely on set-theory not to turn overnight into the theory of some finite group, even though we cannot guarantee that it will not turn into a theory about some complicated arithmetical relation» [Myhill 50].
B. Public: Formalism is too weak to replace informal convention of the standard model. «[T]here seems to be no formal means of assuring that our conception of membership any more more than our perception of a particular sense-quality is the same as another person's. For no finite or even infinite number of formal assertions agreed on by us both could be evidence that his set-theory was not in my sense denumerable. Of course it would not be denumerable in his sense, but I would not know if he meant by `denumerable' what I meant by `denumberable' unless I knew that he meant the same as I mean by `membership.' The second philosophical lesson of the Löwehnheim-Skolem theorem is that the formal communication of mathematics presupposes an informal community of understanding» [Myhill 50, underlining added].
Mathematical Advance by the Axiomatic Method.
«The axiomatic method invented by the Greeks has always been regarded as
the strongest foundation for erecting systems of mathematical thinking. ...
Until recent times the only branch of mathematics that was considered by
most students to be established on sound axiomatic foundations was
geometry.
But within the past two centuries powerful and rigorous systems
of axioms have been developed for other branches of mathematics
...
» [GP 52].
«The 19th century witnessed a tremendous surge forward in mathematical
research. Many fundemental problems that had long resisted solution were
solved; new areas of mathematical study were created; foundations were
newly built or rebuilt for various branches of the discipline. The most
revolutionary development was the construction of new geometries
...
In particular the modification of Euclid's parallel axiom
led to immensly fruitful results ["non-Euclidean geometries"]
...
It was this successful departure that stimulated the development of an
axiomatic basis for other branches of mathematics
which had been cultivated in a more or less intuitive manner.»
«Mathematicians came to hope and believe that the whole realm of
mathematicsal reasoning could be brought into order by way of the axiomatic
method.
Gödel's paper put an end to this hope. He confronted mathematicians
with proof that the axiomatic method has certain inherent limitations which
rule out any possibility that even the ordinary arithmetic of whole numbers
can ever be fully systematized by its means. What is more, his proofs
brought the astounding and melancholy relevation that it is impossible to
establish the logical consistency of any complex deductive system except by
assuming principles of reasoning whose own internal consistency is as open
to question as that of the system itself» [GP 52].
The Nature of Mathematics: Abstract and Formal. «One important conclusion that emerged from [axiomatizing] the foundations of mathematics was that the traditional conception of mathematics as the "science of quantity" was inadequate and misleading. For it became evident that mathematics was most essentially concerned with drawing necessary conclusions from a given set of axioms (or postulates). It was thus recognized to be much more "abstract" because mathematical statements can be construed to be about anything whatsover, not merely about some inherently circumscribed set of objects or traits of objects; more "formal" because the validity of a mathematical demonstration is grounded in the structure of statements rather than in the nature of a particular subject matter. The postulates of any branch of demonstrative mathematics are not inherently about space, quantity, apples, angles or budgets, and any special meaning that may be associated with the postulates' descriptive terms play no essential role in the process of deriving theorems. The question that confronts a pure mathematician (as distinct from the scientist who emplys mathematics in investigating a special subject matter) is not whether the postulates he assumes or the conclusions he deduces from the are true, but only whether the alledged conclusions are in fact the necessary logical consequences of the initial assumptions. This approach recalls Betrand Russell's famous epigram: Pure mathematics is the subject in which we do not know what we are talking about, nor whether what we are saying is true» [GP 52f, underlining added].
Abstractness Makes Consistency Harder to See.
«A land of rigorous abstraction, empty of all familiar landmarks, is
certainly not easy to get around in. But it offers compensations in the
form of new freedom of movement and fresh vistas. As mathematics became
more abstract, men's minds were emancipated from habitual connotations of
language and could construct novel systems of postulates ... Some of these
systems ... did not lend themselves to interpretations as obviously
intuitive ("common sense") as those of Euclidean geometry or arithmetic ...
[This is not the problem because what is intuitive is not fixed and because
intuition is not a safe criterion for truth or fruitfulness.]
However, the increased abstractness of mathematics also raised a more
serious problem. When a set of axioms is take to be about a definite and
familiar domain of objects, it is usually possible to ascertain whether the
axioms are indeed true of these objects, and if they are true, they must
also be mutually consistent. But the abstract non-Euclidean axioms appeared
to be plainly false as descriptions of space, and, for that matter,
doubtfully true of anything. ... [The Riemannian postulates] are apparently
not true of the ordinary space of our experience. How then is their
consistency to be tested? How can one prove that they will not lead to
contradictory theorems?» [GP 53f]
Two methods:
A. Model Theory: The Model Method. «A general method for solving this problem was proposed. The underlying idea is to find a "model" for the postulates so that each postulate is converted into a true statement about the model» [GP 54].
A1. Foundation in Finite Models. «So long as we can interpret a system by a model containing only a finite number of elements, we have no great difficulty in proving the consisteny of its postulates. ... Unfortuately most of the postulate systems that constitute the foundations of important branches of mathematics cannot be mirrored in finite models; they can be satisfied only by non-finite ones. [For example, the successor axiom of arithmetics allows only for infinite models of arithmetics.] It follows that the truth (and so the consistency) of the set [of such postulates] cannot be established by inspection and enumeration.»
A2. The Infinite Regress Problem.
«We may adopt a model ombodying the Riemannian postulates in which the
expression "plane" signifies the surface of a Euclidean sphere; the
repsression "point," a point on this surface; the expression "straingt line,"
an arc of a great circle on this surface, and so on. Each Riemannian
postulate can then be converted into a theorem of Euclid. ...
Unhappily this method is vulnerable to a serious objection; namely, that it
attempts to solve a problem in one domain merely by shifting the problem to
another (or, to put it another way, we invoke Euclid to demonstrate the
consistency of a system which subverts Euclid). Riemannian geometry is
proved to be consistent only if Euclidean geometry is consistent. Query,
then: Is Euclidean geometry consistent? If we attempt to answer this question
by invoking yet another model, we are no closer to our goal. In short, any
proof obtained by this method will be only a "relative" proof of
consisteny, not an absolute proof» [GP 54f].
A3. The Foundation-in-Intuition Problem.
«It may be tempting to suggest ... that a set of postulates is
consistent ... if the basic notions employed are transparently "clear" and
"cretain." But the history of though has not dealt kindly with the doctrine
of intuitive knowledge implicit in this suggestion. In certain areas of
mathematical research radical contradictions have turned up in spite of
"intuitive" clarity of the notions involved in the assumptions, and despite
the seemingly consistent character of the intellectual constructions
performed. Such contraditions (technically called "antinomies") have
emerged, for example, in the theory of infinite numbers devceloped by Georg
Cantor in the 19th cenury. His theory was built on the elementary and
seemingly "clear" concept of class. ...
In point of fact, Bertrand Russel constructed a contradition [precisely
analogous to the contradition discovered in Cantor's theory of infinite
classes] within the framework of elementary logic itself. ...
All classes apparentyl may be divided into two groups: those which do not
contain themselves as members, and those which do. An example of the first
is the class of mathematicians, for patently the class itself is not a
mathematician ... An example of the second is the class of all thinkable
concepts, for [it] is itself a thinkable concept ...
[Now, what kind of class is the class of all classes of the first kind?
It cannot be either, because either choice results in a contradiction.]
This fatal contradiction results from the uncritical use of the apparently
pellucid notion of class.
Other paradoxes were found later, each of them constructed by means of
familiar and seemingly cogent modes of reasoning. Non-finite models by
their very nature involve the use of possibly inconsistent sets of
postulates. Thus it became clear that, although the model method
... is an invaluable mathematical tool, that method does not supply a final
answer to the problem it was designed to resolve» [GP 56].
B. Proof Theory: The Method of Formal Mathematics + Meta-Mathematics.
«The eminent German mathematician David Hilbert then adopted the opposite
approach of eschewing models and draining mathematics of any meaning
whatsover. In Hilbert's complete formalization, mathematical expressions
are regarded simply as empty signs. The postulates and theorems constructed
from the system of signs (called a calculus) are simply sequences of
meaningless marks which are combined in strict agreement with explicitly
stated rules. The derivation of theorems from postulates can be viewed as
simply the transformation of one set of such sequences, or "string," into
another set of "strings," in accordance with precise rules of operation. In
this manner Hilbert hoped to eliminate the danger of using any unavowed
principles of reasoning.
Formalization is a difficult and tricky business, but it serves a valuable
purpose. It reveals logical relations in nakes clarity ... One is able to
see the structural patterns of various "string" of signs: how they hang
together, how they are combined, hot they nest in one another, and so on. A
page covered with the "meaningless" marks of such a formalized mathematics
does not assert anything ... <-- ---it is simply an abstract design or a
mosaic possessing a certain structure-->. But configurations of such a
system can be described, and statements can be made about their various
relations to one another. One may say that a "strinng" ... resembles
another "string," or that one "string" appears to be made up of three
others, and so on. Such statements will evidently be meaningful.
Not it is plain that any meaningful statements about a meaningless syste,
do not themselves belong to that system. Hilbert assigned them to a
separate realm which we called "meta-mathematics." Meta-mathematical
statements are statements about signs and expressions of a
formalized mathematical system: about the kinds and arrangements of such
signs when they are combined to form longer strings of marks called
"formulas," or about the relations between formulas which may obtain as a
consequence of the rules of manipulation that have been specified for
them.
[For example, the arithmetic expression "2+3=5" belongs to mathematics.
OTOH the expression "`2+3=5' is an arithmetic formula"]
does not express a mathematical fact: it belongs to meta-mathematics,
because it characterizes the string of mathematical signs. Similarly the
expression x=x belongs to mathematics, but the statemtent "`x' is a
variable" belong to meta-mathematics. ... Finally, the following statement
also belongs to meta-mathematics: "Arithmetic is consistent" (i.e., it is
not possible to derive from the axioms of arithmetics both the formula 0=0
and also the formula 0/=0)» [GP 57f].
B1. The Formalists' Programme: Foundation in Finite Formal Proofs. «Hilbert attempted to build a method of "absoulte" proof of the internal consistency of mathematical systems. Specifically, he sought to develop a theory of proof whch would yield demonstrations of consisteny by an analysis of the purely structural features of expressions in completely formalized (or "uninterpeted") calculi. Such an analysis consists exclusively of noting the kinds and arrangements of signs in formulas and determining whether a given combination of signs can be obtained from others in accordance with th explicitly stated rules of operation. An absolute proof of the consistency of arithmetic, if one could be constructed, would consist in showing by meta-mathematical procedures of a "finitistic" non-infinite character that two "contradictory" formulas, such as (0=0) and its negation, cannot both the derived from the axioms or initial formulas by valid rules of inference» [GP 58].
| -> | Logical calculi |
B2. The Defeat.
Gödel showed 1931 «that it is impossible to establish a
meta-mathematical proof of the consistency of a system comprehensive enough
to contain the whole of arithmetic---unless, indeed, this proof itself
employs rules of inference much more powerful than the transformation rules
used in deriving theorems within the system. In short, one dragon is slain
only to create another» [GP 64f]
Second, «Gödel showed that Principia, or any other system
within which arithmetic can be developed, is essentially incomplete. In
other words, given any consistent set of arithmetical axioms,
there are true arithmetical statements which are not derivable from the
set. A classic illustration of a mathematical "theorem" which has thwarted
all attempts at proof is that of Christian Goldbach, stating that every
even number is the sum of two primes. No even number has ever been found
which is not the sum of two promes, yet no one has succeeded in finding a
proof that the rule applies without exception to all even numbers. ...
[E]ven if any finite number of other axioms is added, there will always be
further arithmetical truths which are not formally derivable» [GP 65].
«What Gödel aimed at was nothing less than the complete arithmetization of meta-mathematics. If each meta-mathematical statement could be uniquely represented in the formal system by a formula expressing a relation between numbers, questions of logical dependence between meta-mathematical statements could be explored by examining the corresponding relation between integers» [GP 67].
«Gödel's analysus does not exclude a meta-mathematical demonstration of the
consistency of arithemtic; indeed, such proofs have been constructed,
notably by Gerhard Gentzen, a member of the Hilbert school. But these
"proofs" are in a sense pointless, because they employ rules of inference
whose own internal consistency is as much open to doubt as is the formal
consistency of arithmetic itself. Gentzen's proof employs a rule of
inference which in effect permits a formula to be derived from an infinite
class of premisses. And the employment of this non-finitistic meta-
mathematical notion raises once more the difficulty which Hilbert's
original program was intended to solve.
There is another surprise coming. Although the formula G is undecidable, it
can be shown by meta-mathematical reasoning that G is nevertheless
a true arithmetical statement and expresses a property of the
arithmetical integers. ... G corresponds to a meta-mathematical statement
("the formula with Gödel number h is not demonstable") which,
as we have seen, is true, unless arithmetic is inconsistent. It follows
that G itself must be true. We have thus established an arithmetical
truth by a meta-mathematical argument» [GP 69].
«Contrary to previous assumptions, the vast "continent"
of arithmetical truth cannot be brought into systematic order by way of
specifying once for all a fixed set of axioms from which all true
arithmetical statements would be formally derivable»
[GP 69f, underlining added].
Chaitin's constant 
Let programs be encoded with prefix-property (eg. with special end-symbol).
Let P be the set of (encodings of)
all syntactically correct programs which halt.
One can prove that (1)
| vocabulary (lexicon) | formation rules | transformation rules | axioms | additional rules (non-symbolic?) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Formalized Language | + | + | rules of logical inference | ± | semantic rules | ||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Calculus | + | + | + | ± | - | ||||||||||||||||||||||||||||||||||||||||||||||||||||||
| - Logistic system / logical calculus | + | + | rules of logical inference | ± | - | ||||||||||||||||||||||||||||||||||||||||||||||||||||||
| in particular, deductive system | + | + | modus ponens + others | ± | - | ||||||||||||||||||||||||||||||||||||||||||||||||||||||
| · axiomatic system | + | + | -"- (derivable from axioms called "theorems") | + | - | ||||||||||||||||||||||||||||||||||||||||||||||||||||||
| + | finite | -"- (finitely many) | (in)finitely many
| - |
| + | + | -"- | + | - |
· natural deduction system
| + | + | -"- | - | - |
| + | + | -"- | - | - |
| + | + | -"- | - | - |
- Computational calculus | + | + | evaluation rules | (untransformables are called "values") - | - |
· Lambda calculus | + | + | function application | - | - |
Grammar (natural language) | + | PS-rules | ± | ? | morphophonetic/ -graphemic rules |
- Transformation grammar | + | PS-rules | T-rules | ? | -"- |
Formal Language | + | + | - | - | -
| |
"Logistic" systems (Logical calculi) and Formalized languages.
Alonzo Church:
«We distinguish between a logistic system and a formalized language
[>]
on the basis that the former is an abstractly formulated calculus
for which no interpretation is fixed, and thus has a syntax but no semantics;
but the latter is a logistic system together with an assignment of meanings
to its expressions.
«In order to obtain a formalized language it is necessary to add,
to these syntactic rules of the logistic system,
semantical rules assigning meanings (in some sense)
to the well-formed expressions of the system»
[AESA,
continue AESA quotes on formalized languages].
«The "theorems" of the system are all the formulas, including the axioms,
which can be derived from the axioms by applying the transformation rules.
A "proof" consists of a finite sequence of legitimate formulas, each of
which is either an axiom or is derivable from preceding formulas in the
sequence by the transformation rules» [GP 90].
"Deductive" system.
Logistic systems might be classified according
to (the meaning or form? of) its transformation rules,
and thus according to the modes of inference [>]
they formalize: deduction, reduction/induction, abduction.
Deductive systems include the modus ponens rule (or an equivalent rule).
Axiomatic system.
«[A] deductive system is an axiomatic system if it contains axioms,
a natural deduction system if it does not»
[x].
Calculus.
«A calculus is a formal language and rules for manipulating expressions of the
language. For example, by applying algorithms to arabic numerals one can
determine the values of arithmetical functions. A logical calculus is used to
construct valid arguments. It can be described as the syntax of a logic where
syntax has to do only with the shapes and structure of expressions, not their
meanings» [x].
Transformation grammar [EML 259].
A grammar whose syntax component is split into
As primitive basis of a logistic system is suffices to give, in familiar fashion:
(1) The list of primitive symbols or vocabulary ...
(together usually with a classification ... into categories,
which will be used in stating the formation rules and rules of inference).
(2) The formation rules, determining which finite sequences
of primitive symbolsare to be well-formed expressions,
determining certain categories of well-formed of well-formed expressions
- among which we shall assume that at least the category of sentences is included -,
and determining ... which occurrences of variables in a well-formed expression
are free occurences and which are bound occurences.
(3) The transformation rules or rules of inference,
by which from the assertion of certain sentences
(the premisses, finite in number) a certain sentence
(the conclusion) may be inferred.
(4) Certain asserted sentences, the axioms.
If we look at Gentzen's Sequent Calculus, we see that a calculus can include axioms.
Calculi may be classicified according to the meaning of their symbols
into logical calculi (the same as Church's "logistic systems"),
arithmetic calculi, etc.
| more -> | linguistic glossary |
|
t1 t2 ... tn
|