historical... data retrieval [EX Re: [PT] question on ND and sequents]

At 12:14 AM 6/1/2005 -0500, William Tait wrote:

>
>On May 31, 2005, at 12:28 PM, Adrian Rezus wrote:
>
>>a small detail (prof. tait -- absent-minded this afternoon, likely -- was
>>not very careful in stating such trifles, I guess!):
>
>You are possibly right about my absent-mindedness: I can't remember. But
>please tell me what I absent-mindedly overlooked in  stating that
>Gentzen's first consistency proof in effect involves a formulation of
>natural deduction using sequents.
>

(no offense intended! --- my parenhetical remark on ``prof. tait'' was
prompted by the... parenthesis of dr. Strassburger -- I should have used
quotes, perhaps... --, meaning: ``why bother prof. Tait  with such
trifles?'' --- lowercase on proper names is just running e-mail style! ---
I re-styled below...)

your statement is correct, of course (``historically'', say); but -- as you
were asked, anyway (!) --, given your preference for... [typed] \lambda-
(or rather \lambda\pi-) calculus, I would have expected an answer on my
line of thought (proof-theory = typed lambda-calculus), namely something
like: ``(as regards intuitionistic logic / minimalkalkuel) there is no
difference between Gentzen N- and Gentzen L-formulations: both amount to
the same thing: (viz. lambda-calculus)'' ---

this is also one of the points / ``lessons'' we could learn from Howard's
notes (1969, published 1980) on ``formulae as types'';

(
the paper of Garrel Pottinger -- I was referring to -- is from 1976, btw:

``A new way of normalizing intuitionist propositional logic'', Studia
Logica 35, 1976, pp. 387ñ408.
[Likely the first notice ñ in print ñ of the fact that a Gentzen L-system
for the Heyting [propositional] logic is a [special ] form of typed
\lambda-calculus, too. See, however, [Howard 80]. ---

so I should have said earlier: ``first notice in print''; Howard comes first...
)

actually, the N-formulations have only ``intro''-rules, if we pay attention
to the proof-information (recorded in the lambda-calculus notation); for
what is `introduced'' are the ``proof-operations'', in fact (e.g.,
``[functional] abstraction'' and ``[functional] application'', for the
arrow-case, say); whereas the L-formulations have only ``intro-rules'',
even if we look at formulas alone (i.e. if we do... ``proof-theory without
proofs'', so to speak!): once we restore the proof-information, we get back
the ``intro''-pattern (on a slightly more general level);

for instance,

[arrow-]intro-right

     \Gamma, A |-- B;
     -------------------------- (right)
     \Gamma |-- A-->B

becomes

     \Gamma [x : A] |-- b[x] : B
     ----------------------------------------------------- (abs)
     \Gamma |-- \lambda x:A.b[x] : A-->B

and

[arrow-]intro-left

     \Gamma |-- A;  \Delta, B |-- C
     ------------------------------------------ (left)
     \Gamma, \Delta, A-->B |-- C

becomes

     \Gamma |-- a : A;  \Delta, [y : B] |--  c[y] : C
     ------------------------------------------------------------------- (app*)
     \Gamma, \Delta, [z : A-->B] |--  c[y:= (za)] : C

(with the usual typed \lambda notational conventions; b[x] meaning ``x
occurs free in b[x]'' -- fictious case included --, and b[x:=a] meaning
substitution for proof-varianbles: ``x becomes a in b[x]'', etc.),

whence, modulo ``structural''-only transformations, the N-variant of (app*)
is -- more or less (!) -- just a special case of this (take B = C, and
c[y]  to be``the outermost context'' c[y] = y)

     \Gamma |-- a : A;  \Delta, [y: B] |--  y : B
     ------------------------------------------------------------
     \Gamma, \Delta, [z : A-->B] |--  (za) : B

here \Delta, [y: B] |--  y : B coms by weakening / ``thinning'', so, in the
end,

     \Gamma |-- a : A
     --------------------------------------------------------- (app**)
     \Gamma, \Delta, [z : A-->B] |--  (za) : B

and (app**) looks like the N-variant of ``arrow-elim'' (= modus ponens!):

     \Gamma |-- a : A;  \Delta |-- f : A-->B
     ----------------------------------------------------- (app)
     \Gamma, \Delta |--  (fa) : B

(``more or less'', I said, because taken modulo frequent uses of  weakening
and ``cut'' [substitution!]; and the ``cut''  cannot be... ``eliminated''
from \lambda-calculus: it's ``built-in'' in the statement of the
\beta-rules, anyway);

now, coming back to historical matters, there is room to speculate a little
bit: in fact, Gentzen should be also credited with the [co-] discovery of
[typed] lambda-calculus (together with many others)!

this is even more obvious in the... Polish case (Lukasiewicz & co: Tarski,
Ja'skowski etc.):

>
>Your earlier posting on Lukasiewicz's invention of natural deduction is
>interesting. Do you mean that he explicitly wrote down a complete set of
>rules of inference governing sequents? (Studia Logica 1934 is not easily
>available to me now.)
>

Lukasiewicz's own ``invention'' is probably an overstatement; we don't
actually know what he had in mind...

as far as I could gather, Lukasiewicz and some of his students were busy --
during the early twenties -- with analyzing ``proof-theoretically'' the
curious systems of Lesniewski (``protothetics'' and so); this is likely the
general context;

the ``invention'' proper is due to Ja'skowski, but the very idea was ``in
the air'', anyway (in the Lukasiewicz' seminars, I mean);

I would rather say, something else / more: the team (Lukasiewicz, Tarski,
Ja'skowski etc.) was already aware of something similar to [typed]
lambda-calculus / combinatory logic (modulo ``Curry-Howard'', so to speak)!

only scarce evidence survived as regards the real story;

a few items in point:

[1] Tarski (1925 or earlier) claimed (without proof) the following
``axiomatizability result'' [Theorem 8, in Lukasiewicz & Tarski
``Untersuchungen ueber den Aussagenkalkuel'', 1930]:

every system of (propositional) logic that is finitely axiomatizable with
modus ponens (as a single rule of inference) and contains

(k) : A -> (B-->A)

(d) : A -> (B-->((A-->(B-->C))-->C))

as ``theorems'' [or else: CpCqp and CpCqCCpCqrr, in ``Polish'' /
Lukasiewicz notation: I hope I translated back correctly with arrows] is
also axiomatizable with a single axiom and modus ponens (well, putting
aside the ``substitution rule'' for prop. variables: take ``schematical''
formulations, `a la von Neumann, instead) ---

it is easy to see that  (modulo ``Curry-Howard''!) the ``combinatory''
counterpart of (d) is just Church's ``pairing combinator'':

Dabc = cab
(D = \lambda x.\lambda y.\lambda z.z x y, omitting ``typings'')

and (k) is just the usual K-combinator:

Kab = a
(K = \lambda x.\lambda y.x);

the rest is an easy exercise: in order to prove Tarski's statement we must
find a way of ``pack[ag]ing'' a finite list of... dummies (``combinators'',
closed terms, the ``axioms'') in a single ``combinator'', as well as a way
of ``unpack[ag]ing'' this kind of information, by using only K and D; a
solution can be found in the Tarski paper, referred to earlier (this can be
generalized in various way, and K is not even necessary, in fact: in order
to be able to ``unpack'',  we can also fabricate ``projections'' for the
Church pairing with ``local'' K's, say; within so-called \lambda-I-calculus
of Church; I got the idea from Wadsworth and Barendregt, but it was
implicit in Church, anyway);

if we think a little bit about ``the method of proof'', there is,
essentially, no ``other'' way of showing this kind of thing: some way or
another we _must_ use (at least implicitly) ``Curry-Howard''! --- whence...
Tarski should have known something about [typed] combinators and the like,
avant la lettre!

[2] around 1926 (in fact, even in public: at the first Polish Math.
Congress, 1927), Jaskowski comes with ``natural deduction'': if we just...
formalize the ``comments'' (= write down / keep track of every application
of the rules), we get typed lambda-calculus (a variant thereof; for
classical logic, btw); --- well, there is no talk about ``proof-reduction''
and / or ``proof-isomorphisms'' in Ja'skowski, but this is a different
story (yet, Tarski should have known something about, because... he used K
and D, anyway!);

(Ja'skowski' paper has a reprint in: S. McCall (ed.) Polish Logic
1920-1939, Clarendon Press, Oxford UK 1967, pp. 232-258.)

[3] relying on the Lukasiewicz shorthand-notation for ``axiomatic''
derivations, a later student of Lukasiewicz (in Dublin), Carew A. Meredith
(1904-1976) invented (during the early fifties) the so called ``condensed
detachment operator D''; this is just another way of thinking about
``Curry-Howard'' (we get a kind of typed combinatory logic again, with
Meredith's D as ``application'');

extrapolating (``historically''!): nearly any worker on ``proof-theory'' --
including Gentzen, of course -- has eventually ``rediscovered'' (a kind of)
[typed] lambda-calculus or else the [typed] combinators! ---

(aside: although Dag Prawitz never wrote down a single... \lambda on paper
/ in print, his PhD diss. [1965] can be transcribed in ``[typed]
lambda-terms'' entirely: this includes his description of [first-order]
classical and modal logics, things `a la Lewis' S4, S5 --- from my own
point of view, Prawitz missed just a single kind of ``proof-d'etour'', for
the genuinely classical case... --- and even on this I'm not so sure: it
might turn out that he was, long ago, already aware of such things, too!);

after all, there is no ``Curry-Howard [correspondence]''! a ``rule of
inference'' is just a ``proof operator'' (this works -- ad litteram -- for
nearly any ``logic''); the hard work behind this way of thinking about
proofs consists of finding the right kind of ``equational proof behaviors''
(or else, in terms of reduction, the right kind of ``proof-detours'') for
each specific case / ``logic'' (including ``fragments'') ---

>
>Your reference to Hertz does not reassure me on this point. Truth----I
>should probably say credit for truth----is ultimately in the details one
>presents.
>

you are right, but the claim was that Gentzen ``borrowed'' from Hertz just
the idea of a ``sequent'' (in our terms, it was Gentzen who came with the
idea of a ``proof-operator'', at least implicitly; he was also singling out
the right kind of ``proof-d'etours'' for Heyting's logic and so on); ---
Hertz was busy with a slightly different things (he was, basically, a
physicist, after all, and his interest in logic was by... contamination, in
a way: by close contacts with Hilbert and his friend, Paul Bernays, I
suspect --- there have been some rumors, coming from Goettingen, that even
Emmy Noether was involved in such local debates -- on Hertz's ``systems'',
I mean --, some time during the twenties or so; yet, no evidence in print,
so far); in our terms, Hertz was rather interested in characterizing the
``structural rules'' (``cuts'' included) for ``arbitrary systems of logic''
(or else the ``consequence relation'' --- like... Tarski, in fact, later);

on Hertz and his business [= generalized ``modus barbara'' = multi-cuts!],
more details can be found in a recent paper by Peter Schroeder-Heister, I
was not aware of before... yesterday:

PETER SCHROEDER-HEISTER
RESOLUTION AND THE ORIGINS OF STRUCTURAL REASONING:
EARLY PROOF-THEORETIC IDEAS OF HERTZ AND GENTZEN
The Bulletin of Symbolic Logic
Volume 8, Number 2, June 2002 ---

(the author meant to avoid... self-propaganda on the list; I can afford the
citation, however!)

quite interesting and unexpected, in fact (``cut-only normalization''! ---
the slogan ``you should not eliminate the cut!'' was just my own way of
rephrasing an older claim of prof. [Dana] Scott... something like: ``cuts
are not eliminable, in general''; it was in the Tarski Symposium paper, I
think; the one on consequence relations);

as to ``historical data retrieval'' (since I'm not so... shy as PS-H [!],
and won't be able repeat, anyway, once more, a rather long story), it might
be a good idea to have a look some time at the details recorded already
some 15 years ago in a piece called ``Beyond BHK'', Appendix 4 ``Further
reading: a guide to BHK''  [where BHK = Brouwer-Heyting-Kolmogorov];

this is stored privately
@
http://www.vlab.pub.ro/equivalences/_lambda-and-proofs/_ar/beyond.pdf
and only an ``extended abstract'' is in print so far; online copy
@
http://www.vlab.pub.ro/equivalences/_lambda-and-proofs/_ar/bbhk93ea.pdf

there is already a lot beyond... ``Beyond BHK'', but the main remark would
likely fit the half a page I mentioned earlier: it consists of
``stratifying'' / ``typing'' the usual  [type-free] \lambda\pi-calculus [=
``the lambda-calculus with surjective pairing''], with genuinely...
``classical'' types [instead of a ``Church typing'']: the outcome is
``classical proof theory'', once more, and contains already the
\lambda\gamma-calculus [= the ``classical lambda-calculus'' of
``Beyond...'' etc.] --- well, as this is already too long, I'd rather mail
the... half-a-page only to those interested in such trifles, if any!


>   Sincere regards,
>
>Bill Tait (I think)

best regards
a[r]