Alasdair Urquhart
2008
50 pages
Achille C. Varzi, Massimo Warglien 2003 11 pages
Florian Cajori 1916 9 pages
TODO: Read the paper linked with this project Janet Heine Barnett Read 11 July 2020
Charles H. Seibert 2004 32 pages Read 11 July 2020
Philip E. B. Jourdain 1916 20 pages Read 12 July 2020
A good article briefing on the work of Leibniz. Need to trace the work of Jourdain further in logic. He seems to be a regular author for Quarterly Journal of Mathematics.
William Kneale, 1966 12 pages
- Parallels between the logical picture of Wittgenstein and Leibniz’s work is drawn.
- First order and second order natural signs are detailed.
- Poryphry’s exposition of Aristotle’s Categories and it finding a main audience in philosophy through the work of Boethius.
- Natural signs in the soul were called intentiones.
- Leibniz’ idea of constructing a scientific language that will form a thread of meditation (filum meditandi) is outlined.
- The idea that when a dyadical relation is introduced, the relationship modifying each of the two entities involved is detailed, that is the paternity of David to Solomon, grants Solomon the sonship of David.
William Kneale, 1948 27 pages
This is supposedly Kneale’s first work on the history of logic.
Read Part 1 out of 3. The rest two are expositions of his work, which I am deciding to read after perusing his work on logic. Part 1 was a good read that shows the historiographical works available on his life and his moral standings among other details on his life.
TODO: Read Part 2 and 3
Francine F. Abeles and Amirouche Moktefi Read 18 July 2020 22 pages
Describes the influence in Hugh MacColl’s thinking as he read and reviewed the work of Lewis Carroll. MacColl’s interest in logic was rekindled after 13 years when one of his friends sent him a copy of Symbolic Logic by Lewis Carroll. He described this in a letter to Bertrand Russell. In spite of some conflicting views, each modified their arguments to make them more clarified. Interesting read to know about how MacColl corresponded with Carroll by reviewing his books for The Atheneum publication.
Philip E. B. Jourdain 1911 3 pages
Read 18 July 2020
A quick read on what advances where made by Frege, Peano, and Russell. Parallel is drawn between Euclid’s axioms and how modern logic differs from it. Empirical accent of the modern logic is stressed.
Philipp E. B. Jourdain 1919 2 pages
Read 18 July 2020
Attention is drawn to the idea that making a parsimonious system of axioms following Okham’s dictum, is similar to having a least number of dependent variables in a linear system of equations as in the arithmetic.
P. E. B. Jourdain (1915) 6 pages Read 19 July 2020
Details about the work of Berkeley that criticizes Newton, Hegel, and Kant and draws parallels between how then modern day (20th century) mathematics has surpassed these criticisms.
P. E. B. Jourdain (1912) 9 pages Read 19 July 2020
A good read on the work of Russell and how he unified the work of Frege and Peano by using the logic of relations.
There are also interesting historical details and mathematical philosophical details that shine light on the evolution of formalism and work on Russell.
James van Evra 1983 18 pages Read 22 July 2020
Describes how Whately’s work was distinct from others of the period. Draws attention to the work of Aldrich’s work and it acted as the primary reference point for departure for Whately.
The social context is described in which there was a force against diminishing the value of scholastic logic was ongoing and Whately’s work as one which places logic on solid foundations by clearly forming a course of work attempting to delineate it’s subject of discourse. Author also describes how mischaracterization of logic’s value prior to Whately’s work was leading to it’s perception as having diminished value in education.
The idea here that logic was part of humanities at Oxford is a significant point. Against the criticism of Playfair, Copleston defended that logic was neither an art nor a way to gain knowledge, thus dissociating it from Llull’s tradition of Ars Magna and Epistemology. He contented that Playfair had objected to a a mistaken concept of logic.
Whately brought both algebra, and language closer to logic. He explicitly draws an analogy between the letters he employed for the moods of the syllogistic with that of ones used in algebra.
The nominalistic approach in the works of Hobbes is outlined as an earlier precursor to the nominalistic approach of Whately. In my research, I was able to trace this thread going through C.I. Lewis to influence Post to Rosenbloom to Chomsky.
According to Van Evra, the distinction between the substantive theory of reasoning and logic is that between a model and theory. Logic in Evra’s view to Whately was the formal theory of theory of reasoning.
Details are also drawn to the common origin of mistakenly treating both induction as a form of argument and syllogism as a kind of argument. Though I didn’t fully understand this subtlety.
The paper squarely locates Whately as the pioneering figure in influencing later developments in modern logic and wants to group him together with modern logic rather than among the scholastics which is what modern histories of logic tend to group him under.
Raymie E. McKerrow 1987 24 pages Read 22 July 2020
Details about the historical context in which Richard Whately’s book emerged. Precedents to the nominalist take in Whately’s work is linked to John Gillies translation of Aristotle and Richard Kirwan’s Logick.
Towards the end of the paper McKerrow also, draws attention to the idea that the two books of Whately on rhetoric and logic acts as two sides of a coin.
A good description of how Whately proscribed the limits of logic in his nominalist interpretation is given.
McKerrow also compares the innovation of Whately to that of Stephen Toulmin’s Uses of Argument (1958) and The New Rhetoric of Chaïm Perelman and Lucie Olbrechts-Tyteca (1969)
Richard Zach (2006) 9 pages Read 13 January 2021
Short read on the links between ideas of Gödel and Computability and Complexity Theory
Warren McCulloch 1960 13 pages Read 5 February 2021
A nice read on the life and work of McCulloch. Assumes a good knowledge of the history of logic and the role played by the recent innovations since Charles Peirce. There are some parts about probabilistic logic that I couldn’t quite follow. Would need immersal in the work of McCulloch to learn to work with it.
Volker Peckhaus 2004 15 pages Read 7 February 2021
A really good paper that outlines how the two themes in the work of Leibniz: Calculus ratiocinator and Characteristica Universalis went on to influence later developments in the 19th and 20th century.
Author goes on to differentiate between two schools of logic: the algebraic school and the mathematical logic school. The question involves the usefulness of algebra in the actual shape of logic. People like Arthur Prior, Michael Dummett, and W. V. O. Quine are evidenced as people who challenged the primacy of algebraic school of logic.
Quine locates the idea of quantification theory as the emergence of logic as a substantial branch of mathematics.
Works of Jean van Heijenoort (1976b) of dividing “logic as calculus” and “logic as language” is cited. This is said to be developed by the work of Jaakko Hintikka to “languages as calculus” and “language as a universal medium”.
The two ideas are not disjunctive but rather have overlaps in that Frege himself notes that the inferring calculations as a necessary component of a concept script. The concept script as per Peckhaus was meant to emphasize the lingua characterica aspect of logic.
With quantification theory acting as the central powerhorse, lingua characterica is considered by Heijenoort to constitute a language powerful enough perhaps to represent all of scientific knowledge.
Algebraic calculus uses model-theoretic approach where interpretations of operations and categories (classes of concepts) are needed. They can be divided into a structural/syntactic and a semantic side. The latter providing interpretation of the figures used.
The main features of Fregean system is identified as: quantification, universality, internal semantics, a closed/fixed universe of discourse.
Leibniz envisioned an ars characteristica which will represent letters according to the models of mathematics and the notation allows for calculating with concepts according to a set of rules. It allows for mechanically deducing all possible truths from the list of simple thoughts. Characteristic is responsible for the semantic part and calculus ratiocinator forms the syntactic part of the lingua rationalis.
In the initial period of partial realizations of this program, the systems of characters allow various interpretations. In the final (utopian) stage after having reached at the complete designation of all possible simple thoughts, the system would be categorical in nature.
Peckhaus locates the idea of Schröder with an external semantics to be more close to the Leibnizian idea of lingua rationalis.
The article comes to a close by showing how Schröder was influenced by the work of Charles Peirce and his student Oscar Howard Mitchell in creating his own style of quantification in the algebraic school which is close to infinitary logic. Peckhaus uses this idea to underline that quantification theory cannot be taken to be the distinguishing factor for the two traditions in the history of logic
Rolf George and James Vans Evra 2006 14 pages
Read 17 February 2021
A tapestry of logical systems as having dominated before the first half of 20th century.
The book starts with the work of Peter Ramus which identified Dialectic with Logic and which lead to logic to be understood as art of rhetoric and disputation. This therefore, lead to the works in philosophy and literature not advancing or concerning themselves with the subject much.
Francis Bacon, Descartes, and John Locke is said to have hold the opinion that scholastic logic as holding us back from the inquiry into truth. Hume continued Locke’s attack and (one of ?) the most widely read work of that period article in Encyclopédie by Denis Diderot also bashed logic.
Gottfried Wilhelm Leibniz was the great exception to this. In his correspondence with Locke, latter’s representative Philateles eventually admits as being able to perceive logic as universal mathematics.
Theory of terms or concepts, their combination into judgments, and the composition of syllogisms from judgments. (Roughly: Primitives -> Interpretive statements -> Structures).
The elucidation of the structure of logic was prefaced by a discussion of some epistemological preliminaries: the origin of concepts as inherent in the mind or deriving from sensation and perception. The authors claim that in order for logic to take the shape of modern logical theory.
Kant and Whately are said to be the prime movers who played a role in eliminating some material and reorienting logic towards its modern conception.
Kant changed his mind from Locke’s book de intellectu is the ground of all true logica to Locke “speaks of the origin of concepts, but this really does not belong to logic”. While claiming earlier that the logician must know the human soul and cannot proceed without psychology, he now held that “pure logic derives nothing from psychology”.
Organon: Attempts to codify methods of discovery. Canon: A method of evaluation of the discoveries
He held that there is no universal method of discovery and logic to be catering only to form and not to content, and that it can only be a canon (diiudicatio).
He divide logic into theory and practice. This practice was associated with the skill of reasoning and disputation while logic proper as a theoretical inquiry.
Richard Whately posited that the ground for discourse of logic is like objective sciences Chemistry or Mathematics in that its point is the enunciation of principle apart from application.
For Richard Whately logic was not an engine of discover or “an art of rightly employing rational faculties” but was an inquiry into the formal structures. He considered logic to be about language rather than vaguely considered “thought”.
Whately is said to have given logic the characteristic form. He eliminated some associations and gave it a precise definition making it closer to how grammar is to language.
Syllogisms : Articulated Argument :: Grammar : Language
Bernard Bolzano wrote Theory of Science (Wissenschaftslehre) in 1837.
Introduced the idea of the content which is asserted or denied by a proposition is a ‘proposition in itself’.
Propositions are introduced first and any component of a proposition that is not a proposition itself is a Vorstellung (idea or representation ; sounds like an atomic component / primitive in modern parlance).
Bolzano noted that no one had successfully defined the type of combination of terms that generates a proposition. Several of the attempts he examined did not distinguish propositions from complex terms and others defined it in terms of “acts of the mind”, “contaminating” logic with psychology.
Hobbes and Condillac identified propositions with equations. They further maintained that the principle on which all syllogisms rest is that two things equal to a third are equal to each other.
But Bolzano notes that while all equations are propositions, not all propositions are equations and paid no further attention to this doctrine.
Identifying propositions with equations demanded adjustments like the quantification of the predicate. Ploucquet thought that in an affirmative proposition the predicate cannot be different from the subjects: All lions are animals as All lions are some animals. All X are Y as All of X = Part of Y (George Bentham on a commentary to Whately’s book) This doctrine is usually associated with the name of William Hamilton who gave it wider currency.
Bolzano contributed the idea of logical consequence using the mathematical technique of substitution on variables.
The unusual triadic construction of consequence also allows for enthymemes or partly ‘material’ consequences, where only a subset of extralogical terms is varied.
Laws of thought: Identity, Contradiction, and Excluded Middle
Bolzano agreed that these principles are true. Logic he maintained, obeys these laws, but they are not its first principles (or axioms in modern parlance).
Bolzano took mathematics to be a purely conceptual science and disagreed with Kant’s view that it was founded on intuition.
John Stuart Mill attacked logic claiming that formal principles, especially the syllogism, are a petitio principii since they can generate no new knowledge.
Mill claimed that the truths of geometry and arithmetic are empirically discovered by the simplest inductive method, that is enumeration.
Mill took the empiricism and psychological approach to logic, whose “theoretic grounds are wholly borrowed from psychology, and included as much of that science as is required to justify the rules of the logical art”. This holds in particular for the “laws of thought”, which are grounded either in our psychological constitution, or in universal experience.
System of Logic by Mill is best known for formulating rules for the discovery of the causes, his famous ‘canon’: the methods of agreement, difference, residues, and concomitant variation. Popularity of this text in England lend support to the view that logic is methodology and the art of discovery.
Logic was turned into a strong branch of mathematics under the expertise of George Boole, not of philosophy. This would excise methodology, rhetoric, and epistemology. Logic was cast in a symbolic language.
Syllogisms can now be calculated by using arithmetic, specifically by maneuvering the middle term into a position where it can be eliminated. Syllogistics becomes part of the algebra of classes and thus an area of mathematics. If every argument can be formulated as a syllogism, then all of logic is a part of algebra.
Short comings of Boole’s rendition:
Existential propositions were represented as v = xy where v stands for a non-empty class. But how can one define such a class?
His logic was a logic of terms
Recognition of negation came only later in the century
Changing the status of standard copular — is — Augustus De Morgan showed how the bounds of categorical statements could be widened into the realm of relational statements.
“Every man is an animal. Therefore the head of a man is the head of an animal” cannot be accommodated in traditional syllogistic logic.
De Morgan introduced the concept of “universe of discourse”, which targeted statements to a class of objects under discussion rather than the entire universe.
Charles Sanders Peirce first thought logic to be part of semiotics, but then took it to be that theory, and while talking logic to be descriptive first, he later thought it to address cognitive norms.
Gottlob Frege attempted to derive arithmetic from logical concepts.
In his work, a function symbol refers to / denotes a concept, the name/argument an object. Concepts and objects belong to distinct ontological categories. When a concept term is an argument in a sentence, the sentence is said to be on a higher level than those whose arguments refer to objects.
Conceptual structures are used to determine if certain configurations “fall under” them. For a concept: () is a planet, the object Mercury, when substituted in the structure gives Mercury is a planet which is said to map to true and hence to fall under the structure while Sirius is a planet fails to and doesn’t fall under it.
Another profound innovation of Frege was the quantifier. In mathematics, quantification is usually tacit: x + 0 = x, means that for all x, it is a true identity. Whereas to denote the opposite of it, one can say x + 0 != x, but for cases where “Not everything is F” cannot be done so and for that a special sign, a quantifier with a scope is needed. This allows to distinguish between:
not(ForAll(x, F(x))) : Not everything is F(x) ForAll(x, not(F(x))) : Everything is not(F(x))
Frege took quantifiers to be higher level functions. There is a planet was translated as There is at least one thing such that [() is a planet]. The quantifier here is constructed as a function that has another function as its argument.
Frege emphasized the importance of the deductive method. Claims in a deductive science must be justified by a proof which is a sequence of propositions, each of which is either an assumption, or follows from previous members of the sequence by clearly articulated steps of deduction.
With this understanding of the structure of propositions, of quantification, and of the nature of a proof. Begriffsschrift develops an axiomatic system of sentential logic, based on two sets of axioms: one on conditionals and the other on negation.
The rule of modus ponens is employed to generate the first consistent and complete system (proved later) system of sentential logic.
A third principle, substitutivity, is introduced: if a = b, then F(a) is equivalent (as we now say) to F(b). With the introduction of a fourth principle, now ‘universal instantiation’ or ForAll-elimination, a system of second order predicate logic is developed.
Substitutivity fails in so-called oblique/opaque contexts. According to Frege, they are dependent clauses introduced by words as ‘to say’, ‘to hear’, ‘to believe’, ‘to be convinced’, ‘to conclude’ and the like.
‘N believes that the morning star is a planet’ may be true while ‘N believes that the evening star is a planet’ false even though the two heavenly bodies are identical violating the principle of substitutivity.
To save this principle, Frege introduced sense (sinn) and reference (Bedeutung).
Morning star and evening star may refer to the same object, but they have a different sense.
In opaque contexts such expressions do not name an object, but their own sense, allowing substitution with any name of identical sense.
Sentences in oblique contexts have as their reference not their truth value, but the thought or sense they express. In this way, substitutivity, for Frege an incontrovertible principle of logic, can be made to work in opaque contexts.
In Foundations of Arithmetic, Frege attempted to define the sense of a sentence in which a number word occurs. This is associated with the ‘linguistic turn’ foreshadowing and inspiring 20th century analytic philosophy: the question how we come to know numbers is transformed into one about the meaning of sentences in which number words occur.
Context principle: Only in the context of a sentence does a word have meaning.
Hume’s Principle: “When two numbers are so combined as that the one has always a unit answering to every unit of the other, we pronounce them equal”
Fifth principle: Unrestricted comprehension (or abstraction) axiom.
Bertrand Russell’s discovery showed that the axioms of arithmetic (now commonly stated in the form Giuseppe Peano gave them) cannot be formally and consistently derived from Frege’s principles. Only in recent years has it been shown that these axioms follow from the principles of logic (minus the ill-fated Fifth) together with Hume’s Principle. This is now called ‘Frege’s Theorem’.
Franz Brentano observed that all ‘psychological phenomena’ are targeted on some object: when we think, we think of something. These are intentional objects whose existence or nonexistence need not be an issue.
Brentano shied away from allowing the contents of mental acts to have a form of being as this is to be an unseemly Platonism.
His students Kasimir Twardowksi and Edmund Husserl distinguished content from object with the object determined by the content. This is analogues to sense and reference.
Students of Twardowski formed the school of Polish logicians. Lesniewsky was one of them who explored mereology.
Mereology is different from set theor in that an element of a class is not a part of it, though a subset is. Importantly, membership is not transitive: if elementOf(s, t) and elementOf(t, u), then s is not an element of u whereas a part of a part is a part of the whole.
Alexius Meinong, another of Brentano’s students inquired into the nature of intentional acts that lack existing objects and are ‘beyond being and non-being.’
He is credited with inspiring free logic.
Bertrand Russel gave a distinction between proper names and expressions which he titled definite descriptions.
The present king of France is bald was analyzed into:
- location(atLeast(King, 1), France)
- location(atMost(King, 1), France)
- isBald(King, True)
Now each of these condition can be violated giving no king, more than one king and non-bald king.
This logical phrasing style is evidenced to convey the idea that there’s misleading ‘surface structure’ of the sentence which disguises the logical structure.
I feel the idea of ‘present king’ in the temporal aspect is elevated to an eternal status here.
Russell concludes that definite descriptions are not names, as Frege had thought. If so, then they would lead to ontological “excesses” as posited by Meinong.
Natural language structure and grammar are misleading and must be distinguished from the deeper logical structure. This is said to have lead philosophers to argue that metaphysical and political convictions often gain their plausibility from deceptive natural language expressions.
Expressions like definite description, but not only they, can be defined only in their contexts, by definitions in use.
Russell held that logicism could be made to work if the comprehension axiom were restricted. He proposed several solution,s eventually the theory of types, through which Frege’s contributions entered the mainstream of logic.
The theory of types stratifies expressions in a hierarchical order so that elements of a set are on a lower level than the set, making it impossible for a set to be a member of itself. A ‘ramified’ theory of types is introduced to solve as well the so-called semantic paradoxes like the liar paradox.
Type theory is said to have the burden of having to recognize a separate definition for truth at each type level and the inability to define a number as the set of all similar (2 membered, 3 membered etc.) sets. They resolve this by using symbols that are ‘systematically ambiguous’ between types.
Russell and Whitehead did succeed in deriving a significant portion of mathematics from their principles: a comprehensive theory of relations and order, Cantor’s set theory, and a large portion of (finite and transfinite) arithmetic.
Principia was meant to be a kind of Lingua Universalis, a canonical language pure enough to permit construction of disciplined discourse on the skeleton it provided.
In summary, several distinct areas of study were advanced under the name of logic:
- As an investigation on cognitive performance/scientific methodology
- Strategy of discovery
- Branch of rhetoric
Including these, there were two distinct types of theory: syntactical / proof theory and semantic definition of logical consequence, which does not dwell on the process of derivation.
The most important development of logic after Principia was to bring these two strands together. In propositional logic, for instance, truth tables (introduced by Wittgenstein in 1922) allow a semantic test for the validity of formulas and proofs, a continuation of Bolzano’s project. It was then proved that the Principia version of propositional logic is complete, that is to say that every semantically valid formula can be derived in it and that it is consistent, that is only such formulas (and hence no contradiction) can be derived. Kurt Gödel later proved that first order predicate logic is complete as well, but that higher order logic is not. Since the latter is needed to define arithmetic concepts, it is said that this spelled the end of the logicist project.
E.P. Bos and B. G. Sundholm 2006 11 pages Read 19 February 2021
Seven liberal arts were the curriculum at a medieval arts faculty.
Three trivial arts (Trivium): Grammar, Logic (Dialectica), and Rhetoric Four Mathematical Arts (Quadrivium): Geometry, Arithmetic, Astronomy, and Harmony
Aristotle did not use the Greek logikè for the logical art but preferred ta analytic (from the verb analuo: to resolve (into premises or principles))
The Greek logos stands for the smallest meaningful parts of speech.
Greek logical terminology was latinized by Cicero and Boethius.
Cicero is credited with the honor of having named the subject Logica.
Dialectica the alternative Platonic and Stoic name for logic as part of the trivium derives from Greek for conversation as thinking was seen as the soul’s conversation with itself.
The dialectician investigates relations between external ideas which have to be respected if the thinking were to be proper.
Aristotle’s works Categories On Interpretation The Two Analytics The Topics On Fallacies
came to be seen as an Organon. These were seen as instruments for reasoning.
Logic was seen as the study of / use of words for making reasoned claims
Analytics resolves reasoning into simpler parts in order to provide grounds.
Dialectics grounds reasoning in (eternal) relations between logical entities whereas logic is thought of as an organon, it serves as the tool for multiplying knowledge through the use of reasoning.
Today, formal logic is confined to theory of (logical) consequence between well-formed formulas. An analogous position within medieval logic would cover only the topics dealt with in the Prior Analytics.
Topics addressed in medieval logic: Philosophy of language Eg: theories of signification and supposition (reference) Epistemology Theory of demonstration Philosophy of science / methodology Method of analysis and synthesis
Formal logic vs. Material logic Theory of consequence vs Theory of demonstrations (proofs)
Today’s logician is primarily a “dialectician” who studies relations among logical entities, be they meaningful sentences, (abstract) propositions, or the well-formed formulae of a formal language.
The medieval logician, on the other hand, was primarily concerned with the exercise of the faculties of the intellect. The use of reasoning as part of the human act of demonstration was his main concern.
Posterior Analytics was primary over Prior Analytics.
The medieval logician does not primarily study consequence-relations between logical entities; his concern is the act of knowledge that is directed towards real things.
As reasoning proceeds from judgments that are built from terms which are first apprehended as products of mental acts.
I. Apprehension, Grasping -> Concept / Idea / Notion (Cognition) -> Term (Written) II. Judgement - Mental Proposition: S is P (Cognition) -> Assertion / Proposition (Written) III. Reasoning - Mental Inference (Cognition) -> Inference, Reasoning (Written)
After Port Royal Logic (1662), there seems to be a fourth category on Of Method.
Propositions are traditional subject/copula/predicate
But modern propositions come from Bertrand Russell’s translation of Frege’s Gedanke (Thought).
Thus modern propositions are not but contents of judgments.
In modern interpretation of proposition, one can write: that snow is white while for medieval propositions they are a combination of S and P.
Such as: Snow is White Sortes is a Man
14th century complex significabile though plays a role analogous to modern notions of proposition (content).
In medieval logic there’s parallelism between thought and reality, between mind and world.
The important idea of carrying out purely mechanical, formal proofs, irrespective of content emerges only with Leibniz.
The medieval theories as to the truth of propositional combinations of terms - categorical predications - vary.
According to identity theory, both terms are same when they stand for the same entity.
The main rival of the identity theory of truth is the (intensional) inherence theory. Sortes is a man is true when humanity, the property of being a man ‘inheres’ in (is contained in) the nature of what Sortes stands for, namely, Socrates.
Sometimes, both of the theories were used by philosophers.
Substantival predication: Man is an animal, is held to be true because man and animal stand for the same entity, whereas the denominative predication: A Man is white is deemed true because whiteness inheres in what man stands for.
Categorical form: S is P Hypothetical Form: If J then K Disjunctive Judgments: J or K where J, K are judgments
Poryphrian Tree
Predication is transitive when climbing in a Poryphrian tree
What is predicated of a predicate of a subject can also be predicated of the original subject.
Sortes is a man and Man is a category does not give Sortes is a category
In order to account for the failure of transitivity in the case of iterated predication, contemporary logical semantics relies on a reference relation, both relate of which: the expression and its reference are construed as things.
Medieval logic draws upon the two notions of references: signification and supposition.
Stanislaw Lesniewski’s logic was closer to the medieval perspective with its S is P form rather than P(a) form of Fregean function/argument form.
Formal languages were seen as signs where a sign signifies by making manifest its signification to mind. This is close to the notion of reference.
Signification is context independent, and the context dependent variant is supposition.
Supposition of a term is what it stands for in the context in question.
In Man is a word, it has material supposition because it stands for the word and not a person as in Socrates is a man.
Under the influence of Aristotle’s theory of hylomorphism, the subject S is seen as the content/matter of the categorical S is P proposition and the predicate is its form.
Simple supposition is when the word stands for a species or a general category.
Man is a category here stands for the species of man rather than an individual man.
When there’s such supposition changes, there won’t be transitivity in the predicate and hence inferences cannot be drawn.
Aristotle in Prior Analytics organized the syllogisms according to three figures and tried to reduce the valid modes in the later figures to the ‘perfect’ syllogisms in the first mode.
Aristotelian terms were reached by epagogé (Aristotelian induction).
Universal categorical judgments carry ‘existential import’
ForAll(x, Swan(x) => White(x)). Therefore, ThereExists(x, Swan(x) and White(x)) which is not valid in modern logic.
Valid inference here is ForAll(x, Swan(x) => White(x)) => ThereExists(x, Swan(x) => White(x))
The inference from an affirmative universal proposition to an affirmative particular one is an example of ‘alternation’.
The medievals liberated themselves from term-logical straitjacket of the Aristotelian syllogistics by considering singular judgments.
The so called expository syllogism.
Mixed Hypothetical Syllogisms: If P then Q, and if Q, then R. Therefore, If P, then R.
Here the connections are not between terms but between propositions. This shift in perspective led to the appearance of a new logical genre by about 1300.
Implication, consequence, inference, and causal grounding.
Implication: Propositional connection between propositional contents Follows from, is a consequence of Thus, therefore, indicates inference. From premise judgments / assertions to conclusion judgement (assertion). Because, is a causal ground / reason for are indicator words for causal grounding, which is a relation between events or state of affairs.
In medieval logic, if (si), therefore(igitur), sequitur (follows), and quia (because) are all indicator-words for one and the same notion of a consequentia.
This survives in modern logic under two guises, as the notion of logical consequence between WFFS, that derive from Bolzano’s Albeitbarkeit which was made famous by Tarski and one the other hand, as the sequence (Sequenzen) that was used by Gentzen.
The medieval theory of consequences can be seen as a partial anticipation of contemporary sequent-calculus renderings of logical systems.
Formal consequence in medieval theory has something that holds in all terms:
All men are mortal. Sortes is a man. Therefore: Sortes is a mortal.
This consequence remains valid under all (uniform) substitutions (salva congruitate) of other terms put in the place of Sortes, mortal, and man.
Formal consequence is opposed to material consequence which in contemporary notion can be compared to Carnap’s meaning postulates.
A late addition to medieval logic is the theory of obligations, which is concerned with the proper rules for disputation and questioning.
This is said to be closer to the current dialogicial approach to logic and semantics as designed by Lorenzen and Lorenz, or the game-theoretical semantics that is owed to Hintikka.
In medieval period, philosophy served as ancilla theologicae (‘a servant of theology’).
Commentaries on Peter Lombard’s Sentences often contain material that is highly illuminating from a logical point of view.
Robin Smith 2006 13 pages Read 22 February 2021
Ancient Greek logic was inseparable from ancient Greek philosophy. Greek philosophical logic is said to originate with Parmenides. His views set the agenda out of which meany things in Greek philosophy including logic later arose.
Change as the coming to be of what is not and the not being of what is. Multiplicity: Saying that there are two things is to say that something is not something else. The conclusion is that what is, is one: unchanging, uniform, without distinctions.
Greek philosophy is an effort to avoid these consequences and defend the coherence of talk of motion and multiplicity.
Zeno as the originator of the dialectic.
It has three features:
- Directed at someone else
- Takes its start from the premises accepted by the other party
- its goal is the refutation of a view of that other party
Sophists participated in oratory teaching. Their teaching along with lessons on style and diction also includes training in argumentation. It ranged from teaching set pieces of argument useful for specific contexts, all the way upto devising arguments according to principles.
One them that emerges in several sophistic thinkers is a kind of relativism about truth.
This is put forward by Protagoras who says: “Man is the measure of all things; of things that are, that they are, and of things that are not, that they are not.”
Plato interprets this in Theaetetus to mean that whatever seems to be true to anyone is try to that person: that he denied that there is any truth apart from the opinions of individuals.
In Protagoras’ world, persuasive speech creates not merely belief but also truth.
Herodotus’ history of the Persian Wars present a picture of opinions about right and wrong as merely matters of custom by displaying the variability in customs from one people to another.
Dissoi Logoi (Twofold Arguments) gives a series of arguments for and against each of a group of propositions; the implication is that argument can equally well support any view and its contradictory.
Plato in Theaetetus argues that Protagoras’ relativistic concept of truth is self-refuting in that if applied to itself, it becomes meaningless and moreover it implies that the same opinions are both true and false simultaneously.
Plato partially rejects Parmenides’ thesis that only what is can be thought by distinguishing a realm of “becoming” that is not non-being but but cannot also said to be without qualification.
Plato’s theory of Forms/Ideas: Theory of predication — tells what it is for a thing to have a property or attribute.
For an x to be F, say Socrates to be Tall, is for x to stand in a participatory relation to an entity: ‘the tall itself’ (Tallness?)
In Sophist, Plato begins to develop a semantic theory for predications. He observes that truth and falsehood are not properties of names standing alone, but of sentences produced by combining words.
“Theaetetus” and ”is sitting” in isolation indicate ideas, but their combination becomes a proposition which can be judged. This I think is the beginning of apprehension/proposition/judgement triad.
This is said to provide a ground for understanding falsehoods as meaningful.
Aristotle follows Plato’s line of development and analyses simple sentences into noun and verb or subject and predicate.
He develops it in greater detail and extends it to sentences which have general or universal subjects and predicates (katholou: ‘of a whole’).
Aristotle in Metaphysics argues that there is a proposition which is in a way prior to every other truth: “it is impossible for the same thing to be both affirmed and denied of the same thing at the same time and in the same way”.
When Aristotle presupposes principle of non-contradiction, he appeals to a more general thesis concerning demonstration of proof: no system of demonstrations can prove its own first principles.
Posterior Analytics is considered as the oldest extant treatise on the nature of mathematical proof.
Subject of Posterior Analytics is demonstrative sciences: a demonstrative science is a body of knowledge organized into demonstrations (proofs) which in turn are deductive arguments from premises already established.
Proofs are neither a means of finding out new truths nor an expository or pedagogical device for presenting results, but rather are constitutive of knowledge: if a truth is demonstrable, then it is to posses its demonstration.
This means that nothing can be demonstrated except what is necessary and that has a cause/explanation.
Syllogism: an argument in which some things being supposed, something else follows of necessity because of the things supposed. Thus syllogisms captures the idea of a valid argument.
Aristotle thought that all valid arguments could be ‘reduced’ to a relatively limited set of valid forms which he usually refers to as ‘arguments in the figures’ which modern terminology refers to as ‘syllogisms’.
Aristotle maintained that a single proposition was always either the affirmation or the denial of a single predicate of a single subject.
‘Socrates is bathing’ affirms ‘bathing’ of Socrates.
‘Plato is not wrestling’ denies ‘wrestling’ of Plato
He also regarded sentences with general subjects as predications. This is at odds with Frege’s idea of modern logic where they have a radically different structure from predications.
General predications are divided according as the predicate is affirmed or denied of all (universal) or some (particular) of its subject.
Affirmed, Universal: All cars have wheels Affirmed, Particular: Some cars have wheels Denied, Universal: No cars have wheels Denied, Particular: Not every car has wheels
Aristotle then explores combination of two premises that share a term will imply a third sentences having the two non-shared terms as its subject and predicate.
He distinguishes three possibilities based on the role of the shared term (the ‘middle’ in his terminology) in the premises: it can be predicated of one and subject of the other (the first figure), predicate of both (second figure), or subject of both (third figure).
Aristotle then uses these structure to show that from any valid form of argument can be extracted a figured argument.
The author uses the preceding ideas to evidence that Aristotle’s theory developed in Prior Analytics was developed largely to serve the needs of Aristotle’s theory of demonstration. Especially that the logical theory arose to meet the needs of the philosophy of mathematics.
The Regress argument of Posterior Analytics is shown as one of the central concerns of Aristotle in identifying the first causes.
Euclid’s Elements comes a century after Aristotle. We do not know of its contents, Hippocrates of Chios composed an elements in the late fifth or early forth century BCE, and Theudius of Magnesia put together a treatise during Aristotle’s lifetime that incorporated work by a number of other prominent mathematicians including Archytas, Eudoxus, Leodamas, Theaetetus, and Menaechmus.
Common conceptions: Koinai ennoiai And some things asked for: aitemata (customary translation is ‘postulates’).
Further propositions are added to the system by logical deduction from these first propositions and any others already proved; these are called theorems.
This kind of logical structure assumes first propositions which are not demonstrated, or even demonstrable, in that system. Aristotle argues that for such structures.
Aristotle’s response to the regress argument appears at first to be a mere assertion: that there are first principles that can be known without being demonstrated.
Aristotle uses a great deal of argument trying to prove that the regress of premises always ‘comes to a stop’. It is in this argument that he needs the results established in the Prior Analytics.
In Aristotle’s logic it is possible for there to be true propositions which cannot be deduced from any other set of true propositions whatsoever that does not already contain them.
Aristotle calls true but uneducable sentence ‘unmiddled’ (amesos: standard translation immediate, though etymologically correct, is highly misleading).
Since an unriddled proposition cannot be deduced from anything, it obviously cannot be the object of a demonstration. Moreover, any premise regress that encounters such a proposition will come to a stop at that point. If every premise regress comes to a stop in unriddled premises, then it might seem that we have a serious problem for the notion of demonstration, just as the anti-demonstrators of Aristotle’s regress argument claimed.
Given the sum total of all the true propositions, we can apply a set of mechanical procedures to find out which ones are unmiddled. Aristotle in effect gives us such a set of procedures in Prior Analytics I.27. If we did have knowledge of just exactly the unmiddled propositions, then since they are the propositions in which every regress comes to a stop, and since a regress can be reversed to become a deduction, we would have knowledge of premises from which every other proposition could be deduced. Since unmiddled propositions cannot be known except by non-demonstrative means, it follows that the possibility of non-demonstrative knowledge of the unmiddled propositions is both a necessary and a sufficient condition for the possibility of demonstrations.
Since there is no middle term explaining why an unmiddled proposition is true, there is no explanation of its truth: it is, in effect, uncaused and unexplained.
Aristotle’s view is precisely this: demonstrations, which give the causes why their conclusions must be true, ultimately rest on first premises for the truth for which there is no further explanation or cause.
Author remarks that in Parmenides view possibility and necessity collapse into one another. It is said to appear to lead to a universal determinism or fatalism.
Aristotle ascribes the view that the modalities all collapse into one another to ”the Megarians”.
Kleinomachus of Thurri is said to have been the first to write on ‘predications and propositions’. Eubulides is credited with the discovery of a number of paradoxes including the Liar’s paradox and the Sorites.
Aristotle thought that the solution to Eleatic and Megarian arguments against motion and change could be found in a robust notion of potentiality.
Antiphasis: two propositions with the same subject, one of which denies of that subject exactly what the other affirms of it.
- What is past is necessary
- The impossible does not follow from the possible
- There is something possible which neither is nor will be true
Aristotle restricts the application of law of excluded middle to future contingent propositions, thought it is said that it’s not entirely clear how.
For Chrysippus, a proposition that is affirmed or denied is really an incorporeal entity, roughly meaning of a sentence that expresses it. Stoics called this a lekton (sayable), which is claimed by the author to be close to ‘meaning’ or ‘sense’.
Chrysippus considered that propositions about subjects specified by demonstratives/indexicals ceased to exist when the subject ceases to exist.
Using this idea, Chrysippus establishes that it is possible for something impossible to follow from something possible.
Such logical explorations are said to be attempts to philosophically reconcile their views about determinism.
Chrysippus is said to have developed a full-fledged sentential logic which was absent in Aristotle’s work according to the author. This is said to have been so because of Aristotle’s commitment to his notion of potentiality. It works bust with subject-predicate sentences, where possibility can be seen as a matter of the subject possessing a potentiality; it is said to be very difficult to extend it to compound propositions.
The author closes the article by saying that logical theories are closely entwined with a difference in philosophical standpoint.
Volker Peckhaus 1999 16 pages
Read 25 April 2021
In both book of Symbolic Logic, there is astonishingly no definition of the term “logic”.
In 19th century, logic was defined as: The art and science of reasoning (Whately) Doctrine giving the normative rules of correct reasoning (Herbart)
Symbolic logic arose from the old philosophical collective discipline of logic.
The standard presentations of the history of logic ignore the relationship between the philosophical and mathematical side of its development; they sometimes even deny that there has been any development of philosophical logic at all.
In The Development of Logic by Martha and William Kneale, they have written that “But our primary purpose has been to record the first appearances of these ideas which seem to us most important in the logic of our own day,” and these are the ideas leading to mathematical logic.
J. M. Bochenski’s assessment of “modern classical logic” which he scheduled between the 16th and 19th century was a noncreative period in logic which can therefore justly be ignored in the problem history of logic. According to Bochenski classical logic was only a decadent form of this science, a dead period in its development.
Such assessments show that authors adhered to the predominant views on logic of our time, i.e. actual systems of mathematical logic or symbolic logic. As a consequence, they have not been able to give reasons for the final divorce between philosophical and mathematical logic, because they have ignored the seed from which mathematical logic has emerged.
There are also oversimplifications present in treatments like that of Carl B. Boyer where the periods are divided into 1) Greek Logic 2) Scholastic Logic 3) Mathematical Logic skipping over works like Kant’s transcendental logic, Hegel’s metaphysics and Mill’s inductive logic. Whately’s and others works of these period I think gets skimmed over too.
The paper’s abstract says that it will be answering the following questions:
- Reasons for philosopher’s lack of interest in formal logic
- Reasons for mathematician’s interest in logic
- Meaning of logic reform in the 19th century; Were the systems of mathematical logic initially regarded as contributions to a reform of logic
- Was mathematical logic regarded as art, as science or as both?
British logicians regarded Germany as the logical paragon.
The development of the new logic started in 1847, completely independent of earlier anticipations, e.g. by the German rationalist Gottfried Wilhelm Leibniz and his followers. In that year British mathematician George Boole published his pamphlet The Mathematical Analysis of Logic. Boole mentioned that it was the struggle for priority concerning the quantification of the predicate between the Edinburgh philosopher William Hamilton and the London mathematician Augustus De Morgan which encouraged his study.
Hence, he referred to a startling philosophical discussion which indicated a vivid interest in formal logic in Great Britain. This interest was, however, a new interest, not even 20 years old. One can even say that neglect of formal logic could be regarded as a characteristic feature of British philosophy up to 1826 when Richard Whately published his Elements of Logic.
Thomas Lindsay, the translator of Friedrich Ueberweg’s important System der Logik und Geschichte der logischen Lehren was very critical of the scientific qualities of Whately’s book, but he, nevertheless, emphasized its outstanding contribution for the renaissance of formal logic in Great Britain.
One year after the publication of Whately’s book, George Bentham’s An Outline of a New System of Logic appeared which was to serve as a commentary to Whately. Bentham’s book was discussed by William Hamilton in a review article published in the Edinburgh Review (1833). With the help of this review Hamilton founded his reputation as the “first logical name in Britain, it may be in the world”. This was the opinion of De Morgan written in a letter to Spalding which was not sent. For George Boole, Hamilton was one of the “two greatest authorities in logic, modern and ancient”. The other authority is Aristotle.
Hamilton propagated a revival of the Aristotelian scholastic formal logic without, however, one-sidedly preferring the syllogism. His logical conception was focused on a revision of the standard forms by quantifying the predicates of judgments.
The controversy about priority arose, when De Morgan, in a lecture “On the Structure of the Syllogism” given to the Cambridge Philosophical Society on 9th November 1846, also proposed quantifying predicates.
None had any priority, of course. Application of the diagrammatic methods of the syllogism proposed e.g., by the 18th century mathematicians and philosophers Leonard Euler, Gottfried Ploucquet, and Johann Heinrich Lambert, presupposed quantification of the predicate.
German psychologistic logician Friedrich Eduard Beneke suggested quantifying the predicate in his books on logic of 1839 and 1842, the latter of which he sent to Hamilton.
Releasing of The Elements of Logic by Whately revived the interest in formal logic. This interest represented only one side of the effect. Another line of research stood in the direct tradition of Humean empiricism and the philosophy of inductive sciences: the inductive logic of John Stuart Mill, Alexander Bain, and others. Boole’s logic was in clear opposition to inductive logic. It was Boole’s follower William Stanley Jevons who made this opposition explicit.
It seems clear that, in regard to the 18th century dichotomy between German and British philosophy represented by the philosophies of Kant and Hume, Hamilton and Boole stood on the Kantian side.
In the preface to the second edition of his Kritik der reinen Vernunft of 1787, Kant wrote that logic has followed the safe course of a science since earliest times. For Kant this was evident because of the fact that logic had been prohibited from taking any steps backwards from the time of Aristotle. But he regarded it as curious that logic hadn’t taken a step forward either. Thus, logic seemed to be closed and complete. Formal logic, in Kant’s terminology the analytical part of general logic, did not play a prominent role in Kant’s system of transcendental philosophy. In any case it was a negative touchstone of truth, as he stressed. Georg Wilhelm Friedrich Hegel went further in denying any relevance of formal logic for philosophy.
Referring to Kant, he maintained that from the fact that logic hadn’t changed since Aristotle one could infer that it needed a complete rebuilding. Hegel created a variant of logic as the foundational science of his philosophical system, defining it as “the science of the pure idea, i.e., the idea in the abstract element of reasoning”. Hegelian logic thus coincides with metaphysics.
This was the situation when after Hegel’s death philosophical discussion on logic in Germany started. This discussion on logic reform stood under the label of “the logical question“, a term coined by the Neo-Aristotelian Adolf Trendelenburg. In 1842 he published “Zur Geschichte von Hegel”s Logick und dialektischer Methode” with the subtitle “Die logische Frage in Hegel’s Systeme”. The logical question according to Trendelenburg was: “Is Hegel’s dialectical method of pure reasoning a scientific procedure?”. In answering this question in the negative, he provided the occasion of rethinking the status of formal logic within a theory of human knowledge without, however, proposing a return to the old (scholastic) formal logic. In consequence the term “the logical question” was subsequently used in a less specific way. Georg Leonard Rabus, the early chronicler of the discussion on logic reform, wrote that the logical question emerged from doubts concerning the justification of formal logic.
Although this discussion was clearly connected to formal logic, the so-called reform did not concern formal logic. The reason was provided by the Neo-Kantian Wilhelm Windelband who wrote that the technique of correct thinking had been brought to perfection by Aristotelian philosophy.
Windelband was very critical of English mathematical logic. Its quantification of the predicate allows the correct presentation of extensions in judgments, but it “drops hopelessly” the vivid sense of all judgement, which tend to claim or deny a material relationship between subject or predicate. It is “a logic of the conference table”, which cannot be used in the vivid life of science, a “logical sport” which has, however, its merits in exercising the final acumen.
The philosophical reform efforts concerned primarily two areas:
- The problem of a foundation of logic which itself was approached by psychological and physiological means, leading to new discussion on the question of priority between logic and psychology, and to various forms of psychologism and anti-psychologism.
- The problem of logical applications focusing interest on the methodological part of traditional logic. The reform of applied logic attempted to bring philosophy in touch with the stormy development of mathematics and sciences of the time
Both reform procedures had a destructive effect on the shape of logic and philosophy: The struggle with psychologism led to the departure of psychology form the body of philosophy at the beginning of the 20th century. Psychology became a new, autonomous scientific discipline. The debate on methodology emerged with the creation of the philosophy of science which was separated from the body of logic. The philosopher’s ignorance of the development of formal logic caused a third departure: Part of formal logic was taken from the domain of the competence of philosophy and incorporated into mathematics where it was instrumentalized for foundational tasks.
Most of the new logicians in the period where philosophical discussions influenced logic in Great Britain can be related to the so-called “Cambridge Network” (Cannon 1978), i.e. the movement which aimed at reforming British science and mathematics which started at Cambridge.
Science in Culture: The Early Victorian Period (1978)
One of the roots of this movement was the foundation of the Analytical Society in 1812 by Charles Babbage, George Peacock, and John Herschel.
One of the first achievements of the Analytical Society was a revision of the Cambridge Tripos by adopting the Leibnizian notation for the calculus and abandoning the customary Newtonian theory of fluxions. It may be assumed that this successful movement triggered off by a change in notation might have stimulated a new or at least revived interest in operating with symbols. This new research on the calculus had parallels in innovative approaches to algebra which were motivated by the reception of Laplacian analysis.
Firstly the development of symbolical algebra has to be mentioned. It was codified by George Peacock in his Treatise on Algebra (1830) and further propagated in his famous report for the British Association for the Advancement of Science.
Peacock started by drawing a distinction between arithmetical and symbolical algebra, which was, however, still based on the common restrictive understanding of arithmetic as the doctrine of quantity. A generalization of Peacock’s concept can be seen in Duncan Gregory’s “calculus of operations”. Gregory was most interested in operations with symbols. He defined symbolical algebra as “the science which treats of the combination of operations defined not by their nature, that is by what they are or what they do, but by the laws of combinations to which they are subject”. Boole made the calculus of operations the basic methodological tool for analysis. However in following Gregory, he went further, proposing more applications. He cited Gregory who wrote that a symbol is defined algebraically “when its laws of combination are given; and that a symbol represents a given operation when the laws of combination of the latter are the same as those of the former”. It is possible that a symbol for an arbitrary operation can be applied to the same operation (What does this mean?). It is thus necessary to distinguish between arithmetical algebra and symbolical algebra which has to take into account symbolical, but non-arithmetical fields of application. As an example Gregory mentioned the symbols a and +a. They are the same in arithmetic, but in geometry a can denote a point marked by a line, whereas +a denotes the direction of the line.
Gregory deplored the fact that the unequivocity of notation didn’t prevail as a result of the persistence of mathematical practice. Clear notation was only advantageous, and Gregory thought that our minds would be “more free from prejudice, if we never used in the general science symbols to which definite meanings had been appropriated in the particular science”. Boole adopted this criticism almost word for word. In his Mathematical Analysis of Logic he claimed that the reception of symbolic algebra and its principles was delayed by the fact that in most interpretations of mathematical symbols the idea of quantity was involved. He felt that these connotations of quantitative relationships were the result of the context of the emergence of mathematical symbolism, and not of a universal principle of mathematics.
Boole read the principle of the permanence of the equivalent forms as a principle of independence from interpretation in an “algebra of symbols”. In order to obtain further affirmation, he tried to free the principle from the idea of quantity by applying the algebra of symbols to another field, the field of logic.
Principle of the Permanence of Form was formulated by George Peacock.
Boole expressed logical propositions in symbols whose laws of combination are based on the mental acts represented by them. Thus he attempted to establish a psychological foundation of logic, mediated, however, by language. The central mental act in Boole’s early logic is the act of election used for building cases. Man is able to separate objects from an arbitrary collection which belong to given classes, i order to distinguish them from others. The symbolic representation of these mental operations follows certain laws of combination which are similar to those of symbolic algebra. Logical theorems can thus be proven like mathematical theorems. Boole’s opinion has of course consequences for the place of logic in philosophy: “On the principle of a true classification, we ought no longer to associate Logic and Metaphysics, but Logic and Mathematics”.
Although Boole’s logical considerations became increasingly philosophical with time, aiming at the psychological and epistemological foundations of logic itself, his initial interest was not to reform logic but to reform mathematics. He wanted to establish an abstract view on mathematical operations without regard to the objects of these operations. When claiming “a place among the acknowledged forms of Mathematical Analysis” for the calculus of logic, he didn’t simply want to include logic in traditional mathematics. The superordinate discipline was a new mathematics. This is expressed in Boole’s writing: “It is not of the essence of mathematics to be conversant with the ideas of number and quantity”.
The most important representative of the German algebra of logic was the mathematician Ernst Schröder who was regarded as having completed the Boolean period in logic. In his first pamphlet on logic, Der Operationskreis des Logikkalkuls (1877), he presented a critical revision of Boole’s logic of classes, stressing the idea of duality between logical addition and logical multiplication introduced by William Stanley Jevons in 1864. In 1890, Schröder started on the large project, his monumental Vorlesungen über die Algebra der Logick which remained unfinished although it increased to three volumes with four parts, of which one appeared only posthumously.
Schröder’s own survey of his scientific aims and results contained a three part division:
- A number of papers dealing with some of the current problems of his science
- Studies concerned with creating an “absolute algebra”, i.e., a general theory of connections. Schröder stressed that such studies represent his “very own object of research” of which only little was published at that time
- Work on the reform and development of logic
Schröder’s own division of his fields of research shows that he didn’t consider himself a logician: His “very own object of research” was “absolute algebra”, and in respect to its basic problems and fundamental assumptions similar to modern abstract or universal algebra. What was the connection between logic and algebra in Schröder’s research? From the passages quoted one could assume that they belong to two separate fields of research, but this in to the case. They were intertwined in the framework of his heuristic idea of a general science. In his autobiographical note he stressed:
The disposition of schematizing, and the aspiration to condense practice to theory advised Schröder to prepare physics by perfecting mathematics. This required deepening-as of mechanics and geometry— above all of arithmetic and subsequently he became by the time aware of the necessity for a reform of the source of all these disciplines, logic.
Schröder’s universal claim becomes obvious. His scientific efforts served to provide the requirements to found physics as the science of material nature by “deepening the foundations,” to quote a famous metaphor later used by David Hilbert in order to illustrate the objectives of his axiomatic programme. Schröder regarded the formal part of logic that can be formed as a “calculating logic,” using a symbolical notation, as a model of formal algebra that is called “absolute” in its last state of development.
It has to be stressed that Schröder wrote his early considerations on formal algebra and logic without any knowledge of the results of his British predecessors. His sources were the textbooks of Martin Ohm, Herman Günther Graßmann, Hermann Hankel and Robert Graßmann. These sources show that Schröder was a representative of the tradition of German combinatorial algebra and algebraic analysis.
Like the British tradition, but independent of it, the German algebra of logic was connected to new trends in algebra. It differed from its British counterpart in its combinatorial approach. In both traditions, algebra of logic was invented with the enterprise to reform basic notions of mathematics which led to the emergence of structural abstract mathematics. The algebraists wanted to design algebra as “pan-mathematics”, i.e. as a general discipline embracing all mathematical disciplines as special cases. The independent attempts in Great Britain and Germany were combined when Schröder learned about the existence of Boole’s logic in late 1873, early 1874. Finally he enriched the Boolean class logic by adopting Charles S. Peirce’s theory of quantification and adding a logic of relatives according to the model of Peirce and De Morgan.
Although created by mathematicians, the new logic was widely ignored by fellow mathematicians. Both Schröder and Boole received little recognition at the time of their publication. The situation changed after George Boole’s death in 1864.
A broader international reception of Boole’s logic began when William Stanley Jevons made it the starting point for his influential Principles of Science of 1874. He used his own version of the Boolean calculus introduced in his Pure Logic of 1864.
Jevons considered Mathematics as a derivative of Logic. This relationship between mathematics and logic representing an early logicistic attitude is said to be shared by Gottlob Frege, Hermann Rudolf Lotze, and Ernst Schröder.
Jevons abandoned mathematical symbolism in logic, an attitude which was later take up by John Venn. Jevons attempted to free logic from the semblance of being a special mathematical discipline. He used the symbolic notation only as a means of expressing general truths. Logic became a tool for studying science, a new language providing symbols and structures. The change in notation brought the logic closer to the philosophical discourse of the time. The reconciliation was supported by the fact that Jevons formulated his Principles of Science as a rejoinder to John Stuart Mill’s A System of Logic of 1843, at that time the dominant work on logic and the philosophy of science in Great Britain.
Although Mill called his logic A System of Logic Ratiocinative and Inductive, the deductive parts played only a minor role, used only to show that all inferences, all proofs and discovery of truths consisted of inductions and their interpretations. Mill claimed to have shown “that all our knowledge, not intuitive, comes to use exclusively from that source”. Mill concluded that the question as to what induction is, is the most important question of the science of logic, “the question which includes all others”. As a result the logic of induction covers by far the largest part of this work, a subject which we would today regard as belonging to the philosophy of science.
Jevons defined induction as a simple inverse application of deduction. He began a direct argument with Mill in a series of papers entitled “Mill’s Philosophy Tested”.
Another effect of the attention caused by Jevons was that British algebra of logic was able to cross the Channel. In 1877. Louis Liard, at that time professor at the Faculté de lettres at Bordeaux and a friend of Jevons, published two papers on the logical systems of Jevons and Boole.
Although Herman Ulrici had published a first German review of Boole’s Laws of Thought as early as 1855, the knowledge of British symbolic logic was conveyed primarily by Alois Riehl, then professor at the University of Graz, in Astria. He published a widely read paper “Die englische Logik der Gegenwart” in 1877 which reported mainly Jevons’ logic and utilized it in a current German controversy on the possibility of scientific philosophy.
Alexander Bain was a Scottish philosopher who was an adherent of Mill’s logic. Bain’s Logic, first published in 1870, had two parts, the first on deduction and the second on induction. He shared the “[…] general conviction that the utility of the purely Formal Logic is but small; and that the rules of induction should be exemplified even in the most limited course of logical discipline”. The minor role of deduction showed up in Bain’s definition “Deduction is the application or extension of Induction to new cases”.
Despite his reservations about deduction. Bain’s Logic was quite important for the reception of symbolic logic because of a chapter of 30 pages entitled “Recent Additions to the Syllogism”. In this chapter the contributions of William Hamilton, Augustus De Morgan, and George Boole were introduced. Presumably many more people became acquainted with Boole’s algebra of logic through Bain’s report than through Boole’s own writings. One example is Hugh MacColl, the pioneer of the calculus of propositions and of modal logic. He created his ideas independently of Boole, eventually realizing the existence of the Boolean calculus by means of Bain’s report. Tadeusz Batóg and Roman Murawksi (Stanisaw Pi atkiewicz and the Beginnings of Mathematical Logic in Poland, 1996) have shown that it was Bain”’s presentation which motivated the first Polish algebraist of logic, Stanisaw Pi atkiewicz to begin his research on symbolic logic.
The remarkable collaboration of mathematics and philosophy can be seen in the fact that a broader reception of symbolic logic commenced only when its relevance for the philosophical discussion of the time came to the fore.
In Germany in the second half of the 19th century. Logic reform meant overcoming the Hegelian identification of logic and metaphysics. In Great Britain it meant enlarging the scope of the syllogism or elaborating the philosophy of science. Mathematicians were initially interested in utilizing logic for mathematical means, or they used it as a language for structuring and symbolizing extra-mathematical fields. Applications were for example:
- The foundation of mathematics (Boole, Schröder, Frege)
- The foundation of physics (Schröder)
- The preservation of rigour in mathematics (Peano)
- The theory of probabilities (Boole, Venn)
- The philosophy of science (Jevons)
- The theory of human relationships (Alexander Macfarlane)
and juridical questions.
The mathematicians’ preference for the organon aspect of formal logic seems to be the point of deviation between mathematicians and the philosophers who were not interested in elaborating logic as a tool.
Jean-Yves Bèziau 2020 18 pages Read 30 March 2021
Logical notions as presented by Tarski Presents a challenging fifth logical notion Context and origin of Tarski-Lindenbaum logical notions Notions in the simple case of a binary relation Examine in which sense these are considered as logical notions contrasting them with an example of a non-logical relation Formulations of the four logical notions in natural language and in first-order logic without equality, emphasizing the fact that 2 out of 4 logical notions cannot be expressed in this formal language. Relation between these notions using the theory of the square of opposition Notion of variety corresponding to all non-logical notions and it is argued that it can be considered as a logical notion because it is invariant, always referring to the same class of structures Presents an enigma: Is variety formalizable in first-order logic without equality?
At the end of the 1920s, Tarski developed the theory of the consequence operator, and form any years this theory was hardly known outside of Poland. The idea of this theory appeared for the first time in a two-page paper published in French in Poland in 1929. It was translated into English by R. Purdy and J. Zygmunt only in 2012!
- Logical Notions according to Tarski and Lindenbaum in the Perspective of a Childlike Methodology
In “What are logical notions?” Tarski proposes to define logical notions as those invariant under any one-to-one transformation, something he presents as a generalization of an idea of Felix Klein (1849 – 1925), connected tot he so-called “Erlangen program”.
As Tarski says in the paper, edited by Corcoran, the idea of characterizing logical notions in such a way already appears in a paper by Lindenbaum and himself in 1934.
Adolf Lindenbaum was the main collaborator and friend of Tarski when he was in Poland.
It is possible to prove that any nary relation can be expressed / reduced to a binary relation.
Kalmar 1932, 1936, 1939.
Tarski identified, the universal relation, the empty relation, the identity relation, and diversity relation as the only logical binary relations between individuals. This is interesting because just these four relations were introduced and discussed in the theory of relations by Peirce, Schröder, and other logicians of the 19th century.
Papy 1963-67, 1969
An example of a non-logical relation is illustrated.
Using this example, models of a formula are introduce as different configurations described by it.
Tarski 1954 - 55
Tarski talks about individuals in the case of binary relations between individuals.
The same formula that results in an isomorphic representation in the case of two individuals becomes non-isomorphic (and thereby non-categorical?).
Categoricity is said to be a necessary and sufficient condition for logicality If a binary relation can be described by a categorical formula, it is sufficient to consider it to be a logical notion.
Logical notions are defined by invariance.
Hodges 1983
The entities in the case of a binary relation which are not the logical notions are collectively called a variety.
A variety is a complement of the logical notions.
There is invariance in this variety: for every cardinality, it always refers to the same class of models, those not corresponding to logical notions.
The notion of variety collects all the non-logical relations. Since it is an invariant, the variety is seen as a fifth logical notion.
Tarski-Lindenbaum invariance is based on isomorphism, but it can be seen from the higher perspective of notions always referring to the same classes of models.
2006 Solomon Feferman
Read Apr 10 2021
Alan Turing spent the years 1936 – 1938 doing graduate work under the direction of Alonzo Church.
Two years sufficed for him to complete a thesis and obtain the Ph. D.
Systems of Logic based on Ordinals
First systematic attempt to deal with the natural idea of overcoming Gödelian incompleteness of formal systems by iterating the adjunction of statements
Turing’s dissertation in undergraduate was “On the Gaussian error function” which contained his independent rediscovery of the central limit theorem.
He attended the class of topologist M. H. A. (Max) Newman. One of the problems from Newman’s course that captured Turing’s attention was the Entscheidungsproblem, the question whether there exists an effective method to decide, given any well-formed formula of first-order predicate calculus, whether or not it is valid in all possible interpretations (equivalently, whether or not its negation is satisfiable in some interpretation).
Turing became convinced that the answer must be negative, but that in order to demonstrate the impossibility of a decision procedure, he would have to give an exact mathematical explanation of what it means to be computable by a strictly mechanical process.
By mid-April 1936 Turing came up with an idea of Turing machine, an idealized computational device following a finite table of instructions (in essence, a program) in discrete effective steps without limitation on time or space that might be needed for a computation.
Furthermore, he showed that even with such unlimited capacities, the answer to the general Entscheidungsproblem must be negative. Turing quickly prepared a draft of his work entitled “On computable numbers, with an application to the Entscheidungsproblem”
Neither Newman nor Turing were aware at that point that there were already two other proposals under serious consideration for analyzing the general concept of effective computability: one by Gödel called general recursiveness, building on an idea of Herbrand, and the other by Church, in terms of what he called the Lambda Calculus.
In answer to the question, “Which functions of natural numbers are effectively computable?”, the Herbrand-Gödel approach was formulated in terms of finite systems of equations from which the values of the functions are to be deduced using some elementary rules of inference; since the functions to be defined can occur on both sides of the equations, this constitutes a general form of recursion.
But Gödel regarded general recursiveness only as a “heuristic principle” and was not himself willing to commit to that proposed analysis.
Using a representation of the natural numbers in the lambda calculus, a function f is said to be lambda-definable if there is an expression t such that for each pair of numerals n and m, tn evaluates out to m if and only if f(n) = m. In conversations with Gödel, Church proposed lambda-definability as the precise explanation of effective computability (Church’s Thesis), but in Gödel’s view that was “thoroughly unsatisfactory”. It was only through a chain of equivalences that ended up with Turing’s analysis that Gödel later came to accept it, albeit indirectly.
The first link in the chain was forged with the proof by Church and Kleene than lambda-definability is equivalent to general recursiveness. Thus when Church finally announced his “Thesis” in 1936, in An unsolvable problem of elementary number theory, it was in terms of the latter.
In a follow-up paper, A note on the Entscheidungsproblem, Church proved the unsolvability of the Entscheidungsproblem for logic.
The news reached Cambridge a month later, but Turing’s analysis was sufficiently different to still warrant publication.
After submitting it for publication toward the end of May 1936, Turing tacked on an appendix in August of that year in which he sketched proof of equivalence of computability by a machine in his sense with that of lambda-definability, thus forging the second link in the chain of equivalences.
Church reviewed Turing’s paper and he wrote that there are equivalences between three different notions: computability by a Turing machine, general recursiveness in the sense of Herbrand-Gödel-Kleene, and lambda-definability in the sense of Church-Kleene.
From this was born what is now called the Church Turing Thesis, according to which the effectively computable functions are exactly those computable by a Turing machine.
On Newman’s recommendation, Turing decided to spend a year studying with Church.
In the spring of 1937, Turing worked up for publication a proof in greater detail of the equivalence of machine computability with lambda-definability. He also published two papers on group theory, including one on finite approximations of continuous groups that was of interest to von Neumann.
Turing, who had just turned 25, returned to England for the summer of 1937, where he devoted himself to 3 projects: finishing the computability / lambda-definability paper, ordinal logics, and the Skewes number.
Skewes had shown that li(x) < 10_3(34) (triple exponential to the base 10), if the Riemann Hypothesis is true. Turing hoped to lower Skewes’ bound or eliminate the Riemann Hypothesis; in the end he thought he had succeeded in doing both and prepared a draft but did not publish his work. A paper based on Turing’s ideas, with certain corrections, was published after his death by Cohen and Mayhew.
Church would not knowingly tolerate imprecise formulations or proofs, let alone errors, and the published version of Turing’s thesis shows that he went far to meet such demands while retaining his distinctive voice and original ways of thinking.
What Turing calls a logic is nowadays more usually called a formal system, i.e. one prescribed by an effective specification of a language, set of axioms and rules of inference.
Couldn’t precisely follow the technical details section.
One reason that reception of Turing’s paper may have been so limited is that it was formulated in terms of the lambda-calculus, which makes expressions for ordinals and formal systems very hard to understand. Feferman draws attention to the comment of Kleene who changed his notation to that of general recursiveness because of audience reception in 1933-35 period.
Feferman has worked out a paper in which he has cast Turing’s work on ordinal logics as a formal system with notions cast in general recursive functions and recursive notions for ordinals rather than the lambda-calculus.
Judy Green 2004 15
Read 11 Apr 2021
An algebra of logic of the 19th century was a scheme for symbolizing logical relationships as algebraic ones in such a way that logical deductions could be accomplished by algebraic manipulations. Boole wrote three works on logic and none of them is said to have adequately dealt with existential statements. None of Boole’s successors too is said to have adequately dealt with them either, although some of the later versions of the algebra of logic improved substantially on Boole’s treatment.
During the approximately 50 years that constituted the period in which the algebra of logic was the mainstream of mathematical research in logic, logicians never agreed upon a single notation system. Finally, around the turn of the century, the term “algebra of logic” began to be used in the modern sense of Boolean algebra and, because of that, what Boole started in 1847 is now essentially hidden.
What George Boole really started was not Boolean algebra but the algebra of logic.
It was not an algebraic structure defined in terms of operations and axioms that the operations satisfy rather an algebra of logic was a scheme for grounding logical relationships as algebraic ones in a way that logical deductions could be accomplished by algebraic manipulations.logical relationships as algebraic ones in a way that logical deductions could be accomplished by algebraic manipulations. Boole’s development of such a scheme was motivated by work in the calculus of operations in early 19th century Great Britain.
Boole was influenced by Duncan Gregory’s work on the calculus of operations.
Boole quotes from Gregory’s work in “On a General Method in Analysis” and uses this principle in his work in The Mathematical Analysis of Logic. He states that laws of combination can be more general than the quantitative interpretation in which some forms are determined.
Boole defines his symbols so that 1 represents his universe. Uppercase letters which only appear in the text as generic members of classes Lowercase letters are called elective symbols operate on classes.
He states: “the symbol x operating upon any subject comprehending individuals or classes, shall be supposed to select from that subject all the Xs which it contains”.
Also, when no subject is expressed, 1 (the Universe) is supposed to be the subject.
x can be thought of as x * 1, where all Xs are thus selected.
xy means the intersection of all Xs and Ys in modern terms
Interpreting addition as disjoint union, Boole shows that his interpretation requires 3 rules:
- Distribution of Multiplication over Addition
- Commutativity of Multiplication
- Index Law (x ^ n = x)
These rules are stated as being sufficient for the calculus
The statements:
All Xs are Ys and No Xs are Ys can be cast as x(1-y) = 0 and xy = 0 respectively.
But Some Xs are Ys and Some Xs are not Ys makes use of a separate elective symbol v that roughly represents the operation of selecting all elements, V, of a nonempty subset of appropriate terms.
In effect, when a logical premise is interpreted algebraically according to this scheme, the auxiliary equations or conditions become additional premises that carry existential interpretations.
For example, the auxiliary equations for the expression Some Xs are not Ys carry the existential implications that there are Xs and there are not Ys. When an algebraic conclusion is to be reinterpreted in logical terms, the auxiliary conditions, and equations, must be satisfied.
Boole algebraically derives syllogisms by eliminating the variable representing the middle term from the two equations representing the premises.
After discussing the syllogism, Boole extends his 1847 system to deal with a calculus of propositions. As before, the lower case letters that appear in the formulas are given an operational interpretation, x, representing the operation of selecting those cases for which the proposition X is true and 1 - x selecting those for which it is false.
Boole ends The Mathematical Analysis of Logic by considering elective functions and equations, that is functions and equations involving elective symbols, x, y, v, etc. In solving elective equations he uses techniques of the algebra of quantity, such as Maclaurin’s theorem and division, including division by 0.
A discussion on interpretations that can be given to division by 0 and the fraction 0/0 was described by De Morgan in his “On the study and difficulties of mathematics (1831)”. This is then lead up to how Boole interpreted fractions like 0/0 and 1/0 in his work.
It was suggested to Boole to use the copula of >, so that he can eliminate the need for the elective symbol v used for denoting when representing categorical statements that involve quantifier “some”.
Boole gives two different interpretations of the statement No Xs are Ys and says that one is an assertion respecting a proposition and the other as a single categorical proposition.
Boole in his 1854, The Laws of Thought, addresses both categorical and hypothetical propositions, this time referring to the categorical propositions, ones that express relations between things, as primary, and to the hypothetical propositions, ones that express relations between propositions, as secondary.
There is also the suggestion of the theory of Boolean algebras as an algebraic structure.
The logicians who followed Boole also relied heavily on the interpretations in which they were working.
In the development and presentation of these algebras of logic, there was an ongoing interaction between the formulation of the calculus and its intended interpretation that is absent in the more modern formalistic view.
Venn wanted to give particular statements a universal interpretation, while Boole, in his later works, gave his universal statements an existential import.
Venn’s suggestion that a particular statement should be replaced by a reference to a specific object that has the required property bears some resemblance to the modern constructivist development of mathematics.
Even though the successors of Boole were less strict on maintaining the analogy between algebra of logic and the algebra of quantity, their analyses blur some crucial distinctions.
The logic of sets and propositions are often not distinguished from one another. At a more fundamental level, the algebra of logic never achieved separation between syntax and semantics, that is, between the rules of formation of formulas and their manipulation on the one hand, and the interpretation of the symbols on the other.
This distinction was hinted at by Augustus De Morgan in “On the foundation of algebra” published in 1941 (Read on 9 December 1839).
Algebra now consists of two parts, the technical, and the logical. Technical algebra is the art of using symbols under regulations which, when this part of the subject is considered independently of the other, are prescribed as the definitions of the symbols. Logical algebra is the science which investigates the method of giving meaning to the primary symbols, and of interpreting all subsequent symbolic results.
De Morgan credits George Peacock as making the distinction between these two parts of algebra first.
While Boole didn’t use any other copula than the equality symbol, some of the systems developed by his people who came after him used such copula. Ladd writes about them:
Algebras of Logic may be divided into two classes, according as they assign the expression of the “quantity” of propositions to the copula or to the subject. Algebras of the latter class use one copula only — the sign of equality; for an algebra of the former class two copulas are necessary, — one universal and one particular.
The word quantity in the above quotation refers to the distinction between universal and existential statements, that is between statements that involve the concept all and the concept some.
Venn’s Symbolic Logic included 25 different symbolic expressions for No S is P, reflecting not merely differing notational preferences but, in many cases, actual conceptual differences.
Work that is generally considered to have presented the algebra of logic in its most mature form is Ernst Schröder’s three volume Vorlesungen über die Algebra der Logik, published between 1890 and 1905.
Both Schröder and Peirce recognized that the algebra of logic is not really an axiomatic system.
Around the turn of the century, Whitehead and Huntington used the expression “algebra of logic” to denote the formal calculus that can be abstracted from the propositional calculus and naive set theory and that forms the basis of the theory of Boolean algebras.
The term “Boolean algebra” was not used in this sense until H. M. Sheffer coined the term in his 1913 paper, “A Set of Five Independent Postulates for Boolean Algebras, with Application to Logical Constants.”
Although the term had been used by Peirce around 1880, he used it to refer to techniques of symbol manipulation, not to algebraic structures.
The changing meaning and interchangeable use of the two expressions, “algebra of logic” and “Boolean algebra,” has tended to lead to an over-simplified historical picture of the 19th century algebra of logic, which was both less abstract and more ambitious than the theory of Boolean algebras.
35 pages Read 25 April 2021
It is said to be a series of notes than a scholarly treatise. Notes presented here using concepts introduced or formalized by Tarski contribute toward two main goals:
- Comparing Aristotle’s system with one Boole constructed intending to broaden and to justify Aristotle’s
- Giving a modern perspective to both logics
Aristotle is best representative of the earlier period Boole of the transitional period Tarski best of the most recent period
Five great logicians: Aristotle George Boole Alfred Tarski Gottlob Frege Kurt Gödel
Aristotle a prolific philosopher Boole an influential mathematical analyst Tarski an accomplished algebraist, geometer and set-theorist
Aristotle founded logic as organon - as “formal epistemology”. He was the first to systematically attempt a theory of demonstrative proof and the first to develop criteria of validity and invalidity of premise-conclusion arguments. He was the first to treat formal deduction and the first to treat independence proofs. Boole founded logic as science – as “formal ontology”. He was the first to explicitly recognize the role of tautologies in deduction and to attempt a systematic treatment of “laws of thought” – his expression which was later used in essentially the same sense by Tarski. Tarski founded metalogic – the science explicitly conducted in the metalanguage and focusing among other things on syntax and semantics of idealized languages of sciences including logic. Much of Tarski’s theory of metalogic, or “formal methodology”, appeared in the 1933 truth-definition monograph, the 1936 consequence-definition paper, and the 1986 logical-notion-definition paper.
Aristotle: Formal Epistemology Boole: Formal Ontology Tarski: Formal Methodology
Tarski’s three important papers: truth-definition (1933), consequence-definition (1936), logical-notion-definition (1986).
Other useful works of Tarski: Introduction to Logic and to the Methodology of Deductive Sciences (1941 / 1994) Truth and Proof (1969/1993)
Tarski was probably the most prolific logician of all time.
Prior Analytics presented the world’s first extant logical system. Its system, which could be called a logic today, involves 3 parts:
- A limited domain of propositions expressed in a formalized canonical notation
- A method of deduction for establishing validity of arguments having unlimited number of premises
- An equally general method of counterarguments or countermodels for establishing invalidity
Roughly speaking, these correspond respectively to the grammar, derivation system, and semantics of a modern logic.
Laws of Thought presented the world’s first symbolic logic. Boole’s system, which does not fully merit being called a logic in the modern sense, involves a limited domain of propositions expressed in a formalized language as did Aristotle’s.
Boole intended the class of propositions expressible in his formalized language not only to include but also to be far more comprehensive than that expressible in Aristotle’s. However he was not entirely successful in this.
Moreover, where Aristotle had a method of deduction that satisfies the highest modern standards of cogency, soundness and completeness, Boole had a semi-formal method of derivation that is neither sound nor complete.
It is termed semi-formal because Boole was far from clear about the algorithmic specifications of his own symbol manipulations.
Aristotle’s discussion of goals and his conscientious persistence in their pursuit make soundness and completeness properties that a reader could hope, if not expect, to find his logic to have. In contrast, Boole makes it clear that his primary goal was to generate or derive solutions to sets of equations regarded as conditions on unknowns. The goal of gaplessly deducing conclusions from set of propositions regarded as premises, though mentioned by Boole, is not pursued.
The idea that the premises of a valid argument could be regarded as equational conditions on unknowns while the conclusion could be regarded as a solution was revolutionary, unprecedented and totally original with Boole. The fact that it is not only gratuitous but flatly false is ignored by most modern writers, whether out of politeness or inattention.
Gaplessness is designated in Aristotle’s Greek by teleios (complete, fulfilled, finished, perfect, etc.). Tarski uses the German vollständig (complete, entire, whole, etc.) or the English “complete”. But this aspect of logical inquiry is so far from Boole’s focus that he has no word for it. Accordingly, the deductive part of Boole’s algebraic equation-solving method is far from complete: associative laws are missing for his so-called logical addition and multiplication, to cite especially transparent but typical omissions.
As for a possible third par of Boole’s logic, a method of establishing invalidity, nothing answers to this in the realm of equation-solving. Perhaps accordingly, essentially no discussion in Boole’s writings concerns independence proofs demonstrating that a given conclusion is not a consequence of given premises: certainly nothing like a method of countermodels (counterinterpretations, or counterarguments) is to be seen. Boole never mentions the ancient problem of showing that the parallel postulate does not follow from Euclid’s other premises.
Nevertheless Boole’s formalized language went beyond Aristotle’s by including tautologies, or – in Boole’s phrase also used by Tarski — laws of thought, such as Boole’s law of non-contradiction. As Boole’s title emphasized, Laws of Thought brought into a logical system principles formerly thought to belong to philosophy, thereby opening the way to logic in Tarski’s sense quoted above. The idea that logic, not metaphysics, establishes general laws involving concepts common to all sciences was not seriously pursued before Boole showed the way.
By setting forth in clear and systematic fashion the basic methods for establishing validity and for establishing invalidity, Aristotle became the founder of logic as formal epistemology. By making the first unmistakable steps toward opening logic to the study of “laws of thought” — tautologies and metalogical laws such as excluded middle and non-contradiction — Boole became the founder of logic as formal ontology. It is said that ironically, 25 years after Boole presented an expanded view of logic that included concern with logical truth along with the traditional concern with logical consequence, Frege adopted a restricted view of logic focused on logical truth and ignoring, perhaps excluding, logical consequence.
Neither Aristotle nor Boole had much insight into “logicography”, the study of how a logical system is rigorously described, or into the basic methodological premises assumed in the descriptions of logical systems. Consequently perhaps, neither made any effort to determine whether their theories of deduction were satisfied by the “proofs”, or argumentations, that they themselves offered in support of their claims about the merits or adequacy of their systems.
In short, neither applied to his own meta-deductions the standards they themselves had set forth for deduction of object-language conclusions from object-language premises. In effect neither asked of himself whether he was practicing what he was preaching. And there is no sign in either that their own “proofs” had been deliberately or inadvertently affected by their own theories of proof. This lapse of self-awareness resembles a self-excepting fallacy such as an inconsistent accusation of inconsistency or a communication of a claim that communication is impossible. Even more remarkable, none of their immediate successors, neither supporters not critics, understood the theories well enough to notice this now-glaring deficiency.
More generally, neither Aristotle nor Boole had much awareness of the details of their own respective frameworks of terminology. Neither had much insight into meta-language or into what the epistemological-ontological status of its concepts and entities may be, into what we now call metalogic, in the broad sense, or formal methodology.
More than any other logician, Tarski identified and addressed the need for a systematic metatheoretic study of logical theories. His 1933 truth-concept monograph made clear the conception of a formal-sentence language as a subset of a universe of strings – concatenation of characters over a finite “alphabet”. Tarski 1933 calls characters signs and strings expressions. Church calls characters symbols and strings formulas.
Without precedent in the history of logic, it established axiomatic foundations of what is now called string theory – the mathematical theory presupposed by any definitions of fundamental concepts such as “truth”, “consequence”, “logical constant”, and “proof”.
His monograph, a penetrating and innovative philosophical, mathematical, and logical work, clarified, integrated and advanced awareness of basic concepts, principles, and methods of metalogic or formal methodology to such an extent that it has come to occupy a place in the history of logic comparable to Prior Analytics and Laws of Thought. It contains the world’s first axiomatically presented metatheory.
Moreover, although Aristotle took formal deducibility as methodological criterion of consequence as did Boole and Tarski, and although Aristotle took presentation of a counterargument as a methodological criterion of independence (non-consequence) as did Tarski (but surprisingly not Boole), neither Aristotle nor Boole attempted a definition of the fundamental concept of consequence as Tarski did.
Neither Aristotle nor Boole gave more than tantalizing hints as to what they meant by phrases such as ‘logically implies’, ‘follows of necessity from’, ‘is a logical consequence of’, and the like. Although Tarski was neither the first person to notice the need for a definition of consequence nor the first to attempt a definition, he constructed the conceptual framework within which modern definitions are situated, and his 1936 definition formed the paradigm for later attempts.
Bernard Bolzano preceded Tarski in attempting to give a definition of logical consequence.
In the 1936 consequence-definition paper Tarski identifies the chasm in pre-modern logic and, in the eyes of many, filled the chasm with a formally and materially adequate model-theoretic definition of consequence.
Incidentally, one of the most fundamental achievements of Tarski’s 1933 truth-concept paper was to clarify and rigorously exemplify the important but subtle distinction between definitions and criteria (or decision-procedures).
Tarski went on to give a partial criterion to truth: in order to recognize a proposition as true it is sufficient to deduce it from propositions known to be true. This point is highlighted by the title of his paper “Truth and Proof (1969)”.
As Tarski repeatedly emphasized, having a definition of truth is not the same as having a criterion of truth; understanding what it means to say that a proposition is true is not the same as having a method for determining whether it is true.
“The principles of logical inference are universally applied in every branch of systematic knowledge. For over 2000 years mathematicians have been making correct inferences of a systematic and intricate sort, and logicians and philosophers have been analyzing … valid arguments. It is therefore, somewhat surprising that a fully adequate formal theory of inference has been developed only in the last three or four decades. … The most important defect in the classical tradition was the failure to relate logic as the theory of inference to the kind of deductive reasonings that are continually used in mathematics.” — Patrick Suppes, Introduction to Logic (1957)
Early use of deduction in mathematics began long before Aristotle. It has been traced by Immanuel Kant as far back as Thales, who is said to have deduced by logical reasoning from intuitively evident propositions the conclusion, far from intuitively evident, that every two triangles, no matter how different in size or shape, nevertheless have the same angle-sum. This is one of Aristotle’s favourite examples of the power of logical deduction. Its clarification was one goal of Hilbert’s 1899 axiomatization of geometry, as he revealed in a letter to Frege dated 29 December 1899.
Prior Analytics addressed the 2 central problems of logic as formal epistemology:
- How to show that a given conclusion follows from given premises that formally imply it
- How to show that a given conclusion does not follow from given premises that do not formally imply it. Aristotle wanted a decisive test or criterion for determining if the conclusion follows and also one for determining if the conclusion does not follow. Using other equally traditional terminology, Aristotle’s problems were how to establish validity and how to establish invalidity of an arbitrary argument, no matter how many premises or how complicated its propositions.
An argument or, more fully, a premise-conclusion, argument is a two-part system composed of a set of propositions called the premises and a single proposition called the conclusion: Argument: <Premises, Conclusion>. An argument is valid if the conclusion is logically implied by the premise set, and it is invalid otherwise, i.e., if the conclusion contains information beyond that in the premise set. Whether an argument is valid is totally objective having no dependence on any subjective judgement or mental operations.
In this sense, an argument contains no steps of deductive reasoning – in order to know that an argument is valid a person must produce an argumentation, often involving many steps and many intermediate conclusions. Of course,t here are other senses of the word ‘argument’. In fact mathematicians often use it as a synonym for ‘argumentation’ and in that sense an ‘argument’ contains a chain of steps of reasoning going beyond the premises set and ending with final conclusion.
To understand how Boole changed the field of logic, note that Aristotle’s logic was confined to logical epistemology, to concern with determining validity and invalidity of premise-conclusion arguments. Today this is but one concern of logic despite many popular treatments of logic claiming it to be logic’s exclusive concern.
Aristotle’s definition of deduction (sullogismos, syllogism) is broad enough to include any chain of reasoning whose conclusion follows logically form its premise-set, regardless of number of premises, complexity of propositions, or subject-matter. Aristotle’s definition of syllogism is said to be broad to include any valid inference: A syllogism is an argument (logos) in which, when certain things are assumed, something different from what is assumed follows by necessity from the fact that these things are so”.
Aristotle did not solve the problem of formal epistemology in its full generality, nor did he claim to, contrary to what Kant and a few logicians seemed to have thought.
Aristotle would have never written what two respected American logicians wrote: “Given premises and conclusion, logic can determine whether this conclusion follows” (Lewis and Langford 1932)
Mathematical logicians will realize that of its two principal readings one contradicts Gödel’s Incompleteness Theorem and one contradicts Church’s Theorem.
As Boole saw, the case of the problem of formal epistemology that Aristotle did completely solve is a small fragment of what has been accomplished by modern logicians. The class of arguments he treated is just on the threshold of logic. Even though Boole made great progress, the class he treated is still very small by modern standards.
Bertrand Russell was not exaggerating when he wrote: “Anyone in the present day who wishes to learn [modern] logic will be wasting his time if he reads Aristotle or any of his disciples”.
It is of course impossible to identify or construct a method or criterion for recognizing instances of a relation or property without understanding the relation or property. Moreover, in order to understand a relation or property it is not necessary to have a formally and materially adequate definition of it. But such understanding is necessary for discovering a definition. In order to define “human being” it is necessary to understand the concept, to know what human beings are. Likewise, in order to understand a concept or have a definition of it, it is not necessary, or even usual, to have a criterion for determining that it applies in an arbitrary case.
As Tarski noted, an adequate definition need not provide a criterion, and normally does not. In connection with truth definitions he said: “Whatever may be achieved by constructing an adequate definition of truth …, one fact seems to be certain: the definition does not carry with it a workable criterion for deciding whether … sentences … are true ( … it is not designed for this purpose).
The word ‘criterion’ has an ambiguity that is worth attention. Although in the essay it is mentioned that Aristotle had a deductive criterion for validity and a radically non-deductive criterion of invalidity, it might be thought that a criterion for a given property, say validity, is automatically also a criterion for its complementary opposite, in this case invalidity. There are two sense of the word ‘criterion’: a weaker and a stronger. Following Tarski and others, Corcoran uses the word in the weaker sense in which a criterion for a property is a performable method for determining that a given entity has the property if it does. It is widely recognized that such a method may not determine anything if applied to an entity not having the property. In the stronger sense a criterion is a method which determines whether or not the property applies. In the stronger sense, but not in the weaker, every criterion for a given property is automatically a criterion for the complementary opposite. Hilbert and Ackermann use ‘criterion’ in the stronger sense.
Although Aristotle is clear in presenting his two procedural criteria for what amounts to validity and for what amounts to invalidity, nevertheless he gives no hint of a definition of either concept, or of any functionally equivalent concept. More specifically, Aristotle nowhere recognizes a need to define the metalogical concepts “implies”, “consequence”, “follows from”, “valid”, or any of the concepts regarded as interdefineable with them. This raises the question of whether Aristotle may have subscribed in regard to these concepts to an operationalistic or behavioristic positivism that “identifies” concepts, or definitions of concepts, with procedures for detecting their instances, e.g. to a view that would take the meaning of ‘valid’ and that of ‘invalid’ to be respectively the method by which an argument is recognized as being valid and that by which one is recognized as being invalid. The hypothesis would be that Aristotle held an algorithmic or procedural view of metalogical concepts, a view that would repudiate or render futile any need for an explicit definition of validity or invalidity such as that proposed in the 1936 consequence paper. There is no evidence of this. Aristotle’s twin problems invite definitions that he does not supply. In view of Aristotle’s unusual sensitivity to the importance of definition,s the absence of discussion of definition of any metalogical concept such as “follows of necessity from” (or “is a consequence of”) or its negative must be regarded as significant. The issue of whether the absence of this definition was inadvertent or deliberate must remain for future scholars to decide. Moreover, the absence of definitions only increases the significance of the two criteria that he did give us.
There are passages that point to Aristotle’s understanding of the consequence or implication relation. In Chapter 17 of Sophistical Refutations 176a32, he writes that the consequences of a thesis appear to be parts of the thesis itself.
For the initial partial solution to the twin problems, Aristotle presented the world’s first extant logical system. Aristotle’s logic was not a comprehensive “grand logic” such as that of Frege 1879 or Whitehead-Russell 1910. His research strategy was like that of Archimedes in dealing with hydrostatics, a carefully delimited part of fluid mechanics that treats the special case of a fluid at rest. Hydrostatics is a necessary preparation for the wider study that includes hydrodynamics, the study of fluid in motion. The strategy is to deal with a simple, perhaps idealized or even fictitious, case first before attacking the problems in their full generality or perhaps before attacking more complicated special cases.
Aristotle nowhere says that his particular system, the so-called assertoric categorical syllogistic, was a comprehensive and exhaustive logic. Kant is frequently criticized, even ridiculed, for making this claim on Aristotle’s behalf (Bolzano 1837/1972, Hilbert and Ackermann 1928/38/50, Cohen and Nagel 1934/62/93)
Aristotle never said, as some of his less careful but more enthusiastic followers have said, that the syllogistic is adequate for propositional logic. And Aristotle certainly never said anything comparable to the pathetically irresponsible remark of John Stuart Mill that “The whole of Euclid, for example, might be thrown without difficulty into a series of syllogisms, regular in mood and figure.”
The above paragraph addresses the question already raised by logicians and philosophers such as da Costa and Santos (per. comm.) of how to explain the gross inadequacy of the theory of propositions (or formal grammar) underlying Aristotle’s syllogistic and the apparently simplistic narrowness of the class of arguments it treats. These inadequacies have been widely noticed. They are nearly impossible to miss.
They are often not described as virtues, which they clearly are, but as faults to be charged against Aristotle. Regrettably, Corcoran did it himself — ironically, in a paper that was somewhat predicated on the fact that simplifications, even oversimplifications, and unrealistic idealizations play legitimate and important roles in scientific and humanistic progress.
Corcoran addressed this in a 1989 lecture “Logical methodology: Aristotle and Tarski”. He wrote there:
Logical methodology is the study of methods in logic, most notably, methods for determining whether a given conclusion is a consequence of or is independent of a given premise-set. Aristotle pioneered logical methodology and Tarski was its most vigorous modern proponent. Aristotle’s most original, most influential, and most lasting contribution to logic was his methodological theory, not the logical system known as syllogistic logic, which he considered one of many exemplifications of logical methodology, by no means exhaustive of logical phenomena. … The method of deduction for establishing consequence and the method of reinterpretation for establishing independence both originated with Aristotle, who had already distinguished consequence from deducibility – notwithstanding the fact that Aristotle’s languages were always fully interpreted.
In Tarski’s treatment deduction comes to have a syntactical character never envisioned by Aristotle, and consequence comes to have a semantic character hardly conceivable without set theory. In this paper some of Tarski’s most philosophical contributions to logic are explained as natural refinements of logical methods whose epistemic purpose has remained constant since Aristotle.
Tarski never mentions details of the so-called Aristotelian syllogistic system, yet he fully embraces the central ideas of Aristotle’s logical methodology: recognizing validity by a formal step-by-step deduction and recognizing invalidity by a counterargument, or by what amounts to a counterargument. This acceptance of Aristotle’s two-part methodology of deduction and counterinterpretation continues in the most recent logic texts, e.g. Computability and Logic (Boolos, Burgess and Jeffrey 2002), and Deductive Logic (Goldfarb 2003).
To reiterate: Aristotle’s system, which is somewhat similar to a modern logic, involves 3 parts:
- A limited domain of propositions expressed in a formalized language
- A formal method of deduction for establishing validity of arguments having an unlimited number of premises
- An equally general method of countermodel or counterargument for establishing invalidity
Prior Analytics presupposes no previous logic on the part of the reader. However, it does require knowledge of basic plane geometry, including ability and experience in deducing non-evident theorems from intuitively evident premises such as those taken as axioms and postulates a generation or so later by Euclid. Especially important is familiarity with reductio ad absurdum or indirect deduction. Aristotle repeatedly refers to geometrical proofs, both direct and indirect. It also requires readers to ask themselves what is demonstrative knowledge, how do humans acquire it, what is a proof, and how is a proof made.
For Aristotle a proof proves (to those for whom it is a proof) that its conclusion is true. For him, and for many modern logicians, in the strict sense of ‘prove’, there is no way to prove a false proposition. Cohen and Nagel are exceptions. And, through use of the unfortunate expression ‘proof from hypotheses’, Church is an apparent exception. Since ‘prove’ and its cognates are interchangeable respectively with ‘demonstrates’ and its cognates, this means that for Aristotle a demonstration demonstrates (to those for whom it is a demonstration) that its conclusion is true.
Every proof produces demonstrative (apodictic) knowledge of its conclusion. The Socratic proof/persuasion distinction reappears in Aristotle along with the knowledge/belief distinction. A proof does not merely persuade; it produces knowledge, not merely belief. After all, fallacious argumentations produce belief.
The fundamental knowledge-through-proof thesis, that proof establishes knowledge, was never doubted by Boole although he said little worth repeating on the topic. In full awareness that the thesis had been challenged in the years after Boole, Tarski reaffirmed and endorsed it in some of his writings. He wrote:
The notion of proof … refers just to a procedure of ascertaining the truth … This procedure is an essential element of … the axiomatic method, the only method now used to develop mathematical disciplines.
Deduction should be discussed before proof. Deduction is more general. Every proof is a deduction, but not every deduction is a proof. — Aristotle, Prior Analytics
For Aristotle a proof begins with premises that are known to be true and shows by means of chaining of evident steps that its conclusion is a logical consequence of its premises. Thus a proof is a step-by-step deduction whose premises are known to be true. For him, one of the main problems of logic (as opposed to, say, geometry) is to describe in detail the nature of the deductions and to say how the deductions come about.
Thus, at the very beginning of logic we find what has come to be known as the truth-and-consequence conception of proof: a proof is a discourse or extended argument which begins with premises known to be truths and which involves a chain of reasoning showing by evident steps that its conclusion is a consequence of its premises.
The adjectival phrase truth-and-consequence is elliptical for the more informative but awkward ‘established-truth-and-deduced-consequence’.
Nevertheless, we still find otherwise competent logicians seeming to espouse the absurdity that a proposition that is a consequence of truths is proved. (Question to self: Why is this not true? Where does the absurdity arise from? Ans: This is apparently because a consequence if not derived gaplessly, could not be a proof. I think Corcoran is alluding to such consequences here which can be held as consequence of the premises, but without self evident steps. I might need to substantiate this with an example. One good place to make sure this notion is correct is to read Corcoran’s other works on this matter.) This is similar to Quine’s inadvertent statement that “If one statement is held to be true, each statement implied by it must also be held to be true” — which could be improved by changing “implied” to “held to be implied”.
Over and above the premises and conclusion, every proof has a chain-of-reasoning that shows that the (final) conclusion fc follows logically form the premises. An Aristotelian direct proof based on 3 premises: p1, p2, p3, and having a chain-of-reasoning with 3 intermediate conclusions ic1, ic2, ic3, can be pictured as:
p1 p2 p3 ?fc ic1 ic2 ic3 fc QED
Note that in such an Aristotelian proof the final conclusion occurs twice: once as a goal to be achieved and once as it has been inferred. This picture represents only a direct proof. The picture is significantly different for indirect proofs, for reduction-ad-impossible. To represent a simple indirect proof, ~fc (a contradictory opposite of the final conclusion) is added as a new assumption and the X indicates that the last intermediate conclusion ic3 contradicts one of the previous intermediate conclusions or one of the premises.
p1 p2 p3 ?fc ~fc ic1 ic2 ic3 X QED
If we use the word ‘argumentations’ for the genus for which proofs form a species, i.e., for a 3 part system composed of a premise-set, a conclusion to be reached, and a chain-of-reasoning, then the Aristotelian truth-and-consequence proof admits of easy definition in the traditional genus-et-differentia form. In order for an argumentation to be a proof (of its conclusion to a given group of people) it is necessary and sufficient for the premises to be known to be true (by the group) and for its chain-of-reasoning to show (to the group) that its conclusion is a logical consequence of its premises. Every proof has established premises and cogent reasoning. In order for an argumentation to be fallacious (to a given group of people) it is necessary and sufficient for the premises to be not known to be true (by the group) or for its chain-of-reasoning to not show (to the group) that its conclusion is a logical consequence of its premises. Every fallacious “proof” has faulty premises or faulty reasoning.
As suggested above, there is no way to understand Aristotle’s logic without being aware of his rigorous training and deep interest in geometry. The fact that axiomatic presentations of geometry were available to the Academy two generations before Euclid’s has been noted often. Ross points out that “there were already in Aristotle’s time Elements of Geometry”. According to Heath, “The geometrical textbook of the Academy was written by Theudius of Magnesia … [who] must be taken to be the immediate precursor of Euclid, and no doubt Euclid made full use of Theudius … and other available material”.
It would be an exaggeration to suggest that an understanding of Aristotle’s goals and achievements in Prior Analytics would be impossible without attention to his many geometrical examples. Nevertheless, it is fair to criticize the many works on the history of logic which do not mention these examples or which do not mention the axiomatic treatments of geometry available to Aristotle. Even more deserving of criticism are those works on the history of logic, or on logic itself for that matter, which date the origin of the axiomatic method after Aristotle rather than before his time.
Although Tarski does not make the above errors, he still fails to trace the axiomatic method back any farther than Euclid and he mentions Aristotle as the creator of logic without indicating Aristotle’s interests in geometrical proof or in the axiomatic method.
Robin Smith’s description of the Analytics:
From Aristotle’s viewpoint, the Prior Analytics is simply the first part of the Analytics: the second part is the work known to us as the Posterior Analytics. The subject of the latter is proof or demonstration (apodeixis), that is, argumentation which produces scientific understanding (epistēmē). Aristotle makes it clear from the start that this is also the subject of the entire Analytics, and thus of its first part, the Prior. Aristotle conceives of a demonstrative science as a system of demonstrations, which in turn are a type of deduction (sullogismos). Accordingly, the Prior Analytics gives an account of deductions in general and the Posterior discusses the specific character of those deductions which are demonstrations.
Smith’s interpretation echoes that of Alexander, who first explained that Aristotle’s Prior Analytics and Posterior Analytics are about deductions and proofs, respectively, and then adds that the first is called Prior because its subject, deduction, “is by nature” prior to the subject, demonstration.
The Analytics as a whole forms a treatise on scientific knowledge. On Aristotle’s view each item of scientific knowledge is initial, known directly in itself by experience in the broad sense (epagoge sometimes translated ‘induction’), or else it is derivative, deduced ultimately from initial items known in themselves.
The Posterior Analytics deals with the acquisition and deductive organization of scientific knowledge. It is the earliest general treatise on axiomatic method in sciences. The Prior Analytics, on the other hand, develops the underlying logic used in the inference of deductively known scientific propositions from those known in themselves.
Aristotle’s word for a proof or demonstration was apodeixis, from which we get our word ‘apodictic’. He called an ultimate premise of a demonstration an archê apodeixeôs, literally “demonstration beginning”, “beginning of a demonstration”, and less literally, “demonstrative or apodictic beginning”. According to D. Hitchcock (per. comm.), Aristotle seemed to have no special word for the conclusion of a proof per se; he used the same word sumperasma, literally “end”, “conclusion”, for the conclusion of a deduction whether or not it was a proof. Later writers who accepted Aristotle’s insights adopted other terminology for the distinction between the original premises and the conclusion of the demonstrations — some called the former axioms and called the latter theorems (Boole, Tarski); some called the former primary or ultimate propositions, or laws, and the latter secondary (Boole).
As far as can be determined from his published writings, Boole subscribed to the truth-and-consequence conception of proof. In the later 1970s and early 1980s toward the end of his life, Tarski also accepted it (per. comm.), although he does not seem to explicitly endorse it in his published writings. However, he was clear that the truth-and-consequence conception of proof is not implied by the knowledge-through-proof thesis.
On at least two occasions separated by years, he said that he thought Euclid was actually “proving theorems” in some sense but not deducing them from premises and definitions.
Tarski agreed with modern scholars that Euclid “smuggled premises”, i.e., used propositions not among his stated premises and definitions, and he was aware of occasions where Euclid proved something other than what is claimed (Euclid IX.20), thereby appearing to commit the fallacy of “ignoratio elenchi” or wrong-conclusion. But Tarski went on to point out that Euclid never said that his goal was to show that the theorems were logical consequences of his basic propositions (per.comm.). If Euclid accepted the knowledge-through-proof thesis while rejecting the truth-and-consequence conception, he was not the only important figure in the history of logic to do so.
This view of Euclid might seem to conflict with what Tarski wrote in the 1960s about “the science of geometry as it was known to ancient Egyptians and Greeks in its early pre-Euclidean stage”. He wrote of the pre-Euclidean period: “A sentence was accepted as true either because it seemed intuitively evident or else because it was proved on the basis of some intuitively evident sentences, and thus was shown by means of intuitively certain argument to be a consequence of these other sentences”. Thus, Tarski seems to be attributing to pre-Euclidean geometers approximations of both knowledge-though-proof thesis and the truth-and-consequence conception of proof.
But the logic of the Prior Analytics is not designed solely for such demonstrative use. One the contrary, Aristotle subscribes to what may be called the epistemic-neutrality thesis, the thesis that the process of deduction is the same whether the premises are known to be true or whether the premise set contains a mere hypothesis not known to be true and not known to be false, or even if the premises are all known to be false. Aristotle says that whether a person is trying to demonstrate a conclusion from premises known to be true or trying to deduce it from premises merely assumed for purpose of reasoning “it will make no difference as to whether a deduction comes about …”
One point is that scientific knowledge has an initial-plus-derived structure. This is not to say that initially known truths are all obvious to everyone, or even to everyone sufficiently acquainted with the subject matter. Likewise this is not to say that derivations from initially known truths are all obviously cogent to everyone, or even to everyone sufficiently acquainted with the subject matter.
A second point is that the process of deduction is separate from the process of experiential acquisition of knowledge of the initial truths and, moreover, it is the same regardless of the nature of the subject-matter – logic is topic neutral. IN other words, and more generally, methods for determining validity and invalidity of premise-conclusion arguments stand apart from the sciences – some say logic underlies or is under or is foundational for the sciences; others say it transcends or is over or governs the sciences. From an Aristotelian point of view, which troubles some people, a person does not need to know science before learning logic, but a person must have inner knowledge of logic before making much progress in learning science. In the terms used by followers of Aristotle, logic is not a science per se; rather it is an instrument of science, an organon. In that logic stands apart from any science’s subject-matter, it may be considered to be a formal discipline.
A related but third point is that deduction per se produces consequences of whatever it is applied to, deduction makes explicit the implicit content of premise sets; it does not produce new information about the subject-matter of the premises. Deduction per se is merely information processing and not knowledge producing – except in the sense of producing knowledge that a conclusion follows from premises.
In my thinking, this is pretty close to what topology is about; in the sense that it is about information preserving transformations.
This third point, which may be called the non-creativity of deduction, is dramatically illustrated by the contrast between the classical formal conception of proof due largely to Aristotle and the contentual, or cognitivist, conception vigorously articulated by some of Kant’s more independent followers as well as by Frege. To make this contrast it is convenient to use the word deduction as above for the process of coming to know that a given conclusion follows from given premises (without regard to whether the premises are known or not) in contrast with using inference for the process of coming to know that a conclusion is true based on previous knowledge of premises.
The distinction between deduction and inference, often but not always using these very words, has been recognized, even emphasized by most major logicians. The truth of the premises is totally irrelevant to the cogency of a deduction, but there is no such thing as an inference based on false premises, or even on premises not known to be true.
For the classical formalist a proof involves a deduction, a series of deductive steps, which in principle could be grasped and checked by someone who did not even understand much less have knowledge of the premises. In fact, in connection with checking an alleged “proof” to determine whether it is a [genuine] proof, classical formalists want to first determine whether it is even a deduction, and to do this they often recommend bracketing or disinterpreting the sentences expressing the premises, i.e. disregarding their meaning except for the purely formal aspects. For the cognitivist a proof is a series of inferences which are totally inaccessible to a person who did not have full knowledge of the truth of the premises.
Misunderstanding of this third point, which involves the formality of deduction, alternates with understanding of it down through the ages. People who understand it tend to think that it is so obvious that it need not be mentioned. Boole could not have missed this point, but he never makes it. However, a few years after Boole’s 1854 Laws of Thought, Jevons – an English logician who continued the development of Boole’s work – seems very close when he wrote: “The very purpose of syllogism is to deduce a conclusion which will be true when the premises are true. They syllogism enables us to restate in a new form the information … contained in the premises, just as a machine may deliver to us in a new form the material … put into it”
I have to note here that Jevons only says that the conclusion will be true when the premises are true. Note that it doesn’t say anything about the situation when either/both of the premises are false.
For Kazarinoff, a proof is an argument that has convinced and now convinces. It changes according to the standards of the time and place. A mathematical proof is a temporal, communicable phenomenon in the minds of living men.
For Aristotle, once the basic premises are set forth in a proof the fact that they are known to be true is irrelevant to what is done by the thinker thereafter – in the proof itself. Deduction of the conclusion from the premises is simply information processing which would be the same regardless of the cognitive status of the information. In fact, for Aristotle it is irrelevant whether the conclusion is deduced from the premises before the premises are established to be true or whether the premises are established to be true first and then the conclusion is deduced from them. Aristotle’s truth-and-consequence conception of proof could just as accurately be called the consequence-and-truth conception of proof. Moreover, any appeal to the nature of the subject-matter is also irrelevant. In order to deduce a conclusion from premises it is not necessary to be acquainted with the subject-matter of the premises and conclusion of the argument, but only with the logical form of the argument.
A person who accepts the truth-and-consequence conception of proof expects Kant to say that the true method is to logically deduce the proposition from premises that have been established intuitively or experientially. But that is not what Kant says about the first person who discovered the method of proof:
The true method, so he found, was not to inspect what he discerned either in the figure, or in the bare concept of it, and from this, as it were, to read off its properties; but to bring out what was necessarily implied in the concepts that he had himself formed a priori, and had put into the figure in the construction by which he presented it to himself. If he is to know anything with a priori certainty he must not ascribe to the figure anything save what necessarily follows from what he has himself set into it in accordance with his concept.
Kant is saying nothing about starting with premises known to be true, nor about applying information-processing procedures to reveal the consequences implicit in those premises. On the contrary, he is talking about doing intuitive geometrical constructions — something totally irrelevant to Aristotle’s conception of proof. Kant is basing apodictic judgment on processing concepts, not propositions. Kant starts with concepts put into a figure previously constructed; Aristotle starts with propositions previously established. For Kant the diagram is essential; for Aristotle it is irrelevant.
It has been said that Galileo’s greatest achievement was to persuade the world’s scientists that physical reality is mathematical, or at least that science should be pursued mathematically. In his words, ‘The Book of Nature is written in mathematical characters’. In a strikingly similar spirit, Boole (1854, p.12) stated ‘it is certain that [logic’s] ultimate forms and processes are mathematical’. Perhaps Boole’s greatest achievement was to persuade the world’s logicians that logical reality is mathematical, or at least that logic should be pursued mathematically. — John Corcoran 2003
Hilbert-Ackermann Principles of Mathematical Logic says: “The entire later development [of mathematical logic] goes back to Boole.”
Corcoran says decades of historical research only confirm this conclusion about the origin of the continuous development of mathematical logic citing 19th Century Logic between Philosophy and Mathematics (Peckhaus 1999).
If, as Aristotle tells us, we do not understand a thing until we see it growing from its beginning, then those who want to understand logic should study Prior Analytics and those who want to understand mathematical logic should also study Laws of Thought. There are many wonderful things about Laws of Thought besides its historical importance. Of all of the foundational writings concerning mathematical logic, this one is the most accessible.
Contrary to appearances, by the expression ‘mathematical analysis of logic’, Boole did not mean that he was analyzing logic mathematically or using mathematics to analyze logic. Rather his meaning was that he had found logic to be a new form of mathematics, a new form of analysis, and that it was not a form of metaphysics or philosophy as had been thought previously.
Long before Boole there had been “acknowledged forms of Mathematical Analysis” dealing separately with numbers, lengths, areas, volumes, time intervals, weights, and other quantities. But Boole thought of himself as advancing a new non-quantitative form of analysis that dealt with classes. And he somehow took it to be logic. It was this new form of “Mathematical Analysis” that Boole applied “to the expression of the operations of the mind in reasoning”.
Russel says that “The development of mathematical logic dates from Boole’s Laws of Thought (1854).” Although this work begins mathematical logic, it does not begin logical theory. The construction of logical theory began, of course, with Aristotle, whose logical writings were known and admired by Boole. In fact, Boole explicitly accepted Aristotle’s logic as “a collection of scientific truths” and regarded himself as following in Aristotle’s footsteps. He thought that he was supplying a unifying foundation for Aristotle’s logic and at the same time expanding the ranges of propositions and of deductions formally treatable in logic.
Boole thought that Aristotle’s logic was “not a science but a collection of scientific truths, too incomplete to form a system of themselves, and not sufficiently fundamental to serve as the foundation upon which a perfect system may rest”. He was one of many readers of Prior Analytics who failed to discern the intricate and fully developed logical system that Aristotle had devised.
As has been pointed out by Grattan-Guinness, in 1854 Boole was less impressed with Aristotle’s achievement than he was earlier in 1847. In 1847 Aristotle’s logic plays the leading role, but in 1854 it occupies only one chapter of the 15 on logic. Although his esteem for Aristotle’s achievement waned as Boole’s own achievement evolved, Boole never found fault with anything that Aristotle produced in logic, with Aristotle’s positive doctrine.
Philosophical concern with problems of understanding the nature of logical reasoning also predates Aristotle’s time. In a way, concern with understanding the nature of logical reasoning was brought to a climax by Socrates, who challenged people to devise a criterion, or test, for recognizing proofs, a method for determining of a given alleged proof whether it indeed is a proof, i.e., whether it proves to its intended audience that its conclusion is true, or whether, to the contrary, it is fallacious despite any persuasiveness the audience might find it to have (Phaedo 90b-90e). Despite Frege’s impetuous claim, the Socratic challenge has still not been answered. Perhaps the identification of logic as a potential field of study, or as a possible branch of learning, should be taken as the time when humans, having discovered the existence of logical deduction, were able to perceive a difference between objective proof and subjective persuasion. As Gasser puts it: “One of the main objectives of logic is to distinguish between persuasion and proof, and belief and knowledge”.
Boole subscribed to Aristotle’s initial-plus-derivative conception of the structure of each science without reservation. In his own words: “All sciences consist of general truths, but of those truths some only are primary and fundamental, others are secondary and derived.” It is also evident, from the above and many other passages, that he also agreed with Aristotle’s pluralistic conception of the realm of scientific knowledge as composed of many separate sciences. What is not evident from the above quotation, but is nevertheless also true, is that Boole agreed with Aristotle on the fundamental ontological principle that each science had its own domain.
The common view is that Aristotle’s logic conflicts with modern logic whereas Boole’s is in agreement with it.a This view could not be further from the truth. First, as noted above, Boole accepted as valid absolutely every argument accepted as valid in Aristotle’s system. Thus any conflict with modern logic found in Aristotle’s logic would be found in Boole’s to the extent that Boole’s logic is faithful to his own philosophy. Second, as first noted by Smiley (1962), if Aristotle’s logic is correctly translated into modern logic the fit is exact. If categorical sentences are translated into many-sorted symbolic logic according to Smiley’s method or either of the methods given below, an argument with arbitrarily many premises is valid according to Aristotle’s system if and only if its translation is valid according to modern standard many-sorted logic. As Parry showed Corcoran in 1973 (per. comm.), this result can be proved from the combination of Parry’s insights (1965) with Corcoran’s proof of the completeness of Aristotle’s categorical logic (1972).
Quantification of the Predicate and Many-sorted Logic (Parry 1965) Syllogism and Quantification (Smiley 1962)
Aristotelian Logic as Many-Sorted Symbolic Logic Using Sortal Variables: The ranges of the sortal variables are all non-empty as with ordinary one-sorted logic. Each range is assigned independently of all others.
Using Range-Indicators (Common Nouns) with General (Non-Sortal) Variables: Each initial variable occurrence follows an occurrence of a range-indicator or “common noun” that determines the range of the variable in each of its occurrences bound by the quantifier preceding the range-indicator. This is reflected in the practice of Tarski and others of using variables as pronounces having as common nouns as antecedents as in “For every number x, x precedes x + 1”. The word ‘number’ in ‘number x’ determines the range of x in all three occurrences. To each range-indicator a non-empty set is assigned as its “extension”.
A: Every sphere x is a polygon y. ∀Sx∃Py x = y : For every sphere x there exists a polygon y such that x = y.
E: Some sphere x is a polygon y. ∃Sx∃Py x = y: For some sphere x there exists a polygon y such that x = y.
I: No sphere x is a polygon y. ∀Sx∀Py x ≠ y : For every sphere x, for every polygon y, x isn’t y.
O: Some sphere x is not any polygon y. ∃Sx∃Py x = y : For some sphere x, every polygon y is such that x isn’t y.
Many-sorted logic with sortal variables is prominent in Hilbert (Foundations of Geometry, 1899) and merely described in Hilbert and Ackermann (Principles of Mathematical Logic 1938/1950, Introduction to Mathematical Logic, Church 1956). Many-sorted logic with range-indicators and non-sortal variables was pioneered by Anil Gupta in his Logic of Common Nouns (1980) book.
Dana S. Scott 1976 8 pages
Read: 30 May 2021
Logic has long been interested in whether answers to certain questions are computable in principle, since the outcome puts bounds on the possibilities of formalization.
A big question is whether methods of logic have significance in complexity theory.
Programming languages offer an obvious opportunity as their syntactic formalization is advanced; however, the semantical theory can hardly be said to be complete. Though we have many examples, we have still to give wide-ranging mathematical answers to these queries: What is a machine? What is a computable process? How (or how well) does a machine simulate a process? Programs naturally enter in giving descriptions of processes. The definition of the precise meaning of a program then requires us to explain what are the objects of computation (in a way, the statics of the problem) and how they are to be transformed (the dynamics).
So far the theories of automata and of nets, though most interesting for dynamics, have formalized only a portion of the field, and there has been perhaps too much concentration on the finite-state and algebraic aspects. It would seem that the understanding of higher-level program features involves us with infinite objects and forces us to pass through several levels of explanation to go from the conceptual ideas to the final simulation on a real machine. These levels can be made mathematically exact if we can find the right abstractions to represent the necessary structures.
The experience of many independent workers with the method of data types as lattices (or partial orderings) under an information content ordering, and their continuous mappings, has demonstrated the flexibility of this approach in providing definitions and proofs, which are clean and without undue dependence on implementations. Nevertheless much remains to be done in showing how abstract conceptualizations can (or cannot) be actualized before we can say we have a unified theory.
From the 1960s Dana Scott’s work has concentrated on seeing whether the ideas of logic can be used to give a better conceptual understanding of programming languages.
Complementary Definitions of Programming Language Semantics — J. E. Donahue (1976) Theory of Programming Language Semantics — Robin Milne, Christopher Strachey (1976) Data types as lattices — Dana Scott (1976) The Denotational Semantics of Programming Languages — R. D. Tennet (1976) Denotational Semantics — The Scott-Strachey Approach to Programming Language Theory — J. E. Stoy
Category Theory Applied to Computation and Control — Editor: Manes (1976) Lambda Calculus and Computer Science Theory — Editor: Böhm (1975)
Born in California. Started working in early 1950s. Main influence was Alfred Tarski
Learned recursive function theory from Raphael and Julia Robinson
Studied Lambda Calculus of Curry and Church (which apparently literally gave nightmares to Dana Scott at first)
Especially important for his later ideas was the study of Tarski’s semantics and his definition of truth for formalized languages. These concepts are still being hotly debated today in the philosophy of natural language.
Not all problems are solved just by giving denotations to some languages. Languages (like very pure) lambda calculus are well served, but many programming concepts are still not covered.
Graduate work in Princeton in 1958 under the direction of Alonzo Church, who also supervised Michael Rabin’s thesis.
The joint work with Rabin thrower some basic ideas into sharp relief. Scott was trying to give a mathematical definition of a machine. He feels that the finite-state approach is only partially successful and without much in the way of practical implication.
Many physical machines can be modeled as finite-state devices but the finiteness is hardly the most important feature, and the automata point of view is often rather superficial.
Two later developments made automata seem interesting to Scott: The Chomsky hierarchy and the connection with semigroups. From the algebraic point of view Eilenberg, the Euclid of automata theory, in his books has said pretty much the last word. He has avoided abstract category theory. Categories may lead to good things but too early a use can only make things too difficult to understand.
In some ways the Chomsky hierarchy is in the end disappointing. Context-fre languages are very important and everyone has to learn about them, but it is not at all clear to Scott what comes next. There are so many other families of languages, but not much order has come out of the chaos. It was not knowing where to turn, and being displeased with what Scott thought was excessive complexity, that made Scott give up working in automata theory.
Scott tried a certain way to connect automata and programming languages by suggesting a more systematic way of separating the machine from the program. Eilenberg heartily disliked the idea, but Scott was good to see the book by Clark and Cowell, Programs, Machines, and Computation where at the suggestion of Peter Landin, the idea is carried out very nicely.
He says he would like to see a next step that would fall between Manna and Milne-Strachey.
Mathematical Theory of Computation — Zohar Manna (1974)
He thanks Forman Acton for introducing him to the von Neumann machine.
Bob Ashenhurst and Nick Metropolis
Harry Huskey and René de Vogelaere
Dick and Emma Lehmer: The way they get results in number theory by machine.
John McCarthy and Patrick Suppes had much influence on Dana Scott and his views of computing.
Soloman Feferman and Georg Kreisel were the colleagues of Dana Scott.
Richard Platek — Ph. D. student
The academic year 1968/69 was a deep crisis for Dana Scott and still painful for him to think back on it.
Tom Steel was the chairman of IFIP Working Group 2.2 in 1976 (at the time of this talk) called Formal Description of Programming Concepts.
There was a fight and he says fighting brings out the best and worst in people.
He liked the style and ideas of Strachey best and though he think Strachey often overstated the case, what Strachey said convinced Dana Scott that he should learn more.
Jaco de Bakker
There was fervent activity and collaboration with Strachey. Once in Oxford, next up in Princeton.
But Strachey became discouraged over the continuing lack of research funds and help in teaching, and he essentially withdrew himself to write his book with Milne.
Strachey had his attention drawn to the Lambda Calculus by Roger Penrose and had developed a handy style of using this notation for functional abstraction in explaining programming concepts. It was a formal device, however, Dana Scott argued that it had not mathematical basis.
Dana Scott started seeing that computable functions could be defined on a great variety of spaces. The real step was to see that function-spaces were good spaces, and Scott remembers quite clearly that the logician Andrzej Mostowski, who was also visiting Oxford at the time, simply did not believe that the kind of functions Scott defined had a constructive description.
But when Scott saw that they actually did, Scott began to suspect that the possibilities of using function spaces might just be more surprising than we had supposed.
Once the rigidity of logical types that Scott pushed onto Strachey was there, Scott found one of the spaces isomorphic with its own function space, which provides a model of the type-free Lambda Calculus.
But I think types are still there.
Algebra and Logic — edited by J. N. Clossley Reminiscences of logicians reported by J. N. Crossley
Les Fox and Robin Gandy are colleagues of Dana Scott
Scott finds it strange that his Lambda Calculus models were not discovered earlier by someone else; but he is encouraged that new kinds of models with new properties are being discovered, such as the “power domains” of Gordon Plotkin.
A powerdomain construction — Gordon Plotkin (1976)
John Reynolds and Robert Milne have independently introduced a new inductive method proving equivalences, and the interesting work of Robin Milner on LCF and its proof techniques continues at Edinburgh.
The direction of proving things on about models was started off by David Park’s theorem on relating the fixed-point operator and the so-called paradoxical combinator of Lambda Calculus, and it opened up a study of the infinitary, yet computable operators which continues now along many lines.
Another direction of work in Novosibirisk under Yu. L. Ershov which shows quite surprising connections with topological algebra.
Pointed out by Karl H. Hofmann and his group.
Two domains: B, the domain of Boolean values S = B∞, the domain of infinite sequences of Boolean values
B is now equipped with a bottom value. So B = { true, false, undefined }
Partial ordering x < y iff either x = bottom or x = y
We can read <= as saying that the information content of x is contained in the information content of y. The element bottom has therefore, empty information content.
Data types as lattices — Dana Scott
Looking now at S, the domain of sequences, we shall employe a shorthand notation where subscript indicate the coordinates:
x = <x_n> from n = 0 to ∞ for all x in S.
Each term is such that x_n belongs to B because S = B∞.
Technically, a “direct product” of structures is intended, so we define <= on S by
x <= y iff x_n <= y<n, for all n.
A sequence y is better in information than a sequence x iff some of the coordinates of x which were undefined have passed over into being defined when we go from x to y.
Sample iterations of the sequence are:
< undefined, undefined, undefined, undefined … > < true, undefined, undefined, undefined … > < true, false, undefined, undefined … > < true, false, true, undefined, … >
An obvious different between B and S is that B is finite while S has infinitely many elements.
In S, also, certain elements have infinite information content, whereas this is not so in B.
The partial ordering in S can be used to explain abstractly what is meant by finite approximation and limits.
Given any x in S, we can cut it down to a finite element by defining (x ^ m)_n = if(n < m) x_n else undefined
It is easy to see that x ^ m <= x ^ (m + 1) <= m
So x ^ m are build up to a limit; and in fact, that limit is the original x.
We write this as for(let m = 0 to ∞) U(x ^ m)
Where U is the sup or least bound operation in the partially ordered set S. The point is that S has many sups; and whenever we have elements exp(y, <m>) <= exp(y, <m+1>) in S regardless of whether they are finite or not, we can define the limit z where
z = for(let m = 0 to ∞) U exp(y, <m>)
The S here is a topological space and z really is a limit. Thus though S is infinitary, there is a good chance that we can let manipulations fall back on finitely operations and be able to discuss computable operations on S and on more complex domains.
Aside from the sequence and partial-order structure on S, we can define many kinds of algebraic structure. That is why S is a good example. For instance, up to isomorphism the space satisfies
S = S * S
where on the right hand side the usual binary direct product is intended.
Abstractly, the domain S * S consists of all ordered pairs <x, y> with x, y belongs to S, where we define <= on S X S by <x, y> <= <x’, y’> iff x <= x’ and y <= y’
But for all practical purposes there is no harm in identifying <x, y> with a sequence already in S; indeed coordinate wise we can define
<x, y>_n = if(n == 2k) x_k if(n == 2k + 1), y_k
The above criterion for <= between pairs will be verified, and we can say that S has a (bi-unique) pairing function.
The pairing function <., .> on S has many interesting properties. In effect, we have already noted that it is monotonic (intuitively: as you increase the information contents of x and y, you increase the information content of <x, y>.) More importantly, <., . > is continuous in the following precise sense:
<x, y> = for(m = 0 to ∞) <x ^ m, y ^ m>
which means that <. , .> behaves well under taking finite approximations. And this is only one example; the whole theory of monotone and continuous functions is very important to this approach.
Even with the small amount of structure we have put on S, a language suggests itself.
We concentrate on the two isomorphisms satisfied by S; namely S = B * S and S = * S. The first identified S as having to do with (infinite) sequences of Boolean values; while the second reminds us of the above discussion of the pairing function.
We set down a quick BNF definition of a language with two kinds of expressions:
Bool := true | false | head Seq Seq := B* | B Seq | tail Seq | if B then Seq’ else Seq’’ | even Seq | Odd Seq | Merge Seq’ Seq’’
This language has no variables, no declarations, no assignments, only a miniature selection of constant terms. Note that the notation chosen was meant to make the meanings of these expressions obvious.
Thus if Seq denotes a sequence x, then head Seq has got to denote the first term x_0 of the sequence x. As x_0 belongs to B and x belongs to S, we are keeping our types straight.
More precisely, for each expression, we can define its (constant) value . ; so that B in B for Boolean expressions Bool and Seq in Seq for sequential expressions.
Bool* = < Bool , Bool , Bool , Bool , … >
In the same vein
Bool Seq = < Bool , Seq _0, Seq _1 , Seq _2, … >
while we have
tail Seq = < Seq _1, Seq _2, Seq _3, Seq _4, … >
Further along:
even Seq = < Seq _0, Seq _2, Seq _4, Seq _6, … >
merge Seq’ Seq’’ = < Seq’ , Seq’’ >
It should be clear that what we have is really only a selection, because S satisfies many more isomorphisms (e.g. S = S * S * S), and there are many, many more ways of tearing apart and recombining sequences of Boolean values - all in quite computable ways.
The previous treatment leave us on the elementary level of program sachems
The semantics of predicate logic as a programming language — M. H. van Emden and R. A Kowalski (1976)
Mathematical Theory of Computation — Zohar Manna (1974)
What some people call Fixpoint Semantics is only a first chapter. The second chapter already includes procedures that takes procedures as arguments — higher-type procedures — and we are well beyond program schemes. True fixed-point techniques can be applied to these higher-type procedures, but that is not the only thing to say in their favor.
Dana Scott says that he doesn’t like the abbreviated world fixpoint
The semantic structure needed to make this definite is the function space. Scott has tried to stress this from the start in 1969, but many people have not understood Scott well enough.
Suppose D’ and D’’ are two domains of the kind we have been discussing (say, B or B x B or S or something worse). By [D’ -> D’’] let us understand the domain of all monotone and continuous functions f mapping D’ into D’’. This is what is meant by a function space. It is not all that difficult mathematically, but it is not that obvious either that [D’ -> D’’] is again a domain “of the same kind,” though admittedly of a more complicated structure.
< on the function space is defined as: f < g iff f(x) < g(x) for all x in D’
Treating functions as abstract objects is nothing new; what has to be checked is that they are also quite reasonable objects of computation. The relation Box on [D’ -> D’’] is the first step in checking this, and it leads to a well-behaved notion of a finite approximation to a function.
And when that is seen, the way is open to iteration of function spaces; as in [[D’ -> D’’] -> D’’’]. This is not as crazy as it might seem at first, since our theory identifies f(x) as a computable binary function of variable f and variable x. Thus, as an operation, it can be seen as an element of a function space:
[[[D’ -> D’’] * D’] -> D’’]
This is only the start of a theory of these operators (or combinators, as Curry and Church call them).
Let us attempt an infinite iteration of function spaces beginning with S. We define F_0 = S and F_n+1 = [F_n -> S]. Thus F_1 = [S -> S] and F_4 = [[[S -> S] -> S] -> S]
This is all highly constructive because we employ only the continuous functions.
It is fairly clear that there is a natural sense in which this is cumulative. In the first place S is “contained in” [S -> S] as a subspace: identify each x in S with the corresponding constant function in [S -> S]. Clearly by our definitions this in an order-preserving correspondence. Also each f in [S -> S] is (crudely) approximated by a constant, namely f(undefined). This relationship of subspace and approximation between spaces will be denoted by S < [S -> S].
Pushing higher we can say: [S -> S] < [[S -> S] -> S]
but now for a different reason. Once we fix the reason why S < [S -> S], we have to respect the function space structure of the higher F_n. In the special case, suppose f in [S -> S]. We want to inject f into the next space, so call it i(f) in [S -> S] -> S. If g is any element in [S -> S] we are being required to define i(f)(g) in S. Now, since g in [S -> S], we have the original projection backwards j(g) = g(undefined) in S. So, as this is the best approximation to g we can get in S, we are stuck with defining
i(f)(g) = f(j(g))
TODO: I have stopped being able to follow the treatment, so truncating this part, which I will come in and fill if I get sufficient time, interest, and knowledge to do so.
The infinite level of higher type functions is its own function space. As always, this is a consequence of continuity.
What we have done is to sketch why F_∞ the space of functions of infinite type, is a model of the Lambda calculus. The Lambda calculus is a language where every term can be regarded as denoting both an argument (or value) and a function at the same time. The formal details are pretty simple, but the semantical details are what we have been looking at: every element of the space F_∞ can be taken at the same time as being an element of the space [F_∞ -> F_∞]; thus F_∞ provides a model, but it is just one of many.
Without being able to be explicit, a denotational (or mathematical) semantics was outlined for a pure language of procedures (also pairs and all the other stuff described above).
A Leibnizian Approach to Mathematical Relationships: A New Look at Synthetic Judgments in Mathematics
David T. Purser 2009 64 pages Read 13 August 2021
A thesis that examines how arbitrary systems of signification reveal real relationships in possible worlds. It attempts to examine the analytic/synthetic distinction and argues that mathematics is synthetic in nature. A moderate version of mathematical realism called modal relationism is advocated.
The lingua characteristica and calculus ratiocinator projects of Leibniz is examined and the extent to which these ideas influenced the development of philosophical perspectives on the relationship between formal languages and reality is assessed.
Work of Cantor, Gödel, and the paradoxes in mathematics in the early 20th century is considered. The chapter makes Leibnizian connections between Cantor’s diagonal method, Russell’s paradox and Gödel’s Incompleteness theorem.
This chapter assesses whether Gödel realized Leibniz’s vision, in a larger metaphysical context. What do paradoxes tell us about the nature of mathematics and logic? Is there any connection between Leibniz’s thought and these paradoxes? To answer these questions Kantian distinction of arithmetic as synthetic a priori and analytic a priori is discussed. Is arithmetic no more than mere tautology? And if it is, does this imply that mathematics is void of content? Is there any formal system with necessarily true propositions that also contains content? The chapter concludes by examining the distinction between realism and nominalism in the philosophy of mathematics. Leibniz’ distinctions and formulation of formal paradoxes in the early 21th century are explored to shed light on the realism debate.
Leibniz worked his entire life on a universal language, or the lingua characteristic (Universal Characteristic), and on calculus ratiocinator (Logical Calculus).
Universal Characteristic was to reflect the structure of human concepts in a universal way. It would be a language of universal though. In contrast, the Logical Calculus was to provide the method for using the Characteristic in order to adequately represent the reasoning of humans.
Leibniz’ vision for a Universal Characteristic: showing that arbitrary symbols systems make evident real relationships that we could not otherwise see by eliminating the dangers of ambiguity and equivocation.
Logical Calculus: the process of reasoning within an arbitrary symbol system and how his reveals new relationships in the world.
The legacy Leibniz left behind by exploring theory of relations as both mathematically representable and metaphysically real.
Leibniz believed that the Universal Characteristic and Logical Calculus combined would help not only the scientific community make progress in discovering truth but also would help all of humanity by sharpening he minds of all people, not just the elite of society. The need for a universal, scientific language is so that people from all over the world could come and reason together. This allows people to understand and work out problems together with the guarantee of reaching the same conclusions.
The idea of the Universal Characteristic is that humans, not just Leibniz, could produce a universal language that would bring out all the logical connections between the different components of language.
Donald Rutherford (1995) says: The universal characteristic would enable us to construct linguistic characters which are transparent representations of intelligible thoughts.
A formal language that explicitly brings out the logical relationships between propositions would have advantages over natural languages such as avoiding equivocations and ambiguity. The language is also more advantageous because it allows the implicitly logical relationships to become evident to our senses.
The clearer and more precise the symbol of signification the easier the complex relationships between objects or concepts becomes to comprehend.
The Universal Characteristic is composed of two different pars. The first component is the reduction of all concepts to their simplest forms. The second component of the Universal Characteristic is the arbitrary nature of the signs that stand for all of the concepts.
Leibniz believed that all concepts are reducible to simple terms. Deriving the simple terms for every concept is essential to the formulation of the Characteristic.
The alphabet Leibniz conceives of involves reducing all of our concepts to not only simple terms but in reducing our concepts to numbers. Every letter in this formal alphabet will correspond to a specific number. Here we seen an anticipation of, if not a forerunner of Gödel numbering.
Numbers are clear and distinct and therefore numbers allow us to avoid ambiguity/equivocation. As per the author, this goal to reduce all concepts to the simplest terms appears to be a utopian dream that is unachievable.
Universal Characteristic provides a useful way to situate simple terms in an analyzable language.
An analyzable language is desirable for 2 reasons: 1/ It allows for rigor in our language and will allow us to see exactly where inconsistencies appear in our moral, metaphysical and scientific knowledge. 2/ An analyzable language allows us to see the strengths and weaknesses of competing hypotheses more clearly, or for the first time. It might be the case that neither of our hypotheses are perfect, but the analyzable language allows us to see exactly where the faults is in our reasoning, and what steps could correct he fault in order to provide a stronger hypothesis.
Signs are necessary in this alphabet because of the role of signs in all of our language and not just in technical discourse.
Leibniz argues that signs are necessary in Meditations on Knowledge, Truth and Ideas (1684). Leibniz argues that we use signs in all of our thinking. He explains that when solving a mathematical problem we do not think of the entire problem at once, but that we use signs to represent the problem to make things easier for us.
What kinds of signs are most effective? The early work of Leibniz argues that the signs that have the properties we want are numerals. The reason that numerals are useful is because of the accuracy and ease with which they are handled.
Leibniz argues that using numbers, as our arbitrary pasigraphic symbols, allows one to see the certainty of the proofs easier than using any other form of language.
Leibniz realizes that the arbitrary signs which we choose do not matter in the end. The choice of signs does not matter because the important aspect of this language is the relationships between concepts which remains the same no matter what the signs are. Therefore, if we were to change the signs, and do this consistently, it would not change the meaning of our calculations. This implies that it is not the concepts or objects in and of themselves that are important but how they relate to one another.
Arbitrary symbols have the potential to tell us new things about the world. Even though the symbols are arbitrary, this does not mean that the relationships are arbitrary.
In order to make the Universal Characteristic useful there muts be a way to manipulate the symbols and deductively arrive at new theorems.
The universal characteristic provides the alphabet and the logical calculus is the rules of the syntax. The rules of syntax is not only for the manipulation of arbitrary symbols but also for the understanding of the relationship between the symbols and the world.
The Logical Calculus will provide us with a quick way in determining the truth of an argument. It might not always be in our power to find the truth, but given a statement there would be a simple procedure to see if the argument is correct or not. And if the argument is flawed there will be an easy procedure to see where the argument fails.
Leibniz believed that once the Universal Characteristic was created, one would be able to construct numbers that are consistent with every simple concept. The numbers would provide the logician with the ability to calculate the concepts in order to demonstrate all of the rules of logic.
If one calculates according to the rules of the Logical Calculus then one will be able to recognize formal truths. By analyzing form alone, one avoids ambiguity and equivocation.
The Logical Calculus is based on the idea that all truths are derivable from deductive proofs. He states in his dissertation that “Every true proposition can be proved”.
In the paper Necessary and Contingent Truths (1686), Leibniz argues that there are two types of truth. There are necessary and contingent truths. The necessary truths are those propositions whose opposite leads to a contradiction. Leibniz argues that in necessary truths the predicate is contained in the subject. These are commonly called analytic truths. Contingent truths are similar in that the predicate is contained in the subject but one can never demonstrate that this ist he case because one can analyze the terms indefinitely. Leibniz states that, “In such cases it is only God, who comprehends the infinite at once, who can see how the one is in the other, and can understand a prior the perfect reason for contingency; in creatures this is supplied a posteriori, by experience”. For God, contingent truths are demonstrable through a deductive argument, but for humans it is not possible because of the limits of our reason. We would have to have an infinite number of steps in our syllogism to prove deductively a contingent truth.
Leibniz argues this same idea in his logical papers. Leibniz makes it clear that when he says the ‘truths are provable’ he is referring to necessary truths, truths which are necessary in all possible worlds, and not for contingent truths.
In his dissertation, Leibniz is careful to delineate the difference between truths that has its basis in existence, not in essence, and which are true as if by chance, i.e. by the will of God (contingent truths) and those in its essence, which are eternal and which exist not by the will of God, but by their own nature (necessary truths). He says that for contingent propositions, there is no demonstration, but only induction; except that sometimes an observation can be demonstrated through an observation by the mediation of a theorem.
Leibniz realizes that there are certain propositions that the Logical Calculus will never be able to solve because of the difficulty that one has in finding tautological propositions. Someone could search for an infinite amount of time and still never come to a conclusion for certain contingent propositions. Leibniz does not lament the fact that there are certain undecidable truths. Instead he argues, “But we can no more give the full reason for contingent things than we can constantly follow asymptotes and run through infinite progressions of numbers”. He does not appear to be disturbed by this limit of the Logical Calculus but is confident that this limit is only a limit of human knowledge. The totality of the real world, in all its infinite complexity, may elude mortals no matter how well-chose the symbol systems are. However, better systems empower us to see more of the real world than we could without them.
Leibniz desired to have a language that reduced all propositions to their simplest terms. This language Leibniz called the Universal Characteristic. He thought that one would be able to turn the simple terms into numbers and perform calculations on the numbers using the grammar of the language. Using this process, Leibniz thought that all true propositions could be proved.
Jean Van Heijenoort points out that Boole’s system accomplishes only the Logical Calculus aspect of Leibniz’s dream. It was Frege who would try to accomplish the Universal Characteristic aspect of Leibniz’s vision.
Gödel’s thinking was highly influenced by Leibniz. Gödel numbering as a prime example of how a powerful system of signification can show us new things about the world by showing relationship inherent to arithmetic never before seen.
Leibniz thought that all relations were reducible to arithmetical equations. If you take any proposition, then using the rules of arithmetic the truth of the proposition is derivable by means of arithmetical steps. Notice that truth is derivable from the proposition, not just the validity of the argument.
The author contends that instead certain logical systems can determine the necessary relationships, not the truth, of propositions by means of arithmetic. It is commonly thought that the objects or concepts are the important aspects of our thinking. Instead, the author suggests that the concepts in and of themselves are not important. The necessary relationships that exist between concepts or objects are the important aspect of our thought.
Gödel showed that all axiom systems could be turned into arithmetical functions. This idea of Leibniz, which Gödel understood, enables us to see how relations can, and do submit to the same rigor as mathematics.
Leibniz’s idea of a Logical Calculus is important because it points out the isomorphism between the way the world is and the way we think about the world.
Thought: The author asserts that Leibniz was a catalyst for the formation of Boolean logic and Predicate Logic, but doesn’t point out exactly the places where this follows. To my knowledge, Boole wasn’t aware of Leibniz’s work at the time of writing The Mathematical Analysis of Logic. There could be influence via the embedded milieu and imbibed ideas in it, but the author isn’t explicit in pointing these out.
Aristotelian syllogisms studied categories and the relationships between categories, but were not powerful enough to take into consideration isolated propositions. Boolean logic took a step in the right direction by providing algebraic notation and symbols but could only express entire propositions with an isolated symbol. With Frege, formal logic was now capable of accomplishing things that at one point it could not even dream of accomplishing, such as explicitly representing the complexity of the kinds of relationships between sentences, predicates, relationships between relationships and properties of relationships.
After the advent of this representational device, Philosophers no longer solve the problems of metaphysics in simplistic terms e.g. objects, their properties and relations. Instead, relations define the objects and properties become 1-place relations. For example, the successor relationship defines objects by their relationship to other objects.
Cantor’s big idea is that not all infinite sets have the same measure. Some infinite sets are larger than others. Cantor used an innovative method of proof to show his results.
The way by which Cantor showed that there are infinite number of different size infinite sets is using a method called diagonal method.
If proofs are no more than formulas, then assigning the natural numbers seems like a justifiable move. Gödel recognizes that all signs are ultimately arbitrary but that well-chosen signs have a greater capacity to show us relationships that are inherent to the world in which we have never seen, by avoiding the ambiguity or equivocations within another language.
Essentially what Gödel did was what Leibniz suggested be done in the development of logic. Leibniz suggested that if all propositions could be represented by numerals then one could use arithmetic to determine whether the proposition was true or not.
Another benefit of using the Gödel numbering is that it makes a definite decision procedure for all systems possible.
Author uses Gödel’s proof to assert that mathematics is not a purely deductive science in the sense that the logicist movement thought. Instead mathematics is more like a scientific study in which new things are discoverable and new methods are capable of producing new truths. If mathematics is like science in this way then Gödel’s proof might be pointing us toward mathematical realism. Discoverable truth implies that there exists something that is discoverable. Alternatively, nominalism would argue that mathematics is purely a formal game of symbol manipulation. Nominalists are correct to point out the arbitrary and conventional nature of our symbols. However, although the symbols are arbitrary, it does not follow that the relationships between them are arbitrary.
Mathematics is capable of discovering new content and is not reducible to axiom system.
The analytic/synthetic distinction as meaningless when considering Leibniz’s distinction between the lingua characteristica and the calculus ratiocinator.
Kant argued that all mathematical judgments (arithmetical and geometrical) were synthetic a priori. He argues that at first glance, a sentence like, 7 + 5 = 12 is an analytical statement. But nothing but for the union of two numbers into one is the concept here and in this no thought is being taken as to what that single number may be. According ot Kant, it is our intuition that helps us go outside of the concepts 7 and 5 to arrive at the number 12. What makes arithmetical statements synthetic is the way in which our intuition recognizes the relationship between the two numbers. The union of the two numbers into one takes place in addition, according to Kant. Thus, addition is not concerned with the objects, in and of themselves, but is instead concerned with the relationship between the objects.
Another example on considering large number calculations on the basis of relations among concepts which has to be justified on intuitive and synthetic grounds is mentioned. This is used by the author to posit that mathematical relations are considered the synthetic aspect of mathematics.
Also, the reason mathematical judgments are a priori for Kant is self-evident. It is because they cannot be empirical, but they carry with them necessity, which cannot be derived from experience.
All necessary truths, like mathematical judgments, are a priori. Kant’s view is that mathematical relations are both necessary and universal, but dependent on intuition.
Logic, for Kant, is not the same as mathematics. While mathematical judgments are synthetic in nature, logical judgments are analytic. For Kant, logic teaches us nothing regarding the content of knowledge as it is only concerned with abstract relationships. In the Kantian framework, the objects themselves take priority over the relationships between objects and are our source of synthetic insights.
The problem with Kant’s distinction between analytic and synthetic judgments is that Kant considers our logical reasoning to concern objects primarily, while our mathematical reasoning concerns relationships of objects. For Kant logic cannot teach us anything because it cannot tell us anything new about objects. This conclusion, as per the author, does not necessarily follow. Instead, logic does tell us how objects relate with each other because logical truths are isomorphic to mathematical truths. Objects do not have to be our sole source of knowledge in the world. In this way, logical reasoning, by means of an innovative symbol system, can reveal new relationships in the world that we could never have seen before. Once we see logic and mathematics as both primarily with relationships between objects and/or relations then both disciplines can be seen as synthetic in nature.
Frege agreed and disagreed with Kant on the synthetic nature of mathematics. Frege saw geometrical judgments as synthetic but arithmetical judgments as analytic. Frege argues that numbers have meanings but that they are not separate objects or a property of any outward things. Frege is worried that this idea might undermine the content of mathematical statements. Just because we cannot imagine what a number might look like, or precisely what we mean when we say the number 2, it does not follow that the word is meaningless. Frege argues that in the same way that having a mental picture of objects does not mean that our mental pictures are somewhere. We may have an idea of what a number is, but this does not mean that numbers actually exist in some Platonic heaven.
Frege argues later that mathematics is both analytic and synthetic. On the one hand, geometrical judgments are synthetic because they can reveal true things about the world. One the other hand, arithmetical judgments are analytic because they can be proved by pure deduction. He says that mathematical inference expand our knowledge about the world and are thus synthetic, but that they are proved deductively and thus analytic.
Frege’s logicism rests on the assumption that logic and the appeal to logical laws is purely analytic. Arithmetic can be proved deductively, like logical laws, because logical statements are isomorphic to arithmetical statements. But just because mathematics and logic can be proved deductively does not mean that their judgments are analytic. The relationships between the logical objects could be real relationships that exist. They do not have to exist in a Platonic universe somewhere, just like mathematical objects do not have to exist in a Platonic universe. Instead, these relationships exist independent of what material or immaterial objects may exist and have meaning.
Distinction between Russell’s brand of logicism and the Vienna Circle’s is not important for the scope fo this chapter.
The Vienna Circle did not think that any mathematical or logical judgments were synthetic. Every mathematical statement was a tautology and void of any content. Carnap argues that since all arguments of logic are tautologies, it follows that, “all the sentences of mathematics are tautologies”. This is a shift from Frege as not even geometrical judgments classify as synthetic judgments.
Hans Hahn sees a difficulty ith this view. It is that how can empiricism account for the real validity of logical and mathematical statements? Hahn argues that logic and mathematics are both composed of no more than tautologies. Therefore, Hahn is in total agreement with Carnap in this respect. This presents a problem for Hahn. Hahn wants to know what exactly the purpose of logic or mathematics is if it is purely analytic. It is his belief that tautological statements are important because we are not omniscient. If we were omniscient then we would know all tautological statements. Analytic judgments are thus useful because of the limited nature of humans.
Poincaré argues against the Vienna Circle view that mathematics is not wholly tautological. Poincaré questions if all the volumes written on mathematics are but indirect ways of enunciating A is A. This according to the author is the right question to ask. Even if mathematical statements are tautologies, because different tautologies express different relationships, they have value. The statement A = A and A or not A even though they express the same truth value express different relationships.
Quine argues in “Two Dogmas of Empiricism” that the notion of analyticity is circular. One of the problems with analyticity is that analyticity assumes a necessary connection between two objects. Quine does not think that the adverb ‘necessarily’ can account for analyticity. To suppose that it does is to suppose that we have already made satisfactory sense of ‘analytic’. In the essay, Quine shows that all of our notion of synonymy relies on the notion of analyticity. In this awy, the distinction between analytic and synthetic judgments is shown to be a false dichotomy.
As per the author, Quine is right in pointing out that there is a false dichotomy between analytic/synthetic judgments. He says that the distinction is a “metaphysical article of faith”. Instead of holding to this artifice of faith, Quine proposes that all of our theories are revisable and are in need of reevaluation.
The analytic/synthetic distinction imposes a rigid divide between form and content. Kant saw logic as pure form, and thus analytic; whereas, mathematical judgments, being full of content, are synthetic. The distinction between form and content renders meaningless Leibniz’s distinction between the universal characteristic and the calculus ratiocinator.
An aspect of Leibniz’s project is that there is an isomorphism from a language into mathematics. Gödel numbering shows that this indeed is the case. One can take a language, and translate the components into numerals and manipulate the symbols through the rules of arithmetic. In this sense, the content of a proposition is not important. Instead, in this isomorphic relationship, the form is important because the form shows the inherent relationships that exist between arbitrary objects.
Abruptly, without much build up, the author claims that the distinction between form and content is not a real distinction. His idea is that form contributes to the content of any proposition. But I felt that there is no particular delineation or a mapping done to precise ideas being done and clarified before making this claim. By saying that form contributes to content, he says that form is not isolated from content and that content can be isolated from the form. But a few sentences before he was saying that the manipulation of proposition is formal. I think this confusion could have been eliminated if the idea was somehow made mathematically tractable. There seems to be ideas in measure theory going by the name of content. So in a sense I think this might be mappable to quantity (content) vs. quality (form) distinction. So in this sense, logic is topological and analytical study of measures or spans(?) of the concepts and the particular way in which they measure the space being addressed could be made a setting where this sort of vague talk about form and content is discussed. Without this, I think we are left to point out to certain examples which confound both of these without clearly separating the ideas immanent in this space and how exactly the one contributes to the other and forms a symbiotic circle.
The author then goes on to say that all statements, including tautologies, are content-rich because form contributes to content. In the sam way that the innovative system of Gödel numbering was able to show that arithmetic is necessarily inconsistent/incomplete, a new system could be invented that opened our eyes to see new relationships in the world. Leibniz’s project is not a utopian dream of seeing every theorem proved, but instead shows us that the world of ideas, including the world of mathematics, is filled with content. The content produced by mathematics is dependent on different axiom systems. Different axiom systems produced different content. Mathematics studies all the different relationships in possible worlds and reveals necessary relationships for the instantiation of the world in which we live.
Intuitionism and Formalism are said to be two branches of nominalism. Both of these branches see mathematical statements as invented by humans, and thus not real.
The formalisms see mathematics as a play of insignificant notations. The formalist correctly recognizes the arbitrary nature of mathematical symbols.
The author asserts that if mathematics is a game of symbol manipulation, then mathematics could not consistently provide an adequate base for scientific discoveries. What the symbol-sequences of axioms signify makes a difference. Axiom choice, like a choice of signs themselves, is never totally arbitrary.
For the intuitionist, in Michael Dummet’s thinking, the grasp of the meaning of a mathematical statement consists in our ability to recognize, for any mathematical construction, whether or not it constitutes a proof of the statement. For an assertion of such a statement is to be construed as a claim that a proof of it exists or can be constructed, not as a claim that it is true.
Micheal Dummet: The Seas of Language (1993)
Kurt Gödel in Russell’s Mathematical Logic argues that the assumption of mathematical objects is just as legitimate as assuming physical bodies. In the same way that physical laws require physical bodies, mathematical laws require mathematical “bodies” or abstract objects. Mathematical intuition as providing the evidence for mathematical objects.
Mark Steiner calls his realism a more modest version. This is to argue the existence of mathematical objects as guaranteed by their indispensability to science, by our inability to say what we want to say about the world without quantifying over them.
For steiner, natural numbers are objects in the same sense that molecules are objects. Steiner believes that since mathematics studies the natural numbers, the existence of numbers is just as certain as the existence of physical objects.
Purser finds two criticisms to Steiner’s views: 1/ There are other numbers than natural numbers which are indispensable for science. 2/ Steiner’s claim that the subject of mathematics is the number. Applied mathematics moves away from this and studies the relationships that exist between numbers. For Purser, the subject of mathematics is not the numbers themselves, but the relationships between numbers.
Steiner is said to be correct by arguing that the indispensability of mathematics is an argument for mathematical content but the content of mathematics is not solely numbers. The numbers are just arbitrary tags while the relationships are not arbitrary. It is the relationships that exist between numbers that makes mathematical judgments indispensable for science.
Stewart Shapiro in his 1989 work, “Logic, Ontology, Mathematical Practice” adopts a structuralist approach to mathematical realism. Shapiro defines a ‘structure’ as “the abstract form of a system, which focuses on the interrelations among the objects”.
The problem David Purser finds with this is that structuralism relies on another structure for its foundation, namely the structure of a particular logic. Shapiro is said to have attempted to clarify this problem. He says, “There is thus a distinction between the logic internal to a structure - the logic needed to develop insights about its objects and relations - and the logic used to study how it relates to other structures”. There are two problems with this answer. First, structuralism, in this view, would not provide the subject matter of mathematics. Instead, the logical system that one adopts provides the subject matter of mathematics and then the structure are built up from there. Secondly, Shapiro makes a distinction between structures and relations. Shapiro indicates that structures relate to other structures. This is because in structuralism, arithmetic is a study of the natural number structure. Shapiro says, “A natural number is not construed as an individual object, on the contrary, a natural number is a place in the natural number structure”. It is here that Shapiro makes the same mistake that Gödel and Steiner make, by putting priority on mathematical objects, whether a number or a structure. At first it seems that structuralism is similar to the relational model of mathematics that Leibniz provided a foundation for, but upon further inspection structuralism takes a path similar to traditional Platonism.
For Shapiro, the natural numbers are not the subject of mathematics, but the structure of natural numbers. The difference being that the number 2 does not exist, but that the number 2 occupies a specific place inside o the structure of the natural numbers. Mathematical structure are then no more than placeholders for abstract objects. According to structuralism, addition is the relationship between two different places in the natural number structure. Notice that the subject of mathematics is no longer the structure qua structure, but the relationship of places within a structure. In other words, mathematics studies how places within a relational structure interact with one another.
Modal relationalism is constructed from the findings of the lingua characteristica and the calculus ratiocinator of Leibniz. In examining these two thoughts in Leibniz, we see that mathematics is about relationships that necessarily exist in the world and how innovative systems of signification reveal new interesting relationships that we could not see before.
Leibniz claimed that all of our signs are arbitrary tags and thus it does not matter if our signs are numbers or places within the structure of the natural numbers, because the relations will stay the same, no matter what the object. The nominalists are correct in invoking the arbitrary nature of the signs but the realist are correct in assuming that mathematics is more than just a convention.
The lingua characteristica and calculus ratiocinator of Leibniz show us that mathematical relationships may be real, universal and necessary - while the symbolic or representational means by which we recognize these relationships are arbitrary or conventional, yet heuristically powerful.
Modal relationism states that mathematics is the study, not of numbers or structures (even though these might be important aspects of mathematics), but of the relationships between objects in all possible worlds. These relationships do actually exist, but not in some abstract platonic sense. We experience instantiations of these relationships in our world all the time. We see two apples, and then someone takes one and there is only one left. This is a real relationship that is represented by the arbitrary mathematical statement 2 - 1 = 1.
This version of realism also appeases Shapiro’s desire to leave open the possibility of non-classical logics. Modal relationism studies mathematical relations in all possible worlds, which means that the relationships exhibited by non-classical logical systems are relations in that possible world, which might be our world. Any logical system produces new and interesting relationships that could exist in a possible world. The author intuits that if this model of realism is developed further, one could yet articulate universal relationships that hold true in all mathematical theories, not despite Cantor and Gödel’s findings, but because of them.
In conclusion, the analytic/synthetic judgments is a false dilemma. Every statement, even tautologies, express a relationship between possible thing.s Mathematical language is arbitrary but this does not mean that mathematical theorems are mere conventions. Instead mathematical practice opens our eyes ot see new relationships in the world that truly exist, including the relationships that might obtain between possible worlds governed by different axioms. Symbolic language can make evident relationships in our world in the same way that the microscope makes it possible for our eyes to see cellular life.
Richard Zach (2019) 15 pages Read 13 August 2021
The completeness theorems of Gödel is thought to be significant because it establishes, in a mathematically rigorous way, the equivalence between syntactic and semantic definitions of logical equivalence. The incompleteness theorem, on the other hand, is significant because it shows the inequivalence of syntactic and semantic definitions of mathematical truth.
Löwenheim-Skolem theorem is considered philosophically significant because of the use Putnam put it to in his model-theoretic argument in “Models and Reality” (1980).
The Curry-Howard isomorphism in brief is that to every derivation in natural deduction there corresponds a term in a lambda calculus, such that transformation of the derivation into a normal form corresponds to evaluating the corresponding lambda term.
A mathematical result can be significant for a number of reasons. Some of them are:
1/ It elucidates a concept by relating it to others. Example: completeness theorem: it elucidates semantic and proof-theoretic definitions of consequence by showing them to be equivalent (in the case of first-order logic).
2/ It is fruitful in proving other results; it provides methods used in further proofs. Example: compactness theorem: it allows us to show that sets of sentences are consistent (and hence satisfiable) by showing that every finite subset is consistent (or satisfiable).
3/ The breadth of fields for which it is significant, either by elucidating notions, or by providing proof methods, or by paving the way for “practical” applications. Author adds that the line between practical and theoretical application is blurry. By practical application the author chooses to designate a method for finding answers to specific questions or solving particular problems. Inferences from databases, or finite models for formal specifications of circuits can be seen as specific questions that can be solved with proof and model-building methods from mathematical logic.
Soundness, completeness, and compactness results for various logical systems are easily seen to be significant for practical applications. Proof-theoretic results such as cut-elimination and consistency proofs are more generally harder to certify as significant.
Normalization of natural deduction plays an important role in the formulation of proof-theoretic semantics.
Consistency proofs are significant because in the absence of a semantics for a logical formalism, a consistency proof (e.g., a cut elimination result) establishes a kind of safety for the formalism. These results paved the way for the development of formalisms that were amenable to software implementation, i.e., automated theorem proving. Proof search is only feasible if the search space can be sufficiently restricted, and cut-elimination guarantees this. If the cut rule were not eliminable, proof search using analytic calculi such as the sequent calculus would not be feasible - and cut elimination proofs establish this even in the absence of a proof of cut-free completeness.
Strengthenings of consistency proofs also have theoretical significance in mathematical logic. The kind of results arising out of the work of consistency proofs which show that there are procedures that transform proofs in one system into proofs in another, weaker system (at least for certain classes of theorems). These results provide proof theoretic reductions of one system to another (a theoretically significant result inside mathematical logic), provide the basis for what Feferman in his 1992 paper “What Rests on What? The Proof-Theoretic Analysis of Mathematics”, has called foundational reductions (a philosophical payoff)., but also sometimes provides methods for extracting bounds from proofs of existential theorems in various systems of arithmetic or analysis (a mathematical payoff). They also measure (and hence elucidate) the strength of axiom and proof systems in more fine-grained ways that simple consistency strength, as when the proof-theoretic reduction shows a speed-up of one system over another.
Curry in his 1934 work “Functionality in Combinatory Logic” observed a surprising but possibly merely coincidental similarity between some axioms of intuitionistic and combinatory logic. Following Howard (originally circulated in 1969) “The Formulae-As-Types Notion of Construction” and John Reynolds’ “Towards a Theory of Type Structure” (1974), it became clear that the isomorphism applied in a wider variety of cases, and it took on both theoretical and philosophical significance. Its theoretical significance lies in the fact that it can be used to prove strong normalization of natural deduction, i.e., the result that normal derivations do not just exist but that they are unique. Its philosophical significance arose originally out of the claim that the lambda term assigned to a derivation can be taken to be the “computation content” of the derivation. There needs to be some work here to clarify the notions of computation and content here.
The Curry-Howard isomorphism is a correspondence between proofs in natural deduction systems and terms in lambda calculi. The correspondence is explained much more easily if natural deduction is formulated not as it was originally by Gentzen 1934 and Prawits 1965 as inferring formulas from formulas, but as proceeding from sequents to sequents.
In classical natural deduction, initial formulas in a proof are assumptions, some of which may be discharged by certain inference rules. A proof is thought of as establishing that the end-formula follows from the set of assumptions that remain undischarged or “open”.
Derivations in natural deduction normalize, i.e., there is always a sequence of reduction steps which transforms a derivation into a derivation in normal form. A derivation is in normal form if no introduction rule for a connective is immediately followed by an elimination rule for the same connective. This result plays a similar role for natural deduction as the cut-elimination theorem plays for the sequent calculus. In particular, it establishes the subformula property for natural deduction derivations. As noted above, the subformula property is essential for the practical implementation of proof search algorithms, since it limits the search space and so eliminates one source of infeasibility in actually carrying out the search for a derivation.
Normalization is carried out by removing “detours” - application of introduction rules immediately followed by elimination rules - one by one.
The Curry-Howard isomorphism is a correspondence between derivation in natural deduction and terms in a typed lambda calculus. In a term calculus; terms are built up from variables. If t is a term, so is λx -> t, called a lambda abstract. Intuitively, it represents a function (a program) that takes x as argument and returns a value specified by the term t (in which x occurs free). In λx -> t, x is bound. So terms can represent functions; applying a function to an argument is simply represented by (t s), where s is another term representing the argument to the function represented by t.
The lambda calculus is a very simple programming language, in which terms are programs. Execution of a program for an input is the conversion of terms to one that cannot be further evaluated. Such terms are said to be in normal form; they represent outcomes of computations.
Redexes are the terms of the lambda calculus to which reduction can be applied.
In the untyped lambda calculus, it is allowed to apply terms to terms to which they intuitively shouldn’t be applied. For example, if you have projection operators:
proj1(<t, s>) = t proj2(<t, s>) = s
they expect a pair to work, but in the untyped lambda calculus, you can proceed to apply it to arbitrary shapes of lambda terms.
In the typed lambda calculus, the syntax prohibits this. Now every variable comes with a type and a variable can be made to take only values of a certain type. One can think of types as objects of a certain sort (e.g., truth values or natural numbers) but there are also function types (e.g., functions from numbers to truth values). The type A -> B are the functions with arguments of type A and values of type B.
For a program that reverses the terms
λx : A * B -> <proj2(x), proj1(x)> : B * A
This disallows the types of arguments to a function being passed that don’t match. To do this we give formation rules for terms that take the types of variables and subterms into account.
The first part of the Curry-Howard isomorphism consists in the observation that the right-hand side of the type judgments in the rules of term formation for the typed lambda calculus are exactly the introduction and elimination rules of natural deduction.
When considered as term formation and type inference rules, the elimination rule for implication for instance, tells us that if s is a term of type A -> B and t is a term of type A, then (s t) is a term of type B. However, these same rules also allow us to systematically assign terms to sequents in a natural deduction derivation (once variables are assigned to the assumptions).
If we focus not on the term side of the type judgments but on the type (formula) side, we can read the inference rules another way. For instance, in the case of elimination rule for implication, they say that if s has been assigned to the premise A -> B, and t to the premise A, then we should assign (s t) to the conclusion B. In this way, we get that for every derivation in natural deduction we can assign terms from the typed lambda calculus to each sequent (or rather, the formula on the right of the sequent).
The second part of the Curry-Howard isomorphism extends this observation. Applying the normalization procedure to derivations in natural deduction corresponds to evaluation (reduction) of the corresponding terms. In this case where we remove a an introduction/elimination detour of implication, the term assigned to the conclusion is of the form (λx -> t)s and the term assigned to the conclusion of the derivation after applying the normalization step is t[s/x].
Note in particular that a derivation in natural deduction is normal (contains no detours) if and only if the term assigned to it is in normal form: any I/E implication detour would correspond to a redex of the form (λx : A -> t)s and any I/E and detour would correspond to a redex of the form proj_i<s, t>.
In its logical form, the Curry-Howard isomorphism consists of the following facts:
- Natural deduction proofs have associated proof terms
- Normalization corresponds to reduction of the corresponding proof terms.
Curry-Howard isomorphism is theoretically important for one main reason: it allows us to prove what’s called strong normalization. It is relatively easy to prove that there always is a sequence of normalization steps that results in a derivation in normal form. Strong normalization is the claim that any sequence of reduction steps a) terminates and b) results in the same normal form. Via the Curry-Howard correspondence, this statement about derivations and normalizations is a consequence of a corresponding result about lambda calculus and evaluation of typed lambda terms: any sequence of evaluation steps a) terminates in a term in normal form (a value) and b) all possible consequences of evaluation steps result in the same value.
Think there is a mistake in here that Strongly normalizing which guarantees that every sequence of rewrites eventually terminates is confused with Strongly normalizing + Confluence property. Even having weak normalization + confluence is not the same as strongly normalizing.
The Curry-Howard isomorphism, in its computational version, is the basis for a very important body of work developed over the last 30 years, in the area of theorem proving and programming language theory. The computational version results from considering the term (program) side of the isomorphism as primary:
- Well-formed lambda terms have associated type derivations
- Evaluation of terms corresponds to normalization of the corresponding type derivations
The Curry-Howard isomorphism establishes that well-formed terms can always be type checked by a derivation in normal form. Since derivations in normal form have the subformula property, searching for a derivation that type checks a given program can (often) be done effectively.
A programming language is called type safe if it prevents programmers from writing programs that result in type errors. A type error occurs if a program of type A -> B, say, is applied to an argument which is not of type A, or when its evaluation for an argument of type A results in something that is not of type B. The Curry-Howard isomorphism, and properties like it for actual programming languages, guarantees type safety. This has tremendous theoretical and practical importance: programs in type-safe languages cannot hang: there is always a way to continue the execution until a value is arrived at. The Curry-Howard isomorphism has this consequence because it implies two things: If a term is not already a value (i.e., it is not in normal form), the evaluation can continue because it contains a redex that can be reduced. This property is called “progress”. But more importantly - and here the Curry-Howard isomorphism comes in - when a term is reduced, its type stays the same (and there is a corresponding natural deduction derivation which verifies this). This property is called “type preservation”. Together, these two properties establish that if t is a term (program) of type A -> B, and s is a term (argument) of type A, (t s) will always evaluate to a normal term (value) of type B. The strong normalization property for the typed lambda calculus establishes that evaluation always terminates and that any order of evaluation steps results in the same value. The Curry-Howard isomorphism, via its consequence of type preservation, establishes that each intermediate step and the final result, will be a term of type B.
The ability to type check programs, and the property of type safety, are kinds of completeness and soundness properties for programs. Like consistency in the foundations of mathematics, type safety provides a minimal safety guarantee for programs in type-safe languages.
Many frameworks for specifying algorithms have been and are being proposed by computer scientists. What are the fundamental differences between programming languages and according to which criteria should ew compare them? There are obvious candidates, such as efficiency or suitability for specific applications. But to differentiate programming languages and programming paradigms it will be important to consider the conceptual differences between languages, such as the presence or absences, and the power and structure of their type systems.
A. S. Troelstra
1991
32 pages
Read 20 August 2021
More space devoted to developments till 1965
Constructivism is a normative point of view concerning the methods and objects of mathematics. Not only does it interpret existing mathematics according to certain principles, but it also rejects methods and results not conforming to such principles as unfounded or speculative (the rejection is not always absolute, but sometimes only a matter of degree: a decided preference for constructive concepts and methods). In this sense the various form of constructivism are all ‘ideological’ in character.
Constructivism can be thought of as a reaction to the rapidly increasing use of highly abstract concepts and methods of proofs in mathematics, a trend exemplified by the works of R. Dedekind and G. Cantor.
Characteristic for the constructivist trend is the insistence that mathematical objects are to be constructed (mental constructions) or computed; thus theorems asserting the existence of certain objects should by their proofs give us the means of constructing objects whose existence is being asserted.
L. Kronecker may be described as the first conscious constructivist. For Kronecker, only the natural numbers were ‘God-given’; all other mathematical objects ought to be explained in terms of natural numbers (at least in algebra). Assertions of existence should be backed up by constructions, and the properties of numbers defined in mathematics should be decidable in finitely many steps. This is in the spirit of finitism. Kronecker strongly opposed Cantor’s set theory, but in his publications he demonstrated his attitude more by example than by an explicit discussion of his tenets.
The principal constructivist trends in this century:
- Finitism
- Semi-Intuitionism
- Predicativism
- Intuitionism
- Markov’s constructivism
- Bishop’s constructivism
Finitism may be characterized as based on the concept of natural number (or finite, concretely representable structure), which is taken to entail the acceptance of proof by induction and definition by recursion.
Abstract notions, such as ‘constructive proof’, ‘arbitrary number-theoretic function’ are rejected. Statements involving quantifiers are finitistically interpreted in terms of quantifier-free statements. Thus an existential statement thereExists(x, A(x)) is regarded as a partial communication, to be supplemented by providing an x which satisfies A. Establishing not(ForAll(x,A(x))) finitistically means: providing a particular x such that Ax is false.
In this century, T. Skolem was the first to contribute substantially to finitist mathematics; he showed that a fair part of arithmetic could be developed in a calculus without bound variables, and with induction over quantifier-free expressions only. Introduction of functions by primitive recursion is freely allowed. Skolem does not present his results in a formal context, nor does he try to delimit precisely the extent of finitist reasoning.
Since the idea of finitist reasoning was an essential ingredient in giving a precise formulation of Hilbert’s programme (the consistency proof for mathematics should use intuitively justified means, namely finitist reasoning), Skolem’s work is extensively reported by D. Hilbert and P. Bernays. Hilbert also attempted to circumscribe the extent of finitist methods in a global way; the final result is found in ‘Die Grundlagen de Mathemtik’ written by Hilbert and Bernays.
In 1941, Haskell Curry and R. L. Goodstein independently formulated a purely equational calculus PRA for primitive recursive arithmetic in which Skolem’s arguments could be formalized, and showed that the addition of classical propositional logic to PRA is conservative (i.e. no new equations become provable). PRA contains symbols for all primitive recursive functions, with their defining equations, and an induction rule of the form: if t[0] = t’[0], and t[Sx] = s[x, t[x]], t’[Sx] = s[x, t’[x]] has been derived, then we may conclude t[x] = t’[x].
Goodstein carried the development of finitist arithmetic beyond Skolem’s results, and also showed how to treat parts of analysis by finitist means.
Recently W. W. Tait in Finitism (1981), made a new attempt to delimit the scope of finitist reasoning. He defends the thesis that PRA is indeed the limit of finitist reasoning. Any finitely axiomatized part of PRA can be recognized as finitist, but never all of PRA, since this would require us to accept the general notion of primitive recursive function, which is not finitist.
In recent years there has been a lot of metamathematical work showing that large parts of mathematics have an indirect finitist justification, namely by results of the form: a weak system S in a language with strong expressive power is shown to be consistent by methods formalizable in PRA, from which it may bek concluded that S is conservative over PRA. A survey of such results is given in Partial realizations of Hilbert’s program (1988) by Stephen Simpson.
A remark made in various forms by many authors, from G. Mannoury in 1909 onwards, is the observation that already the natural number concept involves a strong idealization of the idea of ‘concretely representable’ or ‘visualizable’. Such an idealization is implicit in the assumption that all natural numbers are constructions of the same kind, whether we talk about very small numbers such as 3 or 5, or extremely large ones such as 9 ^ (9 ^ 9). In reality, we cannot handle 9 ^ (9 ^ 9) without some understanding of the general concept of exponentiation. The objection to finitism, that it is not restricted to objects which can be actually realized (physically, or in our imagination) one might call the ‘actualist critique’, and a programme taking the actualist critique into account actualism/ultra-intuitionism/ultra-finitism.
The first author to defend an actualist programme, was A. S. Esenin-Vol’pin in 1957. He intended to give a consistency proof for ZF using only ‘ultra-intuitionist’ means. Up till now the development of ‘actualist’ mathematics has not made much progress — there appear to be inherent difficulties associated with an actualist programme.
However, mention should be made of Existence and feasibility in arithmetic (1971) by Rohit Parikh, motivated by the actualist criticism of finitism, where is indicated, by technical results, the considerable difference in character between addition and multiplication on the one hand and exponentiation on the other hand. Together with work in complexity theory, this paper has stimulated the research on polynomially bounded arithmetic, as an example of which may be quoted the monograph Bounded Arithmetic (1986) by Samuel Buss.
One cannot extract a unified and coherent point of view from Poincaré’s writings. On the one hand he is a forerunner of the (semi-)intuitionists and predicativists, on the other hand he sometimes expresses formalist views, namely where he states that existence in mathematics can never mean anything but freedom from contradiction.
For the history of constructivism, Poincaré is important for two reasons:
1/ Explicit discussion and emphasis on the role of intuition in mathematics, more especially ‘the intuition of pure number’. This intuition gives us the principle of induction for the natural numbers, characterized by Poincaré as a ‘synthetic judgment a priori’. That is to say, the principle is neither tautological (i.e. justified by pure logic), nor is it derived from experience; instead, it is a consequence of our intuitive understanding of the notion of number. In this respect, Poincaré agrees with the semi-intuitionists and Brouwer.
2/ According to Poincaré, the set-theoretic paradoxes are due to a vicious circle, namely the admission of impredicative definitions: defining an object N by referring to a totality E in particular by quantifying over E), while N itself belongs to E. Poincaré’s standard example is Richard’s paradox: Let E be the totality of all real numbers given by infinite decimal fractions, definable in finitely many words. E is clearly countable, so by a well known Cantor style diagonal argument we can define a real N not in E. But N has been defined in finitely many words! However, Poincaré, adopting Richard’s conclusion, points out that the definition of N as element of E refers to E itself and is therefore impredicative.
The term ‘semi-intuitionists’ or ‘empiricists’ refers to a group of French mathematicians, in particular E. Borel, H. Lebesgue, R. Baire, and the Russian mathematician N. N. Luzin. Their discussions of foundational problems are always in direct connection with specific mathematical developments, and thus have an ‘ad hoc’, local character; also the views within the group differ.
What they have in common is the idea that, even if mathematical objects exist independently of the human mind, mathematics can only deal with such objects if we can also attain them by mentally constructing them, i.e. have access to them by our intuition; in practice, this means that they should be explicitly definable. In addition, pragmatical considerations occur: one is not interested in arbitrary objects of a certain kind, but only in the ones which play an important role in mathematics (which ‘occur in nature’ in a manner of speaking).
According to Borel, one can assert the existence of an object only if one can define it unambiguously in finitely many words. In this concern with definability there is a link with predicativism; on the other hand, there is in Borel’s writings no explicit concern with impredicativity and the vicious circle principle, as in the writings of Poincaré and Hermann Weyl.
With respect to the reality of the countably infinite, Borel takes a somewhat pragmatical attitude: while conceding the strength of the position of the strict finitist, he observes that the countably infinite plays a very essential role in mathematics, and mathematicians have in practice always agreed on the correct use of the notion: “The notion of the countably infinite appears [sic] as a limit possibility conceived by our imagination, just like the ideal line or the perfect circle.”
Borel explains the Richard paradox, not by referring to the impredicative character of the definition of N, but by the observation that N has not been unambiguously defined; the collection E is countable, but not effectively enumerable and hence the construction of N cannot be carried out. This distinction would later obtain a precise formulation in recursion theory.
Borel explicitly introduced the notion of a calculable real number; a function f is calculable if f(x) is calculable for each calculable x, and he observes that a calculable function must necessarily be continuous, at least for calculable arguments. This foreshadows Brouwer’s well known theorem on the continuity of all real functions.
Borel rejected the general notion of an uncountable set, as an essentially negative notion. According to Borel, Cantor’s diagonal argument only shows that the continuum cannot be exhausted by a countable set. Obviously, on this view the continuum presents a problem. On the one hand it is the basic concept in analysis, on the other hand it cannot be described as ’the set of its definable elements’ since it is uncountable.
The term ‘arithmetic theory of the continuum’, or ‘arithmetization of the continuum’, frequently appears in discussions of constructivism in the early part of this century. By this is meant the characterization of the continuum as a set of reals, where the real numbers are obtained as equivalence classes of fundamental sequences of rationals, or as Dedekind cuts. Since the rationals can be enumerated, this achieves a reduction of the theory of the continuum to number theoretical or ‘arithmetical’ functions.
Although the fact is not mentioned by Borel, the idea of a continuum consisting of only countable many definable reals suggests a ‘measure-theoretic paradox’, for if the reals in [0, 1] are countable, one can give a covering by a sequence of intervals I_0, I_1, I_2, … with n from 0 to ∞ |I_n| < 1, where |I_n| is the length of I_n. Such coverings are called singular. The paradox is repeatedly mentioned in Brouwer’s publications as a proof of the superiority of his theory of the continuum.
Motivated by his rejection of the platonistic view of mathematics prevalent in Cantorian set theory and Dedekind’s foundation of the natural number concept, Weyl, in his short monograph ‘Das Kontinuum’ formulated a programme for predicative mathematics; it appears that Weyl had arrived at his position independently of Poincaré and Russell. Predicativism may be characterized as ‘constructivism’ with respect to definitions of sets (but not with respect to the use of logic): sets are constructed from below, not characterized by singling them out among the members of a totality conceived as previously existing.
Weyl accepted classical logic and the set of natural numbers with induction and definition by recursion as unproblematic. Since the totality of natural numbers is accepted, all arithmetical predicates make sense as sets and we can quantify over them. The arithmetically definable sets are the sets of rank 1, the first level of a predicative hierarchy of ranked sets; sets of higher rank are obtained by permitting quantification over sets of lower rank in their definition. Weyl intended to keep the developments simple by restricting attention to sets of rank 1. On the basis of these principles Weyl was able to show for example: Cauchy sequences of real numbers have a limit; every bounded monotone sequence of reals has a limit; every countable covering by open intervals of a bounded closed interval has a finite subcovering; the intermediate value theorem holds (i.e. a function changing sign on an interval has a zero in the interval); a continuous function on a bounded closed interval has a maximum and a minimum.
After his monograph appeared, Weyl became for a short period convert to Brouwer’s intuitionism. Later he took a more detached view, refusing the exclusive adoption of either a constructive or an abstract axiomatic approach. Although Weyl retained a lifelong interest in the foundations of mathematics, he did not influence the developments after 1918.
After Weyl’s monograph predicativism rested until the late fifties, when interest revived in the work of M. Kondô, A. Grzegorczyk and G. Kreisel. Kreisel showed that the so-called hyperarithmetic sets known fro recursion theory constituted an upper bound for the notion ‘predicatively definable set of natural numbers’. Feferman and K. Shütte addressed the question of the precise extent of predicative analysis; they managed to give a characterization of its proof theoretic ordinal. Type free formalizations of predicative analysis with sets of all (predicative) ranks were developed.
The work of Lorenzen may be regarded as a direct continuation of Weyl’s programme.
In his thesis ‘Over de Grondslagen der Wiskunde’ the Dutch mathematician L. E. J Brouwer defended, more radically and more consistently than the semi-intuitionists, an intuitionist conception of mathematics. Brouwer’s philosophy of mathematics is embedded in a general philosophy, the essentials of which are already in place in Brouwer’s Leven, Kunst, Mystic.
With respect to mathematics, Brouwer’s ideas are:
- Mathematics is not formal; the objects of mathematics are mental constructions in the mind of the (ideal) mathematician. Only the thought constructions of the (idealized) mathematician are exact.
- Mathematics is independent of experience in the outside world, and mathematics is in principle also independent of language. Communication by language may serve to suggest similar thought constructions to others, but there is no guarantee that these other constructions are the same. (This is a solipsistic element in Brouwer’s philosophy.)
- Mathematics does not depend on logic; on the contrary, logic is part of mathematics.
These principles led to a programme of reconstruction of mathematics on intuitionistic principles. During the early period, from say 1907 until 1913, Brouwer did the major part of his work in classical topology and contributed little to his programme. In these years his view of the continuum and of countable sets is quite similar to Borel’s position on these matters.
He thinks that mathematical intuition is not capable of creating other than countable quantities in an individualized way. So the conception of continuum as a whole is intuitively given to us; the construction of the continuum to create all its part as individualized is impossible.
On the other hand, already in this early period there are also clear differences; thus Brouwer did not follow Borel in his pragmatic intersubjectivism, and tries to explain both the natural numbers and the continuum as two aspects of a single intuition (the primeval intuition).
Another important difference with Borel is that Brouwer soon after finishing his thesis realized that classical logic did not apply to his mathematics. Nevertheless, until circa 1913 Brouwer did not publicly dissociate from the semi-intuitionists.
Already in Brouwer 1908’s work Over de onbetrouwbaarheid der logische principles (On the unreliability of the principles of logic), a typically unintuitionistic kind of counter example to certain statements A of classical mathematics was introduced, not counterexamples in the strict sense of deriving a contradiction from the statement A, but examples showing that, assuming that we can prove A intuitionistically, it would follow that we had a solution to a problem known to be as yet unsolved. Undue attention given to these examples often create for outsiders the erroneous impression that intuitionism was mainly a negative activity of criticizing classical mathematics.
Example: Consider the set X ≡ { x : x = 1 or (x = 2 and F) } where F is any as of yet undecided mathematical statement, such as the Riemann hypothesis. X is a subset of the finite set { 1, 2 }, but we cannot prove X to be finite, since this would require us to decide whether X has only one, or two elements, and for this we would have to decide F. Intuitionistically, a set is finite if it can be brought into a constructively specified 1-1 correspondence with an initial part of the natural numbers.) So we have found a weak counterexample to the statement ‘a subset of a finite set is finite’.
By choosing our undecided problems suitably, it is also possible to give a weak counterexample to: ‘for reals x, x < 0 or x = 0 or x > 0’ or to ‘for all reals x, x <= 0 or x >= 0’. Brouwer used these examples to show the need for an intuitionistic revision of certain parts of the classical theory, and to demonstrate how classically equivalent definitions corresponded to distinct intuitionistic notions.
G. F. C. Griss, in a number of publications between 1944-1955, advocated a form of intuitionistic mathematics without negation, since one cannot have a clear conception of what it means to give proof of a proposition which turns out to be contradictory.
In reaction to Griss, Brouwer published in 1948 an example of a statement in the form of a negation which could not be replaced by a positive statement. Brouwer’s example involved a real number defined by explicit reference to stages in the activity of the ideal mathematician trying to prove an as yet undecided statement A. An essential ingredient of Brouwer’s argument is that if the ideal mathematician (creative subject in Brouwer’s terminology{ is certain that at no future stage of his mathematical activity he will find A to be true, it means that he knows that not A (Brouwer seems to have used such examples in lectures since 1927).
The argument illustrates the extreme solipsistic consequences of Brouwer’s intuitionism. Because of their philosophical impact, these examples generated a good deal of discussion and inspired some metamathematical research, but their impact on BP was very limited, in fact almost nihil.
Around 1913 Brouwer must have realized that the notion of choice sequence (appearing in a rather different setting in Borel’s discussion of the axiom of choice) could be legitimized from his viewpoint and offered all the advantages of an arithmetical theory of the continuum.
In the period up to 1928 he reconstructed parts of the theory of point sets, some function theory, developed a theory of countable well-orderings, and together with his students B. de Loor, gave an intuitionistic proof of the fundamental theorem of algebra.
After 1928, Brouwer displayed very little mathematical activity, presumable as a result of a conflict in the board of editors of the ‘Mathematische Annalen’. From 1923 onwards, M. J. Belifante and Arendt Heyting, and later also Heyting’s students continued Brouwer’s programme.
The discovery of a precise notion of algorithm in the 1930s as a result of the work of Church, Gödel, Herbrand, Turing, and Kleene did not affect intuitionism. This is not really surprising: most of these characterizations describe algorithms by specifying a narrow language in which they can be expressed, which is utterly alien to Brouwer’s view of mathematics as the languageless activity of the ideal mathematician.
Turing’s analysis is not tied to a specific formalism. Nevertheless he bases his informal arguments for the generality of his notion of algorithm on the manipulation of symbols and appeals to physical limitations on computing; and such ideas do not fit into Brouwer’s ideas on mathematics as a ‘free creation’.
Heyting’s monograph Intuitionism, an introduction from 1956 was instrumental in generating a wider interest in intuitionism.
The fact that Brouwer’s approach to mathematics also required a revision of the principles of classical logic was not yet clearly realized by him while writing his thesis, but in 1908 Brouwer explicitly noted that intuitionism required a different logic. In particular, he noted that the principle of the excluded middle A or not A is not intuitionistically valid.
A first important technical contribution to intuitionistic logic is made in 1924’s work Intuitionistische Zerlegung mathematischer Grundbegriffe that not not not A <-> not A is an intuitionistic logical law.
The standard informal interpretation of logical operators in intuitionistic logic is the so-called proof-interpretation or BHK interpretation. The formalization of intuitionistic logic started before this interpretation was actually formulated.
On the BHK-interpretation, the meaning of a statement A is given by explaining what constitutes a proof of A, and proof of A for logically compound A is explained in terms of what it means to give a proof of its constituents. Thus, for propositional logic:
- A proof of A and B is given by presenting a proof of A and a proof of B
- A proof of A or B is given by presenting either a proof of A or a proof of B
- A proof of A -> B is a construction which transforms any proof of A into a proof of B
- Absurdity (‘the contradiction’) has no proof; a proof of not A is a construction which transforms any supposed proof of A into a proof of contradiction.
Such an interpretation is implicit in Brouwer’s writings and has been made explicit by Heyting for predicate logic an by A. N. Kolmogorov for propositional logic.
Kolmogorov formulated what is essentially the same interpretation in different terms: he regarded propositions as problems, and logically compound assertions as problems explained in terms of simpler problems, e.g. A -> B represents the problem of reducing the solution of B to the solution of A. Initially Heyting and Kolmogorov regarded their respective interpretations as distinct; Kolmogorov stressed that his interpretation also makes sense in a classical setting. Later Heyting realized that, at least in an intuitionistic setting, both interpretations are practically the same.
Kolmogorov’s paper from 1925 O printsipe tertium non datur, written in Russian, is the earliest published formalization of a fragment of intuitionistic logic, and represents a remarkable achievement, but had very little effect on the developments. Kolmogorov does not assume the ‘ex false sequitur quodlibet’ P -> (not P -> Q) which is justifiable on the basis of the BHK interpretation. The system of intuitionistic logic with the ‘ex falso’ deleted became known as minimal logic and is of some interest in connection with completeness problems.
V. I. Glivenko presented in 1928 a (not complete) formalization of intuitionistic propositional logic and derives from this informally not(not(not P or not P), not not not P -> not P, (not P or P -> not Q) -> not Q and uses these theorems to show that the interpretation of Barzin and Errera’s 1927 Sur la logique de M. Brouwer of Brouwer’s logic, according to which a proposition intuitionistically is either true or false or ‘tierce’, is untenable; a nice example of the use of formalization to settle a philosophical debate.
Heyting wrote a prize essay on the formalization of intuitionistic mathematics which was crowed by the Dutch Mathematical Association in 1928; the essay appeared in revised form in 1930. The first of the 3 papers contains a formalization of intuitionistic propositional logic in its present extent. The second paper deals with predicate logic and arithmetic. Predicate logic does not yet appear in its final form, due to a defective treatment of substitution, and the (not quite consistent) germs of a theory permitting non-denoting terms. Arithmetic as presented in the second paper is a fragment of Heyting arithmetic as it is understood today, since there are axioms for addition (in the guise of a definition) but not for multiplication. The third paper deals with analysis. The system is very weak due to a lack of existence axioms for sets and functions.
In 1929 Glivenko formulated and proved as a result of his correspondence with Heyting the ‘Glivenko theorem’; in propositional logic not not A is intuitionistically provable iff A is classically provable.
Kolmogorov in his paper from 1925 describes an embedding of classical propositional logic into (his fragment of) intuitionistic propositional logic, thereby anticipating the work of Gödel, Zur intuitionistischen Arithmetik und Zahlentheorie (1933) and Gentzen, Untersuchungen über das logische Schliessen (also dating from 1933, but published only in 1965), and argues that this embedding is capable of generalization to stronger systems. Gödel’s embedding is formulated for arithmetic, but can be adapted in an obvious way to predicate logic. In Gentzen’s version prime formulas P are first replaced by not not P and the operators … or …, thereExists(x, …) by not(not … and not …), not(ForAll(x, not …) respectively. In Kolmogorov’s version not not is inserted simultaneously in front of every subformulae. The various embeddings are logically equivalent. If * is one of these embeddings, A* <-> A classically, and A* is provable intuitionistically, if and only if A is provable classically.
Gödel’s embedding made it clear that intuitionistic methods went beyond finitism, precisely because abstraction notions were allowed. This is clear e.g. from the clause explaining intuitionistic implication in the BHK-interpretation, since there the abstraction notion of constructive proof and construction are used as primitives. This fact had not been realized by the Hilbert school until then; Bernays was the first one to grasp the implications of Gödel’s result.
Quite important for the proof theory of intuitionistic logic was the formulation in Gentzen’s work of the sequent calculi LK and LJ. Using his cut elimination theorem, Gentzen showed that for IQC the disjunction property DP holds: if entails A or B, then entails A or entails B. Exactly the same method yields the explicit definability or existence property E: if entails thereExists(x, A(x)) then entails A(t) for some term t. These properties present a striking contrast with classical logic, and have been extensively investigated and established for the usual intuitionistic formal systems.
The earliest semantics for IPC, due to the work of S. Jaskowski, M. H. Stone, A. Tarski, G. Birkhoff, T. Ogasawara in the years 1936-1940 was algebraic semantics, with topological semantics as an important special case. In algebraic semantics, the truth values of propositions are elements of a Heyting algebra (also known as Brouwerian lattice, pseudo-complemented lattice, pseudo-Boolean algebra, or residuated lattice with bottom). A Heyting algebra is a lattice with top and bottom, and an extra operation -> such that a and b <= c iff a <= b -> c, for all elements a, b, c of the lattice. An important special case of a Heyting algebra is the collection of open ses of a topological space T ordered under inclusion, where U -> V := Interior (V U (T \ U)). The logical operation and, or, ->, not correspond to the lattice operations join, meet, -> and the defined operation not a := a -> 0, where 0 is the bottom of the lattice. A boolean algebra is a special case of a Heyting algebra.
In the early forties Kleene devised an interpretation which established a connection between the notion of computable (= recursive) function and intuitionistic logic, the realizability interpretation given in On the interpretation of intuitionistic number theory (1945).
The essence of the interpretation is that it so to speak hereditarily codes information on the explicit realization of disjunctions and existential quantifiers, recursively in numerical parameters. The definition is by induction on the number of logical symbols of sentences (= formulas without free variables): with every formula A one associates a predicate ‘x realizes A’, where x is a natural number. Typical clauses are:
- n realizes t = s iff t = s is true
- n realizes A -> B iff for all m realizing A, n • m realizes B
- n realizes thereExists(m, B(m)) iff n is a pair (m, k), and k realizes B(m).
Here • is the operation of application between a number and the code of a partial recursive function. Kleene established the correctness of this interpretation: if HA entails A, then for some number n, n realizes A.
The interest of the interpretation is, that it makes more true than just what is coded in the formalism HA. In particular, the following version of Church’s thesis may be shown to be realizable:
CT_0 forAll(n, thereExists(m, A(n, m))) -> thereExists(k, forAll(n, A(n, k • m)))
a principle which is easily seen to be incompatible with classical logic. Realizability and its many variants have become a powerful tool in the study of metamathematics of constructive systems.
Algebraic semantics was extended to predicate logic, and A. Mostowski in 1949 was the first one to apply topological models to obtain underivability results for IQC. This development culminated in the monograph by The Mathematics of Metamathematics (1963) Rasiowa and Sikorski. Although algebraic semantics has proved to be technically useful in metamathematical research, it is so to speak only the algebraic version of the syntax, as witnessed by he fact that IPC itself can be made into a Heyting algebra (the Lindenbaum algebra of IPC).
More important from a conceptual point of view are two other semantics, Beth models due to E. W. Beth and Kripke models due to Saul Kripke. Both these semantics are based on posets. We call the elements k, k’, k”, … of a poset (K, <=) nodes. In Kripke models the partial order is arbitrary, in Beth models as defined by Beth it is a finitely branching tree. The interest of these models resides in the intuitive interpretation of the partial order. For Beth models, each node represents a state of information in time, and a higher node represents a possible state of information at a later point in time. The branching of the tree reflects the fact that there are different possibilities for the extension of our knowledge in the future. In the Kripke models, it is more natural to think of the nodes as representing possible stages of knowledge; a higher node in the ordering corresponds to an extension of our knowledge. That is to say, passing to a later period in time does not force us to move upwards in a Kripke model, only extension of our knowledge does. In these models one has a notion of ‘A is true at k’, or ‘k forces A’. Falsehood is nowhere forced. It is possible to interpret Beth and Kripke models as topological models of special spaces.
An important aspect of Beth models is the connection with intuitive intuitionistic validity; a formula A(R_1, …, R_n) of IQC, containing predicate letters R_1, …, R_n is intuitionistically valid if for all domains D and all relations R*_i of the appropriate arity. A^D(R*_1, …, R*_n) holds intuitionistically; here A^D(R*_1, …, R*_n) is obtained from A by restricting quantifiers to D, and replacing R_i by R*_i.
From observations by G. Kreisel in 1958 it follows that, for propositional logic, validity in a Beth model is equivalent to intuitive validity for a collection of propositions P^α_1, P^α_2, …, P^α_n depending on a lawless parameter α.
Beth and Kripke proved completeness for their respective kinds of semantics by classical methods. Beth originally believed to have also an intuitionistic completeness proof for his semantics. Veldman was able to show that if one extends the notion of Beth model to fallible. Beth model,s where it is permitted that in certain nodes falsehood is forced, it is possible to obtain an intuitionistic completeness proof for Kripke semantics. The idea was transferred to Kripke semantics by H. de Swart. For the fragment of intuitionistic logic without falsehood and negation, fallible models are just ordinary models. For minimal logic, where ⊥ is regarded as an arbitrary unprovable proposition letter, one has intuitionistic completeness relative to ordinary Beth models. The best results in this direction can be obtain from work by Harvey Friedman from circa 1976.
C. A. Smoryński used Kripke models with great virtuousity in the study of metamathematics of intuitionistic arithmetic.
In essence, the ‘formulas-as-types’ idea (may be ‘propositions-as-types’ would have been better) consists in the identification of a proposition with the set of its (intuitionistic) proofs. Or stated in another form: in a calculus of typed objects, the types play the role of propositions, and the objects of a type A correspond to the proofs of the proposition A.
Thus, since on the BHK-interpretation a proof of an implication A -> B is an operation transforming proofs of A into proofs of B, the proofs of A -> B are a set of functions from (the proofs of) A to (the proofs of) B. Similarly, (the set of proofs of) A and B is the set of pairs of proofs, with first component a proof of A, and second component a proof of B. So A and B corresponds to a cartesian product.
A clear expression to this idea was given in the late sixties (circa 1968–1969) by W. A. Howard, and by N. G. de Bruijn; H. Läuchli around the same time used the idea for a completeness proof for IQC for a kind of realizability semantics.
The analogy goes deeper: one can use terms of at typed lambda calculus to denote natural deduction proofs, and then normalization of proofs corresponds to normalization in the lambda calculus. So pure typed lambda calculus is in a sense the same as IPC in natural deduction formulation; similarly, second-order lambda calculus (polymorphic lambda calculus) is intuitionistic logic with propositional quantifiers.
The formulas-as-types idea is a guiding principle in much recent research in type theory on the borderline of logic and theoretical computer science. It is used in the type theories developed by Per Martin-Löf in An intuitionistic theory of types (1975), Intuitionistic Type Theory (1984) to reduce logic to type theory; thus proof by induction and definition by recursion are subsumed under a single rule in these theories. Formulas-as-types plays a key role in the proof checking language AUTOMATH devised by N. G. de Bruijn and collaborators since the late sixties.
The formula-as-types idea has a parallel in category theory where propositions correspond to objects, and arrows (to equivalence classes of) proofs. J. Lambek investigated this parallel or IPC in Deductive systems and categories III (1972) and later work, culminating in the monograph Introduction to higher order categorical logic (1986).
As already remarked, the continuum presented a problem to the semi-intuitionists; they were forced to introduce it as a primitive notion, while Brouwer in his thesis tried to explain the continuum and the natural numbers as emanating both from a single ‘primeval intuition’.
However, when Brouwer stared circa 1913 with his intuitionistic reconstruction of the theory of the continuum and the theory of pointsets, he found that the notion of choice sequence, appearing in Borel’s discussion of the axiom of choice (as the opposite, so to speak, of a sequence defined in finitely many words, and therefore in Borel’s view of a dubious character) could be regarded as a legitimate intuitionistic notion, and as a means of retaining the advantages of an arithmetic theory of the continuum.
In Brouwer’s intuitionistic set theory the dominating concept is that of a spread (German: ‘Menge’). Slightly simplifying Brouwer’s original definition, we say that a spread consists essentially of a tree of finite sequences of natural numbers, such that every sequence has at least one successor, plus a law L assigning objects of a previously constructed domain to the nodes of the tree. Choice sequences within a given spread correspond to the infinite branches of the tree. Brouwer calls a sequence L(a̅1), L(a̅2), L(a̅3), …, (a̅ as infinite branch) an element of the spread. Below we shall use ‘spread’ only for trees of finite sequences of natural numbers without finite branches, corresponding to the trivial L satisfying L(a̅(n+1)) = an. Since it is not the definition of a spread, but the way the choice sequences are given to us, which determines the properties of the continuum, we shall henceforth concentrate on the choice sequences.
the notion of spread is supplemented by the notion of species, much closer to the classical concept of set; one may think of a species as set of elements single out from a previously constructed totality by a property (as in the separation axiom of classical set theory).
The admissibility of impredicative definitions is not explicitly discussed in Brouwer’s writings, though it is unlikely that he would have accepted impredicative definitions without restrictions.
One the other hand, his methods allow more than just predicative sets over N: Brouwer’s introduction of ordinals in intuitionistic mathematics is an example of a set introduced by a so-called generalized inductive definition, which cannot be obtained as a set defined predicatively relative to N.
A choice sequence a of natural numbers may be viewed as an unfinished, ongoing process of choosing values a0, a1, a2, … by the ideal mathematicians; at any stage of his activity the mathematician has determined only finitely many values plus, possibly, some restriction on future choices (the restriction may vary from ‘no restrictions’ to ‘choices henceforth completely determined by a law’). For sequences completely determined by a law or recipe we shall use lawlike; other mathematical objects not depending on choice parameters are also called lawlike. An important principle concerning choice sequences is the:
Continuity principle or continuity axiom. If to every choice sequence a of a spread a number n(a) is assigned, n(a) depends on an initial segment a̅m = a0, a1, …, a(m-1) only, that is to say for all choice sequences b starting with the same segment a̅m, n(b) = n(a).
This principle is not single out by Brouwer, but used in proofs of what later became known as the bar theorem. From the bar theorem, Brouwer obtained an important corollary for the finitary spreads, the Fan theorem:
If to every choice sequence a of a finitely branching spread (fan) a number n(a) is assigned, there is a number m, such that for all a, n(a) may be determined from the first m values of a (i.e. an initial segment of length m).
The fan theorem can be seen as a combination of the compactness of finite trees with the continuity axiom; Brouwer uses the fan theorem to derive the uniform continuity theorem: Every function from a bounded closed interval into R is uniformly continuous.
Bar theorem: If the universal spread (i.e. the tree of all sequences of natural numbers) contains a decidable set A of nodes such that each choice sequence a has an initial segment in A, then for the set of nodes generated by i) x subsetOf A ii) if all successors of a node n are in X, then n elementOf X, it follows that the empty sequence is in X.
Originally, in Brouwer’s 1919 work Begründung der Mengenlehre unabhängig vom logischen Satz vom augeschlossenen Dritten II: Theorie der Punktmengen, the fan theorem was assumed without proof. In 1923 Brouwer presented an unsatisfactory proof of the uniform continuity theorem, in 1924 he proved this theorem via the fan theorem which in its turn is obtained from the bar theorem.
Brouwer’s proof of the bar theorem has often been regarded as obscure. In this proof Brouwer analyzes the possible forms of a constructive proof of a statement of the form forAll(a, thereExists(n, A(a̅n))) for decidable A.
Nowadays the proof is regarded not so much obscure as well as unsatisfactory. As Kleene and Vesley in their 1965 work The Foundations of Intuitionistic Mathematics, especially in Relation to Recursive Functions observes, Brouwer’s assumption concerning the form of ‘fully analyzed proofs’ is not more evident than the bar theorem itself.
The fully analyzed proof or canonical proof was used later by Micheal Dummet in his 1977 work Elements of Intuitionism in his attempts to give a more satisfactory version of the BHK interpretation of intuitionistic logic.
In Heyting’s third formalization paper from 1930, Sitzungsberichte der Preussischen Akademio von Wissenschaften, Physikalicsh Mathematische Klaase we find for the first time a formal statement of the continuity principle.
For a long time, nothing happened until Kleene worked on the axiomatization of intuitionistic analysis. Kleene based his system on a language with variables for numbers and choice sequences; to arithmetical axioms he added an axiom of countable choice, the axiom of bar induction (equivalent to the bar theorem) and a continuity axiom, a strengthening of the continuity principle.
The continuity axiom was the only non-classical principle, and Kleene established its consistency relative to other axioms using a realizability interpretation (function-realizability). He also showed, by means of another realizability notion that Markov’s principle was not derivable in his system.
In 1963 Kreisel developed an axiomatization based on a language with number variables and two kinds of function variables, for lawlike sequences and for choice sequences. He sketched a proof of the conservativity of the axioms for choice sequences relative to the lawlike part of the system, by means of a translation of an arbitrary sequence into the lawlike part of the theory (the ‘elimination translation’). This work resulted in Formal systems for some branches of intuitionistic analysis (1970) by Kreisel and Troelstra.
J. Myhill in 1967 introduced an axiom intended to express the sequences in the language of analysis of Brouwer’s solipsistic theory of the creative subject called by him Kripke’s scheme since Kripke was the first to formulate this principle:
thereExists(a, ((thereExists(x, ax notEqual 0) -> A) and (forAll(x, (ax = 0) -> not A))))
for arbitrary A. KS conflicts with Brouwer’s principle for functions. Brouwer’s reasoning seems to justify in fact the even stronger thereExists(a, thereExists(x, (ax notEqualTo 0) <-> A)). Myhill’s conceptual analysis of the notion of the choice sequence is considerably more refined than earlier attempts.
An obvious connection between Kripke’s scheme and the theory of the creative subject: For any proposition A, the a in KS may be interpreted as: an notEqual 0 iff the creative subject has found evidence for the truth of A at stage n of his activity.
Brouwer appears to have vacillated with respect to the precise form which restrictions on choice sequences could take, but in his published writings he does not explicitly consider subdomains of the universe of choice sequences which are characterized by the class of restrictions allowed, except for the trivial example of the lawlike sequences.
In 1958 work A remark on free choice sequences and the topological completeness proofs, Kreisel considered ‘absolutely free’ (nowadays lawless) sequences ranging over a finitely branching tree, where at any stage int he construction of the sequence no restriction on future choice is allowed; later this was extended to an axiomatization LS of the theory of lawless sequences ranging over the universal tree. Lawless sequences are of interest because of their conceptual simplicity (when compared to other concepts of choice sequences), as a tool for studying other notions of choice sequence and because they provide a link between Beth-validity and intuitive intuitionistic validity.
As a result of the work of Kreisel, Myhill, and Troelstra, mainly over the period 1963-1980, it became clear that many different notions of choice sequences may be distinguished, with different properties.
Survey on this topic can be found in Troelstra’s Choice Sequences, a Chapter of Intuitionistic Mathematics (1977).
The publication of Foundations of Constructive Analysis (1967) by Bishop led to several proposals for an axiomatic framework for Bishop’s constructive mathematics, in particular a type-free theory of operators and classes and versions of intuitionistic set theory.
A language and axioms for explicit mathematics (1975) Feferman Constructive theory of functions and classes (1979)
Set theoretic foundations for constructive analysis (1977) Friedman Martin-Löf’s theories have also been considered in this connection.
An intuitionistic theory of types: predicative part (1975) Martin-Löf Intuitionistic type theory (1984) Martin-Löf
As shown by Aczel in 1978, one can interpret a constructive set theory CZF in a suitable version of Martin-Löf type theory. CZF does not have a powerset axiom; instead there are suitable collection axiom which permit to derive the existence of the set of all functions from x to y for any two sets x and y; moreover the foundation axiom has been replaced by an axiom of ∈-induction. Much of this work is reported in the monograph Foundations of Constructive Mathematics (1985) by Beeson.
Topological models and Beth models turned out to be very fruitful for metamathematical study of intuitionistic analysis, type theory and set theory. Dana Scott was the first to give a topological model for intuitionistic analysis, in Extending the topological interpretation to intuitionistic analysis (1968) andExtending the topological interpretation to intuitionistic analysis II (1970). In this model the real numbers are represented by the continuous functions over the topological space T underlying the model. For suitable T, all real-valued functions are continuous in Scott’s model.
This later developed into the so-called sheaf models for intuitionistic analysis, type theory and set theory, with a peak of activity in the period 1977-1984. The inspiration for this development not only came from Scott’s model but also from category theory, where William Lawvere in his work (1971) developed the notion of elementary topos — a category with extra structure, in which set theory and type theory based on intuitionistic logic can be interpreted. The notion of elementary topos generalized the notion of Grothendieck topos known from algebraic geometry, and is in a sense ‘equivalent’ to the notion of an intuitionistic type theory.
Even Kleene’s realizability interpretation can be extended to type theory and be recast as an interpretation of type theory in a special topos.
The effective topos (1982) J.M.E Hyland
Some models studied are mathematically interesting for example, analysis without an axiom of countable choice, where the reals defined by Dedekind cuts are not isomorphic to the reals defined via fundamental sequences of rationals.
The function f_a(x) given by f_a(x) = f_0(x) + a where f_0 is given as {(0,-1), (1,0), (2,0), (3,1)}, cannot be constructively proved to have a zero as long as we do not know whether a <= 0 or a >= 0. But even classically we can show that f_a does not have a zero recursively in the parameter a - and this is typically a result of classical recursive mathematics.
Where in constructive recursive mathematics the recursivity in parameters is built into the constructive reading of the logical operators, in RM the recursiveness has to be made explicitly.
Classical recursive mathematics is as old as recursion theory itself, since already Turing introduced “computable numbers” and it is still expanding today.
E. Specker was the first to construct an example of a recursive bounded monotone sequence of rationals without a recursive limit. Such sequences are now known as Specker sequences.
Kreisel and D. Lacombe constructed singular coverings of the interval in 1957; Kreisel, Lacombe and J. Shoenfield showed, also in 1957, that every effective operation of type 2 is continuous (an effective operation of type 2 is a partial recursive operation with code u say, acting on codes x, y of total recursive functions such that forAll(z, (x • z = y • z) → u • x = u • y)) continuity of u means that u • x depends on finitely many values only of the function coded by x.
A. I. Maltsev and Y. L. Ershov developed mainly in the period 1961-1974 the theory of numerations as a systematic method to lift the notion of recursiveness from N to arbitrary countable structures.
La théorie des énumérations (1972) Ershov
In 1974 G. Metakides and Anil Nerode gave the first applications of the powerful priority method from recursion theory to problems in algebra.
Effective content of field theory (1979) Metakides and Nerode
A recent striking result is the construction of a recursive ordinary differential equation without recursive solutions obtained by M. B. Pour-El and J. I Richards in 1979.
Computability in analysis and physics (1989) Pour-El and Richards
A. A. Markov formulated in 1948—1949 the basic ideas of constructive recursive mathematics. They may be summarized as follows.
- objects of constructive mathematics are constructive objects, concretely: words in various alphabets.
- the abstraction of potential existence is admissible but the abstraction of actual infinity is not allowed. Potential realizability means for example, that we may regard plus as a well-defined operation for all natural numbers, since we know how to complete it for arbitrarily large numbers.
- a precise notion of algorithm is taken as a basis (Markov chose for this his own notion of ‘Markov-algorithm’)
- logically compound statements have to be interpreted so as to take the preceding points into account
Not surprisingly classical recursive mathematics can be bodily lifted to CRM and vice versa. Sometimes parallel results were discovered almost simultaneously and independently in classical recursive mathematics and constructive recursive mathematics respectively. Thus the theorem by Kreisel, Lacombe and Schoenfield mentioned above is in the setting of constructive recursive mathematics a special case of a theorem proved by G. S. Tseǐtin in 1959: every function from a complete separable metric space into a separable metric space is continuous.
N. A. Shanin in 1958 work formulated a “deciphering algorithm” which makes the constructive content of mathematical statements explicit. By this reinterpretation an arbitrary statement in the language of arithmetic is reformulated as a formula thereExists(x_1,…, x_iA) where A is normal, i.e. does not contain or, thereExists, and the string of existential quantifiers may be interpreted in the usual way. Shanin’s method is essentially equivalent to Kleene’s realizability, but has been formulated in such a way that normal formulas are unchanged by the interpretation (Kleene’s realizability produces a different although intuitionistically equivalent formula when applied to a normal formula).
The deciphering method systematically produces a constructive reading for notions defined in the language of arithmetic; classically equivalent definitions may obtain distinct interpretations by this method. But not all notions considered in CRM are obtained by applying the method to a definition in arithmetic (example: the ‘FR-numbers’ are the reals corresponding to the intuitionistic reals and are given by a code a for the fundamental sequence of rationals, together with a code b for a modulus of convergence, i.e. relative to a standard enumeration of the rationals <r_n>_n the sequence is <r_an>_n, and forAll(m,m’(|r_bn+m - r_bn+m’| < 2^-k)). An F-sequence is an FR-sequence with b omitted. The notion of an F-sequence does not arise as an application of the deciphering algorithm.)
Markov accepted one principle not accepted in either intuitionism or Bishop’s constructivism: if it is impossible that computation by an algorithm does not terminate, then it does terminate. Logically this amounts to what is usually called Markov’s principle:
MP not not (thereExists(x, fx = 0) → thereExists(x(fx = 0))) (f: N → N recursive)
The theorem by Tseǐtin, mentioned above, needs this principle for its proof.
The measure-theoretic paradox is resolved in constructive recursive mathematics in a satisfactory way: singular coverings of [0, 1] do exist, but the sequence of partial sums summation(n=0, k) |I_n| does not converge, but is a Specker sequence; and if the sequence does converge, the limit is >= 1, as shown by Tseĭtin and I.D.Zaslavskiĭ in 1962.
After circa 1985 the number of contributions to constructive recursive mathematics has considerably decreased. Many researchers in constructive recursive mathematics have turned to more computer-science oriented topics.
In his book ‘Foundations of constructive mathematics’ the American mathematician E. Bishop launched his programme for constructive mathematics. Bishop’s attitude is both ideological and pragmatical: ideological, inasmuch he insists that we should strike for a type of mathematics in which every statement has empirical content, and pragmatical in the actual road he takes towards this goal.
In Bishop’s view, Brouwer successfully criticized classical mathematics, but had gone astray in carrying out his programme, by introducing dubious concepts such as choice sequences, and wasting much time over the splitting of classical concepts into many non-equivalent ones, instead of concentrating on the mathematically relevant version of these concepts. In carrying out his programme, Bishop is guided by three principles:
- avoid concepts defined in a negative way
- avoid defining irrelevant concepts — that is to say, among the many possible classically equivalent, but constructively distinct definitions of a concept, choose the one or two which are mathematically fruitful ones, and disregard the others
- avoid pseudo-generality, that is to say, do not hesitate to introduce an extra assumption if it facilitates the theory and the examples one is interested in satisfy the assumption.
Statements of Bishop’s constructive mathematics may be read intuitionistically without distortion; sequences are then to be regarded as given by a law, and accordingly, no continuity axioms nor bar induction are assumed.
Statements of Bishop’s constructive mathematics may also be read by a Markov-constructivist without essential distortion; the algorithms are left implicit, and no use is made of a precise definition of algorithm.
Thus Bishop’s constructive mathematics appears as a part of classical mathematics, intuitionistic mathematics, and constructive recursive mathematics.
Bishop not only applied the three principles above, but also avoided negative results (only rarely did he present a weak counterexample), and concentrated almost exclusively on positive results.
Two of the most prolific contributors to Bishop’s programme are F. Richman and D.E. Bridges. The topics treated cover large parts of analysis, including the theory of Banach spaces and measure theory, parts of algebra (e.g. abelian groups, Noetherian groups) and topology (e.g. dimension theory, the Jordan curve theorem).
8.2 The relation of Bishop’s Constructive Mathematics to Intuitionistic Mathematics and Constructive Recursive Mathematics
The success of Bishop’s programme has left little scope for traditional intuitionistic mathematics; to some extent this is also true of Constructive Recursive Mathematics. For all of Bishop’s Constructive Mathematics may at the same time be regarded as a contribution to Intuitionistic Mathematics; moreover, in many instance where in Intuitionistic mathematics a routine appeal would be made to a typical intuitionistic result, such as the uniform continuity theorem for functions defined on a closed bounded interval, the corresponding treatment in Bishop’s constructive mathematics would simply add an assumption of uniform continuity, for the relevant function, without essential loss in mathematical content. Thus to find scope for specifically intuitionistic reasoning, one has to look for instance where the use of typically intuitionistic axioms such as the continuity axiom or the fan theorem results in a significantly better or more elegant result, and such cases appear to be comparatively rare.
To some extent the above, mutatis mutandis, also applies to constructive recursive mathematics. Thus for example, the usefulness of the beautiful Kreisel-Lacombe-Schoenfield-Tseǐtin theorem is limited by two factors:
- an appeal to the theorem can often be replaced by an assumption of continuity in the statement of the result to be proved
- in many cases, continuity without uniform continuity is not enough, as witnessed, e.g. by Kushner’s example of a continuous function on [0, 1] which is not integrable.
In the literature contributing to Brouwer’s and Markov’s programme, a comparatively large place is taken by counterexamples and splitting of classical notions. This may be compared with periods in the development of classical analysis and topology in which there was also considerable attention given to ‘pathologies’. In this comparison, Bishop’s recursive mathematics exemplifies a later stage in constructivism.
Finally, in classical mathematics there arise questions of constructivity of a type which has not been considered in the constructivist tradition. For example, one may attempt to find a bound on the number of solutions to a number-theoretic problem, without having a bound for the size of the solutions.
Herbrand-Analysen zweir Beweise des Satzes von Roth: polynomiale Anzahlschranken (1989) - H. Luckhardt
Recent development such as ‘linear logic’ by Girard may be seen as a refinement of intuitionistic logic, obtained by pursuing the idea of a ‘bookkeeping of resources’ seriously.
Gregory J. Chaitin
10 pages
Read 21 August 2021
Panu Raatikainen 22 pages
Read
Revival of interest in the Hilbert’s program.
There are some systematic interpretations of Hilbert’s program which argue in various ways that there is a sound core in the program which was not affected by Gödel’s results.
The roots of Hilbert’s program go back to the foundational debates in the 19th century, especially to Kroenecker’s attack on Cantorian set theory and the abstract analysis juts developed. This debate affected Hilbert permanently.
Hilbert’s own thought went through various important changes, and it would be an error to simply equate Hilbert’s views in, say, 1900, and his mature program, which was formulated only in the early 1920s.
Hilbert was becoming alarmed by the gains that Brouwer’s conception of mathematics was making among the younger mathematicians. To him the program of the Intuitionists represented quite simply a clear and present danger to mathematics. Hilbert interpreted intuitionism as requiring that all pure existence proofs, a large part of analysis and Cantor’s theory of infinite sets would have to be given up. In particular, this would rebut some of Hilbert’s own contributions to pure mathematics.
Bernays has reported that under the influence of the discovery of antinomies, in set theory, Hilbert temporarily thought that Kroenecker had probably been right there. But soon he changed his mind. Now it became his goal, one might say, to do battle with Kroenecker with his own weapons of finiteness by means of a modified conception of mathematics.
It seems that Hilbert never studied Brouwer’s foundational work in detail, but he apparently identified Brouwer’s view with that of Weyl which he knew much better. But in fact Weyl’s view was more restricted than Brouwer’s as was Kroenecker’s. Nevertheless, Hilbert attributed to Brouwer many views of Weyl. More generally, Hilbert and his school simply identified intuitionism with finitism.
Hilbert granted that from the finitistic, contentual point of view, the law of the excluded middle “should not be uncritically adopted as logically unproblematic”. Note, moreover, that he often formulated the LEM as: not(forAll(x, P(x))) → thereExists(x, not(P(x))). Hilbert was convinced and aimed to show that “the application of tertium non datur can never lead to danger.
Hilbert agreed with the long tradition according to which there is no such thing as an actual or completed infinite. Hilbert thought that it is in Kantian terms only a regulative idea of reason. But, unlike Kroenecker and Brouwer, he did not therefore want to rebut all the achievements of infinistic mathematics. What Hilbert rather aimed at was to bring together the safety, or reliability, of critical constructive mathematics and the liberty and power of infinistic set theoretical mathematics to justify the use of the latter by the uncontroversial methods of the former. For his purpose, mathematics should be rigorously formalized. All the propositions that constitute mathematics are converted into formulas, so that mathematics proper becomes an inventory of formulas. Next, Hilbert intended to isolate what he viewed as an unproblematic and necessary part of mathematics, an elementary part of arithmetic he called “finitistic mathematics”, which would certainly be accepted by all parties in the foundational debate, even the most radical skeptics such as Kroenecker, Brouwer and Weyl.
Further, Hilbert divided mathematical statements into ideal and real statement.s The latter are finitistically meaningful, or contentual, but the former are strictly speaking just meaningless strings of symbols that complete and simplify the formalism, and make the application of classical logic possible.
Finally, the consistency of the comprehensive formalized system is to be proved by using only restricted, uncontroversial and contentual finitistic mathematics. Such a finitistic consistency proof would entail that the infinistic mathematics could never prove a meaningful real statement that would be refutable in finitistic mathematics, and hence that infinistic mathematics is reliable.
Hilbert’s characterization of both finitistic mathematics and real statements are somewhat unclear, and the exact extension of these notions remains a subject of debate. Nevertheless, it is in any case clear that the real statements include numerical equations and their negations, bounded existential and universal quantifications of these, and at least some universal generalizations. They are thus included in if not coexistensive with the sentences that logicians nowadays call Pi^0_1 sentences. For simplicity, though not essential to the argumentation, this is the position assumed.
William Tait (1981) has in turn argued that Primitive Recursive Arithmetic captures exactly the part of mathematics that Hilbert took to be finitistic; this interpretation has received quite a wide acceptance.
PRA can be formulated as a “logic-free” equational calculus, and consequently it does not matter whether one adopts classical or constructive logic as one’s logical basis for PRA. This satisfies nicely Hilbert’s need for a neutral, unproblematic background theory.
Second, in replying to Poincaré’s charge that his attempt to justify arithmetical induction by a consistency proof must necessarily use induction and is thus circular, Hilbert emphasized that finitistic metamathematics only uses limited contentual induction. This seems to imply that finitistic mathematics must be weaker than PRA with the unrestricted induction scheme. The standard formulations of PRA have hte induction scheme only for the quantifier-free formulas. It happens to be a logical fact, although a less known one, that, first Sigma^0_1 is conservative over PRA and second that Pi^0_1 is equivalent to Sigma^0_1 induction; therefore, if the induction scheme is restricted to contentual real statements, in Sigma^0_1, which would certainly be the most natural choice, one does not go beyond PRA.
Earlier it was generally thought that it is primarily Gödel’s second incompleteness theorem which challenged Hilbert’s program. But more recently a number of leading foundational thinkers:
What have we learned from Hilbert’s Second Problem? - Kreisel (1976) The Incompleteness Theorems - Smoryński (1977) Self Reference and Modal Logic - Smoryński (1985) Hilbert’s Programme - Smoryński (1988) Philosophical Aspects of Proof Theory - Prawitz (1981) Partial Realizations of Hilbert’s Program - Simpson (1988)
have claimed that even Gödel’s first theorem is enough to refute Hilbert’s program. Micheal Detlefsen, on the other hand, has argued vigorously against this interpretation.
Essentially, Detlefsen denies that the Hilbertian has to require that an ideal theory is a conservative extension of finitistic mathematics which is obviously impossible by Gödel’s first theorem.
More exactly, he argues that an argument based on Gödel’s first theorem must commit the Hilbertian to the assumption that an ideal theory decides every real sentence (real-completeness); without this assumption the conservation condition cannot, according to Detlefsen, be derived from the consistency. And the argument continues, the Hilbertian need not assume this. Deftlefsen concludes that the conservation condition is too strong and should be replaced by the weaker condition that an ideal theory is a consistent extension of finitistic mathematics, that is, one only requires that it does not prove any finitistically refutable real sentence. Raatikainen agrees with Detlefsen’s criticism of Prawitz and Smoryński but disagrees with his overall conclusions.
One could argue that the conservation condition can be derived from the consistency without requiring the real completeness of the ideal theory T.
Kreisel has proved a theorem that:
F: axiomatizable finitistic theory T: ideal theory
T entails phi => F + Conservative(T) entails phi (where phi is Sigma^0_1).
If F entails Conservative(T) as the Hilbertians arguably assume, this reduces to T entails Phi => F entails Phi. But this is just conservativity and moreover the real completeness of T is nowhere assumed!
However, the proof of this theorem depends essentially on the derivability conditions, which makes this theorem a relative of Gödel’s second theorem in being intensional. Hence it is somewhat problematic to appeal to it in arguing that even Gödel’s first theorem is sufficient to refute Hilbert’s program.
But, more importantly, Hilbert explicitly and repeatedly required that an ideal theory is conservative over finitistic mathematics for real sentences.
Hilbert in his 1926 work says that: “The modes of inference employing the infinite must be replaced generally by finite processes that have precisely the same results … That, then, is the purpose of my theory. Its aim is to endow mathematical method with the definitive reliability”. Note that Hilbert here both identifies reliability with conservativity and states that a proof of conservativity is the purpose of his theory.
Hilbert also insisted that a consistency proof entails this sort of conservativity. “If one succeeds in carrying out this proof [of consistency], then … this means that if a numerical statement that is finitistically interpretable is derived from it, then it is indeed correct every time”. Clearly “correct” here can only mean finitistic provability.
The same view is also expressed by Bernays:
[B]y recognizing the consistency of application of these postulates [of arithmetic], it is established at the same time that an intuitive proposition that is interpretable in the finitistic sense, which follows from them, can never contradict an intuitively recognizable fact. In the case of a finitistic proposition, however, the determination of its irrefutability is equivalent to determination of its truth.
To recapitulate: According to Hilbert, the consistency proof guarantees finitistic correctness of all finistically meaningful theorems provable by infinistic means, not just their non-refutability, as Detlefsen suggests. In various passages, Hilbert even straightforwardly presents the conservativity proof as the main aim of his proof theory.
Moreover, Hilbert viewed the expected consistency proof but an application of the more general conservativity property. That is, Hilbert was convinced that one can always eliminate, from a given proof of a real statement, all the applications of infinistic methods, and thus obtain a purely finitistic proof of the real statement. A canonical contradiction, e.g., 0 = 1, is a false statement. Therefore a hypothetical infinistic proof of contradiction could be in particular transformed to a finitistic proof of contradiction - but the latter was considered to be obviously impossible.
This part is not fully clear to me: Note, by the way, that precisely speaking, the idea here is to show that Cons(F) ⇒ Cons(T) (that is T ⊢ 0 = 1 ⇒ F ⊢ 0 = 1), not that F ⊢ Cons(T), as the popular view assumes. Accordingly, the relevant form of Gödel’s second theorem is not e.g. PA not⊢ Cons(PA), familiar from textbook presentations, and trivially Cons(PA) ⇒ Cons(PA), nor PRA not⊢ Cons(PA) etc. The point is rather e.g., Cons(PRA) not⇒ ConS(PA), Cons(PRA) not⇒ Cons(Z_2) etc.
In summary, Hilbert thought both that a consistency proof guarantees the conservativity of the ideal theory, and that the consistency is to be proved via conservativity, that is, the consistency proof allows one to eliminate ideal elements from a proof of a real sentence, and the consistency should be proved by showing that an ideal proof of inconsistency in particular could always be turned to a finitistic proof of inconsistency. Hence, consistency and conservativity were, for Hilbert, just two sides of the same coin. And in as much as the requirement of conservativity is essential to Hilbert’s program, the program is refuted already by Gödel’s first incompleteness theorem. Avoiding this conclusion requires at least some modifications in Hilbert’s original formulations.
More traditionally, it has been generally thought that Gödel’s second incompleteness theorem shows the impossibility of carrying through Hilbert’s program. But Micheal Detlefsen has argued that this is not the case.
Detlefsen’s considerations are based on certain sophisticated technical issues related to Gödel’s second theorem. Namely, unlike in Gödel’s first theorem, where it is enough that one has a predicate that extensionally represents provability, one must now require that the particular way one formalizes provability satisfies certain intensional extra conditions, most necessarily the so-called second derivability condition:
F ⊢ Prov_T(⌜ϕ⌝)→Prov_T(Prov_T(⌜ϕ⌝))
But there are various extensionally correct formalizations of provability which do not satisfy this condition. The earliest and most well known is Rosser’s provability predicate.
Detlefsen calls theories with such a notion of provability “consistency-minded theories”, and he suggests that the Hilbertian could well switch to such theories, and demonstrate their consistency in accordance to Hilbert’s program. These considerations are very interesting and highly relevant for the issue at stake here, but Raatikainen is not convinced that a Rosser-like consistency-minded approach can really be used to save Hilbert’s program from Gödel’s second theorem.
First, Hilbert did not aim at a consistency proof at any price: what he wanted was to justify, also in the infinite domains, the use of the simple laws of Aristotelian logic that “man has always used since he began to think”, “all the usual methods of mathematical inference”, “the usual modes of inference that we find in analysis” without which the construction of analysis is impossible.
Hilbert stated that “the fundamental idea” of his proof theory “is none other than to describe the activity of our understanding, to make a protocol of the rules according to which our thinking actually proceeds”.
In the light of such statements, Raatikainen thinks it would be quite totally against the spirit of this aim of Hilbert to gerrymander the notion of provability in order to obtain a “consistency proof”. Hilbert’s purpose was to justify just the ordinary laws of logic when applied to the infinite, not to devise some ad hoc logic (notion of provability) allowing an apparent consistency proof for the axioms of, say, analysis.
Second, every theory not containing a trivial, explicitly contradiction already at the level of axioms can be proved, even in PRA, to be Rosser-consistent. These theories include, for example, certain theories by Frege, Church, Quine, and Curry, that is, all the famous proposed foundational theories that have turned out to be inconsistent. Thus the resulting consistency predicate is not even extensionally correct. Therefore a consistency proof in terms of Rosserian consistency predicate has absolutely no vaule in securing the foundations of mathematics. It is very doubtful that such an empty victory would have satisfied Hilbert — and certainly it would not have convinced the Kroeneckerian and Brouwerian skeptics of the reliability of infinistic mathematics.
However, Raatikainen thinks that Detlefsen’s real point is, rather than to really claim that a Rosser-like consistency-minded approach should be used to rescue Hilbert’s program, to emphasize the fundamental but rarely noted fact that at the moment our understanding of the whole issue is seriously is incomplete. Here Raatikainen completely agrees. Namely, there is no conceptual analysis which shows that every natural notion of provability necessarily satisfies the derivability conditions. There is only some partial inductive evidence that the natural candidates suggested so far do, and that the few negative cases are clearly unnatural. What is badly needed is a conclusive analysis of the notion of provability in general, an analysis like Turing’s for the notion of effective computability, and consequently, something like the Church-Turing thesis for the concept of provability.
Further, Raatikainen thinks that Hilbert did not aim to prove finitistically just the consistency of some particular theory or a couple of chosen theories. It is plausible to think that he rather thought that finitistic mathematics is able to prove the consistency of any consistent theory. This expectation seems to be present in some statements of Hilbert: “[T]he development of mathematical science as a whole takes place in two ways that constantly alternate: on the one hand we derive new provable formulae from the axioms by formal inference; on the other, we adjoin new axioms and prove their consistency by contentual inference”.
But certainly this idea appears to be highly problematic, to put it mildly, for consistency is known to be as strongly undecidable as a Π⁰₁ property can be. That is, it is Π⁰₁-complete property, and every Π⁰₁ property can be reduced to it. Consequently, if finitistic mathematics would be able to prove the consistency of every consistent theory, it would be complete for all Π⁰₁-statements (and for all real statements) — under the plausible assumption that finitistic mathematics is effectively axiomatizable, this would contradict Gödel’s first theorem. This more abstract, recursion-theoretic way of viewing the matter also emphasizes the basic difficulty in Hilbert’s consistency program: Whatever puzzling technical details there are in Gödel’s second theorem, it is an unquestionable logical fact that no consistent effectively axiomatizable theory can prove the consistency of every consistent theory — this would also entail a decision procedure for the logical validity and contradict the classical undecidability theorem of Church and Turing.
Raatikainen adds in contradistinction to certain more charitable interpretations, that he thinks that Hilbert and most of his collaborators really expected there to be a decision method for the first-order logic. For, even if Hilbert did allow, in his 1900 talk on open problems, also a proof of the impossibility of solution as a possible settlement of a mathematical problem, this seems to apply only to a problem formulated in terms of some definite, restricted methods. But there simply was no definition of a general decision method in the 1920s. Moreover, the classical formulation of the Decision Problem by Hilbert and Ackermann, in 1928, strongly suggest that only a positive solution was expected: “The Decision Problem is solved when one knows a procedure which will permit one to decide, for any given logical expression, its validity or satisfiability … The Decision Problem must be considered the main problem of mathematical logic”.
There is a widely accepted, rather sophisticated logical explication of Hilbert’s program that is essentially due to Kreisel:
1958a: Hilbert’s Programme 1958b: Mathematical Significance of Consistency Proofs 1968: A Survey of Proof Theory 1976: What have we Learned from Hilbert’s Second Problem?
and endorsed by various distinguished logicians, e.g., by Feferman
1988: Hilbert’s Program Relativized: Proof-Theoretical and foundational Reductions 1994: ?
Sieg
1984: Foundations for Analysis and Proof Theory 1988: Hilbert’s Program Sixty Years Later 1990a: Relative Consistency and Accessible Domains 1999: Hilbert’s Programs: 1917–1922
Prawitz 1981: Philosophical Aspects of Proof Theory
Smorynski 1977: The Incompleteness Theorems 1985: Self-Reference and Modal Logic 1988: Hilbert’s Programme
Simpson 1988: Partial Realizations of Hilbert’s Program Kitcher 1976: Hilbert’s Epistemology Giaquinto 1983: Hilbert’s Philosophy of Mathematics
This interpretation relates Hilbert’s requirement of consistency proof closely to the soundness and conservativity properties. It is based essentially on the so-called reflection principles, which may be considered as a sort of soundness statements (“a provable sentence is true”). More exactly, reflection principles are instances of the scheme:
Prov_T(⌜ϕ⌝)→ϕ
Most closely related to Hilbert’s program is the reflection scheme that is restricted to Π⁰₁-sentences, in short, Π⁰₁-Ref. Under rather weak assumptions, it is the case that Π⁰₁-Ref and Cons(T) are equivalent. See e.g., Smorynski (1977)
Note, however, that whereas Cons(T) is a Π⁰₁ sentences, Ref is a scheme and not a particular sentences (instances of Π⁰₁-Ref and Π⁰₁ sentences). Note moreover — and apparently this has not been generally noted that — that the sentences expressing naturally the basic properties of being an extension of a theory and being conservative over another theory are not Π⁰₁ but only Π⁰₂ and thus ideal, not real sentences; more exactly these properties are expressed by forAll(x, thereExists(y, Prf_F(y,x) → thereExists(z, Prf_T(z,x)) and forAll(x, thereExists(y, Prf_t(y,x) → thereExists(z, Prf_F(z,x)) respectively.
Moreover, reflection principles allow one to eliminate ideal elements from a proof of real statements. For, assume that F ⊢ Prov_T(⌜ϕ⌝) → ϕ. If T ⊢ ϕ and Prov_T(x) formalizes (weakly represents) in F provability-in-T, then F ⊢ Prov_T(⌜ϕ⌝); by Modus Ponens, one obtains ϕ in F. This approach thus manages to explicate Hilbert’s claim that a finitistic consistency proof would also entail soundness and conservativity for all real statements. Note, however, that Hilbert’s program, thus viewed, is refuted by Gödel’s theorems.
This is certainly a very interesting rational reconstruction of Hilbert’s program. Nevertheless, Raatikainen thinks that it is somewhat anachronistic to attributed such sophisticated logical ideas to Hilbert. For, if such a line of thought really were behind his consistency program, one would certainly expect Hilbert to explain it in detail. But there is hardly any hint of such reasoning in Hilbert’s work. The only exception is Hilbertś relatively late discussion in his 1927 Hamburg address where there is indeed an informal sketch of the idea of how the consistency proof would allow one to eliminate the infinistic elements from a proof of a real sentence. This passage seems to be the only basis for the later logical interpretation.
But certainly, if Hilbert’s reasons were as ingenious as the later proof-theoretical tradition tends to interpret them, there would be more traces of it in Hilbert’s publications. And yet, for example in his paper ‘On the Infinite’ from 1926, which is the most extensive mature exposition of Hilbertś program, Hilbert simply stated that a proof of consistency amounts to real-soundness and real conservativity, without a word of explanation (the ideal “objects” here are just ideal statements):
#_BEGIN_QUOTE
For there is a condition, a single but absolutely necessary one, to which the use of the method of ideal elements is subject, and that is the proof of consistency; for, extension by the addition of ideals is legitimate only if no contradiction is thereby brought about in the old, narrower domain, that is, if the relations that result for the old objects whenever the ideal objects are eliminated are valid in the old domain.
#_END_QUOTE
It is important to note that the reflection principles etc. occur neither in this paper nor elsewhere in Hilbert’s writing (the first occurrence of anything like the reflection principles Raatikainen have been able to find in the literature is in Gödel’s paper on intuitionistic and modal logic in Einen Intepretation des intuitionistischen Assagenkalküls 1933).
Nicholas Rescher 13 pages
The paper says that Couturat held the view that extensional logic is the only correct one and hence his review of the system fell into the problem of finding Leibniz’ intensional approach defective.
Leibniz’ logic is said to be close to having a logistic system approach. In my mind, this is close to a syntactic treatment, where purely symbolic manipulation of the system leads us to do calculations.
- Variables are terms
- Singularly/binary operators on terms yielding terms
- Binary relations between terms, including equality
- Rule of inference
It is said that Leibniz possessed to an insufficient extent the distinction between object and metalanguage.
But he distinguishes between verae propositions, i.e. assertions of the system and principiae calculi i.e., rules for obtaining further assertions from given ones.
Leibniz’ original definition: “Eadem sunt quorum unum in alterius locum subtitui potst, salve veritate” i. Equality is obtained between term-denoting complexes iff they are inter-substitutable in asserted statements.
Authors say that Leibniz’ classic definition of equality is defective with respect to distinction of use/mention and object/meta-language. I doubt this claim and has a feeling that Leibniz’ conception could be different from the current object/metalanguage distinction in vogue. That is not a claim that Leibniz is infallible, but in many significant cases, such claims of defects results from an aberration in the viewpoint of authors interpreting the work than the source work.
ii. In any asserted statement involving some term-variable this may be replaced throughout by another term-variable, or by some other term-denoting complex, and the result will again be an asserted statement.
iii. The modus ponens rule
Leibniz is said to not have provided an adequate statement of this rule.
Proposition vera ~ Asserted statement If it is an implication, it is a consequentia
- A group of asserted statements which provides the axiomatic basis for the system
Leibniz constructed 3 different logical systems
System in Specimen calculi universalis / Ad specimen calculi universalis 248526343_Minds_machines_and_economic_agents_Cambridge_receptions_of_Boole_and_Babbage
- a est A
- a = non-non-A
- a est b iff non-b est non-A
- If a est b and b est c, then a est C
- a est b and b est a iff a = b
- a ≠ b iff not a = b
- a non est b iff not a est b
- If a = b, then b = a
- If a = b, b = c, then a = c
- a = aa
- ab = ba
- a est bc iff a est b and a est c
- If a est b, then ca est cb
- If b est a and c est a, then bc est a (this is said to be wrong on Couturat’s interpretation)
- If a est b and c est d, then ac est bd
- ab est a
- ab est b
- If a is proper: a non est non-a
- If a is proper: If a est non-b then a non est b
Leibniz does not always state the propriety condition explicitly. He indicates in his writings that he understands the traditional categorical propositions always contain the tacit assumption that the terms which enter are proper.
Set theoretical interpretation
Terms ~ Sets non ~ Complementation Juxtaposition ~ intersection est ~ inclusion Propriety ~ non-nullity
TODO: How is Leibniz’ logic related to modern class logic a la Boole?
One interpretation given by Leibniz for this system is obtained by letting “terms” be predicates taken in intension, i.e., properties. The result of operating on a “term” (property) by non is the property of not having the property in question — non represents the negatio or negation of properties. The result of juxtaposing two terms is the property of possessing both of the properties in question — juxtaposition represents the additio or conjunction, the joining of properties.
A term/property is proper if it is not of universal comprehension (i.e., null extension).
Finally, the result of linking two “term” names by ‘est’ is the statement that the former property contains the latter in its intension or comprehension. Thus ‘a est b’ symbolizes the universal affirmative proposition that whatever is characterized by the property a is also characterized by the property b, i.e., that all a’s are b’s.
A second interpretation is given by Leibniz for this system. This is obtained by letting terms be predicates taken in extension, i.e., classes. The result of operating on a “term”/class by non is the class of all objects not belonging to the class in question. The result of juxtaposing terms is the class of all objects belonging to both of the classes in question. A term/property is proper if it is not of null extension / universal comprehension.
Finally a est b symbolizes the universal affirmative proposition that all a’s are b. That is all extensions of class a are contained in class b.
It is plain that in these two interpretations of his first system Leibniz treats adjectives / property names and subtantives / class names in a dual fashion. He justifies this by remarking that to any adjectival property such as (is an) animal, there is a corresponding substantival class, in this case, the animals. And he asserts that as regards symbolic treatment the distinction between these is irrelevant. By exploiting this duality of property intension / class extension Leibniz is able to provide a twin-interpretation for his first system of logical calculus and so to develop its possibilities of interpretation.
In the first system, Leibniz is able to treat the entire classical doctrine of categorical propositions. Thus, S a P, S e P, S i P, and S o P are rendered (in either interpretation) as S est P, S est non_P, S non est non-P, and S non est P, respectively.
The symbolic version of the entire classical theory of immediate inference and the syllogism is available in the assertions of the system. It is at this point that the propriety condition acquires significance. The assertions which guarantee the validity of two of the classical modes of inference, subalternation and partial conversion are dependent on the propriety of the terms involved. And Leibniz is throughout all of his logical work concerned to preserve the validity of the entire classical theory of immediate inference and of the syllogism.
Leibniz’s second system was developed in the 1685–6 period during which his metaphysical system assumed its final and completed form. This system played a central role in Leibniz’ solution of a logical problem o which he felt the progress of his metaphysics to depend: the problem of reconciling his belief that there are true, contingent propositions with his conviction that all true propositions are analytic.
This system is an extension of the first as it includes all those of the first system but with notational changes.
A new element, the term-constant Ens or Res is introduced.
Propriety is given by the definition: A is proper iff A non est non-Ens.
- If A is proper: A est B iff AB = A
- If A non est non-Ens, then A est Ens
- A est non-Ens iff A non est Ens
- If A is proper: A est B iff A non-B est non-Ens
- If A est Bnon-B, then A est non-Ens
A est B is A = non-Ens or A ⊂ B & AB = non-Ens (Verify)
Interpretations of the classical theory of immediate inference and of the syllogism:
| a: Snon-P est non-Ens | S est P | SP = S |
| e: SP est non-Ens | S est non-P | SP ≠ SPEns |
| i: SP est Ens | S non est non-P | SP = SPEns |
| o: Snon-P est Ens | S non est P | SP ≠ S |
Leibniz employs only the usage of continet for est when dealing with the intensional interpretation, which is quite proper since the fact that A contains B in its intension or comprehension — i.e., that all A’s are B’s — is represented by “A est B.’ On the other hand, if est is to be intrepreted in terms of containment in the extensional interpretation, then “A st B” must be read “A is contained in B,” or else, if est is to be read as “contains,” then A and B must be interchanged. This is explicitly stated by Leibniz in several places. It has been misconstrued as being a statement on Leibniz’s part to the effect that “A est B” may be taken as symbolizing “A contains B (in extension)”, and thus as stating in an extensional interpretation of the system, or rather more accurately, it could be correct only if juxtaposition were to represent alternation (i.e., set union or addition), where it is uniformly and consistently used by Leibniz to represent conjunction (i.e., set intersection or multiplication). Couturat is guilty of this misconstruction, and on this basis he accuses Leibniz of falling into error by misguided adherance to an intensional point of view. The purported error in question is that Leibniz fails, because of intensional prejudice, to take juxtaposition as extensional — rather than intensional — union or addition.
Leibniz offers still another interpretation of this second system, one which makes it the forerunner of C. I. Lewis’s systems of strict implication. In this interpretation “terms” are propositions, non represents negation, juxtaposition represents conjunction, and est stands for the relation of entailment. Ens represents logical necessity or logical truth, and so propriety is logical consistency. Leibniz rightly views this system, thus interpreted, as modal logic, and thus merits Lewis’s estimation of him as a precursor.
In this interpretation, and in it alone, the result of linking terms (propositions) by est is again a term. Thus formulas such as (A est B) est (C est D) are meaningful in this interpretation.
Leibniz’s third and final system of logical calculus was developed in 1690. The writer conjectures that the motivating force underlying its development was Leibniz’s growing conviction that the notions of part, whole, and containment are the fundamental concepts of logic.
Its principal expositions are the tract De formae logicae comprobatione per linearum ductus, as well as several brief, untitled essays reproduced in the seventh volume of Gerhardt’s edition of Leibniz’s philosophical works.
N (sometimes Nihil) is a term-constant. non is a singularly term-operator, + (sometimes ⊕) and - (sometimes ∵) are binary term-operators. A inest B is an alternative form of A est in B or B continnt A. The notation for = is ∞ or half ∞ and for A ≠ B Leibniz uses non A ∞ B. There is also A ⌅ B and its negate A ∧ B, where A ⌅ B is written “communicant A et B” or “communicantia sunt A et B” or “compatibilia sunt A t B”.
Assertions of this system:
Group I: Assertions 1 through 9 of the first system, with “inest” in place of “est”. Group II: 25. A = A + A
- A + B = B +A
- (A + B) + C = A + (B + C) { This is not written down explicitly by Leibniz and he uses it without brackets. }
- IF A inest B and C inest B, then A + C inest B
- If A inest B, then C + A inest C + B
- If A inest B and C inest D, then A + C inest B + D
- A inest B iff B + A = B
- A ∧ B iff not A ⌅ B
- A ∧ B iff B ∧ A
- A ∧ B iff A inest non-B
- A ⌅ b iff there is a C, C ≠ N, such that C inest A and C inest B
- A - B = C iff A = B + C and C ∧ B
- A - B ∧ B
- A - A = N
- A + N = A
- N inest A.
The consistency of this system follows from the existence of the following interpretation: Let “terms” be classes, N the null class, non complementation, + class union, inest class inclusion, and let ⌅, ∧, and - be defined by 35, 32, and 36, respectively.
Leibniz explicitly intends this system to provide an abstract theory of containment. Given a sound application of the concepts of whole and of part, an interpretation of this third system is, Leibniz claims, available. For if such a notion of containing is given, then “A inest B” can be taken to represent “B contains A (in the sense in question),” “non-A” represents that containing everything not contained in A, N is that which contains nothing, A + B contains everything contained in A or in B or both, and all else may be interpreted correspondingly.
In this system, extensionally: a: S inest P e: S ∧ P i: S ⌅ P o: S non inest P
intensionally: a: P inest S e: P ∧ S i: P ⌅ S o: P non inest S
Again, the classical theory of immediate inference and the syllogism is available in the assertions of the system. However, assertion 35 is required both for subalternation and partial conversion, and so both of these inferences must be conjoined with an explicit statement of the non-nullity of the terms involved. In this feature of explicitness, together with its more abstract and general nature, resides the superiority of Leibniz’s third system over the first two.
If Leibniz’s logical calculi do not posses the symmetry and elegance of later algebras of logic it is not because of his intensional conception of logic, but because his greater commitment to traditional logic inclines him to weigh more heavily the logical, rather than algebraic, considerations.
Nicholas Rescher 3 pages
A short piece on how Alonzo Church influenced Rescher’s career
Francis Heylighen 1990
Complexity as the combination of distinction and connection. A formal concept reformulating closure in a relational language based on connections is introduced allowing to reduce low level internal distinctions and highlight high level external distincitons in a network of connections, thus diminishing the complexity of the description.
- Complexity and Distinction-Making
Current definitions of complexity are quantitative in nature. Heylighen goes to the etymological root of complexus = entwined / twisted together to create a definition.
Complexity’s definition given has two aspects: distinction and connection.
Distinction corresponds to variety, to heterogeneity, to the fact that different parts of the complex behave differentl. Connection corresponds to relational constraint, to redundancy, to the fact that different parts are not independent, but that the knowledge of one part allows to determine features of the other parts.
Distinction in the limit leads to disorder and entropy, connection leads to order and negentropy. Complexity can only exist if both aspects are present: neither perfect disorder (statistically studies under law of large numbers) nor perfect order (studied under traditional deterministic methods) are really complex. A provisional quantitative definition of complexity might express this as the product of variety (or entropy which corresponds roughly to the logarithm of variety) with redundancy R (corresponding to the difference between actual variety of entropy, and maximum potential variety). C = V . R where R = Vmax - V C = 0 when V = Vmax { Maximum Variety } C = 0 when V = 0 { Minimum Variety / Total order }
Complexity reaches a maximum when R = V V is a measure of distinction and R of connection
V is an observer dependent factor.
In thermodynamics, V is thermodynamical entropy. For a strange attractor, it might represent fractal dimension. Finite state automaton, the number of different states reachable.
What might look like a variety on a micro level may become a redundancy on macro level.
The complexity of the description will depend on how many distinctions the observer makes, and on how many connections exist between these distinctions.
A model with adequate complexity will be one which is complex enough so that all the properties of teh system relevant to the problem are included, yet minimally complex so as to simplify the problem-solving process.
- Definitionsl of Closure
C: A -> A* with monotonicity, idempotence, inclusion preservation
A set is called closed if A* = A
In cybernetics, a system is said to be organizationally closed if its internal processes produce its own organization, thus continuously rebuilding the system’s identity in a changing environment. The connotation is that of a cyclical, self-referential, self-producing process.
Concept of closure of an algebraic system of transformations:
ForAll(f, g) in F, f o g in F ForAll(a in A, f in F), f(a) in A
If A represents the state space of a system, and F its dynamical processes, then the closure of the system means that the state space is invariant under the internal dynamics.
This representation allows for representing A and F by using recursive starting elements F0 and A0.
The system (A, F) is organizationally closed in the sense that its organization, defined by the set A and teh agebra F with composition as binary operation, is maintained or (re)produced under the application of its internal processes, defined by the transformations f in F.
Closure allows to make a more sharp separation between the inside of a system and its outside or environment.
A can be considered as the closure of some A0 subset of A: A0* = A, equivalently F0* = F. What we achieve by adding the missing elements to (A0, F0) is that all internal processes and structures stay within the system, they can no longer produce elements outside of it.
In the open system, it is possible to transgress the boundary between inside and outside, in the closed system it is not. Hence this boundary becomes an important feature to ditinguish the system (A, F) from its environment in a meaningful way, rather than by an arbitrary convention.
Intuitively, the idea of a closed system as one which you cannot leave or entery from the outside may be generalized to a system whose inside elements cannot be individually distiguished from the outside. Thugh the inside as a whole can be distinguished from the outside. In other words, the inside-outside distinction becomes more important, more invariant, since it can be perceived from all points of view, while the distinction between the inside elements, can only be perceived from the inside itself. Hence closure would be a means of highlighting or singling out distinction between elements of a class and its complement while ignoring other distinctions (eg, the one between a1 in A and a2 in A), thus preferring class A to any other subclass (e.g. A0) of the whole of all elements under consideration.
The simplest way to formulate this is using an equivalence relation E, expressing the lack of external distinction between elements of A.
ForAll(a1, a2 in A), a1 E a2, but forAll(a in A, b not in A, not(a E b))
Think this is much like an abstraction, where if you say children, all children under a parent becomes equivalent under that abstraction. There is no external distinction between them. But internally, the children could be different and this will be represented by their equivalence class.
The closed set A is an equivalence class of relation E and the distinction induced by closure correspond to the partition of the initial universe of discourse U by E.
- Closure in a Relational Language
Instead of starting from a set A with an algebra F, it can be constructed by usin ga set S of “connections”, meaning elements which are defined by the other elements they are connected to.
Connections can be represented by means of a directed graph consisting of nodes (similar to the elements of the set A) and arrows (similar to transformatinos in F mapping elements of A onto elements of A) connecting the nodes. The nodes can also be viewed as connections between the arrows, so that at the lowest level there is no real distinction between node and arrow elements. This is like in category theory where objects are merely a special kind of identity morphisms.
A connection a -> b can be instantiated by a node or connecting element c: a -> b => thereExists(c, such that a -> , c -> b) The inverse implication is only true if there is no branching between a and c (and equivalently c and b). That is, there is no intermediary d such that a -> d, but not d -> c or c -> d.
The rationale for this relational/structural language is to have a representatino system without primitive level, i.e., a level consisting of the elements out of which all the other elements or structures are generated. The system is bootstrapping: each element is determined by the other elements. This can be expressed formally by introducing the input and output set of an element:
I[a] = { c in S | c -> a } and O[a] = { c in S | a in c }
a is then completely determined or defined by (I, O): forAll(a, b in S): (I[a], O[a]) = (I[b], O[b]) => a = b
This axiom allows to formulate a relationship between distinction and connection: two elements a and b are distinct iff they are connected to distinct elements.
This definition is bootstrapping because the distinct elements in I[a] and I[b] are of course themselves only distiguished by virtue of their own connections with distinct elements, including the original a and b. It is not recursive in the conventional sense, because there is no privileged starting set whose elements are used to generate the distinctions between the other elements. Remark also that empty input and output sets cannot be distinguished at all.
Ontological interpretatino: You can only discern something by relating it to something else. Operationally it means that you cannot observe or measure some property without letting the system you observe interact with some other sytsem (your measuring instrument) and comparing the results of that interaciton with other results (your standards).
the postulated identity of a and b is a special case of an equivalence relation. In this sense a and b taken together in one class is a kind of primitive closure operation, defining distinctions of the lowest order. Next the way to distinguish higher order distinctions are touched upon:
We would like to derive another, smaller or simpler set of connections which could replace the lower order one, without any loss of relevant information. What allows us to do this is that A does not consist of independent elements, but of elements in relation, that is to say that there is in general some kind of constraint or redundancy involved.
Not sure why it is said that there is a constraint or redundancy involved.
The set A can be represented as a relation on a set of nodes. IF this relation is transitive and symmetric, then it defines an equivalence relation partitioning the nodes into distinct subclasses. This is the most perfect kind of closure we could imagine. By weakening the requirements defining an equivalence class, we may try to generate “less perfect” types of closure which however still determine essential redundancies. Obvious candidates are relations which are just transitively closed, but not symmetrically, or vice-versa.
By specifying a symmetric relation we can reduce the redundancy that can be obtained by using the fact that it is symmeetricall closed. This means that it is not necessary to give all the inverse connections and can be automatically added to it by using the closure operation.
Relational closure in a network S of connections means that a subnetwork or subrelation A subset of S contains all the connnections which commplement the connections in some non-closed subset A0 in A, so that the knowledge of A0, together with the closure operation, determines A completely. Moreover, the closure of A signifies the internal structure of A becomes less distinct, in the sense that it is no longer nnecessary to explicitly make certain distinctions. For example, if A is symmetrically closed, it is not necessary to distinguish between a closure in one direction and a closure in the inverse direction, since you know that once you have the one, you automatically have the other one. In a transitively closed network, you do not have to distinguish between a simple connection and a path of subsequent connections, because each path has an associated simple connection. Because of the diminished internal distinguishability the closed network as a whole will be more sharply distinguished from its background or environment, thus forming a gestalt.
The absence of all possible connections is similar to the presence of all possible connections: both determine an equivalence relation preventing to make any distinction. Analogously, the absence of a certain type of connections will have a similar, distinction reducing effect as the presence of all connections of that type.
Antitransitive closure as Transitive kernel or complement of a closure.
The type of connections which are present/absent may be defined by what they are connected to, hence, depends upon the point of view from which distinctions are made.
O[a] = { c } I[a] = { d, e } O[b] = { c } I[b] = { s, l }
a and b are absolutely distinct but indistinguishable from teh point of view of their input c alone.
Different types of closures may be recursively combined, generating other types of closure. Transitive and symmetric closure together define equivalence closure. Fourth, certain types of closure may be seen as generalizations or specialization of other types of closure, in the sense that a more general closure is characterized by less strict requirements, and hence is less distinction-reducing or redundancy-generating. For example, a symmetric closure is a specialization of cyclical closure, defined as a connection network where each connection a has an inverse path of connections, forming a cycle leading back to the starting connection. The associated distinction-reduction is that which makes it impossible to distinguish whether a connection in a cyclically closed network comes “before” or “after” another one.
Starting from a few elementary closures, new closure types can be generated by specialization, generalization, complementation, combination and restriction of point of view.
All essential mathematical structures, such as partitions, partial or linear orderings, functions, hierarchies, symmetries, can be reconstructed as combinations of elementary closures.
The closure we will choose will be the one which eliminates the maximum of distinctions. Hence we will prefer more specialized closures (equivalence) to more general ones (cyclical closure), and large ones (involving large set of connections) to small ones. As to the point of view, this is determined by the objective noe has in mind while solving the problem. In a problem representation, distinctions can be ordered hierarchically in a sequence leading from ends to means.
The distinctions higher in the hierarchy will determine the prieleged point of view from which lower-order structures may or may not be distingushed.
For example, it is useless to distinguish between means which have the same effect on the ends one tries to achieve.
French “logique” and British “logic”: On the origins of Augustus De Morgan’s early logical inquiries, 1805 – 1835
The Influence of Aristotelian Logic on Boole’s Philosophy of Logic: The Reduction of Hypotheticals to Categoricals
TODO: Correct URL
Enrique Casanovas
Roy T. Cook
Jesse Endo Jenks
Aaron Sloman
Lauren Richardson
Jean-Yves Bèziau
Tarcísio Penqueno, Jean-Yves Bèziau
John Alison
Sean Coyle
María José Frápolli and Stavros Assimakopoulos
Corine Besson
P. F. Strawson
Wagner de Campos Sanz, Thomas Piecha
Johan van Benthem
Sebastian Georg Werner Speitel Advisor: Gila G. Sher
Notes on Per Martin Löf’s “On the Meanings of the Logical Constants and the Justifications of the Logical Laws”
Joseph Abrahamson
Kosta Došen
Judson Webb
Göran Sundholm
Mario Gómez-Torrente
Gilbert Harman
Christopher Peacocke
J. Hintikka, 1980
T. Smiley, 1994
J, Sagüillo (1999)
Parry (1965)
T. Smiley (1962)
T. Smiley (1973)
Tara R. Abraham (2002)
D. S. Hoffman (2015)
The First Computational Theory of Mind and Brain: A Close Look at McCulloch and Pitts’s “Logical Activity Calculus of Ideas Immanent in Nervous Activity”
Gualtiero Piccinini (2004)
Paul Raatikainen
Wilfred Sieg
12 pages
Roman Murawski (2002)
17 pages
Richard Zach
43 Pages
Wilfried Sieg
39 pages
Andrea Reichenberger
34 Pages
Check if there is more content in the newer versions
Saul A. Kripke
15 pages
Michael Rathjen
31 pages
Technical with details on Martin-Löf’s work
From the Outside Looking In: Can mathematical certainty be secured without being mathematically certain that it has been? (2019)
Matthew Souba
260 pages
Dissertation on Hilbert’s Program.
TODO: I have to research if there are other dissertations like this one.
Giorgio Venturi
27 pages
Leopoldo Bertossi
Slideset
Leo Corry
98 pages
José Ferreirós
41 pages
Giorgio Venturi
34 pages
Stephen Simpson
22 pages
Georg Kreisel
27 Pages
M. Detlefsen
Volker Peckhaus (2000)
17 Pages
José Ferreirós
Ernst Snapper (1979)
J. F. Fries’ Philosophy of Science, the New Friesian School and the Berlin Group: On Divergent scientific philosophies, difficult relations and missed opportunities
Helmut Pulte
Jeremy Avigad and Erich H. Reck
Erich H. Reck (2004)
Which arithmeticisation for which logicism? Russell on relations and quantities in The Principles of Mathematics
Sébastian Gandon 17 July 2008
Sara L. Uckelman August 2021
W. W. Tait
Gregory H. Moore
Gregory H. Moore
John Travis Shrontz
Ansten Klev (2011)
S. M. Bhave
Philip A. Ebert and Marcus Rossberg
José Ferreirós 26 Pages
Hourya Benis-Sinaceur, Marco Panza, Gabriel Sandu
Yuri Manin
A. R. D. Mathias
Haskell Curry (1954)
Laura Fontanella (2019)
Goldfarb
Poincaré on the foundations of arithmetic and geometry. Part 1: Against “Dependency-Hierarchy” interpretations
Katherine Dunlop (2016)
Katherine Dunlop (2017)
Stathis Psillos
José Ferreirós
Reeve Garrett
The “Science of Numbers” in action in Richard Dedekind’s works: between mathematical explorations and foundational investigations
Emmylou Haffner (2014) 562 pages
Steht es Alles Wirklich Schon Bei Dedekind? Ideals and Factorization Between Dedekind and Noether (2017)
Leo Corry 19 pages
José Ferreirós
Irrational Philosophy? Kronecker’s Constructive Philosophy and Finding the Real Roots of a Polynomial (2021)
Richard B. Schneider
Israel Kleiner
Harold M. Edwards
Janet Heine Barnett
Janet Heine Barnett
Emmylou Haffner (December 2018)
TODO: Add works on Aristotle by Corcoran