Started reading: 21 August 21 8:19 pm IST
The idea of formalization of reasoning starts from the middle ages and reached its maturity in modern logic that is in Frege → Peano → Russell and Whitehead → Hilbert → Łukasiewicz → Gödel → Tarski → Jaśkowski → Leśniewski etc.
Elimination of quantifiers results in reducing whole of logic into binary algebra.
Formalization of logic effectively resulted in us pursuing inquiry into the nature of intelligence by providing us a suitable base.
Reasoning stands for deduction in this volume.
A thinking machine is an information-processing system that has a hardware component, the processing being aimed at growth of information; Information processing is found in a continuous interplay with data processing, the former being construed as operating on abstract objects (numbers, propositions, etc.), the latter as operating on physical tokes (e.g., numerals produced with ink, or by magnetization of some spots, etc.) which represent pieces of information.
Logic is the theory which deals with a special kind of information processing, namely that which preserves the truth of information.
Two sense of mechanization:
1/ Mechanization as synonymous with formalization. Formalization as in Post production systems, where you can deduce theorems through syntactic manipulations 2/ Mechanization in the narrow sense that there exists a device and a software to operate on it in order to process sentences (syntactically defined string of tokens) according to an algorithm involved in the given formalization.
Formalization or mechanization in the sense of 2/ consists in using a device and a mapping to this device of an abstract machine.
The work of Shannon in interpreting circuits as performing boolean logic allowed for the method of reducing predicate logic to propositional logic due to Skolem, Hilbert, and others which enabled the use of binary digital circuitry for mechanizing proofs in predicate logic.
One more significant step in this direction is the cut-free formalisms of Herbrand and Gentzen of the predicate-calculus. The cut is a schema representing a number of inference rules, one of them being the familiar modus ponendo ponens, whose use in a proof requires some ingenuity on the side of the reasoner to identify the premises from which the conclusion is being cut must be found.
On the other hand, in a proof produced with the cut-free formalism, each step is determined by the syntactic structure of the formula processed, hence the need for intervention is extremely reduced, and the whole procedure becomes fairly mechanical.
Gentzen demonstrated that any proof involving the cut rule can be transformed into a proof in which the cut does not appear, and this implies availability of a mechanical procedure for any proof formalized in predicate logic.
CU = <Information + Data + Machines?; Natural Machine, Artificial Machine, Selves; Rec[d,i] PrI[i,j] PrD[d,e] PrT[t1,t2,i], Cns[s1,x]>
Rec[d,i]: Piece of data d is assigned the information i. PrI[i,j]: Transforming information into pieces of information PrD: Transforming data into data PrT: Transforming Things into Things (or, a state of a thing into its another state) through a piece of information such as a dog acting to the command of a master. CnS[s1,x]: Self conscious minds. A mind is capable of being conscious of any object whatever including its own acts. This kind of consciousness is called apperception.
Information pieces are entities which are involved in the interaction between the physical world and the world of abstract entities.
What all information pieces have in common is their relation to some physical objects termed as data. The relation involved may be called expressing, representing, articulation,g, formulating, signifying, recording etc.
Verb Recording is considered standard here.
Thus an uttered (spoken or written) sentence is a physical event being a datum to record a proposition. A score, as a sheet of paper covered with notes is a datum to record a piece of music. A drawing is a datum to record the design, say of a house. A configuration of polarized spots on a magnetic medium forms data to record, e.g., a program for computer.
To some extent, the elusiveness of the notion of IP can be remedied by a certain combination of the idea of recording relation with the concept of equivalence (or abstraction class) as defined in logic and set theory.
An equivalence relation is reflexive, symmetric, and transitive. Whenever one has an equivalence relation on a set S, the set can be partitioned into a number of disjoint sets called equivalence classes such that all the members of any one equivalent class bear the relation R to each other but not to any members of S outside that equivalence class.
Cardinal numbers are defined by reference to equivalence classes of equinumerous sets. E.g., number 2 is presented as the set of all pairs. This does not mean that the terms 2 and the class of all pairs denote the same entity. It is certainly true that # > 2 but this does not imply that triples is greater than the class of pairs, hence the respective arguments of the predicate ‘is greater than’ do not prove interchangeable.
The method of introducing abstract objects through equivalence classes, as exemplified above, especially to examine relations between information-processing and data-processing. The idea to be developed is to the effect that pieces of information are abstract entities, in a way assigned to respective equivalence classes of pieces of data.
Author is trying to establish a correspondence between two chains, that of data and that of entities represented by data. The most basic is the correspondence between numeral sequences as data and numbers as entities represented by such sequences. They belong to 2 different domains. Successor operation turns a number 10 to 11 and in the codomain it turns the numerals ‘10’ into ‘11’. I think it might have been better if the author used the word encode to represent the act of transforming the semantics into the syntax.
The item represented is called an information item and the item used to encode this is called the data.
Data items are recorded in objects such as machines and organisms, and owing to these records information can be stored in objects and processed by them.
Information as the abstract entity and data as the physical entity.
Processing applied to information and data are not independent; they are so related that data-processing is a means of information-processing.
The term ‘sentence’ denote a physical object made from ink, or air waves, or electric impulses, etc. (while the terms ‘proposition’, or ‘statement’, or ‘judgment’ will never appear in this role).
Thus sentences belong to the category of data.
Information pieces recorded in sentences are called propositions, so sentences like 2 + 3 encoded in Roman numerals, Decimal, or Binary representation record the same proposition. Obviously, P is not identical with any of the members of the equivalence class E. Neither with E itself. Were it identical with E, then it would be sensible and true to say, e.g., that P contains the empty class which would be a kind of nonsense.
Then there are information pieces which are abstract entities, each of them being associated with exactly one equivalence class of data.
The notion of blind thinking (caeca cogitatio) was used by Leibniz to indicate the mechanical deduction carried out by computers without a notion of the semantics(?) of say a collection of six objects dividing into two triples.
To sum up the domain of information-processing involves numbers and the domain of data-processing involves numerals. In reasoning, the former consists of propositions, the latter of sentences.
Operation involved in data-processing are formal that is concerned with the form, or structure of strings of characters, that is data, and not with a content. About a reasoning which proceeds solely according to formal rules we say that it is formalized. Should such a reasoning be carried out by a machine, we call it mechanized.
However, there are important difference between these two domains of information-processing which are crucial for our discussion. Data-processing in the sphere of computing, i.e. mechanical calculation on numerals as representing numbers is a usual and unavoidable procedure. But data-processing in the sphere of reasoning, i.e., formalized inference, is a relatively new invention which has a clearly artificial character. Though it has proved necessary for metamathematical research, as well as useful and inspiring for philosophy of mind, it does not prove necessary for efficient reasoning.
In a formalized logical system, we have:
a and b y infer not y → not a or not base
This is natural language is:
Matter and its motion results in time and space
If matter nd its motion disappeared, there would no longer be any space or time.
Are there entirely wordless reasonings, such that they do not resort to any piece of a text? If there are, what, then, are the data to be processed? What about the principle that every reasoning is a truth-preserving information-processing, where abstract pieces of information are represented by data as physical entities?
Suppose we say that there are indeed wordless reasonings, what shall we call them? That is the class of reasonings in which information-processing is not supported by any text-processing. Let it be called the class of model-based reasonings. Another designation might be given after Popper in Unended Quest (1982) who observe that we do think in words as well as by means of schemata.
The answer in the affirmative is supported by various kinds of evidence. Due to some natural laws governing organisms, people and animals are capable of forming, e.g., internal pictures of things. Such pictures and similar devices, some of them of more abstract character, can be called models. This term enjoys sufficient generality and, like ‘picture’ involves the notion of similarity in its content.
Why should a craftsman, or an engineer try to name all the states of the engine under repair, when she seems them with her eyes, and can test her unspoken estimations with movements of her fingers? Her reasoning consists in transforming such visual and tactile data in her imagination; seh is not bound to record them in her notebook and adopt predicate calculus for their inferential processing. In a model based reasoning, the data processed are models, and those are due to records made in a code inside a processing system (e.g., a visual percept encoded in a brain).
These records are also data to represent pieces of information, while in a text-based reasoning information pieces are represented by data formed as sentences. In both cases appear pieces of information of which either truth or falsity can be predicated (e.g, the truth of a percept involved in a model), hence the difference in their representing by verbal data in one case and model data in the other does not affect the nature of reasoning as a truth-preserving transformation.
The point to be vindicated is to the effect that there are reasoning which the reasoner is not aware of, i.e., those which do not occur at the level of conscious reflexion. We shall briefly speak of them that they are not apperceived, taking the term in Leibnizian sense.
Leibniz needed the word perception to denote all acts of living individuals (i.e., substances) as reacting to certain impulses, while fully conscious perceptions were by him distinguished with the specially coined term apperception. He defined it as the reflective knowledge of an inner state, which is not given to all souls, nor at all times to the same soul.
Now the point can be stated briefly that there are unapperceived reasonings in humans and still more briefly there are covert ones. This statement is of great import for the study of intelligence. Provided it is right, the attempts to create artificial intelligence, which would be as close as possible to natural thinking, should not lead toward the text-based mechanical reasonings. Instead, artificial minds should be able to simulate model-based and covert reasonings as proving most efficient in those situations in which the subject of reasoning is not liable to be described in words, and in addition, it has to be grasped in a fraction of the second.
Model-based reasoning is unavoidable in that kind of mental activities which is termed knowing how (in contradistinction to knowing that) by Ryle in The Concept of Mind (1949), and more commonly is called ‘know-how’. This problem was tackled by Herbert Breger in Das Postulat der Explizierbarkeit in der Debatte um die kiinstliche Intelligenz (1988)
There is, actually, no mystery either in model-based or in covert reasonings, they are simply facts of every-day life. Nevertheless, there are philosophical schools such that one of them denies possibility of covert mental acts, and the other possibility of model-based reasonings. From the latter point of view, that of behaviorists, there is a mystery in the conception that some reasonings might be non-verbalized since any thinking is by them construed as an inner silent speaking.
On the other hand, a covert reasoning is regarded as impossibly by the Cartesian philosophy of mind in which the mind is identified with the subject of conscious acts.
According to Descartes, there can be no covert reasonings, as reasoning is the affair of consciousness alone: I reason then and only then, if I know that I reason. There is no necessity for reasonings - meant Descartes - to be recorded in words (hence a model-based reasoning might be admitted), but it is necessary for them to be self-conscious. This is why Descartes denied animals any capability of reasoning; he regarded them as mere automata so unable to make inferences as is unable, say, a clock.
Refer Dipert (1994) - Leibniz’s Discussion of Obscure, Confused, and Inadequate Ideas.
In the Leibnizian perspective reasoning is conceived as a kind of information-processing accomplished through data-processing, while the data are not necessarily linguistic; they may be some records in an organic machine which function as models of those pieces of reality which form the subject-matter of our reasonings.
The main mechanical-intelligence problem can be stated in the terms of processing Encoded Potential Concepts. That there do exist Encoded Potential Concepts in human bodies, is a philosophical hypothesis to motivate a research project.
An instance of EPCs on which attention of scholarly circles was focussed in recent decades is concerned with the notion of linguistic competence as introduced by Noam Chomsky; to start acquiring a language, a human being must have some innate potential notions of language, communication, predication, etc. Even if one does not endorse a materialistic point, it is advantageous to imagine those notions as encoded in our bodies, as a kind of data to be processed, presumably in the central nervous system.
An example of Socrates eliciting the idea of Pythagoras theorem in the boy’s mind is described as an example of potential concept encoded.
Besides grammatical and mathematical encoded potential concepts, there are logico-ontological EPCs which prove indispensable at the start of any language acquisition. Among them are those of a class, individual and of equivalence relation.
These 3 ideas are involved in any act of realizing that an individual object shown in the moment should represent a class to be named so and so, namely the class of those individuals which are identical - in a certain respect with that being produced (i.e., an equivalence class). No communicative act involving ostention would be possible without functioning these logical EPCs, hence they must be innate in every human individual.
A mechanized reasoning with the utmost clearness reveals that any reasoning is a truth-preserving information-processing carried out by means of data-processing, the data being entities as physical in their nature as are electric impulses, or magnetized spots, while the property of truth-preservation is revealed in the explicit application of deductive rules.
The author seems to suggest a program for achieving artificial general intelligence.
One should i) discover mechanisms of model-based reasoning in order to imitate them with artificial devices ii) furnish such devices with a set of encoded potential concepts similar to that enjoyed by humans iii) master the process of transforming unconscious, only potential ideas into fully apperceived concepts
The Formalization of Arguments in the Middle ages
The key notions in the story are those of data-processing and information-processing. The former can be entrusted to machines provided that information items (abstract objects) are represented by data (physical objects), hence the results of data processing due ot a machine can be read off by a human as results of information-processing. In a process of reasoning, the formalization consists in recording propositions (information items) as data, and in putting forth inference rules as operating on physical objects.
The notion of Llull as the forerunner of mechanization though no traces of formalization appear in his doctrine as propagated in works on history of logic and history of computer science:
Formale Logik — I. M. Bocheński (1956) Logic, Machines, and Diagrams — Gardner (1958)
Llull’s candidacy to the status of the principal predecessor of Leibniz and the initiator of the mechanization of arguments proves untenable.
It is true that Leibniz had predecessors in the Middle Ages, but these are rather to be sought in the trend that was in opposition of the Neo-Platonic orientation represented by Llull, namely in the nominalistically-oriented logica modernorum in the late Middle Ages, also called terministic logic because of its semiotic inquiries into the so-called proprietates terminorum.
Risse in his Die Logik der Neuzeit (1964) says:
“The Lull school is to be understood solely through Lull, not by reference to Leibniz. True, Leibniz owes many particular ideas to it but he organizes them in his own way. For with Lullists logic was neither primarily nor essentially connected with mathematics […] (Leibniz’s) calculus ratiocinator rooted in Vieta’s algebra speciosa, is a product of the 17th century, and ars magna played no noticeable role in it”
The opinion that Renaissance mathematicians invented variables must be taken with a grain of salt. It is not groundless to ascribe that idea to Aristotle ast he author of syllogistic schemata. Others, for instance A. N. Whitehead, ascribe the principal merit to Archimedes. When it comes to such a sophisticated concept one may assume in advance that it was developing for centuries stage by stage, and whichever stage is taken to be the turning point in that process, the decision will always be arbitrary.
Dissertation de arte combinatoria in qua, Arithmeticae fundamentis, Complicationum ac Transpositionum Doctrina novis praeceptis exstruitur, et usus ambarum per universum scientarum orbem ostenditur; nova etiam Artis Meditandi seu Logicae Inventionis semina sparguntur. Prefixae est Synopsis totius Traclatus, et additamenti loco Demonstratio existentiae Dei ad Mathematicam certitudinem exacta. - Leibniz (1646)
The problem of a certain formalization of arguments was for centuries discussed in terms of the logic of discovery, and hence in terms of processes which we now treat as typically creative and not subject to mechanical procedures.
That was due to a combinatory interpretation of the process of discovery, which involved finitism and formalism. Finitism because effectiveness requires that the number of combinations be finite. Formalism because combinations must be carried out on some discrete object that can be unambiguously identified; these conditions are in a model way satisfied by material symbols owing to their visible shapes (or forms, hence the term ‘formalism’) and discrete arrangement. That finitistic formalism started in the late Middle Ages and culminated in the 17th century.
The position of theory of reasoning in the structure of traditional logic. Tripartite ordering schema ordered by singling out three hierarchically arranged operations of the mind:
Fundamental operation: Grasping things by concepts. Simplex apprehensio. It is the simplest one in the sense that in that part of the act of grasping thing which occurs at the level of consciousness, and so is accessible to introspection, we do not perceive any components that could be clearly isolated.
The second operation of the mind, second in the sense that it assumes the existence of concepts and is more complex than conceptualization, is the formation of judgement. According to Lullistic logic, nad scholastic logic in general, it consists in the combination of concepts into a judgement (judicium). This had suggested to Llullus the idea of a combinatorial procedure of generating judgements.
This is said to be an Utopian plan because in the construction of sentences we can admit predicates with an arbitrary number of arguments; and the imposition of any constraint upon the number of arguments would either be conventional or appeal to intuitions that are far from being mechanizable.
A judgement was treated as an invariable tripartite structure consisting of the subject, the copula, and the predicate, the copula expressing either affirmation (‘is’) or negation (‘is not’). This is how a judgment (protasis) was understood by Aristotle. For a properly limited dictionary of terms (i.e., expressions which can function as either the subject or the predicate) this yields a realistic algorithm to produce the list of all possible judgements. From such a list one would then have to choose those judgements which are true and as such are suitable as premises of those syllogisms that are to yield truth. Today we find it difficult to imagine what algorithm which is not a proof (because the proof, e.g., a syllogism, comes later as the operation that is next to the formation of judgments) could be constructed for that purpose: empirical truths are beyond the reach of any algorithms whatever. The point is, however, that for the representatives of the Platonic-Aristotelian views (which came to be opposed by modern empiricism) truth in the strict sene of the term was identical with necessary truth or (approximately) analytic truth, that is, the glorified logic of discovery, ars inventionis, which preoccupied many outstanding minds in the Middle Ages and the Renaissance until 18th century.
The third operation of the mind, the most complex one in the sense that it assumes the two preceding ones and brings the most complex product, consists in the proof, construed in the Aristotelian logic as a syllogism. This identification of proofs with syllogism in that tradition is essential for the present discussion because syllogistic combinatorics, which is the foundation of mechanization can then be identified with the theory of proof taken as a whole, which would allow one to conclude that all proofs can be mechanized.
By a proof Aristotle means a syllogism that creates scientific knowledge. Hence if knowledge is such as we have stated, then the premises of demonstrative knowledge must be true, primitive, direct, better known (than the conclusion) and must be its cause.
According to Aristotle’s interpretation the difference between a proof and a syllogism is epistemological and not formal logical in character: a proof is a syllogism hose premises meet the epistemological conditions of scientific knowledge (episteme) as distinguished from common belief (doxa). Hence in science there are no proofs other than syllogisms, even though not every syllogism is a proof. Thus syllogistic exhausts the whole formal logical part of the theory of scientific proofs to which, in Aristotle’s intention, his Prior Analytics (concerned with formal logic) and Posterior Analytics (concerned with methodology of science) were dedicated.
Someone who knows the history of Greek and later mathematicians might object the point that logicians of that time identified a proof with a syllogism. They must have known the procedure employed in proofs by Euclid and other mathematicians which hardly resembled syllogistic forms. If so, why did they claim that every proof should be a syllogistic inference?
Nowadays it is well-known fact that syllogistic can be interpreted in the monadic predicate calculus which is a decidable theory. This fact may have been intuitively sensed in practicing syllogistic inferences, and together with identifying the whole of logic with syllogistic that might have led to the belief in the possibility of mechanizing all reasonings. This belief seems to have been favoured by other factors in the cultural context in which logic existed for two millennia. That context involved two philosophical tendencies, namely finitism and formalism.
In the Greek philosophy of mathematics finitism established its place for good owing to the paradoxes of Zeno of Elea (490-430 B.C.) which showed how formidably perplex are the problems resulting from the concept of (actual) infinity. That was reinforced by the authority of Aristotle who in his Physics and Metaphysics advanced arguments, to be later repeated for centuries, against the existence of actually infinite domains. The opinion was also represented in antiquity by other schools (TODO: Research which ones held to this idea) but Aristotle’s voice sounded more loudly, especially when supported by Christian thought: the major part of his representatives reserve infinity for the Creator alone while denying it to the creature. The finitist camp included such influential authors in Christian antiquity as Origen (185 – 254), with whom centuries later Cantor himself would engage in vehement disputes, Proclus of Constantinople (410 – 485), an influential commentator of Euclid, and - in the period of the flourishing of medieval philosophy - Thomas Aquinas (1225 – 1247), the greatest Christian Aristotelian.
That camp did not include Augustine of Hippo (354 – 430), but his standpoint, voiced only in connection with other problems and hence likely to be overlooked, was fully understood probably only by Cantor (who sought in him as ally in polemics with contemporary theologians).
Thus the intellectual climate in which the Lullists were active favoured finitism. The view which implied the finiteness of both the domain of individuals and the set of concepts provided people with reasons to postulate the decidability of the system of human knowledge. True statements would be deducible from a finite set of first principles (as Aristotle claimed), and false ones would be refutable by demonstrating that they contradict those principles.
The ideas of the potential infinity of human cognition, of the limits of verbalization, of the approximative nature of scientific theories, and the like, have become familiar to the modern mind only recently.
As long as it was believed that concepts and judgements had adequate mappings in language, on the one-to-one basis, there were reasons to believe that thoughts could be fully replaced by words, and these, being material objects, could be processed mechanically.
Augustinism opposed Aristotelianism both by its infinitism and its doctrine of illumination, which stressed the intuitive, non-mechanizable elements of cognition; that tendency even more manifested itself in the gnostic movements. But as for the problems with which we are concerned here the essential point is that both the finitistic and the formalistic trend were firmly rooted in the medieval thought.
Inventio medii: The problem of finding the middle term.
It was typical of logica inventionis, that is, the logic of discovery, postulated also by Lull, who wrote, among other things, the treatise entitled Ars inventiva veritatis.
Averroes (1126 – 1198) one of the greatest Arab Aristotelians, was the first medieval author known to have coped with the issue. On the other hand, Albert the Great (1193–1280) was the first who, following Averroes, assimilated that problem to Christian scholasticism. Albert’s another merit consisted in that he took up, after the Arabs, combinatorial investigations concerning the number of all possible syllogistic structures in order to find all possible correct syllogisms. A similar combinatorial approach can be found in hte Jewish logician named Albalag, who was a contemporary of Lullus and like the latter was active in northern Spain. As can be seen, when it comes to the combinatorial approach, Lull was by far not the first among the schoolmen, and if he did not take that problem for instance from Albert the Great, then he must have most probably owed it, as Albert did, to the Arabs.
Dzieje filozofii europejskiej w XV wieku. Tom II: Wiedza - S. Swiezawski (1974)
Among the authors who took up those problems after Albert the Great special mention is usually given to George of Brussels and Thomas Bricot. They belonged tot he nominalistic trend in the 15th century (logica modernorum), which had originated with he great Oxford masters, William of Ockham and Richard Suiseth, whose teachigns transferred to the Continent by Paul of Venice took strong roots at the universities in northern Italy and central and eastern Europe, including Prague, Cracow, and Leipzig.
Thomas Bricot presents a sort of algorithm on how to find the middle term. The full set of such rules in the form of a graphical schema, nicknamed pons asinorum, was given by Petrus Tartaretus in his commentary to Poryphyry’s Isagoge and to Aristotle’s logical writings; the diagram itself is supposed to have been constructed ca. 1480. The term ‘bridge of asses’, to this day preserved, oscilattes between two meanings. Tartaretus himself, in his desire to prevent his students from experiencing anxiety in view of the complexity of the diagram, explained that such anxiety would be as groundless as that which is felt by asses which are to enter a bridge, because that diagram is to ensure a safe passage, and not to render it difficult. In the other meaning, until today to be found in dictionaries, one takes into consideration the feature of facility which marks algorithms, that is, mechanical procedures that do not require inventiveness on the part of the user, and as such are manageable even by proverbial asses.
The picture that emerges from the foregoing overview does not confirm the opinion about Lull’s role in shaping the idea of the mechanization of arguments. The key role was played by late medieval nominalists with their definitions of logic as pertaining to terms, and hence physical objects on which mechanical operations can be performed (note in this connection that the leading nominalists, such as Ockham, Suiseth, and Buridan, were also forerunners of modern mechanics). It was nothing else than terministic logic, that logica modernorum which formed the main link between Aristotle (whose texts admit a “terministic” interpretation but do not forejudge it) and Leibniz, who, after having found himself, together with his Leipzig masters and Thomas Hobbes in the sphere of nominalistic inspiration, transformed it in his vision of logic embedded in a mechanism.
There was vehement polemics with Aristotelian and scholastic logic which took place in the Renaissance and the 17th century. What strikes us today as the value represented by the formalist wing of logic, namely the approch to possible mechanization, was severely criticized, at first by numerous humanists, who postulated that logic should “come closer to life”, the postulate marked by their practical and psychologistic attitude, typical of rhetoric.
At the same time there was criticism in the vein of Francis Bacon, which demanded that logic should discover hard natural facts ad not mere terms (such as the middle term to be found with medieval recipes).
In the 17th century, in turn, the formalistic trend had its main opponents in Descartes and his followers, who ascribed to logic the role of the healer of minds. According to that programme logic was to protect human minds against deviations, including the scholastic and formalistic ones, and to make them capable of finding the truth. In that respect it also deserved the name of logicae inventionis, but in a new sense, namely that of Cartesian rules for the seacrh for the truth with the natural light of reason, which formed a certain linkage to the Platonic/Augustinian tradition with its key concept of illumination.
One could hardly deny the pertinence of Cartesian criticism when it was aimed att he triviality and sterility of such formal systems of rules as pons asinorum. In fact, an acute human mind never makes use of them in its search for the truth. Today we realize even better than the Cartesians did that inventive intuition is what can never be mechanized. Hence, should the only task of logic consist in the guidance or reinforcement of human minds, one could, and even had to, agree with the Cartesian critique of scholastic formalism. Yet it turned out, and that just in our century, that logic can be used to mechanical processing of knowledge.
Bridge of asses refers to the relations of inclusion and mutual exclusion which is present in the extensions of the term involved in the thesaurus of a language with a grammar and a vocabulary. ALl this is, self-evidently, the same as the formulation of a certain axiom system of language, that system playing the role of axiomatic rules in the sense as understood by Ajdukiewicz in Sprache und Sinn (1934). The axioms in that system should be independent of one another, which makes the system desirably economical. Endowed in this way the computer becomes a master of ars inventionis in the sense of scholastic formalists, for it can faultlessly find the middle term required in the proof of a given thesis. It will do that by searching the vocabulary and accepting for a given proof those terms which bear to one another extensional relations required by the rules of the bridge of asses.
The term ‘follows’ in it being interpreted in the sense of set theoretical inclusion. This makes me think of filters in lattice theory, where an ultrafilter stands as evidence for weaker truths above it.
For our discussion it is of minor importance that the formal apparatus of scholastic logic is so limited as compared with the needs of the automatic processing of knowledge. The essential poitn to be seen in the similarity of programmes, which makes us understand the rules of logic as rules of operations on physical objects of a definite form (hence formalism) which at the point of departure constitue a discrete and finite set (finitism). That approach to logic, which may be read between the lines in Aristotle, was consciously taken by medieval formalists, and then developed by Leibniz and (independently of him) by later authors, especially by George Boole; it was Boole likewise Leibniz from whom Frege took the idea of his logical enterprise.
Frege’s 1880/81 manuscript contains a comparison between Leibniz’s, Boole’s and his own approach.
Ramon or Raymundus Lullus was born in 1232 in the capital of Majorca, an island recovered from the Arabs in 1229 by the Catalan army led by Jacobus I or Aragonia.
Lull’s famous invention discussed in the history of logic was called ars magna by himself. It covers a certain technique of forming judgements and also something which might be compared to an axiomatic system in the field of philosophy and theology.
Most formal part of Lull’s art, which might be termed combinatorial syllogistic, is to be found earlier in Albert the Great; the latter took it over from still earlier Arab authors, and the problem originated with Aristotle who asked about the way of finding the middle term. The fact that Lull’s thoughts were imbued with that methodology can be sufficiently explained by his being versed in Arab logic, which he presented in his earlier writings, such as Logica del Gazzali (the Catalan version of the name of an Arab logician), written by him in Arabic and translated by himself into Latin and Catalan.
The core of the argumentation of Lull in the most concise form is tob e found in the discussion which he had with an Arab dignitary during one of his later missionary travels (the discussion ended in Lull’s imprisonment at the moment when his Arab opponent ran short of arguments).
Lull had earlier agreed with his opponent that their discussion would take as the starting point the common belief in goodness as one of the principal attributes (dignities) of God. The belief that God has all those attributes was part of the common heritage of both Christian and Arab metaphysics of those times, shaped in the Neo-Platonic melitng pot. By departing from that common point Lull argued in his discussion, like in every other one in which he engaged, that in accordance with the Neo-Platonic principle (also common to his opponents) bonum est diffusivum sui, the goodness of God must spread of necessity. If that diffusion did not consist in giving rise to the second and third person of Trinity, then God would have to manifest himself only by the creation of the world, and then the manifestation of his goodness would depend on something which is not necessary, and hence imperfect and thus unworthy of God. In his first speech in Tunisia Lullus expressed that by saying that without the internal activeness within the Trinity God’s dignitates, including his goodness, would be idle and hence would not be as perfect as it becomes the Absolute.
It is pointed out in the book that the reasonings one derives out of the judgement could be both correct and wrong ones as there is no mechanical procedure of verification of certain formations as deriving only the true statements in Lull’s Ars Magna.
By bringing in a combinatorial exhaustion of the space, Lull intended for his machines to allow to reach those combinations which are fundamental and natural, their truth being grasped with “the natural light of the mind” (to use the Cartesian phrase, which is due to the same Augustinian tradition).
In a sense, the procedure like that may be interpreted as the search for a third term. In a debate, say, one denies that human acts are subjected to deterministic causation, hence are not free, and in order to prove his point one resorts to the concept of divine concurring as one that yields the middle term. Thus one argues: “Every act of human will is supported by divine concurring; every act supported by divine concurring is free, hence every act of human will is free.” Note, however, that this kind of pursuing the third term is quite a different thing than that prescribed, e.g., for the pons asinorum procedure. No rules of the formal correctness of an argument are at stake but merely a heuristic device to activate memory, and so to find a concept which otherwise might have remained unnoticed. Once noticed, the concepts in question are perceived as connected in a necessary way, on the basis of an intellectual intuition. This should put an end to the legend of Lull as an author of a program of arguments mechanization.
In Part XIII, the last one, in which the method of using the Art is discussed, we find an advice for the teacher that he should make it plain to his disciples that the Art cannot be used without recourse to its close companions, that is, the reason, the subtlety of intellect, and good intentions. In particular, the reference to good intentions, which is by far not incidental but results from Lull’s mystical attitude, disproves the claim that Lull’s Art, as a theory of argument, was a medieval anticipation of the program of algorithmization or mechanization of proofs. Even if there were such anticipations of formalistic approach to reasoning in Lull’s times, they are to be sought (as shown above) in the nominalist, i.e., terminist trends, and not in his intuitionistic doctrine.
A promising way to gain them starts from reading Leibniz’s dissertation De arte Combinatoria in which Lull’s project appears in a very wide spectre of similar enterprises, all of them grown in the same culture of syllogistic; in that culture the reduction of logic to certain subject-predicate forms created the illusion of the decidability of all problems through exhaustive combinations of subjects and predicates.
Thus the said title proves symptomatic of that philosophy of knowledge, and of the resulting research programmes, which started with Aristotle, and did not entirely disappear until the scientific revolutions of our own century (quanta, relativity, evolutionistic cosmology, Gödel limitative theorems). When taking advantage of the cosmological concept of stationary universe (as opposed to the evolving universe), and linking it with the familiar logical idea of the universe of discourse (as the totality of the things under study i.e., those represented by variables), we can introduce the analogical pair of notions: that of the stationary universe of discourse and that of the evolving universe of discourse.
The combinatorial approach is associated with the vision of the stationary universe of discourse, in which the set of concepts forming our knowledge, and thus constituting the universe of discourse, is definitely fixed and closed. Then the whole cognitive enterprise would consist in searching for those combinations of members of the universe which yield true propositions, while logician’s task would involve providing people with a proper method of doing that. It was just the programme of the famous logica inventionis as mentioned in the subtitle of De arte combinatoria. The combinatorial approach, though, turned out quite sterile as far as the development of knowledge is concerned, since the universe of discourse of scientific theories rapidly expands as ever new concepts appear, and that would require ever new recombinations.
On the other hand, the combinatory strategy is fairly suitable in the problem-solving as carried out by computers. It can be seen in the mechanical checking of a proof, where each formula has to be resolved into its atomic components being combinatorily surveyed in order to detect inconsistencies among them, if there happen to be any.
The author whom Leibniz praised most is Thomas Hobbes to whom he owed the idea that every mental operation consists in computing.
The author divides the components of analysis of Lull’s merit to the claim of being a pioneer to computation into: combinatorial and formalistic. It is said that while formalistic is to be given more significance in assessing Lull’s role (by which Lull hasn’t anything much novel), Lull’s combinatorial aspect should not be entirely disregarded.
Nevertheless, the combinatorial aspect should not be entirely disregarded. It played a crucial role in the erroneous belief in the stationary universe of discourse, i.e., that human knowledge can be definitely and safely established by combinatorial procedures. That human brains were mistaken for computers in those ages in which nobody dreamt of the latter, it was one of those errors which paved the way to new understandings.
Leibniz’s Idea of Mechanical Reasoning at the Historical Background
Since Aristotle up to our times, and specially in the 17th century, logic was addressed to human beings to improve their intellectual performances. Those intentions notwithstanding, the most important final result of that process, which started with the rise of logic, consists in the invention of reasoning machines. That human minds can do without a logical theory, when relying on their inborn logical capabilities alone, is obvious when one observes the history of discoveries and other manifestations of creative thinking. But the mechanical mind’s inference are due to some devices for which a logical theory forms an indispensable foundation.
The possibility of mechanical reasoning depends on the existence of what we call the logical form of a linguistic expression, that is to say, a structure determined by those terms which are relevant to logical validity. When a reasoning is so formulated that its validity can be recognized on the basis of its form alone, we call it a formalized reasoning. It may be called mechanized as well, but in a broader sense, namely that a mechanical procedure, i.e., one that does not appeal to our understanding of the content, is sufficient to judge the validity.
When we take the term ‘mechanized’ in a strict meaning, then formalization is a preparatory step towards mechanization. The latter consists, so to speak, in expressing the logical form in a language of physical states subjected to some causal laws of physics, be it mechanics (as, e.g., in Babbage’s machine), be it the domain of electronics (as in modern machines). Thus hte logical operations is identified with physical processes occurring in a machine, and this, let us repeat, yields the mechanization of reasonings in the strict meaning. This explaining of the role of formalization of reasonings as crucial for their mechanization should make obvious why so great import is attached to the former in the story being told in this volume.
The merit of founding logic goes back to Plato and Aristotle, the former as the one who discovered logical validity, the latter as the discoverer of how that validity depends on logical form.
As for Plato’s contribution, the core of Socratic method of argument, as presented in Plato’s dialogues, consists in discerning between the truth of a statement and its being deduced with a valid inference. In a typical argumental dialogue, Socrates helps his interlocutor to deduce some consequences forme a view which the partner claims to be true. When, nevertheless, the consequence proves falso, the partner is bound to acknowledge the falsity of his initial view; this reveals how the validity of an argument can be independent of the truth of its premises. Such is the constant strategy of Socrates, though no attempt is made to theoretically justify that practice.
To justify it, one should have resorted to the form of the sentences involved in an argument. This was done by Aristotle by introducing letters to represent variable contents (subjects and predicates) while the form, rendered by expressions as ‘every … is’, ’‘is not’, etc. remains constant. Though originally there was no direct translation of that form into physical states of a machine, the later development from syllogistic to Boole’s algebra of classes, and then the transforming of the latter into Frege’s algebra of truth functions, and next the invention of the method (due to Claude Shannon) to represent truth-functions by some states of an electrical device, has led to the nowadays mechanization of reasoning.
In spite of its appearance of mechanical (because of the rotating wheels) Lull’s art was no step toward mechanization of arguments, for it did not involve any thought of mathematical operations. It was Hobbes who perceived an analogy between reasoning and computing, and then it was Leibniz who enthusiastically endorsed the idea and contributed to its accomplishment in an algebraic manner. This is why Leibniz so appreciated the idea of logical form as found in some medieval students of syllogistic, as akin to the form of algebraic calculations.
There was methodological feedback between logic and geometry consisted in the fact that the ideas worked out in logical theory used to pass to the praxis of geometricians, who in turn provided logicians with the best patterns of proofs. Aristotle, when writing his Analytics, drew from the interpretations of geometry that were known to him the pattern of necessary knowledge and reliable inference, while Euclid, when writing his Elements half a century later, availed himself of the methodological concept of common axioms that is, those that are not specify, say, to geometry, but are drawn from some more general theory; note in this connection that the Aristotelian example of such an axiom — “if equals be taken from equals the remainders are equal” – occurs on the list of axioms in the first book of Euclid’s Elements.
When arithmetic and algebra, born in Babylonia, met in the Hellenistic period with Greek geometry and logic, they gave rise to that gigantic ‘tree of knowledge’ of which our civilization is the fruit. Arab scholars made great achievements in the development of algebra, continued by European scholars.
The realization of the breakthrough manifested itself in the birth of the term analytica speciosa to single out mathematics using such notation that one symbol does not correspond to a single object but to a class or species of some numbers. It was Descartes who became the coryphaeus of that analytics when in 1637 he published his Geometry, to which Discours de la méthode was the annex; in this work he gave a synthesis of geometry with algebra or analytics.
Owing to the maximal generality which the notation using letters gave to algebra, Leibniz was in a position to realize that al etter need not refer to a class of numbers, but can refer to any class of objects of any kind. The use of letters was invented for logic already by Aristotle, but only the successes of algebra could give birth to the idea of an algebraic treatment. That was one of the greatest of Leibniz’s ideas concerned with logic. It was partly materialized by himself, but it was first published in print two hundred years later, after the same discovery had been made in he meantime by other authors.
The permanent imprint of algebra upon the mentality of people living in the 17th and 18th century consisted in their experience of how an appropriate language renders thinking more efficient and signally contributes to the solution of problems. This fact played its role in the development of a movement for improving the whole language of science.
The second discovery of the algebra of logic took place in England in the mid-19th century, and was due to a Pleiad of prominent algebraicians, of whom George Boole rendered the greatest services to logic. He was helped in that respect by the then nascent comprehension of the abstract nature of algebra, which is to say that an algebraic theory does not refer to any specified domain (which was particularly emphasized by George Peacock). Algebra can, find application or, more precisely interpretation, in a class of structurally similar domains that can be described with the means provided by a given algebraic theory. In this way algebra, after having developed from the old science of solving equations, has become the most general theory of structures, that is systems of objects for which certain operations are defined. Such operations are described from the point of view of their properties, e.g., commutativity or its lack or the performability of operations with a neutral element (such as zero for addition in a certain algebra having an interpretation in the arithmetic of natural numbers), and the like.
One of the interpretations of this calculus called Boolean algebra corresponds to that part of logic which is known as the truth-functional calculus. The same algebra has another interpretation in tradition syllogistic, and it was just that interpretation which was so penetratingly anticipated by Leibniz.
Boolean algebra can be interpreted arithmetically, the domain of natural numbers being limited to zero and unity. It can also be interpreted in many other ways, but two interpretations, one in the domain of logical sentences, and the other in that of sets, are fundamental for logic.
In the domain of sentences, multiplication is interpreted as the linking of sentences by conjunction (and); complement is interpreted as the negation of a given sentence: 1 as truth, 0 as falsehood. If a formula consisting of those symbols and variable symbols standing for sentences is always true, that is, if it is true regardless of whether truth or falsehood is assigned to the variables which occur in that formula, then it is a law of logic and belongs to the logical theory termed truth-functional, or sentential, calculus.
When interpreting Boolean algebra in the domain of sets (which traditionally were referred to as extensions of names) we can in a natural way express the four traditional kinds of categorical sentences, which form the building material of syllogisms.
Every A is B: A * not B = 0 No A is B: A * B = 0 Some A is B: A * (B + 0) ? or A * not B notEqual 0
Such a translation of traditional logic into Boolean algebra enables us to activate a strong deductive apparatus of algebra for obtaining economical and elegant proofs of the theorems of traditional logic.
The anticipation of that interpretation, to be found, in Leibniz’s treatise entitled Generates inquisitiones de analyst notinum et veritatum (inquiry into a general theory of concepts and judgements), differs from the modern form mainly by the fact that in place of the symbols notEqual 0 it has the Latin phrase est ens i.e., ‘is an entity’ (or ‘exists’), while the symbols = 0 have the analogue in ‘non est ens’ i.e., ‘is not an entity’ (or ‘does not exist’). These phrases can be interpreted in at least 2 ways: as stating the existence of objects which are the extension of a certain concept, i.e., a certain set (extensional interpretation), or as stating the existence or non-existence of combinations of properties, i.e., the intension of a certain concept (intensional interpretation). Leibniz himself was open to both interpretations; he valued the extensional one as technically effficient, but believed the intensional one to be better because of certain philosophical considerations. The idea of the translation of a sentence consisting of subject, copula, and predicate, such as “every man is intelligent” into an existential sentence of the kind “non-intelligent manhood does not exist”, was of scholastic provenance, to which Leibniz clearly referred. The brilliance of his own idea consisted in noticing an analogy between such sentences and equations of the algebra he had formulated (which included the operation of linking concepts and negating a concept). In those equations on the one side we find such a combination of concepts (one of which may be negated), and on the other, one of the two ‘magnitudes’ expressed by the terms ‘ens’ and ‘non-ens’.
The founders of the algebra of logic, that is G. W. Leibniz and G. Boole, and also A. De Morgan, E. Schröder, C. S. Peirce and others were convinced that the whole of logic can be contained in algebraic calculus. They were also aware of the fact that traditional logic, even after its algebraic reconstruction, lacked the means required to describe relations (for instance, it was impossible to render in its language even such a simple relational sentence as “for every number there is a number greater than it”). That was why the next stage was to consist in adding the algebra of relations to the already existing algebra of sets (i.e., the analogue of the traditional theory). These new researches, carried out mainly be De Morgan, Schröder, and Peirce, gave rise tot he theory of relations, which became an important and indispensable discipline in the border area between logic and set theory, but its language (combined with that of the algebra of sets) did not suffice to express mathematics in its entirety, either.
The 19th century, regardless of the intentions of the various authors, witnessed the need, and at the same time the possibility, of constructing a universal symbolic language of mathematics in which well defined symbols and precise syntactic rules would replace the vocabulary and syntax drawn from natural language.
At the turn of the 19th century, logic entered a new path by providing mathematics with a universal and rigorous symbolic language, which had also far-reaching (though not universal) applications in other disciplines and in everyday discourse. For that to happen the 17th century program of a universal language had to be revived, which did take place owing to the publication for the first time, in 1840 by J. E. Erdmann of some logical writings of Leibniz which formulated the program. There were three founders of contemporary logic, independent of one another when it comes to ideas even though they had intensive contacts with one another: Gottlob Frege, Giuseppe Peano, and Bertrand Russell. All of them referred to Leibniz’s ideas, and two of them believed themselves outright to be the executors of his testament by carrying out his programme of universal language.
Frege in 1879 published a work which presented the whole of contemporary logic (i.e., the sentential calculus and the predicate calculus) under the title Begriffsschrift, meaning conceptual writing, and can in Latin be pointedly rendered by Leibniz’s term ‘characteristica rationis’.
When new logical calculi developed at the turn of the 19th century, namely the predicate calculus (which overcame the limitations of algebra) and the sentential calculus (which may be treated as a certain interpretation of Boolean algebra), new vistas were opened to the logicians. On the one hand, it was now possible to develop and improve the calculi themselves by formulating ever new versions and by constructing other calculi themselves by formulating ever new versions and by constructing other calculi that could be superstructed upon the former (such as modal logics). On the other, since those calculi abounded in problems to be investigated, it was also possible to pose questions about the consistency of each of them, their completeness, the purposes they could serve, the relations among the axioms and concepts of a given system (the problem of independence), and finally the relations among the various systems (the interpretability of one of them in terms of another, the consistency of one of them on the assumption of the consistency of another, etc.). Precisely the same questions can be posed about mathematical theories. Among these, the arithmetic of natural numbers is of particular importance from the logical point of view, because the remaining branches of mathematics can in a way be reduced to arithmetic.
Thus, when at the world congress of mathematicians in 1900, David Hilbert presented the mathematical community the task of proving the consistence of mathematics (in view of the antinomies discovered at that time), it was known that it would suffice to concentrate on the problem of the consistency of the arithmetic of natural numbers using for that purpose the logical apparatus, both that which was already known at that time and that which was still to be created. We owe to Hilbert the term ‘metamathematics’ to denote such studies. They were carried out intensively in the period 1920s – 1930s and brought out astonishing results due to Hilbert’s companions as well as critics such as Herbrand, Gentzen, Turing, Gödel, and Tarski.
As metamathematics developed, it was more and more penetrated by mathematical concepts and methods as indispensable instruments of research. They were in particular drawn from arithmetic (e.g., the use of recursive functions initiated by Gödel), algebra (e.g., Tarski’s algebraic approach to non-classical logics), topology and set theory.
The development of all ideas, and hence also that of logic in the 17th century, is immersed in the melting pot of general civilizational development, in the cultural ferment of the period. The century which will be described here brings out with particular clarity the fact that the masterpieces of intellect grow from the roots of tradition but also from a lively dialogue with the milieu that is contemporaneous with their authors. And that milieu means not only congenial individuals, but also the audience consisting of readers, disciples, opponents, snobs etc., in a word, the entire enlightened public.
During the 17th century, the demarcation line between scientists and craftsmen was liquid at that time, which is illustrated by the large number of craftsmen in the London royal Society, the greatest collective authority in science of the period.
There was one more heritage of the Renaissance from which the 17th century benefited, namely Pythagorean and Platonic philosophy, from its earliest beginnings most closely intertwined with mathematics. The Platonic trend was always present in European thought, especially from the time when it was reinforced by the idea of Plotinus and in that new form, called Neo-Platonism by historians, established contacts with young and vigorous Christendom, in both its orthodox version and that marked by the influence of gnosis. A significant example of that synthesis can be seen in the person of Proclus of Constantinople, one of the widest known commentators of Euclid and a Platonizing theologian, to who ideas Kepler used to refer. The first Christian writers and Church fathers were as a rule Neo-Platonians. This applies also to the greatest of them, St. Augustine of Hippo, whose ideas were truly reincarnated in the 17th century in the work of Descartes, Pascal, and the milieu of Port Royal, and in the late 19th century came to the rescue of Georg Cantor, the authority of the theory of infinite sets, in his clash with the philosophy of mathematics that followed the Aristotelian approach to infinity.
Marsilio Ficino, Nicolaus, of Cusa, Leonardo da Vinci, Nicolaus Copernicus, Galileo Galilei, Johannes Kepler all endorsed Platonic vision of the world.
In the 17th century two vast currents, one of them linked to technology and economics and ideologically based on the catchword ‘the kingdom of man’, and the other permeated by Platonic metaphysical speculation. Both influenced logic when postulated that logic should give the human mind an instrument whereby it could arrive at the truth. While they had one and the same goal in view they disagreed as to the method of reaching the truth: the former staked on induction, whereas the latter, preoccupied iwth mathematics in the Platonic manner, postulated a purely deductive method (more geometrico).
The idea of reform logic developed in the 16th century; and the 15 century was still busy with commenting the classics, namely Summulae logicales of Petrus Hispanes (as Pop he was known as John XXI), and later achievements, such as those dating from the 14th century. A special merit for that continuation went to Paul of Venice, whose Logica Parva continued to be taught at many universities for two centuries to come. A certain logical idea of Paul of Venice in his Logica Magna found its way to the writings of Leibniz and came to play a certain role in the development of extensional logic.
The history of the reform of logic begins with Peter Ramus, remembered as a vehement opponent of Aristotle who he blamed for being unnatural in his approach to logic. Nevertheless, he took over a great deal from Aristotle, namely the theory of definitions, the theory of judgment, and the theory of inference. Two things made him differ essentially from Aristotle, but one of them was in the sphere of programmes (in which one can relatively easily become an innovator), and the other has its source in age-old tradition, but not the Aristotelian.
In his programme Ramus included the requirement that logic be adjusted to natural human thinking, without that artificial abstractedness for which he blamed Aristotle. His followers took up those slogans, and for the two centuries that followed we find in the title of numerous logical compendia various psychological terms connected with the conception of logic as the science of living human thinking and not of any abstract entities.
Port Royal logic is the best known titles of this kind. Others are Tschirnhaus’s Medicina mentis sive artis inveniendi praecepta generalia, Christian Thomasius’s Introduction ad Philosophiam Aulicam. The same may be said about the title of the work written by Wolff, a philosopher who at first was an adherent of the Cartesian school in logic, and hence an opponent of syllogistic, but later, under Leibniz’s influence, became an advocate of syllogistic.
The psychologism in logic was terminated(?) only in the late 19th century by the concentrated attack against psychologism in logic from the position of the mathematically-oriented philosophy of logic (G. Frege, E. Husserl, J. Łukasiewickz, and others).
Another novelty relative to Aristotle’s ideas consisted in the division of logic into the science of judgments and inference and the science of making inventions, in which much space was dedicated by Ramus to definitions (the connection between the method of making inventions and the formulation of definitions will be fully seen in Leibniz0. it was not an absolute novelty, because such a division was introduced by the Stoics more than dozen centuries earlier and was transmitted to the Middle Ages by Boethius, but turning it into the principal claim which fitted with the aspirations of the epoch was the work of Ramus.
When it comes to Francis Bacon, not only one half of logic but the whole of it was to consist, in his opinion, in the art of making discoveries which would pave the way for the kingdom of man. Bacon designed a logic of induction, which was totally to replace the existing logic of deduction. The characteristic feature of deduction is that the conclusion does not contribute any information that would not be contained in the premises: it cannot convey more information than the premises do. He was not the only one to attack logic in this way, because a whole chorus of critics, among whom the voice of Descartes sounded loudest, blamed syllogistic (the only theory of deduction universally accepted at that time) for not contributing anything new to our knowledge. But while Descartes and his followers wanted to replace syllogism by another deduction, modelled on the experience of mathematical thinking, whose creative character would not be questionable, Bacon, guided by an empiricist ideology, failed to perceive such an alternative solution. Hence, if logic was directly to serve the expansion of human knowledge, he had to stake everything on the inductive method. But at that infantile stage of the logic of induction people failed to realize that for an increase of information one has to pay with a decrease of certainty, or, to put it more precisely, a lessening of probability which has certainty as its upper limit. This is so because a general law is intended to be a conclusion drawn from observations to infinitely many possible cases, and therefore tells us more than the observations refelected in the premises, which always cover finitely many cases. But it uncertainty which is the price paid for such an increment of knowledge, because while Nature may to a given moment confirm that general conclusion, there are no reasons to be sure that it will confirm it in each subsequent case.
If this is so, then the logic of induction is not any alternative solution to the logic of deduction but can at most be its complement (which, by the way, to this day is still in a stage of planning, rather than in that of achievement).
The greatness which logic was destined to attain (?) and which it did attain in our century, was reached by the old Aristotelian road when it merged with the path along which mathematics was developing.
The problem of how logic should be is not merely a matter of logical theory. It deeply penetrates the philosophical vision of the world and the mind. Bacon’s design for a reform of logic originated from the empiricist conception of cognition which ascribes to the human mind the role of a passive receiver: it is like a screen on which Nature casts the image of itself through the objective of man’s sense organs, and if the mind is active in any respect then only by posing questions to Nature.
Such empiricism is opposed by apriorism, also termed rationalism (in one of the meanings of that word), which states that there are truths which man comes to know before all sensory experience; they are given to him as it were in advance. In that sense, reason (Latin ratio) is independent of experience. According to the rationalists, the essence of cognition consists in the realization by the human mind of those truths, given it a priori, which are general and necessary. Premises drawn from sensory experience and experimental data may be helpful in that process of deduction, but they never suffice to lay the foundations of our knowledge. Hence logic as an instrument of cognition, interpreted in the rationalist sense, must be a logic of deduction which not only serves the presentation and ordering of the truths that are already known but it can also lead one to discoveries and reveal truths that had been unknown earlier.
Deduction consists in transferring to the conclusion, the content, that is information already contained in the premises, hence in the conclusion there can be as much information as there is in the premises but no more. On the contrary, a discovery consists in arriving at new information one did not have previously. This is why (deductive) logic as an instrument for making discoveries may seem unthinkable. But whoever raised such an object against the concept of creative deduction would be guided by a conception of the mind that differed from that which marked the 17th century reformers of logic. The opinion characteristic of those times had its roots in Platonism, which dominated enlightened minds in the 16th and 17th century from Florence to Cambridge (two famous strongholds of Platonism). In the Platonic interpretation, apriorism involves a certain conception of what we would today call subconsciousness. In Plato himself that conception was associated with the theory of anamnesis, which mean cognition as reminiscence of truth originating from the pre-existential phase of the mind. Hence a discovery meant nothing else than bringing to daylight a truth that was formerly concealed. In other words, it could metaphorically be described as the shaping of the truth as it were from a substance which was given earlier, in the similar way bud and a fruit are shaped from the substance of a given plant.
That theory was linked to, and brought in fuller relief by, the characteristically Platonic conception of the teacher as someone who helps his disciples to bring to light what was in the shade or a penumbra. Socrates as described in Platonic dialogues defined that activity by metaphorically comparing it to obstetric art, and St. Augustine coined the term illuminatio to name that process whereby human thought comes to light. This gave rise to the conception of dialogue as illuminating interactions, and also the conception of dialectic as the theory and art of dialogue which has deduction as its main instrument which can clearly be seen in Plato’s dialogues. Dialectic later came to be termed logic. Thus from the very inception of Platonism logic was to serve the process of causing the truths that are innate to the mind to pass from the state of latency to that of clear presence. Thus it is not new contents that we owe to logical deduction but a new way in which they exist in human minds. And the fundamental question of the new programme of logic was as to what rules are to be used in decoding the truths encoded in our minds.
Cartesian school: Baruch Spinoza E. W. von Tschirnhaus Port Royal School
The four rules of Descartes:
- Not to accept anything as true before it comes to be known as such with all self-evidence; this is to say, to avoid haste and prejudice and not to cover by one’s judgement anything except for that which presents itself to the mind so clearly and explicitly that there is no reason to doubt it
- To divide every problem under consideration into as many particles as possible and is required for its better solution
- To guide one’s thought from the simplest and easiest objects in order to rise, later on, slowly to the cognition of more complex ones; in doing so one has to assume regular connections even among those which do not form a natural series
- To make every where precise specifications and general reviews so as to be sure that nothing has been omitted
The Discours of Descartes in its first edition appeared as the annex to Analytic Geometry. This work helped Leibniz and Newton to invent mathematical analysis (differential and integral calculus). That gigantic step toward the integration of mathematics aroused such an admiration and such hopes in the contemporaries that the second half of the 17th century was animated by the vision of a future science, termed mathesis universalis, which would cover the whole of knowledge, philosophy included, in the form of a single mathematized theory.
Discourse de la méthode provided a description of the appropriate operations preformed by the human mind that allows for arriving at the self-evident statements needed as premises of proofs. It also contained an exposition of geometry which from the methodological point of view can be seen as the model for the deduction of theorems from initial self-evident facts formulated in axioms.
The problem of finding self-evident premises needed to prove theorems expanded in the Cartesian school and its milieu to a vast set of problems pertaining to the distinction between the deduction of consequences from theorems already known, which was then called the synthetic method, and the search for premises to support a given theorem, called the analytic method.
Quote from Logic of Port Royal
Method can be described generally as the art of a good arrangement of a series of thoughts in arguments used either for the discovery of truth, if it is not known, or for its demonstration to others, if it is already known. There are thus two methods. One of them is the method discovering the truth, termed analysis or the method of solution; it might also be termed the method of invention. the other is the method of making the truth which has already been found accessible to others. It is termed synthesis or the method of composition, and it might also be termed the method of exposition.
The terms method of solution and the method composition which occur in that description were to render a similar distinction existing already in scholastic logic and earlier in Euclid and Pappus.
The theory of the analytic method, that is of the ars inveniendi, on which the efforts of that generation of philosophers were focussed, evolved in two opposite directions, the psychological and the formalistic. The psychological trend, which more and more concentrated on advice pertaining to the attitudes and behaviour of the mind (with the accompanying moralizing tendency) was particularly strongly voiced in the writings of Christian Thomasius and in those o his adherents, grouped in the then recently founded university in Halle. Thomasius, who followed Ramus in that respect, shared with the latter the (so to speak) practical orientation in logic. His disciples and adherents were strongly influenced by Protestant pietism, which at that time had its centre in Halle, and were thus influenced by the sentimentalist movement with its inclinations to irrationalism.
No wonder, therefore, that ultimately the idea of the methodological identity of mathematics and philosophy, and hence the idea of mathesis universalis was abandoned by them. This ends, in the late 17th century, one of the ramifications in the evolution of logic.
But the 17th century also witnessed the emergence of an antipsychological trend that raised the problem of the art of discovery owing to the idea of algorithm. This is associated with the name of Leibniz.
*** Leibniz on the mechanization of arguments
Algorithm as a recipe for the mechanical performance of tasks of a given kind. The concept of logical form has developed from the observation that certain sentences, e.g., in English, are accepted as true solely on the basis of their structure, with disregard of empirical and any other extralinguistic data.
In order to define the concept of logical truth in a general manner, and hence also the concept of logical form, one makes use of the partition of all expressions of a given language into logical terms (and, or, not, if … then, some, every, =, and the like) and extralogical ones.
A sentence is called a logical truth if it remains true after the replacement in it of extralogical expressions by any expressions, drawn from the same grammatical category — with the proviso that such a replacement is made consistently, which is to say that on replacing A by B in one place we do so in all those (and only those) places in which A occurs in that sentence.
Thought: In this fashion, Lambda Calculus rewrite can be thought of as that which preserves the logical form.
Such replaceability is of great significance for the recording of logical truths. Logical truths expressed in a schematic form by replacing the extralogical content with variables are called laws of logic.
The fact that logical truths are truths solely in virtue of their form paves the way to the construction of algorithms of two kinds: those which give us a mechanical method of deciding whether a sentences is a logical truth, and those which give us a mechanical method of deciding whether a sequence of sentences claimed to be a so-called formalized proof is in fact a proof of that kind.
The invention of algorithms which would serve those purposes was one of the great plans of Leibniz who expected that the invention would result in an epoch-making progress of human knowledge. His expectations came true only in our century, and that was accompanied by the discovery of the fact that they can come true only to a certain extent, because it is not possible to algorithmize the whole of mathematics (Gödel’s famous result proving the incompleteness of arithmetic), and hence that it is a fortiori impossible to algorithmize the whole of our knowledge.
The first flash of the intuition concerned with logical form must be seen in indirect reasoning, that is reasoning by reduction to absurdity, which is to be found in the enquiries of early Greek mathematicians, and which is particularly frequent in Plato’s dialogues (where as a rule it is used by Socrates, who treated it as main tool of his dialectic). An indirect proof starts from the assumption that the statement to be proved, say C (for conclusion) is false. If this assumption results in a contradiction, this means that it is false; but if the assumption of the falsity of C is false, then C itself has to be true.
The very fact of making use of such proofs points to the sensing of logical form, because in an indirect proof two desirable properties of our thinking are separated clearly from one another as if in a prism: the factual correctness, that is truth, of the premises and conclusions, and the formal correctness, that is agreement of inferences with the laws of logic.
Aristotle of Stagira is credited for creating the first system of formal logic. He made skillful use of indirect proofs, but what made him the founder of logic was the fact that in formulating the laws of inference he used for that purpose letters in the role of name variables. This is not to say that he already had a clearly shaped concept of logical form, but it is beyond doubt that his epoch-making invention in the sphere of notation guided the thoughts of all his followers toward the idea of that form.
Stoic Logicians were undoubtedly aware of the formal nature of logic obtained as a result of the use of variable symbols. They used numbers as sentential variables and thus created the nucleus of the logical theory which we now call the sentential calculus, while Aristotle’s syllogistic was a calculus of names.
Logicians active in the late Middle Ages made a successive important step forward by linking the logical form to the functioning of those expressions which were termed syncategorematic and analyzed them in detail. The realization of the fact that syncategorematic expressions determine the logical form of a sentence is particularly clear in the case of John Buridan. We find in Buridan a conception of logical form which resembles the contemporary one and includes the distinction between categorematic terms and syncategorematic ones, the latter being those which determine the logical form of a given sentence. He also took into consideration the impact of the categorematic terms upon logical form; for instance, the form of a sentence ‘A is A’ differs from the form ‘A is B’. Such a concept of logical form was taken over from Schoolmen by Leibniz, who turned it into the focal point of his conception of logic. Yet he remained isolated in that respect, perhaps because of the strong antiformalistic and scholastic tendencies which emanated from the milieu of both ramus and Descartes. That concept was rediscovered only in the mid-19th century by Augustus De Morgan, one of the founders of the algebra of logic. Thus Leibniz had to play the historical role of being the last Schoolman and at the same time the first logician of our epoch.
Cartesian methodology called for a direct contact of the mind with the object of cognition. Leibniz’s methodology pointed to the indispensability of another way of thinking, in which the contact of the mind with the object of cognition is not direct, but takes place through the intermediary of signs as those instruments of thinking which represent the object assigned to them. One of the ways of using signs as instruments consists in our grasping with our thought the sign instead of the object (its designatum).
That intermediate way of thinking about things, in which the thing itself is not present in the sphere of our attention, was called blind thinking (caeca cogitatio) by Leibniz. Operations on large numbers are its simple example. With large numbers, we are deprived of our visual contact or models and have to rely on sequences of figures which represent them. Such sequences are physical objects assigned to abstract objects, namely numbers, and operations on figures are unambiguously assigned to the corresponding operations on numbers.
If we add to cecae cogitatio one element more, then we obtain the concept of algorithm. The term ‘algorithm’ itself was not used by Leibniz, that role was played by the term calculus or by metaphorical expressions like caeca cogitatio and filum cogitationis (thread of thinking). The latter term referred to Ariadne’s thread, that is to the tool which enabled Theseus to move about int he Labyrinth and to find his way out, that is to solve his problem without any thinking, and without the knowledge of the Labyrinth itself.
Algorithm: a procedure consisting of a series of steps such that every step unambiguously determines the next one in accordance with precisely defined rules. Those rules determine the successive steps in the procedure under consideration by referring solely to physical properties (such as size and shape) of objects, e.g., the shape of figures, and the positions they occupy. On joining the self-evident condition that the number of the steps must be finite we obtain the full description of algorithm, which can be summed up as follows:
An algorithm is a recipe for a procedure pertaining to a definite class of tasks (e.g., addition of sequence of figures), which in each case guarantees the obtaining of the correct result after the performance of a finite number of operations, and that owing to the fact that the objects of such operations (e.g., sequence of figures) are reliably identifiable owing to their perceivable physical properties (e.g., shape, position).
In that melting pot of ideas which was Leibniz’s mind, the idea of mechanical computations merged with his looking at logical form through the prism of algebra as it was known at that time, and also with two other ideas, which he received from the past but transformed and combined in his own way. One of them, propagated by Joachim Jungius of Hamburg, consisted in the opinion that the essence of thinking consists in the analysis of concepts, that is in decomposing compound concepts into simpler ones, until one arrives at the simplest ones possible. Those simple and non-decomposable elements form, as Leibniz used to say, the alphabet of human thoughts. He saw the model of such a procedure in the decomposition of a number into factors which yields a product of prime numbers. Another idea, very popular in the 17th century, was that of a universal ideographic language, whose single symbols would be assigned not sounds but, as in Chinese, directly to concepts. That planned language was then called philosophical language, conceptual script, universal script etc.
Gregor Delgarno - Ars signorum John Wilkins - An Essay Toward a Real Character and a Philosophical Language
Logical Form + Algorithm + Algebra + Alphabet of Human Thought + Numerical factorization + Universal Language
According to Leibniz, this conceptual language should be constructed in compliance with Jungius’s idea, which is to say that simple symbols, elements of the alphabet, should represent the simplest non-decomposable concepts, while combinations of symbols, analogically to algebraic operations, should express appropriate compound concepts. The rules pertaining to such operations on symbols were to form a logical calculus that would be algorithmic in nature and would guarantee error-free reasoning.
It is said by Leibniz in a letter to Oldenburg dated October 28, 1675 that the truth would be delivered in a visible manner and irrefutable owing to an appropriate mechanism. His similar idea was that one could easily avoid errors in reasoning if theorems were given in a physically tangible manner, so that one could reason as easily as one counts.
Leibniz’s ideas deserve to be extensively commented. However, the problem of their historical influence is a matter that must be handled in a sophisticated manner. Only his programme for mathematical logic and his idea of the universal formalized language were known to posteriority, while his results themselves were not discovered until the end of the 19th century.
This is a precarious position, indeed. The assessment of Leibniz’s position therefore requires a sophistication which does not attribute too much to him, and at the same time is able to acknowledge the great role he nevertheless played — as a symbol of epoch-making ideas and and of the civilizational turn.
Descartes’ and Pascal’s preoccupation with the mind’s inner life counterbalances Leibniz’s tendency toward replacing mental acts by operations on symbols which could be formalized and mechanized. In the Cartesian-Pascalian perspective we see the mind as dealing with objects and relations which are so numerous, subtle and involved that in many cases a verbalization or symbolization must prove inadequate.
Between Leibniz and Boole: Towards the Algebraization of Logic
The algebraization of logic initiated by Leibniz marked the decisive step towards the mechanization of argument.s Equally important was the introduction of variables combined with the conception of logical consequence as dependent solely on the logical form as, in turn, dependent solely on logical constants. But that was not so much a single step as the age-long process from Aristotle to the late scholasticism. The next turning point after algebraization is to be seen in the invention by Frege and later Russell of the calculus of quantifiers, which turned logic into a universal instrument of reasoning, yet at the price of what if we follow Hilbert who defined the axioms of that calculus as transfinite might be termed the infinitism of logic. In order to return to algebraic equations which offered the possibility of mechanical combinatorics performable by the computer it was necessary to find methods of eliminating the quantifiers, that is to do something which might in turn be termed the finitization of first order logic. As is known, that was achieved owing to Skolem, Gentzen, Herbrand, and Beth.
Thus the mechanization of logic proceeded in the three-stages development consisting of formalization, algebraization, and infinitization (intended to increase the strength of proofs) combined with the possibility of reducing the latter to a finitized form that can be processed mechanically.
Bernoulli brothers. For Bernoulli algebra was superior to logic
Christian Wolff: Abandoned the Cartesian view of logic under Leibniz’s influence. Cartesian view was marked by a negative assessment of all formalism, especially the syllogistic one, and postulated the pursuit of logic as a normative theory of controlling the mind, with the disregard of the role of language.
After turning to Leibniz’s side, Wolff became an ardent adherent of syllogistic and the programme of pursuing it in the algebraic way as operations on symbols alone, whose meanings might be entirely disregarded. Wolff himself did not contribute to the implementation of that programme of algebraization of logic, but in view of the scope and strength of his influence one may assume that his agitation helped to consolidate that state of consciousness which ultimately brought the perfect rendering of logic in algebraic terms.
Johann Lambert, who rendered the greatest services to the algebraization of logic in the 18th century, worked under Wolff’s influence.
Gottfried Plocquet, a German author of French origin, was busy in developing the Leibnizian ideas of universal language and logical calculus. He studied diligently the then accessible logical texts of Leibniz, including Difficultates quaedam logicae. Ploucquet as the author of many works written in German and engaged in public discussions with Lambert, was well known to 19th century German philosophers. He was quoted, although with disapproval, by Hegel, which contributed to his being known in the next century.
The fact that syllogistic constitutes a small fragment of logic and that it was erroneously identified with logic as a whole was not an obstacle to the effectiveness of such a search. That fragment was well suited as the experimental field for the algorithmization of proofs, and further the fact that the medieval endeavors were naïve and little successful was due to the inability of the early authors to combine them with the calculatory approach. But two things were essential: the formulation of the problem and the proper establishing of the area of research. When in the 17th century algebra provided the paradigm that could be used in logic, a new and promising field of research was opened. It is in that field that we find Ploucquet as its typical representative.
Ploucquet tested the efficiency of his algebraic symbolism on the language of syllogistic. For the recording of statements forming the so-called square of opposition he adopted a new syntax, in which he succeeded symbolically to express both a kind of the quantification of both the subject and the predicate, which made it possible to render the structure of a categorical sentence by juxtaposition alone as in algebra, where juxtaposition happen to be a symbol of some operation. Thus by drawing from the traditional language the symbols S and P to denote, respectively, the subject and the predicate he makes a distinction between any of those terms being taken in its whole extension and its being taken in part of its extension, the distinction being indicated, respectively, by a capital and a lower-case letter. The distinction between distributed and non-distributed terms was a scholastic invention on the path to the algorithmization of syllogistic (admired by Leibniz) and hence we have here to do with the scholastic idea in a new symbolic attire.
Ploucquet devised a calculus where the middle term taken universally is placed first and the other is connected to it so that the middle term is placed in the middle.
Men: m Living Beings: P S: Aristotle All men are living beings Mp, Sm
When the middle term is universally taken twice, the order of its position is indifferent. When m is subsumed under M, if PM is true, then pm is true too. Hence Mp, Sm becomes pmS, when m is deleted, we have pS or Sp, which is to say that all S is some P or all S is P. This text, deliberately setting up a syllogistic calculus, should be interpreted in the light of the explanation given several pages earlier in Ploucquet’s work and pertaining to the identity of the extension of subjects and predicates in affirmative sentences. Such an interpretation of the structure of the categorical affirmative sentence proves inseparable from the quantification of predicate.
Since in every affirmation the identity of the subject with the predicate is asserted, it is obvious that if the subject is denoted by S and the predicate by p, then p can be substituted for S, and reciprocally, S for p. Thus Sp is identical with pS.
It can be seen from this text that we, as it is customary today, interpret Sp in the quantification calculus as the implication
forAll(x, S(x) => p(x)), and not as the equivalence, forAll(x, S(x) <=> p(x)) that would be at variance with the reversibility (reciprocality) stated in the text quoted above. This is a warning against the interpretation of traditional logic in terms of the quantification calculus with disregard of the context of the old traditional theory. This is so because in those theories which use the algorithm of the recognition of the correct conclusion, based on the concept of distribution of terms, the predicate in a general affirmative sentence has as its extension a certain subset o the set denoted by that predicate in other contexts (or outside of context) precisely that subset which coincides with the extension of the subject.
Now we can follow the reasoning having in view the fact that with our author juxtaposition is a syntactical indicator of affirmative sentences, whereas for negative ones he used his own symbol of the relation of exclusion.
This is reasoning for testing the correctness of syllogism, which is an algorithm that refers solely to syntactic features, that is the shape and position of symbols, as arithmetical algorithms do. We have to do with the following rules:
- It is allowed to transpose letters
- It is allowed to replace a capital letter by a lowercase one
- Given a sequence of pairs of letters such that the consequent in every pair is identical with the antecedent of the next one. It is allowed to accept the sequence of letters consisting of all antecedents and the last consequent, for instance to pass from ab, be to abc (to be read: a is b and c, for instance from “the lion is a cat” and “the cat is predator” we pass to “the lion is a predatory cat”.
- In such a sequence of letters it is allowed to omit any letter except for the first and last one.
After such a reconstruction of Ploucquet’s procedure it can better be understood why he considered it as a procedure analogical to the calculus carried out on symbols. Its discouraging intricacy largely explains why, even though Ploucquet’s works were popular in his times, he did not become the Boole of the 18th century.
Ploucquet is an important witness of his epoch in which syllogistic played an important role as the experimental field for the endeavours to transform logic into an algebraic calculus.
The same trend was embraced by Georg Jonathan Holland, an adherent of Ploucquet in the latter’s polemic with Lambert.
Lambert’s works on logic fill at least seven volumes.
Lambert’s work Logische und Philosophischen Abhandlungen (1782) had an editorial introduction written by Christoph Heinrich Müller, Lambert’s compatriot and friend. It mentions a certain conception of the mechanization of arguments. That conception must have been sufficiently interesting and comprehensible to the learned readers of that period, which is borne out by the fact that such an experienced editor as Müller, who was busy publishing German literature from the period 1050 – 1500, commented on it in such a way as the problem were something being a vogue.
Lambert was directly influenced above all by Locke and Wolff.
We are here to do with a case in which the intersection, at a certain point of time, of two mutually independent processes opens a new stage in history. Such intersection may also appear in the fact that a certain group of scholars is engaged with similar intensity in both processes. This was just in the case under consideration: people strongly rooted in the tradition of scholastic logic came to be interested in algebra, and some of them proved creative in that newly born discipline called then logistic speciosa universalis, that is (in a free translation), the general theory of calculating with variables (i.e., sign denoting species of objects, e.g. numbers, instead of individual objects).
Two ideas were drawn from the logic of Aristotle and the schoolmen. Each of them entered into a natural relationship with a certain algebraic concept in such a way that all components came to form a coherent whole. One of the ideas was that of finding the middle term as a means of constructing the proof. The problem consists in the fact how that still unknown middle term is to be found on the basis of what is known, namely the external terms and the intended conclusion. This task was generalized as the problem of finding new data of a definite kind on the basis of given data of a given kind. The logic conceived as the theory of such a search was termed logica inventionis which can be rendered as inventive logic or (more freely) logic of discovery.
Thus generalized programme of inventive logic was characteristic of the Renaissance rather than of the Middle Ages, and had its standard-bearer in Francis Bacon, but the point of departure should be seen in the Middle Ages; a story related to that problem can be traced in Leibniz’s dissertation De arte combinatoria. Moreover, many scholars who combined interests in logic and algebra must have then been impressed by the analogy between such a finding of new data and the finding of the unknown in an algebraic equation.
But if use was to be made of that analogy, the sentences considered in logic had to have a form analogical to that of equations. That would also result in the attractive possibility of constructing proofs by replacing one side of an equation by an expression equivalent to it (this was how the nature of the proof was conceived by Leibniz). But it is well known that none of the four types of categorical sentences of Aristotelian logic possesses the form of an equation.
The theory of suppositions made medieval logicians used to thinking that what determines the logical function of an expression is not only its external form and the related lexical meanings, but also its context, and the intention of the speaker marked in some way. Hence, according to the context in question, an expression one and the same in its form could stand for an individual, either definite or indefinite; Latin did not make any formal distinction in that respect as it lacked articles; in another context a name could refer to a class of individuals, to a universal, etc. Upon that habit of thinking there was imposed the theory of the distribution of terms in categorical sentences. Taking a general term on one occasion in its full extension and on another occasion only in a part of the extension would amount to different suppositions. The latter of the two, that is the use of a term as denoting a subset (of the set which is the extension of a given term in its lexical meaning) can be indicated by a separate word (for instance aliquis i.e., ‘some’) or by the position in the context of a definite sentential structure, for instance, the position of the predicate in a general affirmative sentence (customarily denoted by SaP).
There was the last step to be made. In contemporary logic, when traditional logic is interpreted in terms of the predicate calculus, SaP is treated as a record of an inclusion because both terms in the sentences are taken in their full extension. But if P is taken in a part of its extension, namely that which coincides with the extension of the subject, then SaP is expressing an equation which should be interpreted as =. In this way, we arrive at a form comparable with the form of an algebraic logic. It is worth noting that for the logicians who lived in the 17th and 18th century that interpretation was so obvious they did not think it necessary to explain the matter to the reader, which they would have to do if they addressed their texts to the 20th century readers (who have forgotten the old teachings on suppositions and the distribution of the syllogistic terms).
Lambert says:
Logical analysis is an art of deducing unknown or sought concepts from known or given ones by means of identities. Since nothing can be found out of nothing, concepts have to be given to allow one to find the unknowns … General analysis (analytica logica speciosa, logistica speciosa universalis) is an art of deducing concepts from general and indefinite ones. Since the concepts needed for that purpose are indefinite, one cannot use words as these denote definite concept. The most appropriate thing is, therefore, to use letters and other signs as it is also the case in algebra.
An example:
A certain technical solution which makes it possible to impart to a sentences of the type SaP the form of identity: S = xP,
where juxtaposition is the logical equivalent of the algebraic operation of multiplication, and the symbol x stands for an object which, when multiplied by P yields an object identical with V. For instance, the sentence, “Every Greek is intelligent” is interpreted as:
The set of Greeks is identical with a certain subset of intelligent beings. That subset is obtained by the intersection of the set of intelligent beings with some other set, in the above formula represented by j, that is, according to Lambert’s expression, an indefinite coefficient. Thus, the syllogism Barbara is reconstructed as the following set of identitieus:
M = xP, s = yM
On replacing M in the second premise by xP, we arrive at the conclusion: S = yxP
Leibniz als Identifikationsfigure der Britischen Logiker des 19. Jahrhunderts - Volker Peckhaus (1994)
The research of Volker Peckhaus is to the effect that Boole and his British colleagues first discovered the algebra of logic, and then learned that it has been alreday discovered by Leibniz. This is not to mean that the same was made twice; in Leibiz one finds just some primordial ideas. Anyway, the consciousness of anticipating those achievements by Leibniz proved a significant circumstance in the further development. The problem of how much modern logic, especialyl, algebra of classes was anticipated by Leibniz belongs to main issues in Leibniz scholarship. In this book a rather conservative attitude is assumed, for bolder interpretations require more research. Among those who pioneer such a bolder approach there is Wolfgang Lenzen.
The statement of that sigificance may seem strange, since the lack of any causal nexus between a forerunner and a genuine originator, in the case of Leibniz and Boole confirmed by most recent investigations sohuld imply that the history would have developed in the identical way even if the forerunner had never existed. However, this is not the case in the ihstory in question, which can be explained by a kind of feedback between own results and their later detecte anticipation. Boole and other British logicians, including Jevons (specially important because of the step he made from algebraization to mechanization) not only produced technical results but also entertained some philosophical ideas which did not conform to the empiristic trend, characteristic of the British philosophy. It required a strong belief that the laws of thought were independent from empirical reality, in order to overcame the pression of the British empiristic orthodoxy; that belief gained a new vigour, due to its meeting with Leibniz’s tenets, in the period in which it must have fought for recognition and standing in the British philosophy (had not such a recognition become the case, there would not have been the way paved to Russell’s (1900) seminal work on Leibniz).
For instance, William Stanley Jevons contrary to the teachigs of John Stuart Mill, William Whewell, etc., tried to deductively establish the scientific method on the basis of Boole’s logical principles. As for Boole himself, he voiced his conviction that the laws of logic have a real existence as laws of the human mind, independent from any observable facts (contrary to the creed of the British empiricism). As commented by Peckhaus, such statements of Boole prove his affinity with Leibniz. This may be taken as a proof of reality of what in German is called Geistesgeschichte, that is the history of objective ideas which must come into being, due to their internal logic, in a way which is relatively independent from biographical circumstances.
The English Algebra of Logic in the 19th Century
The idea of the mathematization of logic and the development of the formal algebra in the 19th century were sources of the algebra of logic established by De Morgan, Boole, and Jevons. It was in fact the beginning of the mathematical logic. The old idea of a logical calculus which would enable the analysis of logical reasoning with the help of a procedure similar to the procedure of solving equations in algebra was realized.
In traditional logic, we have statements of the form:
SaP SiP SeP SoP
called the categorical sentences.
Aristotle observed that one can build valid schemas of inference consisting of two premises and a conclusion being categorical sentence - they are called categorical syllogisms. If we assume that every term in a syllogism stands for a non-emptyc lass then we get that 24 out of 256 possible combinations are valid inferences.
Attempts were made by Francis Bacon, Christoph von Sigwart, and Wilhelm Schuppe.
Quantification of Predicate
William Hamilton noticed that the predicate term in each of Aristotle’s four basic assertions SaP, SiP, SeP, SoP is ambiguous in the sense that it does not tell us whether we are concerned with all or part of the predicate. Hence one should increase the precision of those four statements by quantifying their predicates. In this way we get 8 assertions instead of Aristotle’s four:
all S is all P all S is some P no S is all P no S is some P some S is all P some S is some P some S is not all P some S is not some P
Using those 8 basic propositions we can combine them to form 512 possible moods of which 108 prove to be valid. The usage of statements with quantified predicates allows us higher precision than it was possible before. For example, the old logic would treat “All men are mortal” and “All men are featherless bipeds” as identical in form; whereas in the new system we see at once that the first statement is an example of “All S is some P” and the second is an example of “All S is all P”. But there arose some problems. It was difficult to express those new statements with quantified predicates in a common speech. Without developing a really complete and precise system of notation one finds himself forced to employ words in a clumsy and barbarous way. Hamilton was aware of it and attempted to remedy the obscurity of phrasing by devising a curious system of notation. Though it was really curious and rather useless in practice it was important for two reasons: it had the superficial appearance of a diagram and it led Hamilton to the idea that by transforming the phrasing of any valid syllogism with quantified predicates it may be expressed in statements of equality. The latter suggested that logical statements might be reduced to something analogous to algebraic equations and so gave encouragement to those who were seeking a suitable algebraic notation. Some logicians such as Howard Gardner in his Logic, Machines, and Diagrams (1958) are of the opinion that this was Hamilton’s only significant contribution to logic.
The idea of quantification of predicate in the syllogism can be found also in papers of another English logician Augustus De Morgan. He was a mathematician and worked not only in logic but also in algebra and analysis. It was De Morgan who introduced the notion “mathematical induction” which was popularized later thanks to the book on algebra written by Isaac Todhunter.
Augustus De Morgan’s earlier logical works written before 1859 were devoted to the study of the syllogism. He introduced independently a system more elaborated than Hamilton’s one. Hamilton accused him of plagiarism and for many years the two men argued with each other in books and magazine articles. This debate had also serious consequences. Namely, it caused George Boole’s renewed interest in logic which led him to write the book Mathematical Analysis of Logic published in 1847.
Trying to reshape and to enlarge the Aristotelian syllogism (cf. the book Formal Logic, or the Calculus of Inference Necessary and Probable of 28147) De Morgan observed that in almost all languages there are so called positive and negative terms. Even if in a language there are no special words indicating this dichotomy, nevertheless every notion divides the universe of discourse into two parts: elements having properties indicated by the given term and those which do not have those properties. Hence if X denotes a certain class of objects then all elements of the universe which are not X can be described as not-X. The latter is denoted by De Morgan by x. In this way the difference between positive and negative terms disappears and they are possessing equal rights. This enable De Morgan to consider instead of two terms of the traditional syllogistic X, Y, four pairs of terms: X, Y; x, y, X, y; x, Y which give 16 logical combinations, 8 of which are different. He introduced various types of notations for them. The first two consisted of letters and resembled the traditional notation: a, i, e, o; the latter two consisted of systems of parentheses.
all X is all Y | A: X ) Y | X))Y no x is all Y | E: X.Y or X)y | X).(Y some X is Y | I: XY | X()Y some X is no y | O: X : Y or X)y | X(.(Y or X()y no x is no y | a: x)y or Y)X | x))y or X((Y no x is no y | e: x)Y or x.y | x )) Y or x(.)Y some no x is no y | i: xy | x()y or X)(Y some no x is all Y | o: xy or x : y or Y : X | x()Y or x).)y
We see that De Morgan’s symbols introduced to express the old and new types of syllogisms were not algebraic. But he found that his symbols can be manipulated in a way that resembled the familiar method of manipulation of algebraic formulae.
He established certain connection between the above statements which he called simple. The sign = was used by De Morgan in two meanings. It meant both “equivalent” and “implies”.
Having introduced some fundamental relations De Morgan developed his theory of syllogism. He considered not only syllogism with simple premises but also with complex ones (which he called complex syllogism).
After having introduced operations which we call today the negation of a product and sum he established the following connections:
negation of PQ is p * q negation of P * Q is pq
He noted also the law of distributivity: (P * Q)(R * S) = PR * PS * QR * QS
Here we see that developing the theory of syllogism, De Morgan came to the idea of what we call today Boolean algebra. He did it independently of George Boole.
De Morgan not only extended the traditional syllogistic but introduced also new types of syllogisms. In Budget of Paradoxes (1872) he summarized his work under six heads, each propounding a new types of syllogism: relative, undecided, exemplar, numerical, onzymatic and transposed.
De Morgan’s most lasting contribution to logic is when he moved beyond the syllogism to investigate the theory of syllogism in “On the syllogism no IV and on logic in general” from 1859. His ideas and conceptions were later on developed by various logicians, first of all by Charles Sanders Peirce, Ernst Schröder, Giuseppe Peano, Georg Cantor, Gottlob Frege, and Bertrand Russell. Charles Peirce wrote that De Morgan was “one of the best logicians of all time and undoubtedly a father of the logic of relatives”.
In the work “On the syllogism no IV”, De Morgan noted that the doctrine of syllogism, which he had discussed in his Formal Logic (1847) and in earlier papers was only a special case in the theory of the composition of relations. Hence he went to a more general treatment of the subject. He stated that the canons of syllogistic reasoning were in effect a statement of the symmetrical (De Morgan called it convertible) and transitive character of the relation of identity. He suggested symbols for the converse and the contradictory (he said “contrary”) of a relative and for three different ways in which a pair of relatives may be combined (by “relative” he meant what some logicians had called a relative term, i.e. a term which applies to something only in respect of its being related to something else).
De Morgan showed that the converse of the contradictory and the contradictory of the converse are identical. He set out in a table the converse, the contradictory and the converse of the contradictory of each of the three combinations and proved that the converse or the contradictory or the converse of the contradictory of each such combination is itself a combination of one of the kinds discussed.
Papers of De Morgan, though containing new and interesting ideas were not easy to read. They were full of ambiguities and technical details which made them difficult to study. Nevertheless they contributed in a significant way to the development of mathematical logic.
Boole was interested in logic already in his teens, working as an usher in a private school at Lincoln and educating himself by extensive reading. From that time came his idea that algebraic formulae might be used to express logical relations.
Boole and De Morgan were in correspondence over a long period (1842 – 1864). They exchanged scientific ideas and discussed various problems of logic and mathematics.
The main logical works of George Boole are two books:
- The Mathematical Analysis of Logic, Being An Essay Toward A Calculus of Deductive Reasoning (1847)
- An investigation of The Laws of Thought, on which are founded the Mathematical Theories of Logic and Probabilities (1854)
The second book of George Boole, An investigation of the Laws of Thought was not very original. It was the result of Boole’s studies of works of philosophers on the foundations of logic. The chief novelty of the book was the application of his ideas to the calculus of probabilities. There was no important change on the formal side in comparison with Mathematical Analysis of Logic.
We should also mention here also his paper “On the calculus of logic” (1848) which contained a short account of his ideas from the pamphlet from 1847. It may be supposed that it was more widely read among mathematicians than Mathematical Analysis of Logic.
Boole was not satisfied with the exposition of his ideas in his books. He was working towards the end of his life on the new edition of the Laws of Thought preparing various improvements. From the drafts published in Studies in Logic and Probability (1952) it follows that what he had in mind was a development of his epistemological views rather than any alteration of the formal side of his work. He mentions in particular distinction between the logic of class (i.e. his calculus of logic) and a higher, more comprehensive, logic that cannot be reduced to a calculus but may be said to be “the Philosophy of all thought which is expressible in signs, whatever the object of that thought”.
What stimulated the interest of Boole in mathematical logic was not only the dispute between De Morgan and Hamilton but also the discussion of the nature of algebra shortly before he wrote his papers. The papers of Peacock, Sir William Rowan Hamilton, De Morgan, and Gregory (a personal friend of Boole and the editor of “Cambridge Mathematical Journal”) are worth mentioning here. Boole’s aesthetic interest in mathematics led him to value very highly all attempts to achieve abstract generality.
Boole started from the following ideas which were at least implicitly in papers of his contemporaries: i) there could be an algebra of entities which are not numbers in any ordinary sense ii) the laws which hold for types of numbers up and including complex numbers need not all be retained in an algebraic system not applicable to such numbers. He saw that an algebra could be developed as an abstract calculus capable of various interpretations.
What is really new in Boole’s works is not the idea of an unquantitative calculus, it was already by Leibniz and Lambert but a clear description of the essence of the formalism in which the validity of a statement “does not depend upon the interpretation of the symbols which are employed, but solely upon the laws of their combination”. Boole indicates here that a given formal language may be interpreted in various ways. Hence he sees logic not as an analysis of abstracts from real thoughts but rather as a formal construction for which one builds afterwords an interpretation. This is really quite new in comparison with the whole tradition including Leibniz.
One can say that the relation of Boole to Leibniz is the same as was the relation of Aristotle to Plato. In fact, we find by Boole, as it was by Aristotle, not only the ideas, but also a concrete implementation of them, a concrete system.
What was built by Boole was not a system in our nowadays meaning he did not distinguish between properties of operations which are assumed and properties which can be proved or derived from the assumptions.
Symbols x, y, z, etc. denoted classes in Boole’s papers. He did not distinguish very sharply between class symbols and adjectives. Sometimes he called the letters x, y, z etc. elective symbols thinking of them as symbols which elect (i.e. select) certain things for attention. The symbol = between two class symbols indicated that the classes concerned have the same members. He introduced 3 operations on classes: i) intersection of 2 classes denoted by xy (i.e. the class consisting of all the things which belong to both those classes) ii) the exclusive union of two classes, i.e. if x and y are two mutually exclusive classes then x + y denotes the class of things which belong either to the class denoted by x or to the class denoted by y iii) subtraction of two classes, i.e. if every element of the class y is an element of the class x then x - y denoted the class of those elements of x which are not elements of y.
He introduced also special symbols for two classes which form, so to say, limiting cases among all distinguishable classes, namely the universal class, or the class of which everything is a member (denoted by 1) and the null class, or the class of which nothing is a member (denoted by 0). The introduction of those classes involves an interesting novelty with respect to the tradition coming from Aristotle who confined his attention to general terms which were neither universal in the sense of applying to everything nor yet null in the sense of applying to nothing. Boole denoted by 1 what De Morgan called the universe of discourse, i.e. not the totality of all conceivable objects of any kind whatsoever, but rather the whole of some definite category of things which are under discussion.
Having introduced the universe class, Boole wrote 1 - x for the complement of the class x. The operation of intersection of classes resembles the operation of multiplication of numbers. But there is an important peculiarity observed by Boole. Namely if x denotes a class then xx = x and in general x^n = x. Boole says in Mathematical Analysis of Logic that it is the distinguishing feature of his calculus. The analogy between intersection and multiplication suggests also the idea of introducing to the calculus for classes an operation resembling division of two numbers. Boole writes that this analogue may be abstraction. Let x, y, z denote classes related in the way indicated by the equation x = yz. We can write z = x/y expressing the fact that z denotes a class we reach by abstracting from the membership of the class x the restriction of being included in the class y. But this convention has two limits. First the expression x/y can have no meaning at all in the calculus of classes if the class x is not a part of the class y and secondly, the expression x/y is generally indeterminate in the calculus of classes, i.e., there may be different classes whose intersections with the class y are all coextensive with the class x.
The introduced system of notation suffices to express A, E, I, and O propositions of traditional logic (provided that A and E propositions are taken without existential import). If the symbol x denotes the class of X things and the symbol y the class of Y things, then we have the following scheme:
all X is Y | x(1-y) = 0 no X is Y | xy = 0 some X is Y | xy not= 0 some X is not Y | x(1-y) not= 0
Since the last two statements are represented by inequalities and Boole preferred to express all the traditional types of categorical propositions by equations, he wrote:
some X is Y as xy = v some X is not Y as x(1-y) = v
The letter v seems to correspond to the English word “some”. IT is said to stand for a class “indefinite in all respects but one”, namely that it contains a member or members.
But this convention is unsatisfactory. In Boole’s system, the letter v can be manipulated in some respects as though it were a class symbol. This may suggest mistaken inferences. For example one may be tempted to infer from the equations: ab = v and cd = v that ab = cd. Boole himself did not fall into such fallacies by putting restrictions on the use of the letter v which are inconsistent with his own description of it as a class symbol. It seems that a reason and purpose of introducing the symbol v is the desire to construct a device for expressing all Aristotelian inferences, even those depending on existential import.
He had the following formulae indicating the connections between various operations on classes:
- xy = yx
- x + y = y + x
- x(y + z) = xy + xz
- x(y - z) = xy - yz
- if x = y then xz = yz
- if x = y then x + z = y + z
- if x = y then x - z = y - z
- x(1 - x) = 0
The formula 1-7 are similar in form to rules of ordinary numerical algebra. Formula 8 is different. But Boole pointed out that even it can be interpreted numerically by thinking of the variables as admitting only the values 0 and 1.
It might be tempting to think that Boole’s system is a two-valued algebra. But this is a mistake. In fact, Boole did not distinguish sharply between his original system and a narrower system satisfying additionally the following principle: 9) either x = 1 or x = 0
If we interpret the system in terms of classes, then the principle 9) is not satisfied and if we interpret it numerically then the system satisfies even 9.
In both his books, The Mathematical Analysis of Logic and An Investigation of the Laws of Thought, Boole suggested a convention that the equations x = 1 and x = 0 may be taken to mean that the proposition X is true or false, respectively. Consequently the truth-values of more complicated propositions can be represented by combinations of small letters, e.g. the truth-value of the conjunction of the proposition X and Y by xy and the truth-value of their exclusive disjunction by x + y. This enables us to interpret the Boole’s system in terms of the truth-values of propositions with symbols 1 and 0 for truth and falsity respectively. This interpretation was worked out by Boole himself without use of the phrase “truth-value” which was invented later by Frege.
In Laws of Thought Boole abandoned the elective interpretation and proposed that the letter x should be taken to stand for the time during which the proposition X is true. This resembles opinions of some ancient and medieval logicians.
In Mathematical Analysis of Logic, Boole says that the theory of hypothetical propositions could be treated as part of the theory of probabilities and in Laws of Thought we have an interpretation according to which the letter x stands for the probability of the proposition X in relation to all the available information, say K.
Hence we have
- if X and Y are independent then Prob_K(X and Y) = xy
- if X and Y are mutually exclusive then Prob_K(X or Y) = x + y
We see that Boole’s system may have various interpretations and Boole himself anticipated the fact. The essence of his method is really the derivation of consequences in abstract fashion, i.e. without regard to interpretation.
The fundamental process in the formal elaboration of Boole’s system is so called development. Let f(x) be an expression involving x and possibly other elective symbols and algebraic signs introduced above. Then we have f(x) = ax + 6(1 - x). It can easily be seen that a = f(1) and 6 = f(0). Hence, f(x) = f(1)x + f(0)(1-x)
It is said that this formula gives the development of f(x) with respect to x.
If we have an expression g(x,y) with two elective symbols x, y (and the usual symbols of operations0, then according to this method we obtain the following development of it:
g(x, y) = g(1, y)x + g(0, y)(1-x) g(1, y) = g(1,1)y + g(1,0)(1-y) g(0,y) = g(0,1) + g(0,0)(1-y) and consequently using the rule 3)
g(x,y) = g(1,1)xy + g(1,0)x(1-y) + g(0,1)(1-x)y + g(0,0)(1-x)(1-y)
Factors x, 1 - x in the development of f(x) an xy, x(1-y), (1-x)y, (1-x)(1-y) in the development of g(x,y) are called constituents. We see that for one class x we have 2 constituents, for 2 classes x, y, we have 4 and in general for n classes, we have 2^n constituents. The sum of all constituents of any development = 1, their product is equal to 0. Hence they may be interpreted as a decomposition of the universe into a pairwise disjoint classes.
The development of an expression is treated by Boole as a degenerate case under Maclaurin’s theorem about the expansion of functions in ascending powers.
The development of elective expressions served Boole to define two other operations, namely solution and elimination. Assume that we have an equation f(x) = 0, where f(x) is an expression involving symbol x and may be other elective symbols. We want to write x in terms of those other symbols. Using development of f(x) one has: f(1)x + f(0)(1-x) = 0 [f(1) - f(0)]x + f(0) = 0 x = f(0) / (f(0) - f(1))
Observe that Boole introduces here the operation of division to which he has assigned no fixed interpretation. But he suggest here a special method of elimination of this difficulty. Developing this expression, we get a sum of products in which the sign of division appears only in the various coefficient, each of which must have one of the four forms: 1/1, 0/0, 0/1, 1/0. The first is equal to 1 and the third 0. The fourth can be shown not to occur except as coefficient to a product which is separately equal to 0, hence it in not very troublesome. The second 0/0 is curious. Boole says that it is a perfectly indeterminate symbol of quantity, corresponding to “all, some, or none”. Sometimes he equates it with the symbol v, but it is not quite correct. It is better to use another letter, say w. Hence we have:
x = 1/1 * p + 0/0 * q + 0/1 * r + 1/0 * s x = p + wq
We can interpret it saying that the class x consists of the class p together with an indeterminate part (all, some, or none) of the class q. In an unpublished draft, Boole wrote that the coefficients 1/1, 0/0, 0/1, 1/0 should be taken to represent respectively the categories of universality, indefiniteness, non-existence, and impossibility.
To describe the rules of elimination, assume that an equation f(x) = 0 is given. We want to know what relation,s if any, hold independently between x and other classes symbolized in f(x). Solving this equation, we get x = f(0) / f(0) - f(1)
Hence,
1 - x = -f(1) / f(0) - f(1)
But x(1-x) = 0, hence f(0) * f(1) / ( f(0) - f(1) )^2 = 0 i.e. f(0)f(1) = 0
We have now two cases: i) the working out of the left side of this equation yields 0 = 0 ii) it yields something of the form g(y, z, …) = 0. In the case i) we conclude that the original equation covers no relation independent of x, in the case ii) we establish that the full version of the equation f(x) = 0 coverse some relation or relations independent of x.
In all those reasonings we see that they involve expressions for which there is no logical interpretation. But Boole has adopted a rule according to which if one is doing some calculation sin a formal system then it is not necessary that all formulas in this calculating process have a meaning according to a given interpretation - it is enough that the first and the last ones have such a meaning.
Boole’s calculations were sufficient to represent all kinds of reasonings of traditional logic. Inp articular syllogistic reasonings might be presented as the reduction of two classes of equations to one, followed by elimination of the middle term and solution for the subject term of the conclusion.
Consider for example, the following reasoning:
Every human being is an animal Every animal is mortal Hence every human being is mortal
h: human beings m: mortals a: animals
We have
h(1-a) = 0 a(1-m) = 0
Hence h - ah + a - am = 0
Developing this with respect to a we get
(h - h*1 + 1 - 1*m)a + (h - h*0 + 0 - 0 * m)(1 - a) = 0 (1-m)a + h(1-a) = 0
Eliminating now a, we have (1-m)h = 0 This means that every human being is mortal
What was the meaning and significance of Boole’s ideas for the development of mathematical logic? First of all we must note that he freed logic from the domination of epistemology and so brought about its revival as an independent science. He showed that logic can be studied without any reference to the processes of our minds.
The chief novelty in his system is the theory of elective functions and their development. Those ideas can be met already by Philo of Megara but Boole was the first who treated these topics in a general fashion. What more, Boole’s methods can be applied in a mechanical way giving what is called today a decision procedure.
To give the full account of the development one should mention here also Hugh MacColl, who in the paper “The Calculus of Equivalent Statements” has put forward suggestions for a calculus of propositions in which the asserted principles would be implications rather than equations (as it was by Boole). He proposed an algebraic system of the propositional calculus in the spirit of Boole. This was an attempt to overcome the lack of Boole’s systems and may be treated as a climax in the development of mathematical logic before Frege, who proposed a complete calculus of propositions.
One of the persons who saw importance of Boole’s work was William Stanley Jevons, a logician and economist. He regarded Boole’s achievements as the greatest advance in the history of logic since Aristotle. But he noticed also defects of Boole’s system. He believed that it was a mistake that Boole tried to make his logical notation resemble algebraic notation. He saw the weakness in Boole’s preference for the exclusive rather than the inclusive interpretation for “or”.
His own system was supposed to overcome all those defects. Jevons devised a method called by him the “method of indirect inference”.
He introduced the following operations performed on classes: intersection, complement, and inclusive union (denoted by him originally by . | . to distinguish it from Boole’s exclusive union). The null class was denoted by 0 and the universe class by 1. The expression X = Y indicated the equality of the classes X and Y, i.e. the fact that they have the same elements. To express the inclusion of X in Y, Jevons wrote X = XY. He noted the following properties of those operations:
XY = YX X + Y = Y + X X(YZ) = (XY)Z X + (Y + Z) = (X + Y) + Z X(Y + Z) = XY + XZ
He also used the principle of identity X = X, of contradiction Xx = 0 (Jevons symbolized a complement using a lowercase letter, he borrowed this convention from De Morgan) as well as tertium non datur X + x = 1and the rule of substitution of similars. The last rule is used by him for verification of inferences.
For Barbara, SaM MaP SaP
The first premise is written by Jevons as S = SM, the second as M = MP. Substituting M for MP in the first premise, we get S = S(MP) = (SM)P. But S = SM, Hence S = SP, i.e. SaP.
Jevons developed his logic using properties of operations and Boole’s idea of constituents. The easiest way to explain it is to given an example.
Consider the following syllogistic premises: “All A is B” and “No B is C”. First we write a table exhausting all possible combinations of A, B, C and their negations (cf. Boole’s connstituents)
ABC ABc AbC Abc aBC aBc abC abc
Jevons called such a list an “abecedarium” and later a “logical alphabet”. The premise “All A is B” tells us that the classes Abc and AbC are empty. Similarly from “No B is C”, it follows that ABC and aBC are empty. The final step is now to inspect the remaining classes, all constituents with the premises, to see what we can determine about the relation of A to C. We note that “No A is C” (there are no remaining combinations containing both A and C). In this way, we got a reasoning known in the traditional logic as Celarent. Similarly, under the additional assumption that none of the three classes A, B, C is empty, we can conclude that “Some A is not C”, “Some not-A is C” etc. What is important here is the fact that Jevons’ system was not limited to the traditional syllogistic conclusions (and he was very proud of it).
Jevons, as most of other logicians of that time, confined his attention almost exclusively to class logic. He combined statements of class inclusion with conjunctive and disjunctive assertions but almost never worked with truth-value relations alone. He preferred also, like Boole, to keep his notation in the form of equations (writing for example A = AB to express the fact that all A is B). This preference for “equational logic” as Jevons called it was one of the reasons of the fact that he did not consider problems of a truth-value nature (though his method operates very efficiently with such problems).
The methods of Boole and of Jevons were suitable for a mechanization. Jevons devised a number of laborsaving devices to increase the efficiency of his method. The most important were his “logical abacus” and his “logical machine”.
Jevons created a logical machine to express the formalisms and get the computed output. It had some defects:
- Since statements should be fed to the machine in a clumsy equational form, it is made unnecessarily complicated
- There was no efficient procedure of feeding “some” propositions to it
- It was cumbersome to extend the mechanism to a large number of terms (Jevons planned to build a machine for ten terms but abandoned the project when it became clear that the device would occupy the entire wall space of one side of his study)
- the machine merely exhibits all the consistent lines of the logical alphabet but it does not perform the analysis of them to indicate the desired conclusion.
Jevons’ idea of building a logical machine was developed after him. Several other devices were proposed. Allan Marquand, Charles P. R. Macaulay, Annibale Pastore were some of the notable efforts.
The first electrical analogue of Jevons’ machine was suggested by Allan Marquand in 1885 and in 1947 an electrical computer was constructed at Harvard by T. A. Kalin and W. Burkhart for the solution of Boolean problems involving up to 12 logical variables (i.e. propositions or class letters).
What was the import of Jevons’ contribution to the development of logic? First of all he developed the ideas and methods of Boole removing some of their defects, e.g. introducing the inclusive interpretation of “or” what made possible a great simplification and what was welcome by all later writers on the algebra of logic. He did also very much to mechanize Boole’s methods inventing various devices which facilitated the practical usage of them.
There was a strong rivalry between Venn and Jevons. In Venn’s opinion the aim of symbolic logic was to build a special language which would enable “to extend possibilities of applying our logical processes using symbols”.
He used Latin letters as symbols of classes, 0 and 1 as symbols of the null and universe classes, respectively, introduced complement, intersection, union, subtraction and division of classes. By x - y he meant the class remaining after elimiantion from the class x the elements of the class y provided that y is a part of x. Subtraction was a converse operation to the union. Similarly division was considered as a converse to the intersection. It was not determined uniquely. The expression x > 0 denoted the fact that the class x is not empty. It was a negation of the expression x = 0. The equation x = y was understood by Venn as the sentence “there are no entities which belong to x but do not belong to y and there are no entities belonging to y but not to x”. He wrote it as x*y^c + x^c*y = 0.
As one of the main aims of symbolic logic Venn considered solutions of logical equations and elimination of variables. Contrary to Boole and Jevons he considered not only equations but also inequalities. For solving such problems he used algebraical methods as well as diagrams.
One can define a logical diagram as a 2D geometric figure with spatial relations that are isomorphic with the structure of a logical statement. Historically the first logic diagrams probably expressed statements in what today is called the logic of relations. The tree figure was certainly known to Aristotle, in medieval and Renaissance logic one finds the so called tree of Porphyry which is another example of the type of diagram. We see diagrams in various “squares of opposition”, in “pons asinorum” of Petrus Tartaretus.
As a first important step toward a diagrammatic method sufficiently iconic to be serviceable as a tool for solving problems of class logic we may consider the use of a simple closed curve to represent a class. It is impossible to say who used it first. We must mention here J. Ch. Sturm and his Universalia Euclidea (1661), G. W. Leibniz (who used circles and linear diagrams), J. Ch. Lange (and his Nucleus logicae weisianae, J. H. Lambert (and his linear method of diagramming explained in Neues Organon) and L. Euler. The latter introduced them into the history of logical analysis.
John Venn’s method is a modification of Euler’s. It has elegantly overcome all limitations of the latter.
There are diagrammatic methods invented by Allan Marquand, Alexander Macfarlane, W. J. Newlin, W. S. Hocking, and Lewis Carol.
Venn’s diagrams can be used for solving problems not only in the class logic but also in the propositional calculus. Using this procedure we can solve with the help of diagrams various problems of propositional logic which concern simple statements without parentheses. In the latter case some insolvable difficulties arise.
It is not true that Venn only improved slightly Euler’s method by changing shapes of figures. The main difference between Euler and Venn lies in the fact that Venn’s method was based on the idea of decomposition of the universe into constituents (which we do not have by Euler). Diagrams served Venn not only to illustrate solutions obtained in another way but they were in fact a method of solving logical problems.
The analogy between logic and algebra which led to the origin of the algebra of logic was the following: a solution of any problem by solving an appropriate equation is in fact a derivation of certain consequences from the initial conditions of the problem. Hence the idea of extending this method to problems of unquantitative character. This tendency had a source and a good motivation also in Leibniz’s works and ideas.
The problem was to develop, in analogy to the algebra, a method of expressing unquantitative information in the form of equations and to establish rules of transformation of those equations. This led to the construction of systems called today Boolean algebras.
Thought: The distinction between Boole’s algebra and Boolean algebra is noted here.
They were formulated in the language of classes as extension of concepts. Later another interpretation - namely the logic of propositions was developed. In this way logic was freed from the domination of epistemology and so its revival as an independent science was brought. It was shown that logic can be studied without any reference to the processes of our mind.
Later logicians such as Peirce, Gergonne, and Schröder developed the algebra of logic, removing the imperfections.
The 20th Century Way to Formalization and Mechanization
The logic of 20th century where the development of the idea of formalization and mechanization took place, there were two traditions. The first, often called algebraic, originated with Augustus De Morgan and George Boole and grew through the researches of their English followers such as Jevons and Venn, as well as those of Peirce in the United States and Schröder in Germany. They treated the analogy between the laws of algebra and the laws of logic as a guide in their investigations. Their aim was to develop a method of expressing unquantitative information in the form of equations and to establish rules of transformations of those equations. Systems constructed by them have various interpretations: class-theoretic, propositional etc. Generally speaking they investigated the following sort of questions: given an equation between two expressions of the calculus, can that equation be satisfied in various domains. It should be admitted that they had no notion of a formal proof.
The second tradition, often called the logistic method, can be characterized by a new aim. It was developed to build foundations of mathematics as science and consequently mathematics and mathematical methods were no longer treated as a pattern for logic but rather as a subject of logical studies. Peano and Frege can be seen as founders of this tradition. It was later developed and perfected by Bertrand Russell.
Early logical works of the italian mathematician Giuseppe Peano were based on the ideas of the algebra of logic.
Calcolo Geometrico secondo I’Ausdehnungslehre di H. Grassmann, preceduto dalle operazioni della logica deduttiva (1888)
Peano used there the logic of George Boole, Peirce, and Schröder in mathematical investigations but introduced into it a number of innovations: he used for example different signs for logical and mathematical operations, introduced the distinction between categorical and conditional propositions that was to lead him to quantification theory.
Already in this paper one can observe that Peano set great store by mathematical symbolism. The propagation of a symbolic language in mathematics and the invention of a good symbolism is just one of his greatest merits. Peano’s activity in this direction was strongly connected with the idea of characteristica universalis of Leibniz. He considered the realization of Leibniz’s ideas as a main task of the mathematical sciences.
Peano developed a symbolic language to use it later for axiomatization of mathematics. The first attempt in this direction was his book Arithmetices principia nova methodo exposita (1889). It contains the first formulation of Peano’s postulates for natural numbers.
The logical part of the work presents formulas of the propositional calculus, of the calculus of classes and a few of the quantification theory. The notation used is much better than that of Boole and Schröder. Peano distinguishes between the propositional calculus and the algebra of classes.
The aim of the book is to rewrite arithmetic in symbolic notation. The primitive arithmetical notions are: number, one, successor, and equality. Peano formulates 4 identity axioms and 5 proper arithmetical axioms.
In the sequel Peano develops on the basis of these axioms not only the arithmetic of natural numbers but deals also with fractions, real numbers, even with the notion of limit and definitions in point-set theory.
Peano introduced new notions by definitions. They were in fact recursive definitions not satisfying the general conditions he put on definitions. He claimed namely that a definition must be of the form x = a or a properSubsetOf x = a where a is a certain condition, x is a notion being defined and a is a “an aggregate of signs having a known meaning”. He formulated no theorem like Theorem 126 from Dedekind’s 1888 paper which would justify definitions by recursion.
It is not the only defect of Peano’s Principia. A more grave one is the fact that formulas are simply listed, not derived and they could not be derived, because no rules of inference were given and no notion of a formal proof was introduced. This is perhaps a consequence of the fact that Peano was interested in logic only as in a tool which helps us to order the mathematics and to make it more clear. He was not interested in logic for itself.
What is presented by Peano as a proof is actually a list of formulas which are such that, from the point of view of a working mathematician, each formula is very close to the next. But one cannot speak here about derivation or deduction. This brings out the whole difference between axiomatization and formalization.
The absence by Peano of, for example, the modus ponens is connected with his inadequate interpretation of the conditional. He read ‘a properSubsetOf b’ as ‘from a one deduces b’ which remains vague. He did not use truth values at all.
In a series of papers, Principii di logica matematic (1891), Formule di logica matematica (1891), Sul concetto di numero (1891) Peano undertook to prove the logical formulas that he simply listed in Principia. But again those proofs suffer from the absence of rules of inference.
Some of Peano’s remarks could suggest that his logical laws should be taken as rules of inference, not as formulas in a logical language. But this would not yield a coherent interpretation of his system.
Geometry was just the second domain of mathematics where Peano successfully applied his symbolic-axiomatic method. His system of geometry is based on two primitive notion,s namely on the nation of point and interval. It is similar to the approach of Pasch. Investigating the foundations of geometry Peano popularized the vector method of H. Grassmann and brought it to perfection. In this way he also gave a certain impulse to the Italian school of vector analysis.
The idea of presenting mathematics in the framework of an arithmetical symbolic language and of deriving then all theorems from some fundamental axioms was also the basic idea of Peano’s famous project Formulario. It was proclaimed in 1892 in the journal Rivista di Matematica. This journal was founded by Peano in 1892 and here his main logical papers and papers of his students were published. The aim of his project was to publish all known mathematical theorems.
Peano treated Formulario as a fulfillment of Leibniz’s ideas. He wrote “After two centuries, this ‘dream’ of the inventor of the infinitesimal calculus has become a reality … We now have the solution to the problem proposed by Leibniz”.
He hoped that Formulario would be widely used by professors and students. He himself immediately began to use it in his classes. But the response was very weak. One reason was the fact that almost everything was written there in symbols, the other was the usage of latino sine flexione (that is Latin without inflection - an artificial international language invented by Peano) for explanations and commentaries.
What was the real significance of Peano’s writings for the formalization and mechanization of reasonings, what were his real merits and achievements? One should admit that his works were of minor significance for logic proper, but they showed how mathematical theories can be expressed in one symbolic language. Peano believed that this would help to answer the question: “how to recognize a valid mathematical proof?”
The influence of Peano and his writings on the development of mathematical logic was great.
In a letter to Jourdain from 1912, B. Russell wrote: “Until I got hold of Peano, it had never struck me that Symbolic Logic would be any use for the Principles of mathematics, because I knew the Boolean stuff and found it useless. It was Peano’s, together with the discovery that relations could be fitted into his system, that led me to adopt symbolic logic.”
It should be admitted also that Russell learned of Frege and his works just through Peano.
Frege’s system ushered in the modern epoch in the history of logic. The year 1879 the year of the publication of Frege’s Begriffsschrift is considered as the beginning of modern logic. George Boole and the whole algebraic tradition wished to exhibit logic as a part of mathematics. Frege wanted to realize a different aim which seemed to be inconsistent with the former – namely, he wished to show that arithmetic, and consequentyl mathematics (the so-called arithmetization of analysis has already shown that analysis and in particular the theory of real and complex numbers can be reduced to arithmetic of natural numbers) is identical with logic. There is in fact no inconsistency between these two tendencies.
Frege demanded a formal rigour within the study of logic but tried also to show that numbers can be defined without reference to any notions other than those involved in the interpretation of his calculus as a system of logic. Frege built a precise system which included the traditional material and the newer contributions of Leibniz and Boole, a system being more regular than ordinary language and having the property that everything that is required for the proof of theorems is set out explicitly at the beginning and the procedure of deduction is reduced to a small number of standard moves in Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reínen Denkens (1879).
Wanting to free logic from too close attachment to the grammar of ordinary language, Frege devised a language that deals with the conceptual content which he called Begriffsschrift. This term is usually translated into English as ‘ideography’ (a term used in Jourdain’s The Development of the Theories of Mathematical Logic and the Principles of Mathematics (1912) - this paper was read and annotated by Frege) or as Austin has proposed, as ‘concept writing’.
Frege wrote about his language (in an unpublished fragment dated 26 July 1919): “I do not start from concepts in order to build up thoughts or propositions out of them; rather, I obtain the components of a thought by decomposition(Zerfällung) of the thought. In this respect by Begriffsschrift differs from the similar creations of Leibniz and his successors in spite of its name, which perhaps I did not chose very aptly”.
Answering to the censure for wrecking the tradition established in the previous 30 years he wrote in 1882:
“My intention was not to represent an abstract logic in formulas, but to express a content through written signs in a more precise and clear way than it is possible to do through words. In fact, what I wanted to create was not a mere calculus ratiocinator but a lingua characteristica in Leibniz’s sense”.
Frege’s ideography is a ‘formula language’, a language written with special symbols, ‘for pure thought’, that are manipulated according to definite rules. Wanting to construct a system of logic which would provide a foundation for arithmetic he could employ neither the algebraical symbolism nor the analogies between logic and arithmetic uncovered by Boole and others. Though the subtitle of Frege’s book says that his ideography is to be modeled on the language of arithmetic still the main resemblance is in fact in the use of letters to express generality.
One of the great innovations of Begriffsschrift is the analysis of a sentence not in terms of subject and predicate, as it was so far, but in terms of function and arguments. This idea, coming from mathematics, had a profound influence upon modern logic.
According to Frege, all symbols have meaning. The meaning of a sign which is a subject int he linguistical sense, is an object. In a symbolic language every expression must denote an object and one cannot introduce any symbol without meaning. Expressions of such a language denote either objects or functions. The word ‘object’ (Gegenstand) must be understood here in a narrower sense it denotes a described individual, a class or the logical value (which means here ‘truth’ (das Wahre) and ‘falsity’ (das Falsche). But sometimes Frege used the word ‘object’ more generally, speaking about ‘saturated objects’ (i.e. objects in a proper sense) and about ‘unsaturated objects’ (i.e. functions). By calling functions ‘unsaturated objects’ he meant that they are not completely defined. They have one or more unsaturated places. In particular, functions with one unsaturated places whose values are truth values he called concepts, and functions with more unsaturated places - relations. Those functions were for him timeless and spaceless ideal objects.
Frege introduced also a symbol for identity of content. If J and K are names o any kind, i.e. not necessarily propositional signs, then the expression |- (J = K) means “The name J and the name K have the same conceptual content, so that J can always be replaced by K and conversely”. Note that the judgement |- (J = K) is about names (signs) and not about their content.
One can formulate strong arguments against such a conception. The recognition of them has forced Frege to split later the notion of conceptual content into sense (Sinn) and reference (Bedeutung).
Frege used a 2D notation as opposed to linear 1-dimensional form used previously for this purpose.
Frege introduced a sign of content and a sign of judgment. If A is a sign or a combination of signs indicating the content of the judgment then the expression -A means: ‘the circumstance that A’ or ‘the proposition that A’, and the symbol |- A expresses just the judgement that A.
Let |-A stand for (bedeutet) the judgement ‘opposite magnetic poles attract each other’; then -A will not express (ausdrücken) this judgement; it is to produce in the reader merely the idea of the mutual attraction of opposite magnetic poles, say in order to derive consequences from it and to test by means of these whether the thought is correct.
In modern symbolism, the axioms used by Frege are as follows:
- p -> (q -> p)
- [p -> (q -> r)] -> [(q -> (p -> r)]
- [p -> [q->r)] -> [(q -> (p -> r)]
- (p -> q) -> (not q -> not p)
- not not p -> p
- p -> not not p
- c = d -> f(c) = f(d)
- c = c
- forAll(x, f(x -> (a))) ?
Frege stated that he used only one principle of inference in derivations of theorems from the axioms, but in fact he used four principles. TODO: Verify what Hume’s principle is and how it applies here. The rule explicitly mentioned by him is the rule of detachment. It explains why he has chosen just negation and conditional as the only primitive connectives: he wanted to preserve the simple formulation of the rule of detachment. Beside the latter Frege used in Begriffsschrift also an unstated rule of substitution, the rule of generalization and the rule leading from A -> F(x)A -. forAll(x, F(x)) provided that x does not occur free in A.
In the framework of this system Frege proved various theorems giving detailed proofs of them. Those proofs, even in the absence of some explicit rules, can be unambiguously reconstructed. His axioms together with the 4 rules form indeed a complete set of axioms in the technical sense of that phrase. Frege himself did not raise, of course, any question of completeness or consistency or independence. Note that the third of Frege’s axiom is redundant, since it can be derived from the first two. It is also possible to replace, in the presence of 1 and 2, the axioms 4, 5, and 6 by a single new axiom for negation, namely:
not p -> not q -> (q -> p)
Frege used the whole machinery presented above to develop, in the third part of Begriffsschrift, a theory of mathematical sequences. He introduced the relation called later by Whitehead and Russell the ancestral relation. It served him for the justification of mathematical induction in Grundlagen der Arithmetik and generally to the logical reconstruction of arithmetic what was his main purpose in Grundgesetze der Arithmetik. In this way, Frege became the founder and the first representative of logicism in the philosophy of mathematics.
Though Frege’s system constructed in Begriffsschrift has turned out to be inconsistent - this was discovered in 1901 by Russell who built in this system a paradox of the class of classes that do not contain themselves as elements, known today as Russell’s paradox - nevertheless Frege’s achievements remain really great. Begriffsschrift was the first comprehensive system of formal logic and it contains all the essentials of modern logic.
TODO: Examine how Schröder’s quantification theory holds up. Its main novelties were the analysis of the proposition into function and arguments rather than subject and predicate, the quantification theory, the truth-functional propositional calculus and what is most important here, a system of logic in which derivations are carried out exclusively according to the form of the expressions.
Frege repeatedly opposed a lingua characteristica to a calculus ratiocinator. In works of his predecessors calculus of propositions and classes, logic, translated into formulas, was studied by means of arguments resting upon an intuitive logic. Frege constructed logic as a language that did not need to be supplemented by an intuitive reasoning. Therefore he was very careful to describe his system in purely formal terms (speaking for example of letters rather than of variables to avoid any imprecision and ambiguity).
The reception of Frege’s work was rather bad. One of the reasons was certainly his symbolism. Though it has many advantages it facilitates inferences by detachment, allows to perceive the structure of a formula at a glance or to perform substitutions with ease - it has also some disadvantages. One of them is the fact that it occupies a great deal of space and is not easy to print. Frege himself said that “the comfort of the typesetter is certainly not the summum bonum”, but it cannot be denied that his symbolism very often hindered to grasp the importance of his ideas or even to understand the contents of his papers. On the other hand one should admit that Frege presented too many difficult novelties at once and with too little concessions to human weakness. Logicians have recognized the merits of Frege’s ideas only when they themselves became ready to discuss the questions he raised.
The first who gave serious recognition to Frege’s works was G. Peano. They corresponded with each other, exchanged copies of their paper,s exchanged comments and remarks on them. The real reception of ideas of Frege began from Russell who learned of Frege and his works through Peano. Russell studied Frege’s papers very carefully and appreciated their importance. This had deep consequences and strongly influenced the development of logic.
The projects of Peano and Frege presented in the previous sections found their fulfillment in the monumental work Principia Mathematica written by Alfred North Whitehead and Bertrand Russell, and published in 3 volumes in the year 1910–1913. It is a detailed study of logic and set theory and a construction, on that basis, of the classical mathematics.
In June 1901 when studying the first volume of Frege’s Grundgestze der Arithmetik Russell discovered the paradox of the class of all classes that do not contain themselves as elements. This meant that the system of logic to which Frege wanted to reduce mathematics was inconsistent. Russell communicated his discovery to Frege on 16 June 1902. In this situation, the task of the reduction of mathematics to logic should be resumed.
Discussing ‘the contradiction’, as he called it, in The Principles of Mathematics, Russell mentioned, without much elaboration, that “the class as many is of a different type from the terms of the class” and that “the class as many is of a different type from the terms of the class” and that “it is the distinction of logical types that is the key to the whole mystery”. He examined also other solutions but found them less satisfactory.
TODO: I have to examine how Aristotle’s sortals compares to the idea of type theory up here.
Soon after publishing The Principles of Mathematics, Russell abandoned the theory of types. In a paper written in 1905, he proposed 3 theories to overcome the difficulties raised by the paradoxes (at that time Russell knew of other paradoxes as well; for instance the Burali-Forti paradox and that of the greatest cardinal). They were: 1) the zigzag theory (“propositional functions determine classes when they are fairly simple, and only fail to do so when they are complicated and recondite”), 2) the theory of limitation of size (“there is no such a thing as the class of all entities”), 3) the no-classes theory (“classes and relations are banished together”). Notice that the theory of types is not mentioned here. Add also that Russell believed that the no-classes theory “affords the complete solution to all the difficulties”.
Those hopes disappeared soon and Russell turned back to the theory of types and proceeded to develop it in detail. It was done in a paper “Mathematical logic as based on the theory of types” published in 1908 and later in a monumental work Principia Mathematica written together with his teacher A. N. Whitehead.
Russell saw the key to the paradoxes in what he called the vicious circle principle: “No totality can contain members defined in terms of itself”. This is connected with the principle of Poincaré forbidding impredicative definitions of objects, which Russell incorporated into his system. To realize it Russell saw the universe as dividing into levels or types. All conditions and properties we can consider form an infinite hierarchy of types: properties of the first types are properties of individuals, properties of the second type are properties of properties of individuals etc. We can speak of all the things fulfilling a given condition only if they are all of the same type. These intuitions led to the ramified theory of types developed by A. N. Whitehead and B. Russell. It made possible the elimination of paradoxes. This theory, rather complicated and formulated ad hoc, was simplified later by F. P. Ramsey and L. Chwitsek and is known today as the simple theory of types.
The theory of types was the basis of the system of Principia Mathematica. Whitehead and Russell’s aim they wanted to realize in it was the reduction of the pure mathematics to logic. They used of course some ideas and achievements of Peano and Frege. The whole work was written in a symbolic language, the symbolism of Peano was adopted rather than that of Frege. The derivations of theorems were performed with the same rigour as it was by Frege. The system of logic of Principia was the propositional calculus, adorned with other features such as the theory of definite description,s introduced there especially to define mathematical functions. Set theory was widely used, but a set X was reduced to a propositional function via the contextual definition of a property (or functional function) which X satisfied. The propositional calculus was based on two primitive notions: negation and disjunction, all other connectives were defined in term of those two, namely: p ⊃ q = not p or q p . q = not(not p or not q) p identicalTo q = p ⊃ p and q ⊃ p
The basic axioms were:
A) the propositional calculus (p or p) ⊃ p q ⊃ (p ⊃ q) (p or q) ⊃ (q or p) [p or (q or r)] ⊃ [(p or q) ⊃ r] (q ⊃ r) ⊃ [(p or q) ⊃ (p or v)]
B) the quantification theory (x, y are here variables of the same type and x is not free in p):
(x) Fx ⊃ Fy (x) (p or F(x)) ⊃ (p or (x)Fx)
C) The axiom of reducibility D) identity E) The axiom of infinity F) The axiom of cohice
Łukasiewicz in Demonstration de la compabilitité des axiomes de la théorie de la deduction (1925) and Bernays in Axiomatische Untersuchungen des Aussagen-kalküls der Principia Mathematica (1926) observed that the axiom (A4) could be derived from the others and therefore it is superfluous.
The basic rules of inference were the rule of detachment (i.e. modus ponens), the generalization, and the (unspoken but used) rule of substitution.
Remark that there is a certain inelegance in this system. Since the logical sign of negation and disjunction are to be taken as primitive, they should be used in the formulation of the axioms and rules of inference to the exclusion of all other signs. Of course, one can replace p ⊃ q by not p or q in those axioms but they become then rather complicated.
Peano and Frege constructed symbolic languages making possible the axiomatization (Peano) and formalization (Frege) of mathematics and mathematical reasonings. Russell and Whitehead improved their systems eliminating difficulties and paradoxes they met, improving their symbolism and bringing out the formal development of mathematics.
It is worth noting here that for Russell every logical formula had a fixed meaning, hence there was no question of reinterpreting any sign (as it was the case by the algebraists). For Russell (and for Frege as well) logic was about something, namely everything. The laws of logic have content: they are the most general truths about the logical furniture of the universe. Russell wrote: “Logic is concerned with the real world just as truly as zoology, though with its more abstract and general features”. Observe also that Frege’s and Russell’s conception of logic was all-embracing in that it included indiscriminately both logical and metalogical topics. Therefore neither Frege nor Russell raised any serious metasystematic questions at all. For them logic was the system – the results of logic were simply the logical truth,s and were to be arrived at by deriving them in the system.
Leopold Löwenheim paper “Über Möglichkeiten im Relativkalkül” which dealt with a problem connected with the validity, in different domains, of formulas of what we call today the first order predicate calculus and with various aspects of the reduction and the decision problems.
Löwenheim was squarely in Schröder’s school, i.e. in the algebraic tradition. He used in the paper we are discussing here Schröder’s notation, he held that all of mathematics can be framed within the relative calculus.
In a paper in 1940, he argued that mathematics can be “Schröderized”. We can suspect that he did not fully grasp the notion that by means of formal representation we may fully exhibit the intuitive content of mathematical discourse and the inferential relations among mathematical sentences.
Theorem 2 in Section 2 of Löwenheim’s paper from 1915 is the now famous Löwenheim theorem. It states that if a finitely valid well-formed formula is not valid, then it is not k-valid. In other words if a well-formed formula is k-valid then it is valid provided there is not some finite domain in which it is invalid.
To prove this theorem Löwenheim shows first of all that for any given first-order formula one can obtain a formula that has a certain normal form and is equivalent, so far as satisfiability is concerned, to the given formula. Observe that he shifts here from validity to satisfiability. The reason is the fact that the formula constitutes the left side of an equation whose right side is 0 and to write that a formula is equal to 0 amounts to writing a negation sign in front of the formula. The formula in normal form contains existential quantifiers, universal quantifiers and a quantifier-free expression. The number of existential quantifiers depends on the number of individuals in the Denkbereich, in particular for infinite domains there are infinitely many quantifiers and we get an infinitely long expression.
Note also that Section 3 of Löwenheim 1915 contained the positive solution of the decision problem for the singularly predicate calculus of first order with identity. The proof of the result was later simplified by Skolem in Untersuchungen über die Axiome des Klassenkalkülus und über Produktations- und Summationsproblem, welche gewisse Klassen von Aussagen betreffen (1919) and Behmann in Beiträge zur Algebra der Logick, insbesondere zum Enscheidungsproblem (1922). Section 4 presented the reduction of the decision problem for the first-order predicate calculus to that of its binary fragment. This result was later sharpened by Herbrand in Sur le problème de la logique mathématique (1931) and Kalmár in Ein Beitrag zum Enscheidungsproblem (1932), Über einen Löwenheimschen Satz 1934, Zurückführung des Entscheidungsproblem auf den Fall von Formeln mit einer einzigen, binären, Functionsvariablen 1936.
In Logisch-kombinatorische Untersuchungen über die Erfülbarkeit oder Beweisbarkeit mathematische Sätze nebst einem Theoreme über dichte mengen (1920) the Löwenheim’s theorem was extended by the Norwegian mathematician and logician Thoralf Skolem. Skolem generalized it to denumerably infinite sets of formulas and proved that if a countable set F of first-order propositions is satisfiable, i.e. has a model, then there exists a denumerable submodel of this model in which all formulas of F are satisfied.
To demonstrate the theorem Skolem proved that every formula of the first-order predicate calculus has special normal form that is called today a Skolem normal form for satisfiability. Such a form consists of a string of universal quantifiers, a string of existential quantifiers and then a quantifier-free part. It was shown that a formula is satisfiable in a given domain if and only if its Skolem normal form for satisfiability is satisfiable in the domain. The denumerable submodel needed in the theorem was obtained by Skolem from the original model by a process of thinning out. This process was performed with the help of the axiom of choice. The usage of the normal form of a formula enable Skolem to dispense with the infinite strings of quantifiers considered by Löwenheim. Note that in 1929 Skolem gave a simplified version of the proof using again the axiom of choice, more exactly König’s lemma which can be regarded as a version of the axiom of dependent choices.
Skolem normal forms of formulas have become one of the logician’s standard tools. They constitute a reduction class for quantification theory.
In 1922 T. Skolem published a paper “Einige Bemerkungen zur axiomatischen Begründung der Mengenlehre” in which he proved a weaker version of his theorem not using this time the axiom of choice. He showed that if a set F of formulas is satisfiable then it is satisfiable in a denumerable universe (i.e. in the domain of natural numbers). There was no mention of submodels. To prove this Skolem first set up effective functions on the integers and then showed, by constructing numerical quantifier-free instances of the given quantified formula, that these functions can act as evaluations for the existential variables.
From our point of view of the development of the idea of formalizing and mechanizing the reasonings, the most important paper is the one from Uber die mathematische Logick (1928). It was a lecture delivered before the Norwegian Mathematical Society. Skolem proposed there a proof procedure for the first-order predicate calculus. To describe it consider an arbitrary closed formula tp in the prenex form that is, a phi consists of a string of universal and existential quantifiers and then of a quantifier-free matrix. We put it into what one calls today its functional form for satisfiability - all quantifiers are dropped and the occurrences of each variable bound by an existential quantifier are replaced by a functional term containing the variables that in phi are bound by universal quantifiers preceding the existential quantifier. For example, if phi is of the form (x)(y)(Ez)(u)(Ew)ip(x, y, z, u, w) where Psi is quantifier-free then the functional form of phi denoted by phi’ will be psi(x,y,f(x,y),u,g(x,y,u))
where f(x,y) and g(x,y,u) are functional terms (to be honest we should note that Skolem did not use this notion), f and g being new function symbols.
Introduce now constants of various levels. 0 is the constant of the 0th level. Constants of the nth level are the expressions obtained when in each functional term of phi’, the functional form of phi, the variables are replaced by constants that include at least one constant of, but no constant beyond, the (n-1)th level. In this way, we can generate from 0 the lexicon of phi’ (the term ‘lexicon’ was introduced by Quine in A Proof Procedure for Quantification Theory (1955)). The subset of the lexicon of phi consists of all constants of levels n, we shall call the lexicon of level n.
Take now a formula X which is the functional form phi’ of or any truth-function part of phi’. By a lexical instance of X we shall mean the formula obtained from X by replacing all the variables of X by elements from the lexicon of phi’. A solution of the nth level is an assignment of truth-values of lexical instance of atomic parts of phi’, such that it verifies the conjunction of all the lexical instance of phi’ formed from the lexicon of (n-1)th level of phi.
It can be seen that 1) any solution of the nth level is an extension of a solution of the (n-1)th level
- Either i) for some n there is no solution of the nth level or ii) for every n there is a solution of the n level. In the case i) phi is not satisfiable (Skolem used here the phrase ‘contains a contradiction’ (enthält einen Wider-spruch). In this way we get that if phi is satisfiable then for every n there is a solution of the nth level. In papers from 1922 and 1929 Skolem obtained also the converse, namely if for every n there is a solution of the nth level, then phi is satisfiable (in fact he actually proved that phi is k-satisfiable). In this way one gets a proof procedure for the first-order predicate calculus: given a formula phi in prenex form and a number n, we can effectively decide whether or not there is a solution of the nth level for phi if for some n there is no solution of the nth level, then phi is not satisfiable, hence not phi is valid. Observe that this approach is an alternative to the axiomatic one developed by Peano, Frege, and Russell and continued by Hilbert and his school. Note also that Skolem was a constant opponent of all formalist and logicist foundational programs. He insisted that foundations of mathematics lay in what he called ‘the recursive mode of thought’.
Add that in the paper from 1928 Skolem considered also the decision problem from the point of view of his proof procedure. Namely for certain class of formulas one can effectively decide whether or not for every n there is a solution of the nth level. An example of such a class is the class of formulas whos prefix consists of a single universal quantifier followed by any number of existential quantifiers (a subclass of this class consisting of formulas of the form (x)(Ey)x, X being quantifier-free was considered earlier by Bernays and Schönfinkel (1928), the whole class studied independently and simultaneously with Skolem by Ackermann whose results go beyond that of Skolem. (cf. Ackermann Über die Erfüllbarketi gewisser Zahlenausdrücke (1928)).
Skolem considered also the subclass of formulas of the form (x_1)…(x_m)(Ey_1)…(Ey_n)x where x is quantifier-free and such that all variables x_i,…x_m occur in each of the atomic parts of it.
To sum up we may say that Skolem was interested in analyzing statements in terms of truth-functional logic. Towards this end he introduced a notion of expansion. Being inspired by Löwenheim (1915) he eliminated the need for first fixing a universe over which to expand a formula and considered expansions which were finitely long (whereas Löwenheim’s were not, in fact they could even be “uncountably long”). An expansion of a formula was simply a finite conjunction of quantifier-free instances of the formula obtained by following certain instantiation rules which reflect the idea of making successive choices (in the sense of picking symbols).
As we have mentioned above Skolem saw the foundation of mathematics in “the recursive mode of thought”. In a opposite direction were working the German mathematician David Hilbert ad his school. Hilbert’s interest in foundations dates back to his investigations of geometry. In his famous lecture at the International Congress of Mathematicians in Paris in 1900 he mentioned the consistency of analysis as a second problem on his list of 23 main problems in mathematics that should be solved. Hilbert elaborated on this problem later but in a rather obscure manner in 1904. This paper is important also for other reasons: namely Hilbert introduced here the themes that he was going to develop, modify, or make more precise in his further works.
He returned to foundational questions in 1918. At that time a great advance had been made in formal method.s Particularly influential was Principia Mathematica which Hilbert called “the crowning achievement of the work of axiomatization”. But Hilbert’s view of this achievement was quite different from Russell’s. As we pointed out earlier Russell claimed that Principia contained a system of logic on which all mathematical reasoning should (and can) be based. It had an epistemological priority. For Hilbert Principia provided an empirical evidence of the possibility of formalization. This work showed that all mathematical results can be captured by appropriate formal systems. Hilbert claimed that we can think of the content of much of mathematics as given by its formal representation.
Hilbert used this possibility in his famous program of proving the consistency of mathematics, called today Hilbert’s program. His proposal was Kantian in character. He wrote in 1926 as follows:
Kant taught - and it is an integral part of his doctrine - that mathematics treats a subject matter which is given independently of logic. Mathematics, therefore, can never be grounded solely on logic. Consequently, Frege’s and Dedekind’s attempts to so ground it were doomed to failure.
As a further precondition for using logical deduction and carrying out logical operations, something must be given in conception, viz., certain extralogical concrete objects which are intuited as directly experienced prior to all thinking. For logical deduction to be certain, we must be able to see every aspect of these objects, and their properties, differences, sequences, and contiguities must be given, together with the objects themselves, as something which cannot be reduced to something else and which requires no reduction. This is the basic philosophy which I find necessary not just for mathematics, but for all scientific thinking, understanding and communicating. The subject matter of mathematics is, in accordance with this theory, the concrete symbols themselves whose structure is immediately clear and recognizable.
Such concrete objects are just natural numbers considered as numerals (certain systems of symbols): 1, 11, 111, … One can exactly describe them and relations between them. The part of mathematics talking about those objects is certainly consistent (because facts cannot contradict themselves). But in mathematics, beside such finitistic, real theorems describing concrete objects, we also have infinitistic, ideal ones talking about the actual infinity (to which no real objects correspond). And therefore mathematics needs a justification and foundations. The convincing proof of the consistency of mathematical theory ought to be a finitistic one (i.e. a proof using no ideal assumptions). Hilbert thought that such a proof was possible and proposed a program for providing it. It consisted off two steps:
1/ Formalization of mathematics (Hilbert, first of all, thought here about arithmetic, analysis, and set theory). It ought to be carried out by fixing an artificial symbolic language and rules of building in it well-formed formulas. Further axioms and rules of inference ought to be fixed (the rules could refer only to form, to the shape of formulas and not to their sense or meaning). In such a way theorems of mathematics become those formulas of our formal language which have a formal proof based on a given set of axioms and given rules of inference. There was one condition put on the set of axioms: they ought to be chosen in such a way that they suffice to solve any problem formulated in the language of a considered theory, i.e. they ought to form a complete set of axioms.
2/ Give a proof of the consistency of mathematics. Such a proof could be carried out by finitistic methods because it was enough to consider formal proofs, i.e. sequence of symbols, and to verify if there were two sequences such that one of them finishes with formula phi and the other with formula not phi. If there were such proofs then mathematics would be inconsistent, if not, then it would be consistent. But the study of formal proofs deals with infinite, concrete objects (namely sequences of symbols formed according to some rules) and hence is finitistic.
Observe that for Hilbert formalization was just the way in which we, as finite intelligences, can in fact deal with the infinite. We attain to the infinite by means of signs. He recognized in quantifiers that constituent of formal systems that allows us to do this.
The most comprehensive publication in this direction is the two volume monograph published with P. Bernays Grundlagen der Mathematik (1934, 1939) which explained the situation and set forth the results achieved up to the time of publication.
Hilbert based his system of logic on the following axioms:
I. Axioms of implication:
- A -> (B -> A)
- (A -> (A -> B)) -> (A -> B)
- (A -> B) -> ((B -> C) -> (A -> C))
II. Axioms of conjunction
- A & B -> A
- A & B -> B
- (A -> B -> ((A -> C) -> (A -> B & C))
III. Axioms of disjunction
- A -> B A or B
- B -> A A or B
- (A -> C) -> ((B -> C) -> (A V B -> C))
IV. Axioms of equivalence
- (A ~ B) -> (A -> B)
- (A ~ B) -> (B -> A)
- (A -> B) -> ((B -> A) -> (A ~ B))
V. Axioms of negation
- (A -> B) -> not B not not A
- A -> not not A
- not not A -> A
VI. Axioms for quantifiers
- forAll(x, A(x) -> A(a))
- A(a) -> thereExists(x, A(x))
The following three rules of inference were allowed
i) the rule of detachment ii) A -> B(a) | A -> forAll(x, B(x)) iii) B(a) -> | thereExists(x, B(x) -> A) where a does not occur in B(a) and the variable a does not occur in A.
In fact Hilbert needed also the principle of substitution in derivations of theorems from axioms. Note that the given set of axioms is really perspicuous and natural.
In the early days of his program Hilbert introduced also a simplifying device in the formal systems, called today Hilbert-terms. He regarded them as auxiliary, proof-theoretical notations for use in obtaining proofs and shortening their presentation.
A term ε_xA(x) was to denote an element of x of which A holds, provided there are some. If A contains free variables then ε_xA(x) represents a function of those variables which picks out a suitable value for x given any values for those variables. In this way the very notation exhibits choice-like nature of quantification. Hilbert stated the following axiom:
A(a) -> A(ε_xA(x)) and indicated that the quantifiers ‘for all’ and ‘there exists’ can be defined by means of ε, namely thereExists(x, A(x)) as A(ε_xA(x)) and forAll(x, A(x)) as A(ε_x(¬A(x)).
Observe that this approach resembles the Skolem’s approach exploiting the similarities between the quantifier (or, more exactly, quantifier-dependence) and choice functions, but they went in different directions: Skolem used these similarities to denigrate the power of quantification and Hilbert was impressed with how much the quantifier does, insofar as it acts like a choice function.
Hilbert indicated a purely auxiliary character of Hilbert-terms showing that if any ‘ordinary’ sequent is proved with Hilbert-terms occurring in the proof, it can be proved without them occurring in the proof.
Though the program of Hilbert could not be fully realized (the incompleteness result of Kurt Gödel from 1931 showed that it is impossible), nevertheless the study started by Hilbert has been extremely fruitful.
One of the most important results of investigations generated by Hilbert’s program is the fundamental theorem of Jacques Herbrand.
The work of Herbrand can be viewed as a reinterpretation, from the point of view of Hilbert’s program, of the results of Löwenheim and Skolem.
Having adopted Hilbert’s finitistic viewpoint, Herbrand spoke not about satisfiability and validity, as Löwenheim and Skolem did, but used syntactic notions such as provability and (in)consistency.
The fundamental theorem contains a reduction (in a certain sense) of predicate logic to propositional logic, more exactly it shows that a formula is derivable in the axiomatic system of quantification logic if and only if its negation has a truth-functionally inconsistent expansion. Herbrand intended to prove this theorem by finitistic means.
Herbrand considered an axiomatic system of quantification logic similar to the system of Principia Mathematica and of Hilbert and Ackermann Grundzüge der theoretischen Logik (1928). He proved that it is equivalent to the quantification theory used by Whitehead and Russell.
Herbrand correlates with each formula Z of the predicate calculus an infinite sequence of propositional formulas having the form of a disjunction:
H_n(Z) = A_1 or … or A_n
These formulas are today called the Herbrand disjunctions. The definition of H_n is effective, i.e. H_n can be obtined from Z and n by means of a fixed algorithm. One can establish now the following relationship: Z is provable in the predicate logic if and only if there is an n such that H_n is a theorem of the propositional calculus.
To give the idea of how H_n(Z) is constructed consider the following example. Assume that Z is (x)(Ey)(z)M(x,y,z) where M is quantifier free Let tp be an arithmetical function such that phi(i) > i and phi(i) phi(j) for all integers i, j such that 1 <= i, j. Form the disjunction
or(from(i <= n), M(x_1, x_phi(i)) and replace in it every atomic formula by a propositional variable in such a way that different atomic formulas are replaced by different propositional variables. The resulting formula is the n_th Herbrand disjunction.
One may interpret the formula in the following way: suppose that we are trying to build a counterexample to the formula Z. We will then look for an element a and a function f correlating with each p an element f(p) such that ¬M(a, p, f(p)) is true. Let us substitute for p arbitrary values p_1, …, p_n. Hence the conjunction: and(from(i <= n), ¬M(a,p_i, f(p_i)) is true. The formula with the disjunction may thus be interpreted as a statement that whatever our choice of a and of the function f will be, our attempt to build a counterexample to Z will fail in the field of at most n elements.
We should prove now that the disjunction formula is provable in the propositional calculus if and only if Z is provable in the predicate logic. One part of this equivalence, namely the implication from the left to right is rather easy to prove. The proof of the other part is more difficult. Note that proving it Herbrand came very close tot he discovery of the completeness theorem. One can suspect that he did not make the decisive step only because he was constrained by the finitistic attitude of Hilbert’s program.
Remark that Herbrand’s proof of the fundamental theorem was fallacious. In 1939 Bernays wrote that “Herbrand’s proof is hard to follow”. Gödel claimed in 1963 that in the early forties he had discovered an essential gap in Herbrand’s argument but he never published anything on this subject. A detailed analysis of errors in Herbrand’s paper was published by Dreben, Andrews and Aanderaa in 1963. Note that a correct, strictly finitistic proof of the fundamental theorem was given by Bernays in Hilbert and Bernays’ 1939 work.
A detailed analysis of the proof of Herbrand’s theorem shows that we are able to get rid of the rule of modus ponens altogether. Herbrand considered this fact as an important one. It implies that if a formula Z is provable in the predicate calculus then there exists a proof of it consisting exclusively of subformulas of Z. This is connected with the Hauptastz of Gerhard Gentzen who rediscovered and greatly improve many of Herbrand’s results.
Herbrand showed an example of applications of his fundamental theorem in the paper “Sur la non-contradiction de l’Arithmétique” published in 1931. The manuscript of this was received by the editors on 27 July 1931 - on the same day Herbrand had an accident while climbing in the Alps and was killed in a fall. He proved there consistency of a fragment of arithmetic in which the formula that can be substituted into the induction scheme does not contain any quantifiers, or if it does, does not contain any function but the successor function. This result as well as the fundamental theorem discussed above, i.e. the analysis of quantification in terms of truth-functional properties of expansion can be treated without any doubt as an important contribution to the realization of the Hilbert’s school program.
Gentzen started his scientific career by publishing the paper “Über die Existenz unabhäangiger Axiomensysteme zu unendlichen Satzsystemen”. This relatively unknown paper which has received less attention since its publication than it deserves. Gentzen has shown in it that not all sentence systems possess independent axiom systems, whereas all ‘linear’ sentence systems do possess an independent axiomatization. This paper also reveals another source of inspiration for Gentzen’s investigations. It was the work of Paul Hertz. Gentzen used not only Hertz’s methodology but also some of his terminology. In his 1935 and later works, we find, for example, the terms ‘antecedent’ and ‘succedent’ of a sequent borrowed from Hertz, also the notion ‘logical consequence’ as used by Gentzen was largely inspired by Hertz’s work.
The most important from our point of view is his work “Untersuchungen über das logische Schliessen” from 1935. There he broke away from the traditional formulations of predicate logic as they were developed by Frege, Russell and Hilbert and presented two basically different verisons of predicate logic both in two variants, classical and intuitionistic. It should be noted here that similar attempt was made independently and simultaneously by S. Jaśkowski in his On the Rules of Supposition in Formal Logic (1934). Jaśkowski published a different version of ‘natural deduction’ based on ideas first put forward in Łukasiewicz’s seminar in 1926.
Gentzen’s idea of a ‘natural deduction’ came from detailed analysis of Euclid’s proof of the nonexistence of a largest prime number. It revealed to him what properties a system of natural deduction should have and led him to a calculus based on assumption formulae instead of the usual axiom formulae and to the separation of the rules for the logical operators into ‘introduction’ and ‘elimination’ rules.
Gentzen introduced two versions of predicate logic: one, called by him natural deduction (der Kalkül des natürlichen Schliessens) and denoted by NK (classical natural deduction and NJ (intuitionistic natural deduction) and second called logistic calculi (again in two variants: the classical LK and intuitionistic LJ). The second one was later called the sequent calculus or Gentzen’s calculus.
Introduction rules
&-I A B -> A & B
or-I A | A or B B | A or B ->-I A |- B | A -> B
not-I A |- False | not A
forAll-I
A(a) | forAll(x, A(x))
thereExists-I A(a) | thereExists(x, A(x))
Elimination rules &-E A & B | A A & B | B
or-E A or B A |- C B |- C | C
->-E A A -> B | B
not-E A not A | A not not A | A
forAll-E
forAll(x, A(x)) | A(a)
thereExists-E
thereExists(x, A(x)) A(a) |- B | B
There are some restrictions placed on the free object variable a (called the eigenvariable) in the case of introduction of forAll and elimination of thereExists(?). It must not occur in the formula forAll(x, A(x)) nor in any assumption formula upon which the formula depends, and it must not occur in the formula thereExists(x, A(x)) nor in B nor in any assumption formula upon which that formula depends, with the exception of the assumption formula A(a). To obtain NJ, we eliminate the rule not elimination i.e the rule ¬¬A -> A.
Gentzen wrote:
A closer investigation of the specific properties o the natural calculus finally led me to a very general theorem which will be referred to below as the Hauptsatz.
The Hauptzatz says that every purely logical proof can be reduced a definite, though not unique, normal form. Perhaps we may express the essential properties of such a normal proof by saying: it is not roundabout. No concepts enter into the proof other than those contained in its final result, and their use was therefore essential to the achievement of that result.
In order to formulate precisely the Hauptsatz and to prove it Gentzen had to introduce a logical calculus suitable to this purpose, since the calculi NK and NJ proved unsuitable. Therefore he introduced the calculi of sequents LK and LJ. The characteristic feature of this calculus is just the usage of sequents (Seuquenz). They may be seen as the most general form of a scheme of inference. A sequent is an expression of the form:
A_1, …, A_n => B_1, …, B_m
where A_1, …, A_n, B_1, …, B_m are formulas (the symbols => and , are auxiliary and not logical ones). The formulas A_1, …, A_n form the antecedent (Antezdens) and the formulas B_1, …, B_m the succedent (Sukzedens) of the sequent. Both expressions may be empty. The sequent A_1, …, A_n => B_1, …, B_m can be understood as: A_1 & … & A_n => B_1 or … or B_m
IF the antecedent is empty, the sequent reduces to the formula B_1 or … or B_m, if the succedent is empty, the sequent means the same as the formula not(A_1 & … & A_n) or (A_1 & … & A_n) -> false.
A derivation in the system LK or LJ consists of sequents arranged in a tree form such that it begins always from an initial sequent A => A, where A is any formula and in which sequents are transformed one into another according to the following rules which are of two types: structural and operational.
Structural rules:
thinning T => U | A, T => U T => U | T => U, A
contraction A, A, T => U | A, T => U T => U, A, A | T => U, A
interchange T, A, B, U => X | T, B, A, U => X T => U, A, B, X | T => U, B, A, X
cut T => U, A A, X => Y | T, X => U, Y
The operation rules are as follows:
&-IS T => U, A T => U, B | T => U, A&B
&-IA
A,T => U | A & B, T => U B,T => ? | A&B, T => ?
V-IA
A, T => U B, T => U | A or B, T => U
V-IS
T => U, A | T => U, A or B
T => U, B | T => U, A
not-IS A, T => U | T => U, notA
not-IA
T => U, A | not A, T => U
-> IS A, T => U, B | T => U, A -> B
-> - IA T => U, A B, X \> Y | A -> B, T, X => U, Y
forAll - IS T => U, A(a) | T => U, forAll(x)A(x)
thereExists - IA A(a), T => U | thereExists(x)A(x), T => U
forAll - IA A(a), T => U forAll(x, A(x)), T => U
thereExists - IS T => U, A(a) | T => U, thereExists(x, A(x))
There is a restriction on the eigenvariable a in the schemata false-IS and IA: it must not occur in the lower sequent of the inference figure.
The rules just described constitute the classical logistic calculus LK. To obtain the intuitionistic logical calculus LJ we add one restriction in the succedent of any sequent no more than one formula may occur.
Gentzen’s new approach to the predicate logic turned out to be equivalent to the axiomatic one - in the paper from 1935 Gentzen proved the equivalence of the calculis NJ, NK and LJ, LK with calculi modelled on the formalism of Hilbert, more exactly NJ and LJ are equivalent with the intuitionistic calculus and NK and LK with the classical one.
The calculi LK and +LJ have the important property mentioned already above under the name Hauptsats. Gentzen proved namely that the cut-rule can be eliminated from every purely logical proof. Consequently, we obtain the subformula property which says that in a cut-free proof all formulas occurring in the proof are compounded into the ‘endsequent’, i.e. the formula to be proved.
Those theorems have many interesting applications indicated already by Gentzen, who gave a consistency proof for classical and intuitionistic predicate logic, the solution of the decision problem for inutitionistic propositonal logic and a new proof of the nonderivability of the law of the excluded middle in intuitionistic logic. observe also that the formalism of LK and LJ enables u to characterize very simlpy classical and intuitionistic logics by restricting the number of ‘succedent formulas’ in intuitionistic sequents to a single formula.
For classical calculus LK, the Hauptsatz can be strengened to the sharpened Hauptsats (Gentzen called it verschärfter Hauptsatz; it is also known in English as the midsequent theorem, the normal form theorem, the strengthened Hauptsatz, and the extended Hauptsatz). It says that a proof in LK can be broken up into two parts: one patr belonging exclusively to propositional logic, and the other essentially consisting only of application instances of the rules of quantification. This version of the Hauptsatz enabled Gentzen to give a new proof of consistency of arithmetic without complete induction. This is a rather weak form of arithmetic, “of little practical significance” as Gentzen wrote in his 1935 paper. But the problem of consistency of arithmetic with the full induction is much more difficult. Gentzen solved it in two later papers from 1936 and 1938 using just the new formalisms introduced in the paper from 1935. His first consistency proof for elementary number theory was formulated in terms of the calculus NK. Gentzen proved the consistency of arithmetic using the transfinite induction up to the ordinal epsilon naught. The usage of the formalism of natural deduction NK caused the fact that the presentation was neither simple nor elegant. Hence in the later paper from 1938 he used the formalism NK in order to simplify the consistency proof (but this time he lost some of the naturalness in procedure). In a following paper from 1943 Gentzen showed that the transfinite induction up to epsilon naught is really necessary in his consistency proof - it cannot be replaced by the induction up to a small ordinal α < epsilon naught.
Those examples indicate already the distinguishing positive marks of the formalism introduced by Gentzen in comparison with the axiomatic approach. First of all they simulate the natural reasonings, moreover they are an interesting tool which enables us to obtain deep metamathematical results (let us mention here at least the consistency proofs). The formalisms of Gentzen proved to be very flexible - his method is applicable to many non-classical systems, e.g. to the minimal logic in Untersuchungen zum Prädikatenkalkül (1944) by Ketonen, to modal logics in A Theory of Formal Deducibility (1952) Curry or even to systems based on certain infinitistic rules of proof (cf. Beweistheoretische Erfassung der unendlichen Induktion in der Zahlentheorie (1951) by Schütte) where a Gentzen style formalization of an arithmetic based on the w-rule is given). Gentzen’s analysis of the predicate logic in terms of natural deduction influence also the development of semantic tableaux of Beth which are the method for the systematic investigation of the notion of “logical consequence” and the dialogical logic (cf. Logik und Agon (1960) by P. Lorenzen and Arithmetik und Logik als Spiele (1961) by K. Lorenz)
It is worth noting here some connection between the work of Herbrand and that of Gentzen. Gentzen claimed in his 1935 work that Herbrand fundamental theorem was a special case of his own vershärfter Hauptsatz because it applied only to formulas in prenex form. In fact, Herbrand’s theorem is more general that Gentzen’s and what more the study of Herbrand supplies more information on the midsequent than Gentzen’s sharpened Hauptsatz is able to provide. Gentzen’s Hauptsatz on the eliminability of the cut rule is the analogue of Herbrand’s result stating that modus ponens is eliminable in quantification theory. On the other hand, Gentzen’s Hauptsats (but not his sharpened Hauptsatz) can be extended to various non-classical logics (intuitionistic, modal) while there is no similar extension of Herbrand’s result.
Summing up the discussion of Gentzen’s work one must admit that Gentzen has in fact presented logic in a fashion more natural than that of Frege, Russell and Hilbert. The formalisms proposed by him have many important features which we tried to indicate above. Admittedly the number of rules in his systems is greater than the number of rules and axioms in, for example, Principia Mathematica but here each sign is introduced separately. The Hauptsatz shows an important property of Gentzen’s formalisms which has many interesting applications and which leads to many deep mathematical results.
The analysis of predicate calculus in terms of natural deduction due to Gentzen has had an influence on the development of logic in another direction. Evert W. Beth Semantic Entailment and Formal Derivability (1955), The Foundations of Mathematics (1959) and independently Jaakko Hintikka in Form and Content in Quantification Theory (1955) and Kurt Schütte in Ein System des verknüpfenden Schliessens (1956) devised a method dual to the method of Gentzen called today the tableaux method. As we have shown in the previous section natural deduction was essentially a systematic search for proofs in tree form. The tableaux method is a systematic search for refutations in upside-down tree form. It is based on the construction of a counterexample in cases in which a given formula is not a logical consequence of a given list of formulas. One the other hand it enables us to obtain a cut-free proof of a given true sequent by carrying out a thorough, systematic attempt to build a counterexample for it and finding the attempt blocked at some stage from being taken any further.
The semantic tableaux of Beth (1959) is based on the following intuition: We want to know if a given formula B is a logical consequence of formulas A_1, …, A_n. We test it by constructing a suitable counterexample which should show that it is not the case. If such a counterexample will be found, then we will have a negative answer to our question. And if it will turn out that no suitable counterexample can be found, then we will have an affirmative answer. A systematic method for constructing such counterexamples is provided by drawing up a semantic tableau.
The method of semantic tableaux turns out to be equivalent to the natural deduction. In fact, if a semantic tableau does close, i.e. if the construction of a counterexample fails, then one can rearrange it so as to obtain a straightforward derivation, and, conversely, every derivation in a suitable system of natural deduction provides us with a tableau showing that no suitable counterexample can be constructed. Beth proved that his system of tableaux is complete and that it satisfied Gentzen’s subformula principle. Consequently, as Beth in 1959 work writes, “such celebrate and profound results as the theorem of Löwenheim-Skolem-Gödel, the theorem of Herbrand, or Gentzen’s subformula theorem, are from our present standpoint within (relatively) easy reach”. And he adds that his approach “realizes to a considerable extend the ideal of a purely analytic method, which has played such an important role in philosophy”. The method of tableaux has also another philosophical, more exactly epistemological significance, namely it shows in some sense, simply the record of “an unsuccessful attempt to describe a counterexample” Hintikkia The Philosophy of Mathematics (1969). Observe that it cannot be estimated in advance how many steps in the construction of a counterexample by the method of tableaux will be needed, hence the system of the predicate logic is not decidable.
The method of semantic tableaux of Beth was developed by various authors. In particular Kleene in Mathematical Logic (1967) extended it to a Gentzen-type L-system and Kripke in A Completeness Theorem in Modal Logic (1959), The Problem of Entailment (1959), Semantic Analysis of Modal Logic I: Normal Modal Propositional Calculi (1963) use it in semantics for modal logics. it was also applied in the dialogue logic of Lorenzen (cf. Lorenzen 1960, Lorenz 1961). Smullyan in First Order Logic (1968) using the method of Beth and some ideas of Hintikka introduced the method of analytic tableaux. In some aspects it is similar to the method of semantic tableaux - both try to construct a counterexample. The main difference between them consists in the fact that rules of the analytic tableaux are only rule of elimination of logical constants and that we don’t have here two columns of formulas (valid, invalid) but only one in which formulas which in Beth’s method would be written in the right column, here stand with negation.
The construction of an analytic tableau can be characterized in the following way. We want to know if the formula B is a consequence of the formulas A_1, …, A_n. So write simply formulas A_1, …, A_n and the negation of B, i.e. ¬B. Then, applying certain rules, construct a tree which consists of subformulas of A_1, …, A_n, B. If every branch of this tree is closed, i.e. if it contains a pair of contradictory formulas, then we conclude that B is a consequence of A_1, …, A_n. Otherwise the answer is negative. In each step of the construction of the tree we use that rule which can be applied to the main functor of the formula. The rules are the following:
(¬¬) ¬¬A | A (&) A & B | A,B (¬&) ¬(A & B) | ¬A ¬B (or) A or B | A | B (¬or) ¬(A or B) | ¬A,¬B (->) A -> B | ¬A | B (¬->) ¬(A -> B) | A, ¬B (E) (Ex)A(x) | A(a) (¬E) ¬(Ex)A(x) | ¬A(a) (U) (x)A(x) | A(a) (¬U) ¬(x)A(x) | ¬A(a)
In the case of (E) and (¬U) we have the following restrictions: the parameter a must not occur earlier in formulas other than A.
The method of analytic tableaux, which is in a sense of a syntactic character, provides us with a sort of an algorithm - of course it is not an algorithm because the system is undecidable, but in practice it has some features of an algorithm. This method as well as the method of Beth, both based on the idea of decomposition of formulas into simpler components may be treated as realizations of Leibniz’s idea of calculus ratiocinator.
The beginnings of formalization and mechanization may be seen in the work of Giuseppe Peano who developed the idea of axiomatization of mathematics. The next step formed papers of Gottlob Frege, by whom we find the idea of formalization and in particular the first comprehensive system of logic in which derivations are carried out exclusively according to the form of the expressions. The projects and ideas of Peano and Frege found their fulfillment in the work of Bertrand Russell who realized the idea of formalizing mathematics in his monumental Principia Mathematica written together with A. N. Whitehead. This trend was further developed by David Hilbert and his school. They applied the idea of a formal system to the metamathematical studies of mathematical theories. in this way “the work of Leibniz and Frege has produced results of importance to the progress of mathematics”.
One should also mention in this context works of Polish logicians from the so called Lvov-Warsaw logical school, especially Jan Łukasiewicz, S. Leśniewski, A. Tarski, B,. Sobociński, M. Wajsberg, A. Lindenbaum, S. Jaśkowski and others. They developed first of all formal systems of the propositional calculus and their metatheory paying attention to such properties of systems as independence of axioms or their completeness. They reached really a great formal perfection and they were conscious of the role they were playing in the process of formalization and mechanization of reasonings.
Filozoficzna szkola Iwowsko-warszawska - Jan Wolenski (1985)
New direction in researches of formalization and mechanization of reasonings was suggested by Leopold Löwenheim and Thoralf Skolem who attempt to analyze quantified statements in terms of truth-functional logic. It was further developed by Jacques Herbrand. Another new approach was introduced by Gerhard Gentzen who broke away from the traditional formulations of predicate logic as they were developed by Frege, Russell and Hilbert and presented the systems of natural deduction which are closer to the real reasonings and which enable us to prove various interesting metamathematical results.
One should add to all that still one minor remark concerning the mechanization of the process of verification and if a given formula of the propositional calculus is a tautology or not. We can find already in Boole’s work the notion that a necessarily true proposition should reveal itself as such in the process of development. About the year 1920 it occurred to several logicians independently that when truth-function had been defined by means of truth tables a rule of thumb calculation would suffice to determine whether a complex proposition expressed by the use of truth-functional signs was necessarily true (i.e. a tautology), necessarily false (i.e. a contratautology), or contingent. The best known account of such a decision procedure is that given by Wittgenstein in Tractacus logico-Philosophicus (1922). A more straightforward discussion of the technique is in Post Introduction to a General Theory of Elementary Propositions (1921); note that the method was also known to Łukasiewicz at this time.
All those achievements made it possible to develop the mechanization of reasonings. The artificial formal languages and the idea of formalization afforded possibilities for representing appropriately thoughts and for grasping and expressing properly the fundamental relations in reasonings. The methods developed by Skolem, Herbrand, Gentzen and Beth provided procedures which enabled the simplification of reasonings and further their mechanizations, for a reasoning, is, after all a kind of computation. Those methods made it possible to construct concrete computer programs which could prove some theorems of, say, predicate calculus. For example, P. C. Gilmore using Beth’s semantic tableaux technique constructed the first working mechanized proof procedure for the predicate calculus and did prove some theorems of modest difficulty. Hao Wang developed a program which proved 220 theorems of Principia Mathematica (in 37 minutes) the program was organized around Gentzen-Herbrand methods. These were the beginnings of the study of the automated theorem proving which is developed nowadays with great intensity.
A Program for the Production of Proofs for Theorems Derivable within the First Order Predicate Calculus from Axioms (1959) - P. C. Gilmore
A Proof Method for Quantification Theory (1960) - P. C. Gilmore Toward Mechanical Mathematics - Hao Wang (1960) Proving Theorems by Pattern Recognition - Part I (1960), Part II (1961) - Hao Wang
In 1936 Alan Turing and Alonzo Church proved two theorems which seemed to have destroyed all hopes of establishing a method of mechanizing reasonings. Turing in 1936–37 reduced the decidability problem for theories to the halting problem for abstract machines modelling the computability processes (and named after him) and proved that the latter is undecidable. Church solving Hilbert’s original problem proved the undecidability of the full predicate logic and of various subclasses of it.
On the other hand results of Skolem and Herbrand showed that if a theorem is true, then this fact can be proved in a finite number of steps - but this is not the case if the theorem is not true (in this situation either one can prove in some cases the falsity of the given statement or the verification procedure does not halt). This semidecidability of the predicate logic was the source of hope and the basis of further searches for the mechanized deduction systems. Those studies were heavily stimulated by the appearance of computers in early fifties.
All those studies led to the idea of automated theorem proving by which one means the use of a computer to prove non-numerical result, i.e. determine their truth (validity). One can demand here either a simple statement “proved” (what is the case in decision procedures0 or human readable proofs. We can distinguish also two modes of operation: 1) Fully automated proof searches and 2) Man-machine interaction proof searches
Note that the studies of mechanization of reasonings and automated theorem proving were motivated by two different philosophies. The first one which we shall call the logic approach can be characterized “by the presence of a dominant logical system that is carefully delineated and essentially static over the development stage of the theorem proving system. Also, search control is clearly separable from the logic and can be regarded as sitting ‘over’ the logic. Control ‘heuristics’ exist but are syntax-directed primarily. The second philosophical viewpoint is called the human simulation approach. It is generally the antithesis of the first one. It can be characterized shortly by saying that the “the thrust is obviously simulation of human problem solving techniques”. Of course the logic and human simulation approaches are not always clearly delineated. Nevertheless this distinction will help us to order the results and to consider the influence of each of the approaches on various particular systems.
In 1954 Martin Davis wrote a program to prove theorems in Presburger arithmetic on the computer “Johniac”. The complexity of this decision procedure is very high and therefore the program proved only very simple facts (e.g. that the sum of two even numbers is also an even number; this was the first mathematical theorem in the history proved by a computer!).
TODO: Verify this claim, it feels like there might be other approaches before Davis’ work.
The second achievement in the field of automated theorem proving called the logic theorist should be included among examples of the human simulation approach. It was built by Allan Newell, John Shaw, and Herbert Simon and presented at the Dartmouth conference in 1956. This program could prove some theorems in the propositional calculus of Principia Mathematica of Whitehead and Russell. Its goal was to mechanically simulate he deduction processes of humans as they prove theorems of the sentential calculus. Two methods were used: 1) substitution into established formulas to directly obtain a desired result and, failing that, 2) to find a subproblem whose proof represents progress towards proving the goal problem. This program was able to prove 38 theorems of Principia.
The Geometry Theorem proving Machine of Gelernter and others from 1959 is also an example of the second approach. It applied the idea of Marvin Minsky that the diagram that traditionally accompanies plane geometry problems is a simple model for the theorem that could greatly prune the proof search. The program worked backwards, i.e. from the conclusion (goal) towards the premises creating new subgoals. The geometry model was used just to say which subgoals were true and enable to drop the false ones. It should be noticed that this program was able to prove most high school exam problems within its domain and the running time was often comparable to high school student time.
Simultaneously with the Geometry Theorem-proving Machine two new efforts in the logic framework occurred. We mean here works of Gilmore and Hao Wang. They used methods derived from classical logic proof procedures and in this way rejected opinions that logical methods cannot provide a useful basis for automated theorem proving. Such opinions were rather popular at that time. They were founded on the fact that logic oriented methods were inefficient and one the fact that the methods of Newell, Shaw, Simon and Gelernter proved to be successful. The method of P. C. Gilmore was based on Beth’s semantic tableau technique. It was probably the first working mechanized proof procedure for the predicate logic - it proved some theorems of modest difficulty.
Hao Wang developed the first logic oriented program of automated theorem proving at IBM in summer 1958 and continued work at Bell Labs in 1956 – 63. Three programs were developed: 1/ for propositional calculus 2/ for a decidable part of the predicate calculus 3/ for all of predicate calculus
Those programs were based on Gentzen-Herbrand methods, the last one proved about 350 theorems of Principia Mathematica (they were rather simple theorems of pure predicate calculus with identity).
During the Summer Institute for Symbolic Logic held at Cornell University, U.S.A, in 1954 Abraham Robinson put forward, in his short lecture, the idea of considering the additional points, lines and circles — which must be used in search for a solution of a geometrical problem — simply as elements of the so called Herbrand universe. This should enable us to abandon the geometrical constructs and to use directly Herbrand’s methods.
This idea turned out to be very influential and significant. One of the first programs that realized it was implemented in 1960 – 62 by Martin Davis and Hilary Putnam. By Herbrand’s theorem, the question of validity of a predicate calculus formula Z can be reduced to a series of validity questions about ever-expanding propositional formulas. More exactly one should consider so called Herbrand disjunctions A_1 V … A_n (which can be effectively obtained from Z). It holds that Z is valid if and only if there exists an n such that the disjunction A_i V … A_n is valid. The formulas A_i are essentially substitution instances over an expanded term alphabet of Z with quantifier removed. So one can test now A_i V … A_n for ever-increasing n for example by truth table and conclude that Z is valid if among formulas A_v … A_n a tautology was found. But truth tables happen to be quite inefficient. The procedure of Davis and Putnam tried to overcome this difficulty. IN fact they were considering unsatisfiability (instead of validity) of formulas and worked with conjunctive normal forms. Such a form is a conjunction of clauses, each clause being a disjunction of literals, i.e. atomic formulas (atoms) or their negations. The Davis-Putnam procedure can be described as follow: “[it] made optimal use of simplification by cancellation due to one-literal clauses or because some literals might not have their complement (the same atomic formula but only one with a negation sign) in the formula. A simplified formula was split into two formulas so further simplification could recur anew”.
The procedure of Davis and Putnam described in the last section had some defects. The main one was the enumeration substitutions - prior to this point substitutions were determined by some enumeration scheme that covered every possibility. Prawitz in An improved proof procedure (1960) realized that the only important substitutions create complementary literals. He found substitutions by deriving a set of identity conditions (equations) that will lead to contradictory propositional formula if the conditions are met. In this way one got a procedure of substituting Herbrand terms. It is called today unification.
Martin Davis developed right away the idea and combining it with the procedure of Davis-Putnam implemented it in a computer program based on a so called Linked-Conjunct method. See Davis Eliminating the Irrelevant from Mechanical Proofs (1963). This program used conjunctive normal forms of formulas and the unification algorithm developed by D. McIlroy in November 1962 at the Bell-Telephone Laboratories. It was the first program which overcame the weaknesses of Herbrand procedure and improved it just by using conjunctive normal form and the unification of algorithm.
Theorem Proving by Matching - T.J. Chinlund, Martin Davis, P. G. Hineman, D. Mcllroy (1964)
Simultaneously at Argonne National Lab near Chicago a group of scientists (G. Robinson, D. Carson, J. A. Robinson, L. Wos) was working on computer programs proving theorems. They used methods based on Herbrand theorem recognizing their inefficiency. Studying papers of Davis-Putnam and Prawitz they came tot he idea of trying to find a general machine-oriented logical principle which would unify their ideas in a single rule of inference. Such a rule was found in 1963–64 by John Alan Robinson and published in (1965). It is called the resolution principle and is today one of the most fundamental ideas in the field of automated theorem proving.
The resolution principle is applied to formulas in a special form called conjunctive normal form. Given a formula A of the language of predicate calculus we first transform it into prenex normal form i.e to the form ? where Q, (i = 1, …, n) are universal or existential quantifiers and B is a quantifier-free (B is called matrix). one can show that the prenex normal form of a formula A is logically equivalent to the formula A. As an example consider the following formula (stating that function f is continuous):
forAll(e {e > 0 → thereExists(d, (d > 0 and forAll(x, forAll(y(|x - y| < d → |f(x) - f(y)| < e}))
The prenex normal form is:
forAll(e, thereExists(d, forAll(x, forAll(y, e > 0 → d > 0 and (| x - y | < d → | f(x) - f(y) | < e))
Observe that prenex normal form of a formula is not uniquely determined but on the other hand all prenex normal forms of a give formula are logically equivalent.
The next step of the transformation of formulas we need is skolemization. Recall here only that it consists of dropping of all the quantifiers and of replacing every occurrence of each variable bound by an existential quantifier by a functional term containing the variables that in this formula are bound by universal quantifiers preceding the considered existential quantifier. A formula obtained in this way is said to be in a skolemized prenex normal form or in its functional form for satisfiability. The skolemized prenex normal form of the formula from our above example is the following:
e > 0 → g(e) > 0 and (| x - y | < g(e) → | f(x) - f(y) | < e
Note that the skolemized normal form of a formula is not equivalent to the given formula but is satisfiable (inconsistent) if and only if the given formula is satisfiable (inconsistent).
The next step of getting the conjunctive normal form consists of the elimination of connections ↔ and → and moving all negation signs to the atoms. We proceed according to the following rules:
A ↔ B is logically equivalent to (A → B) and (B → A)
A → B is logically equivalent to (¬A or B)
not(A or B) is logically equivalent to (not A and not B) not(A and B) is logically equivalent to (not A or not B)
not not A is logically equivalent to A
A formula obtained in such a way is said to be in the negation normal form. For example the negation normal form of the formula considered above is:
not e > 0 and (g(e) > 0 and (not(|x - y|) < g(e) or |f(x) - f(y)| < e
Note that atoms and negated atoms are usually called literals.
The last step of the considered transformation consists of the application of the following distributivity laws:
A or (B and C) ↔ (A or B) and (A or C) (A and B) or C ↔ (A or C) and (B or C)
In this way the obtained formula is of the form of conjunctions of disjunctions of literals. Such a form is called the conjunctive normal form and the disjunctions of literals are called classes. Clauses consisting of a single literal are called unit clauses. Clauses with only one positive literal are called Horn clauses. They correspond to formulas of the form A_1 and … A_n → B. To illustrate the last step note that the conjunctive normal form of our formula stating that a function f is continuous is the following:
(not e > 0) or (g(e) > 0 and not(|x - y|) < g(e)) or (g(e) > 0 and |f(x) - f(y)| < e)
Note that if A^1_1 or … or A^1_n1) and … and (A^1_l or … A^1_nl) is a conjunctive normal form of a formula A then we sometimes write it also as:
A^1_1 or … A^1_n1, …, A^l_1 or … A^l_nl
or as
((A^1_1, …, A^1_n1), …, (A^l_1, …, A^l_nl))
This form is called the clause form. In this way we have shown that for any formula A of the language of predicate calculus there exists a formula A’ in conjunctive normal form such that the formula A is satisfiable (inconsistent) if and only if the formula A’ is satisfiable (inconsistent).
Having described the needed form of formulas we can introduce now the resolution principle. First observe that a formula B is a logical consequence of formulas A_1, …, A_n if and only if the formul A_1 or … or A_n or not B is inconsistent, i.e. unsatisifable. Let u denote an emptly clause (i.e. a contradiction) and let formulas A_1, …, A_n not B be in conjunctive normal form. Hence to show that B follows logically from A_1, …, A_n it suffices to prove that ? is contained in the set S of all clauses constituting A_1, …, A_n, not B or that ? c;an be reduced from this set (the sense of the word ‘deduce’ will be explained below). This is the main idea of the method of resolution. Hence we can say that this method is a negative test calculus.
The resolution calculus introduced by J. A. Robinson in (1965) is a logical calculus in which one works only with formulas in clause form. It has no logical axioms and only one inference rule (the resolution rule).