🚀 go-pugleaf

Jeff Rubard wrote:
> First rule of writing: it's important to work with your editor.  First
> in a series, comments welcome.
> 
> Logic and Politics, #1: The Political Significance Of The Sequent
> Calculus
> 
> Men make their own history, but they do not make it as they please;
> they do not make it under self-selected circumstances, but under
> circumstances existing already, given and transmitted from the past.
> The tradition of all dead generations weighs like a nightmare on the
> brains of the living. And just as they seem to be occupied with
> revolutionizing themselves and things, creating something that did not
> exist before, precisely in such epochs of revolutionary crisis they
> anxiously conjure up the spirits of the past to their service,
> borrowing from them names, battle slogans, and costumes in order to
> present this
> new scene in world history in time-honored disguise and borrowed
> language. Thus Luther put on the mask of the Apostle Paul, the
> Revolution of 1789-1814 draped itself alternately in the guise of the
> Roman Republic and the Roman Empire, and the Revolution of 1848 knew
> nothing better to do than to parody, now 1789, now the revolutionary
> tradition of 1793-1795. In like manner, the beginner who has leaned a
> new language always translates it back into his mother tongue, but he
> assimilates the spirit of the new language and expresses himself
> freely in it only when he moves in it without recalling the old and
> when he forgets his native tongue.
> 
> Marx, *18th Brumaire*
> 
> Leaving aside the theoretical solution Engels proposes for the problem
> of the relation between determination in the last instance -- the
> economic -- and those determinations imposed by the superstructures --
> national traditions and international events -- it is sufficient to
> retain from him what should be called the accumulation of effective
> determinations (deriving from the superstructures and from special
> national and international circumstances) on the determination in the
> last instance by the economic.
> 
> Althusser, "Contradiction and Overdertermination"
> 
> Everything begins in a mystique and ends in a politique.
> 
> Charles P�guy
> 
> What Is Proof Theory? Proof Theory's Not Semantics
> 
> The logical subdiscipline of proof theory was invented by Gerhard
> Gentzen is something one can say without meaning very much, because
> aficionados of mathematical logic generally fall into two camps: those
> who believe that the study of proof is the proper business of logical
> analysis and those who are still looking for a convincing proof of
> something they care about deeply. Combinatorics aficionados aside,
> Hilbert's formalism still casts a long shadow upon the logical
> analysis of language: the idea that the only thing
> which should be done with meaning is its being explained away is still
> attractive to many due to the persistence of Quinean scruples
> concerning "other people's problematics".  Others have heard the word
> of Etchmenedy, that the model-theoretic definition of logical
> consequence is too much or not enough depending on your purposes.  Are
> there barbarians who threaten to upset this delicate perplexion? 
> Well, I haven't seen 'em, but if such people existed I expect they
> would derive their scruples not from analytic philosophy, but from
> intellectual traditions which "thickly" attempt to handle the business
> of life as though it were more tractable than it is. And if such a
> person were to examine the situation concerning the use of proof
> theory in analytic philosophy, I suppose they would be confused by the
> failure of logically-minded philosophers to consider the material
> conditions of possibility of their theoretical knowledge.
> 
> Namely, the discipline of proof theory, considered in a formalist or
> anti-formalist spirit, permits of the very neat recursive definition
> given above: which leaves room for all the messy facts about
> incompleteness and complexity which have been discovered in the last
> half-century, but also for a rather
> wider set of valuations for those facts than have traditionally been
> permitted.
> For example, the standard-bearer of proof theory -- Gentzen's
> "Investigations Into Logical Deduction" -- has been intensively
> studied for almost seventy years without certain questions being put
> to it. And to my mind, the most important question which has not been
> widely asked of it is: "Do the different proof systems disclose
> different facts about language? Are there non-metatheoretical reasons
> to prefer one over the other for various
> purposes?" George Boolos discovered one such fact, that systems
> without the cut rule cannot effectively handle relatively simple
> derivations: but to my mind there are a variety of such facts. But
> what these facts are not is normative: the development of
> interpretational proof theory shows that no particular proof-structure
> ought to be considered "semantically defined". In fact, I think hints
> of a very different kind of logic provided by Husserl (and obscured by
> what ought to frankly be called Frege idolatry) should suggest to us
> that proof theory not only provides conditions of adequacy for
> semantics, but also the Stoff for a "computational complexity theory"
> which need not be particularly concerned with the vicissitudes of von
> Neumann machines or their
> (professional and/or habitual) operators. 
> 
> (In my opinion this is all that ought to remain of Hilbert's program:
> people who still want to replace semantics with proof theory ought to
> have their books examined.  But the perhaps the aforementioned
> combinatorics junkies ought to have their books taken away from them
> and be given random inputs of various viscerally unpleasant kinds.)
> 
> There's Nothing Natural About Deduction: The Sequent Calculus Made
> Easy
> 
> In "Investigations Into Logical Deducton", Gentzen presented two
> systems for formalizing logic.  The first system, "natural deduction",
> is widely-known and forms the basis of the popular philosophical
> doctrine of "conceptual role semantics": the second kind of system,
> called variously the sequent calculus, a "Gentzen system", or a
> "consecution calculus", is for the most part the province of logical
> specialists due to the relative complexity of its
> notation and the widespread belief that it is of limited interest. But
> in reality, forms of reasoning made perspicuous by the sequent
> calculus are of the utmost importance for natural-language semantics,
> and so I shall provide a "potted" account of the sequent calculus here
> and draw the reader's attention to a few salient elements.  The first
> difficulty with the sequent calculus is evident; the logical
> statements manipulated by the sequent calculus, sequents, are not
> individual propositions but chains of reasoning involving such
> propositions. Natural deduction is based on two sets of rules for
> logical symbols, "introduction" rules for proving propositions
> involving a given symbol and "elimination"; rules for proving
> propositions from a proposition involving a given symbol; the idea is
> that this closely matches "natural" patterns of reasoning. The sequent
> calculus is based on three sets of rules; two sets of "introduction"
> rules for chains of reasoning involving given symbols, and a set of
> "structural"; rules governing all chains of reasoning. Much attention
> has been given to the structural rules, the modification of which
> permits the study of "substructural" logics (relevance and entailment,
> e.g.), but later here I will be drawing attention to the bipartite
> distinction between "left" and "right"; introduction rules, in a
> spirit quite foreign to philosophical logic as it has been previously
> practiced.
> 
> A set of rules for the sequent calculus, save the Mix rule, can be
> found at Wikipedia:
> 
> Unfortunately, as regards the clarity of sequent rules: when you see
> them, then you don't.  Unlike natural deduction rules, each sequent
> "rule"; is really a schema for an infinite number of definite
> substitution rules: the gamma, delta, and sigma symbols stand for
> groupings of formulae ("context"). Additionally, the commas separating
> components of a sequent have two different meanings depending on
> whether they appear before the arrow (in the antecedent) or afterwards
> (in the "succedent"); in the former case they are disjunctive, the
> latter case conjunctive.  However, pace Nuel Belnap, it seems clear
> that
> Gentzen's including them in the class of "improper symbols"; was
> well-founded, as improper symbols in logic belong to a class of
> symbols someone once called
> "circumstructure"; without anyone paying too much attention: Gentzen's
> comma could well be taken as paradigmatic of a circumstructure, rather
> than as an invitation to impose arbitrary structures on proofs.
> 
> These rules suffice for rendering all the well-formed formulae of
> classical and intuitionistic logic (about which more later), but more
> importantly rendering them in a manner perspicuous for
> metamathematical purposes. Proofs formulated in the sequent calculus
> without using the cut rule obey the subformula property: only
> subformulae of the final result occur in a deduction. This is an
> eminently desirable property from the point of view of demonstrating
> consistency, but unfortunately it almost never occurs in any kind of
> proof we would be tempted to engage in practical thinking: even in
> formal logic, "rules of thumb"; are an essential part of economically
> proving theorems (that is, within the amount of time allotted to the
> luckiest of us on Earth). The cut rule (together with weakening, which
> would perhaps more accurately be called "dilation") is a catch-all
> device for including such rules of thumb as valid forms of inference,
> but it does not prove that such rules are "conservative extensions";
> of the other rules. For this purpose, a cut-elimination theorem must
> be proven: and Gentzen had an illuminating thing to say about such a
> proof, that it demonstrated no "intermediate" concepts were necessary
> for the purposes of proof which could not be justified in terms of the
> initial premises and final results.
> 
> Gentzen's proofs of cut-elimination theorems (*Hauptsaetze*) for
> classical and
> intuitionistic logic employ a variant of the cut rule, the mix rule. 
> The purpose of the mix rule is to make prooftrees for a cut rule
> tractable, i.e. to demonstrate that the cut formula can in theory be
> systematically eliminated from any antecedents of a sequent involving
> it.  Although there are now methods for proving cut-elimination
> theorems which do not use the mix rule, the element differentiating
> the mix rule from the cut rule (the repetition of the cutformula) is
> worth considering. What the principle behind the mix rule (in whatever
> form) states is that, although unlike natural deduction the sequent
> calculus does not require that a rule of inference be justified in
> terms of immediately obvious applicability of "introduction rules", a
> valid cutformula must be genuinely "rulish", in principle capable of
> multiple instantiation; a "formula" which is not repeatable is merely
> a glyph without content.  The resonances of that formulation are
> intentional and deserve further study, as
> does Gentzen's "super-logical" principle of "reduction"; (the mention
> of which may only have the appropriate resonances for serious students
> of Althusser and formal logic). But now on to the primary topic of
> this "squib".
> 
> A variant of the sequent calculus, the "one-sided"; Gentzen-Schuette
> systems, only permit statements in the succedent. These are adequate
> for the purposes of metamathematically characterizing classical and
> intuitionistic logic, but there are a few reasons to think that the
> "natural" valences of "right" and "left"; for inhabitants of the
> modern era are not irrelevant here, and deserve a great deal more
> scrutiny than they usually get. To begin with, if "right"; and "left"
> *spatialize* the political sphere they do not do it in any
> straightforward way.  The expressions derive from an early parliament
> during the French Revolution, where radical members sat on the king's
> left, royalists on his right, and moderates in the middle, so the
> distinction does not serve as an absolute measure of the political
> spectrum (unless there is a tacit populist premise involved). But on
> the other hand, the distinction traditionally repeats itself within
> political parties without a hereditary ruler, and the question of the
> necessity of an "imaginary" space marked out by dividing the party
> into
> "left" and "right" factions is the question of "democratic centralism"
> as advocated by Lenin in response to what he perceived as left-wing
> extremists within Bolshevism weakening the party's tactical strength;
> and it is actually the second of these uses which can be clarified by
> the consideration of the sequent calculus.
> 
> As I said, the one-sided systems are adequate for the purpose of
> mathematical proofs.  But it seems to me that what two-sided,
> multivalent sequent calculi are uniquely suited to "displaying" is the
> rhetorical effectivity of political statements, what is spoken of as
> "running to the left" or to the right. This argument hinges on a
> conjecture about the linguistic structure of the political sphere,
> that the interpretations abroad concerning past historical events are
> generally favorable to the political left, whereas the interpretations
> "in
> season" for contemporary occurrences, those that have weight with
> decision-makers, are generally favorable to the political right. When
> this is connected up with the logical truism that antecedents were
> made for succedents and vice versa, this suggests that there are two
> well-founded political strategies: leftists should try to show that
> the lessons maximally radical past movements teach us have as
> consequences "minimal" conservative positions (that is, constitute the
> lower bound of political positions conservatives must take
> seriously) and rightists should try to show that minimally "radical"
> (that is, maximally corporatist) past political movements have as
> consequences the liberal shibboleths of the day.  (These strategies
> apply for left-right disputes within a single party as well.)
> 
> Gentzen's association with the Nazi party has been the subject of some
> discussion recently (in Germany, that is), and this formulation may
> suggest that any truth-content of political rhetoric is being elided
> with such strategies. However, no other area of discourse is as
> well-established as political rhetoric in popular sentiment as being a
> "social technology", a
> means to produce desired effects in a social formation, rather than
> solely for the purpose of conducting inquiry; and it seems that simply
> giving the view that the business of politics is "manufacturing
> consent" a sharper formulation does no great harm; and a third element
> (as well as the question of the social effectivity of rhetorical
> "models", which as I said is one for another day) prevents such
> tactics from constituting the whole of discourse about politics. The
> famous aphorism of P�guy quoted above suggests a third attitude to
> political rhetoric, one of distaste and resignation: and this attitude
> is most markedly present in "libertarian" political outlooks, not only
> in right-wing defenders of free enterprise and property-rights against
> "nanny states", but in libertarian leftist movements battling the
> control of individuals by profit-motivated organizations.
> 
> In America such groups have historically drawn inspiration from
> anarcho-syndicalism, but recently there has been a salutary increase
> of interest in the "left-wing Communists"; of the 1920s and 30s, who
> were not interested in "propaganda of the deed"; but also not in the
> "deed of propaganda", distortion of political facts to serve the aims
> of the party.  Such groups quickly dissociated from the Third
> International (and it seems important to note that their points of
> origin should be located in the parties of the anti-war Zimmerwald
> Left, rather than in Bolshevism: groups like the German Workers' Party
> were in truth more closely aligned with members of the pre-Communist
> "Second-and-a-Half International"; than the Stalinists of the 30s,

To take up an oldie but goodie for the benefit of the "uninformed": I 
was not here referring to the German Worker's Party founded by Anton 
Drexler after World War I and transformed by its seventh member Hitler 
into the NSDAP, but rather to the Kommunistische Arbeitungspartei 
Deutschlands ("transliterally": "Germany's *Communistic* Labor Party"), 
an even less well-known organization than that ephemeral one -- and I 
was attempting to translate its such that would assimilate to the names 
of similar American political formations outside the Third International 
fold.  As such those *au fait* with the mindset of the Proletarian Party 
and other "unknowns" need no explanation, but I must say that such 
"verbal distinctions" are quite of the moment in terms of the ideas 
presented in this (later updated) essay; to my mind there is not a 
"mapping" between the DAP and the KAPD because they are mutually 
exclusive as regards political rationality and cannot be interpreted to 
have stood for the same things *nolens volens*.

Either one or the other makes sense, *not both or neither* (don't break 
out those vels) and by virtue of some concrete difference in their 
political outlooks.  But such considerations are something of an acid 
test for the left (outside the scope of this essay) and not others -- 
there is an end to proof, or there isn't, and it doesn't take a genius 
to figure out to what end the latter attitude can be put.  And I suppose 
whether or not such considerations dominate your understanding of social 
reality or not depends on the extent to which you feel the true and the 
made are convertible in a sense exceeding "conditions of application", 
but this question pertains to "everything new under the sun" and as such 
is a fine one for the first day of the year.

Jeff Rubard