Intensional and Extensional Semantics in Programming Languages and Type Theory
The subtitle of this post is "What is a proof and of what is a proof a proof?".
Recently Thomas Forster wrote that he had been revising his SEP entry on NF. (There is apparently some excitement about a surprising theorem that it recently proved, something to do with failure of well-ordered choice). See Quine’s New Foundations by Thomas Forster. In the 11 page 1937 American Mathematical Monthly paper where he introduced the theory, Quine opens with:
In Whitehead and Russell's Principia Mathematica we have good evidence that all mathematics is translatable into logic. But this calls for the elucidation of three terms: translation, mathematics, and logic. The units of translation are statements; also statement forms, i.e., expressions abstracted from statements by supplanting constants by variables. Thus it is not held that every symbol or combination of symbols of mathematics, say "Δ" or "d/dx," can be equated directly to an expression of logic. But it is held that every such expression can be translated in context, i.e., that all statements and statement forms containing such an expression can be systematically translated into other statements and statement forms which lack the expression in question and contain no new expressions beyond those of logic. These other statements and statement forms will be translations of the original ones in the sense of agreeing with them in point of truth or falsehood for all values of the variables.
Given such contextual translatability of all mathematical signs, it follows that every statement or statement form consisting solely of logical and mathematical notation is translatable into a statement or statement form consisting solely of logical notation. In particular, thus, all principles of mathematics reduce to principles of logic – or to principles, at least, whose formulation needs no extra-logical vocabulary. [footnote: For a fuller account, he references W. V. Quine, Philosophical Essays for A. N. Whitehead (0. H. Lee, editor), pp. 90-102].
After clarifying that what he means by 'mathematics' here is essentially everything formalised in Principia Mathematica including Geometry as far as it follows from algebraic analytic geometry, he goes on:
It must be admitted that the logic which generates all this is a more powerful engine than the one provided by Aristotle. The foundations of the Principia are obscured by the notion of propositional function, but, if we suppress these functions in favor of the classes and relations which they parallel, we find a three-fold logic of propositions, classes, and relations. The primitive notions in terms of which these calculi are ultimately expressed are not standard notions of traditional logic; still they are of a kind which one would not hesitate to classify as logical.
He goes on to define a very simple system of logic with only three elements: a membership relation, a binary logical operator and universal quantification. Then he produces rules of abbreviation which allow him to express all the logical operations appearing in Principia Mathematica in a very economical way, using Carnap's idea of a syntax language with variables standing for expressions in terms of which the abbreviations comprising the translation are written. This system is enough to express the Russell paradox and then Quine can explain stratification, the syntactic means by which Whitehead and Russell eliminated the possibility of expression of syntactic antinomies. He then goes on to show how one small modification to the rule of abstraction, limiting its use to stratified formulae, makes it impossible to express the Russell paradox.
Although Quine is writing well after the publication (over a decade earlier) of Ramsey's The Foundations of Mathematics, he makes no mention of the suggestions made therein concerning the superfluity of the axiom of reducibility in regard to the 'group B' paradoxes of Principia Mathematica, which result in the so-called Simple Theory of Types. See § 4.1.2 o the SEP article on Principia Mathematica. Quine's objections to the theory of types concern its stratification of the variables:
But the theory of types has unnatural and inconvenient consequences. Because the theory allows a class to have members only of uniform type, the universal class V gives way to an infinite series of quasi-universal classes, one for each type. The negation -x ceases to comprise all non-members of x, and comes to comprise only those non-members of x which are next lower in type than x. Even the null class Λ gives way to an infinite series of null classes. The Boolean class algebra no longer applies to classes in general, but is reproduced rather within each type. The same is true of the calculus of relations. Even arithmetic, when introduced by definitions on the basis of logic, proves to be subject to the same reduplication. Thus the numbers cease to be unique; a new 0 appears for each type, likewise a new 1, and so on, just as in the case of V and Λ. Not only are all these cleavages and reduplications intuitively repugnant, but they call continually for more or less elaborate technical manoeuvres by way of restoring severed connections.
I recently found the paper A type-theoretical alternative to ISWIM, CUCH, OWHY by Dana S. Scott. This was written in 1969 and widely circulated as an unpublished manuscript until 1993. The reason was that shortly after writing it Scott was embarrassed to discover a denotational model for the untyped lambda calculus (something he had until then considered implausible) and so models of the simply typed lambda calculus became somewhat devalued, but many people had found the approach to computable functions practically fruitful and it inspired LCF and many other developments in automated theorem proving. (See About Logic - Interview with Dana Scott). In this paper Scott voices the opinion that it is only a matter of luck that Quine's NF had so far not been proven inconsistent. This appears right in the first paragraph of the introduction:
No matter how much wishful thinking we do, the theory of types is here to stay. There is no other way to make sense of the foundations of mathematics. Russell (with the help of Ramsey) had the right idea, and Curry and Quine are very lucky that their unmotivated formalistic systems are not inconsistent.’
And he added a footnote in the 1993 publication that he still believed that Russell and Ramsey's is the right idea and that if the 'unmotivated formalistic systems' of Curry and Quine are not inconsistent then it is just through good luck. Nowadays it would be hard to support the claim that things turned out otherwise — type theories are everywhere — but whether they are all the same sort of theory Scott was thinking of in 1969 seems rather doubtful to me. What is at stake is not just a matter of fashion in mathematics and logic, it goes much deeper, I think. It is about what constitutes a meaningful mathematical statement.
To put Quine's contribution in context, it was written in 1936, the same year as Church's An Unsolvable Problem of Elementary Number Theory and Turing's On Computable Numbers with an Application to the Entscheidungsproblem.
With regard to the latter, it is interesting to read Alonzo Church's Review: On Computable Numbers, with an Application to the Entscheidungsproblem by A. M. Turing published in The Journal of Symbolic Logic, Vol. 2, No. 1 (Mar., 1937), pp. 42-43 (2 pages).
Here is the final paragraph of the latter, to which Church refers in his criticism:
Cf. [Alonzo Church, An unsolvable problem of elementary number theory, American Journal of Mathematics, vol. 58 (1936)], pp. 346, 356-358. Actually the work already done by Church and others carries this identification considerably beyond the working hypothesis stage. But to mask this identification under a definition hides the fact that a fundamental discovery in the limitations of the mathematicizing power of Homo Sapiens has been made and blinds us to the need of its continual verification.
I have found the distinction between meaning and denotation puzzling, ever since I was first exposed to the idea of Tarski's Semantic Definition of Truth which was part of a Discrete Maths course that Glynn Winskel lectured for second-year Computer Science undergraduates at Cambridge. Tarski's idea was to define truth-in-some-domain in terms of the meaning of logical sentences one could form about elements of that domain. (See § 1.4.2 Models, on page 22 of the notes). This "meaning" is just a simple truth value, so in this framework, one says that the denotation of a logical sentence is simply its truth value. This attitude to semantics is widely considered to have begun with Frege who was a contemporary of Cantor and was writing around the same time (1874-1884).
In any such structural semantic interpretation of a language, what it is we translate the language into, i.e. whatever is the meaning we endow to its sentences, depends entirely on the metalanguage we use to describe the translation. So the answer to the question as to what a sentence means must be in the most general sense "whatever it is we said!" But there is surely no harm in saying "But what precisely did we mean when we said that?" and so we can set out to refine our metalanguage and endow it too with an interpretation, and this extra precision will hopefully allow us to say more about the properties of, say, proof systems which we may use to formally prove theorems in that language. This seems to me to have been Quine's explicit intent in NF.
Saul Kripke on Non-standard Models and Gödel's theorem. Talk recorded in 2012 at the 70th birthday celebration of Melvin Fitting, who wrote the Stanford Encyclopedia of Philosophy entry on Intensional Logic.
Saul Kripke died in September 2022, while I was in a jail in Arizona. That was around the time Queen Elizabeth II died, but nobody told me about Kripke.
Subscribe to Yegor Bryukhov (Егор Брюхов).
See also A Well Ordering Is A Consistent Choice Function and Rethinking set theory by Tom Leinster.
On interpretations of models: Mathematical Objects arising from Equivalence Relations, and their Implementation in Quine’s NF by Thomas Forster.
Halls of Mirrors in Scheme: see Intensions and Extensions in a Reflective Tower by Olivier Danvy & Karoline Malmkjær.
By some amazing coincidence, the Topos Institute colloquium talk today was this one:
15:11 I had never heard of pragmatics before, but this sounds like a serious attempt to deal with the phenomena of interference in representation that Jenann Ismael describes.
See Reasons for Logic, Logic for Reasons Pragmatics, Semantics, and Conceptual Roles
By Ulf Hlobil and Robert B. Brandom. Here is a review, by John Horty, of the book.
Here are the slides.
Subscribe to Topos Institute.
Comments
Post a Comment