🚀 go-pugleaf

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,
although practicing the political tactic of "abstentionism").  What
makes abstentionism (pointed non-participation in elections) a
political tactic is its recognition of the reality of the political
sphere; the Amish are not
abstentionists. What makes abstentionism (which can be practiced
within parliamentary parties, as the Mississippi Freedom delegation at
the 1964 Democratic convention demonstrated) a "libertarian"; tactic
is its denial of the reality of a particular piece of political
discourse, assigning to it the character of "para-politics".  (The
distinction between politics and para-politics cuts across the
legitimacy/illegitimacy distinction: the Continental Congress was
illegitimate by the standards of British rule but genuinely political,
whereas the Nazi party came to power by "legitimate"; means which were
then perverted to serve extra-parliamentary interests).

Gentzen's sequent formulation of intuitionism, LJ, is exactly like LK
save for its not permitting more than one formula in the succedent;
and this suggests itself as an excellent framework for understanding
(and practicing) abstentionism.  Intuitionism is the metamathematical
doctrine that mathematical truth cannot exceed means of proof, but it
is not as "puritanical"; in this as is commonly supposed:
intuitionistic choice functions permit the use of mathematical objects
generated by infinite processes of effective construction,
rather than banning the concept of uncountable infinity from
mathematics entirely.  And in this intuitionism resembles another
Dutch specialty, council communism.  Council communism is not
equivalent to left-wing communism. However, it gives perhaps the
purest formulation of the strict political demand of communism, that
political sovereignty cannot exceed the legitimacy granted it by
participation and that political bodies which do not meet this
criterion (parliaments) ought to be discarded in favor of ones that do
(worker's councils).  And abstentionism or "political intuitionism";
-- which political activity is limited solely to arguing for the
legality of particular exercises of personal freedom, and the
illegality of particular exercises of individual coercion, -- is a
means of preserving what is of value in liberal democracy (uniformity
of treatment under the rule of law) without legitimating what is not
(excesses of the bureaucratic state), and which does not deny the
reality of the polity's claim on us ("minarchism" doesn't sound so
good if you've ever tried to prove much without *ex falso*.)

Excursus: On Superstructural Logic

I mentioned the field of "substructural logics", but none of what I
have to say here has anything to do with relevance logic, the Lambek
calculus or other propositional calculi with restricted canons of
inference.  Instead, the natural fit between the sequent calculus and
questions of political rhetoric (worked by political power being one
of Parsons' "generalized media of communication" which coordinate
action without explicit consent --
similar links exist between the Hilbert systems and scientific truth,
natural deduction and love, and the resolution calculus and money)
naturally leads to another question: whether we should not speak of
another class of logics -- "superstructural logics" -- with extended
rules of inference.  It does so because acknowledgment of those
widespread views (e.g., that of Oakeshott) which hold politics in
general is not "rational" in the sense of being
axiomatic, but rather defined in terms of cultural *Gestalten*, does
not bar one from allowing that there is a significant role for
scientific knowledge in politics; including scientific knowledge
defined in terms of strict (that is, modally rigid) laws.  I think we
should make provisions for the inclusion of such rules in sequent
calculi (at least on grounds of realism), but that the presentation
above suggests that existing techniques for including extended rules
of inference (such as modalities) in a sequent calculus are
misleading at best, since "intensional" operators are of a
fundamentally different class.

It may be objected that quantifiers are non-truth-functional and still
included in the sequent calculus proper; but as indicated above the
left and right quantifier rules are not introduction rules
simpliciter, but contain significant substitutional constraints,
whereas both structural and connective rules have no restrictions.  So
instead, I would propose that
intensional operators generally be understood in terms of the above
explication of the rules of Weakening and Cut (for example, operators
for normal modal logic are special cases of Weakening justified in
terms of closure under Cut -- i.e., the applicability of the
Necessitation rule -- rather than Contraction to avoid "runabout
inference ticket" claims).  This does not provide for a "elegant"
representation of rules of inference pertaining to
modal logic, but such elegance is rather contrary to the nature of
modal logic (Hilbert calculi are ideally suited to weighing the subtle
differences between modal systems, which distinctions form the bulk of
the study of modal logic, and which are not well-represented in
natural deduction and sequent calculi), but it does provide for an
understanding of "intensionality" which naturally connects it to the
more widespread theoretical notion of superstructure and de-links it
from the concept of "circumstructure" or normative fact introduced in
the third essay in this series.

Objections mounted to intensional logic on Brentanian grounds may be
less strenuous if it is understood that what is being talked about is
not quite the "appearance" of traditional epistemology, but patterns
in social discourse about such appearances which subsist independently
of individual glosses on experience.  And objections mounted to
"essentialist metaphysics" conducted in the guise of reflections on
modality may abate if the multiplicity of modal systems and operators
currently studied is well-understood.  For example, one "logical
modality", the difference operator, does not say anything about
necessity or possibility; what it states is that some other possible
world in a model satisfies a proposition; its dual states that every
other possible world in a model satisfies a given proposition. 
Blackburn, de Rijke and Venema introduce the difference operator with
grins, likening it to a hammer in the bottom of a tool chest only used
when no other tool will do, but in reality it and its dual are very
powerful tools for understanding a concept never before analyzed in a
logical manner, Carl Schmitt's friend/enemy distinction.

The distinction between friend and enemy in Schmitt is not one between
personal friend and personal "foe", but the founding division of
politics: according to Schmitt, when considering members of other
nations in belligerent situations, there is some one thing they are
all not, namely possessing a groundless commitment to our way of life.
 But the point of "modal political theory" in this style is to show
that Schmitt's other obsession, the ius publicum Europaeum (the
opposite of 20th-century partisan or total warfare) can be
understood as positing a (unchecked) homology between the mores of our
country and some similar configuration in another system, i.e.
employing the aforementioned difference operator and not its dual. 
And thusly the bumper-sticker saw "War does not determine who is
right, only who is left" can be seen in light of this as really saying
something like: the discourse of unchecked political conflict derives
from antecedents of said conflict, indicates the depth of support for
a position in past solidarities, rather than creating new
ones.  Diplomats have traditionally reasoned in this way all the time;
so if "conservative revolutionaries" are to judge "rationalism in
politics" impossible, the cogency of employing scientific discourse in
politics is what needs to be knocked down, not the straw man of a
"scientific mode of dress", on pain of nothing new under the gun; and
a "traditional" suggestion is that this thought disturbs them not at
all.