Quotes
A Klee painting named ‘Angelus Novus’ shows an angel looking as though he is about to move away from something he is fixedly contemplating. His eyes are staring, his mouth is open, his wings are spread. This is how one pictures the angel of history. His face is turned toward the past. Where we perceive a chain of events, he sees one single catastrophe which keeps piling wreckage and hurls it in front of his feet. The angel would like to stay, awaken the dead, and make whole what has been smashed. But a storm is blowing in from Paradise; it has got caught in his wings with such a violence that the angel can no longer close them. The storm irresistibly propels him into the future to which his back is turned, while the pile of debris before him grows skyward. This storm is what we call progress.
— Walter Benjamin, Theses on the Concept of History (Thesis IX).
Everything turns on grasping and expressing the True, not only as Substance, but equally as Subject.
— Georg Wilhelm Friedrich Hegel, The Phenomenology of Spirit (§17).
So, summing up our opinion about this tradition {the “syntactic” tradition}, it is always in search of its fundamental concepts, which is to say, an operational distinction between sense and syntax. Or to put these things more concretely, it aims to find deep geometrical invariants of syntax: therein is to be found the sense.
— Jean-Yves Girard, Proofs and Types (1.1.2).
Roughly, the “syntactic” tradition starts with the proof-theoretic tradition of logic descending from Gentzen. In programming languages, it largely pertains to type theory in static semantics and operational semantics in dynamic semantics. It is all about, as the name suggests, syntax — but it is more accurate to say the syntax of proof than the syntax of propositions (though they are of course intimately related). On the other hand, the “algebraic” tradition is about semantics in the sense of models — interpreting syntax into constructs which are “conceptual” or “fundamental”: hence, model theory of course belongs here, as does denotational semantics — but so does abstract interpretation / dataflow on the side of static semantics.
There is an interesting parallel in philosophy drawn up by Rorty between inferentialists and representationalists. “Algebraic” are exemplars of latter-day representationalists. However, representationalism is taken by Rorty to have dominated the tradition since Descartes, though, so there are plenty of others besides. Representationalism is associated, like the “algebraic” tradition, with semantics. Inferentialism, on the other hand, is associated with pragmatics — Wittgenstein, Austin, Sellars, and many a continental philosopher (including of course Hegel) go in this bucket. But inferentialism and the “syntactic” tradition are allied — how can this be? Syntax seems even more abstract than semantics. This is why I say that the “syntactic” tradition pertains to the syntax of proof and not of propositions — the dynamics of use and not of the mere construction of propositions.
Knowledge is inseparable from a social practice — the practice of justifying one’s assertions to one’s fellow-humans. It is not presupposed by this practice, but comes into being along with it.
— Richard Rorty, Introduction to Empiricism and the Philosophy of Mind (pg. 4).
For we want already to build the Kingdom of Heaven while we are still here on Earth.
— Heinrich Heine, Germany, a Winter’s Tale (Caput 1).
There is no way out of entanglement. The only responsible course is to deny oneself the ideological misuse of one’s own existence, and for the rest to conduct oneself in private as modestly, unobtrusively and unpretentiously as is required, no longer by good upbringing, but by the shame that in hell, there is still air to breathe.
— Theodor Adorno, Minima Moralia, Antithesis.
The envisaged third phase of Geist is a form of life exhibiting the practical recognitive normative structure of expressive recollection: forgiveness, confession, and trust. It realizes not only a new cognitive and theoretical form of self-consciousness, but also a new magnanimous practical form of self-conscious agency. The story told in these pages accordingly concludes by describing how Hegel thinks we can combine the reachievement of the heroism of traditional agency, without its accompanying tragic subjection to fate, and the individual self-consciousness achieved by modernity, without its accompanying alienation.
— Robert Brandom, A Spirit of Trust, Introduction.
I have used a myth [the myth of Jones] to kill a myth — the Myth of the Given. But is my myth really a myth? Or does the reader not recognize Jones as Man himself in the middle of his journey from the grunts and groans of the cave to the subtle and polydimensional discourse of the drawing room, the laboratory, and the study, the language of Henry and William James, of Einstein and of the philosophers who, in their efforts to break out of discourse to an arché beyond discourse, have provided the most curious dimension of all?
— Wilfrid Sellars, Empiricism and the Philosophy of Mind, §63.
To think one is obeying a rule is not to obey a rule. Hence it is not possible to obey a rule ‘privately’: otherwise thinking one was obeying a rule would be the same thing as obeying it.
— Ludwig Wittgenstein, Philosophical Investigations, §202.
Whether the objects known to the individual only as representations are yet, like his own body, phenomena of a will, is, as stated in the previous book, the proper meaning of the question as to the reality of the external world. To deny this is the meaning of theoretical egoism, which in this way regards as phantoms all phenomena outside its own will, just as practical egoism does in a practical respect; thus in it a man regards and treats only his own person as a real person, and all others as mere phantoms. Theoretical egoism, of course, can never be refuted by proofs, yet in philosophy it has never been positively used otherwise than as a sceptical sophism, i.e., for the sake of appearance. As a serious conviction, on the other hand, it could be found only in a madhouse; as such it would then need not so much a refutation as a cure. Therefore we do not go into it any further, but regard it as the last stronghold of scepticism, which is always polemical.
— Arthur Schopenhauer, The World as Will and Representation, §19.
We have now to keep in mind that the Hauptsatz — under various disguises, e.g. normalization in λ-calculus — is used as possible theoretical foundation for computation. For instance, consider a text editor: it can be seen as a set of general lemmas (the various subroutines about bracketing, the size of pages etc.), that we can apply to a concrete input, let us say a given page that I write from the keyboard; observe that the number of such inputs is practically infinite and that therefore our lemmas are about the infinite. Now when I feed the program with a concrete input, there is no longer any reference to infinity… In mathematics, we could content ourselves with something implicit like “your input is correct”, whereas we would be mad at a machine which answers “I can do it” to a request. Therefore, the machine does not only check the correctness of the input, it also demonstrates it by exhibiting the final result, which no longer mentions abstractions about the quasi-infinite potentiality of all possible pages. Concretely this elimination of infinity is done by systematically making all concrete replacements — in other terms by running the program. But this is exactly what the algorithm of cut-elimination does. — Jean-Yves Girard, Linear Logic: Its Syntax and Semantics
When I first learnt about Curry-Howard, it seemed utterly banal. Of course when you restrict logic to be constructive, its proofs are constructions and hence computations — no duh! It is not surprising that the arrow (implies) means the arrow (is a function), and while it is a tiny bit more surprising that times means and and plus means or, it is still by no means earthshattering.
But Curry-Howard is not surprising on account of what it says about the syntax of propositions — no, the real contribution of Curry-Howard is what it says about normalization. Proofs have normal forms, and so too do terms — the normalization of proofs is the normalization of terms. The normalization of proofs is achieved by the elimination of intermediate lemmas. The normalization of terms is achieved by computation. That these things are the same is very surprising!
The theorem that the elimination of intermediate lemmas leads to normal forms is called the Hauptsatz. In (usually constructive) logics which admit the subformula property, it has consistency as a direct result. (I always thought Hauptsatz was German for “cut elimination” until I started German on Duolingo and realized it just meant “central theorem”, which goes to show how important Gentzen thought cut elimination was).
The theorem that computation leads to normalization in certain languages is rather surprising — this is the strong normalization of, e.g. the simply-typed lambda calculus, or System F. These languages cannot be Turing-complete — yet they remain quite useful.