This Week's Finds in Mathematical Physics (Week 40)
Matthew P Wiener
>(I could be wrong about this, so if there are any linear logicians
>out there, they should correct me if I've got it wrong.)
The only thing I know of called linear logic is a system in between
classical and intuitionistic. Not all excluded middles are allowed
in, but I think "p=>q v q=>p" is, and that this characterizes linear
logic.
When Cohen invented forcing, he gave the most obvious treatment of
negation, and the forcing logic came out intuitionistic. Dana Scott
realized this was backwards, and the complications should be in the
way forcing handles negations, so that the logic comes out classical.
But Kripke exploited this initial clumsiness brilliantly, and showed
that the original Cohen forcing can be recast as a naturally intuitive
model theory ("Kripke semantics") for intuitionistic logic.
The point of this digression is that forcing involves partial orders.
If one restricts Kripke semantics to linear orders, one gets linear
logic. (Classical logic corresponds to the trivial order.)
--
-Matthew P Wiener (wee...@sagi.wistar.upenn.edu)
Mike Oliver
>In article <37vi3l$r...@galaxy.ucr.edu>, baez@guitar (john baez) writes:
>>(I could be wrong about this, so if there are any linear logicians
>>out there, they should correct me if I've got it wrong.)
>The only thing I know of called linear logic is a system in between
>classical and intuitionistic. Not all excluded middles are allowed
>in, but I think "p=>q v q=>p" is, and that this characterizes linear
>logic.
While it's conceivable that there's something that I'm missing, my belief
is that you're both wrong. Linear logic is *more* restrictive than
intuitionistic logic. In a Gentzen-style system you get intuitionistic
logic from classical by dropping the rule
(not A),Gamma |- False
-------------------------
Gamma |- A
(or something equivalent; it's been a while since I've done this). To get
linear logic you further drop the rules weakening and contraction;
i.e. you no longer have
A,Gamma |- B A,A,Gamma |- B
-------------- --------------
A,Gamma |- B,C A,Gamma |- B
Then you add rules for these other weird connectives like tensor, but
they don't allow you to prove all the things you could prove in intuitionistic
logic.
--
"Oh, sorry, Maggie. I'm sure you'd like to be alone with your manifestation."
John Baez
John Baez
When I was an undergraduate I was quite interested in logic and the
foundations of mathematics --- I was always looking for the most
mind-blowing concepts I could get ahold of, and Goedel's theorem, the
Loewenheim-Skolem theorem, and so on were right up there with quantum
mechanics and general relativity as far as I was concerned. I did my
undergrad thesis on computability and quantum mechanics, but then I sort
of lost interest in logic and started thinking more and more about
quantum gravity. The real reason was probably that my thesis didn't
turn out as interesting as I'd hoped, but I remember feeling at the time
that logic had become less revolutionary than in it was in the early
part of the century. It seemed to me that logic had become a branch of
mathematics like any other, studying obscure properties of models of the
Zermelo-Fraenkel axioms, rather than questioning the basic presumptions
implicit in those axioms and daring to pursue new, different approaches.
I couldn't really get excited about the properties of super-huge
cardinals. Of course, I knew a bit about intuitionistic logic and
various forms of finitism, but these seemed to be the opposite of
daring; instead, they seemed to appeal mainly to grumpy people who
didn't trust abstractions and wanted to do everything as conservatively
as possible. I was pretty interested in quantum logic, too, but I
tended to think of this more as a branch of physics than "logic" proper.
Anyway, it's now quite clear to me that I just hadn't been reading the
right stuff. I think Rota has said that the really interesting work in
logic now goes under the name of "computer science', but for whatever
reason, I didn't dig into the Journal of Philosophical Logic, other
logic journals, or proceedings of conferences on category theory,
computer science and the like and find the stuff that would have excited
me. It goes to show that one really needs to keep digging! Anyway, I
just went to a conference called the Lambda Calculus Jumelage up in
Ottawa, thanks to a kind invitation by Prakash Panangaden and Phil
Scott, who thought my ideas on category theory and physics might
interest (or at least amuse) the folks who attend this annual bash. It
became clear to me while up there that logic is alive and well!
Of course, I don't actually understand most of what these people are up
to, so take what I say with a large grain of salt. My goal here is more
to draw attention to some interesting-sounding ideas than to explain
them.
One interesting subject, which I think I'm finally beginning to get an
inkling of, is "linear logic". This was introduced in the following
paper (which I haven't gotten around to looking at):
1) Linear Logic, by Jean-Yves Girard, Theoretical Computer Science 50
(1987) pp. 1-102.
When I first heard about linear logic, it made utterly no sense. It
seemed to be a logic suitable for use in some completely different
universe than the one I inhabited! For example, there were the familiar
logical connectives "and" and "or", but they had weird alternate
versions called "tensor" and "par", the latter written with an
upside-down ampersand. There was also an alternate version of
the material implication "->", and a strange operation called "!"
(pronounced "bang") that somehow mediated between the logical
connectives I knew and loved and their eerie alter egos.
I understand a wee bit about these things now; one can get a certain
ways just by getting used to "tensor", since the rest of the weird
connectives are defined in terms of this one and the familiar ones.
(I won't worry about the "!" here.) One key idea, which finally
penetrated my thick skull, is that there is a good reason why "tensor"
does not satisfy the following deduction rule so characteristic of "and":
S |- p S |- q
-------------------
S |- p & q
meaning: if from the set of premisses S we can deduce p, and from S we
can also deduce q, then from S we can deduce p&q. The point is that in
linear logic one should not think of S as a *set* of premisses, but
rather as a *multiset*, meaning that the same premiss can appear twice.
The idea is that if we use one premiss in S to deduce something, we *use
it up*, and we can only use it again if S has several copies of that
premiss in it. As they say, linear logic is "resource-sensitive" (which
is apparently why computer scientists like it). So the idea is that in
linear logic,
S |- p&q
means something like "from the premisses S one can deduce p if one feels
like it, or alternatively one can deduce q if one feels like it, but not
necessarily both "at once", since there may not be enough copies of the
premisses to do that." On the other hand,
S |- p tensor q
is stronger, since it means something like "from the premisses S one can
deduce both p and q at once, since there are enough copies of all the
premisses in S to do it." Thus "&" satisfies the above deduction rule
in linear logic just as in classical logic, but "tensor" does not;
instead, it satisfies
S |- p T |- q
-------------------
S U T |- p tensor q
where S U T denotes the union of the multisets S and T (so that if both
S and T have one copy of a premiss, S U T has two copies of it).
Well, let me leave it at that. I should add that there is a paper
available online,
2) Linear logic for generalized quantum mechanics, by Vaughan Pratt,
available in LaTeX format (compressed) by anonymous ftp from
boole.stanford.edu, as the file pub/ql.dvi.Z,
which relates linear logic and quantum logic, and which is part of a body
of work relating linear logic and category theory, with the key idea
being that "linear logic is a logic of monoidal closed categories in
much the same way that intuitionistic logic is a logic of Cartesian
closed categories" --- here I quote
3) Hopf algebras and linear logic, by Richard Blute, to appear in
Mathematical Structures in Computer Science.
I suppose to most people, explaining linear logic in terms of monoidal
closed categories may seem like using mud to wipe ones windshield.
However, to some of us monoidal closed categories are rather familiar
things, and in fact anyone who knows about vector spaces, linear maps,
and the vector spaces Hom(V,W) and V tensor W knows a really good
example of a monoidal closed category. Thus monoidal closed categories
can be viewed as an abstraction of linear algebra, and indeed this is
how "linear logic" got its name.
It seems that I should read the following papers, too, before I really
understand the connection between linear logic and category theory:
4) Linear logic, *-autonomous categories and cofree coalgebras, by R. A. G.
Seely, in Categories in Computer Science and Logic, Contemp. Math.
92 (1989).
5) Quantales and (noncommutative) linear logic, by D. Yetter, Journal of
Symbolic Logic 55 (1990), 41-64.
A terse summary of linear logic in terms a categorist might like can be
found in Section 3.5 of Pratt's paper cited above. I should add that
Pratt has lots of other interesting papers available online (try the
file pub/README).
--------------------------------------------------------------------------
Previous issues of "This Week's Finds" and other expository articles on
mathematics and physics (as well as some of my research papers) can be
obtained by anonymous ftp from math.ucr.edu; they are in the
directory "baez." The README file lists the contents of all the papers.
On the World-Wide Web, you can attach to the address
http://info.desy.de/user/projects/Physics.html to access these files and
more on physics. Please do not ask me how to use hep-th or gr-qc;
instead, read the file preprint.info.
john baez
>However, one thing puzzles me. The linear logic you describe sounds like fun
>stuff. But whether you regard it as multi-set premised logic, or as computer
>science with non-reusable inputs for sentence derivation, or whatever, it still
>seems to me to be "a branch of mathematics like any other", and hardly the
>"mind-blowing concept" or "revolutionary" approach to foundations that we all
>yearned for as undergrads (and perhaps still do).
>This is in no way meant to be a put-down, (and indeed I'm grateful for the tip
>to read up on linear logic); but it seems there's no real connection between
>your initial plaint and your later (clearly justified) enthusiasm.
>Am I missing something here?
Hmm. Clearly (as various followup posts indicate) I don't understand
linear logic very well. But I think it's more than just classical logic
repackaged in a new way, as your two descriptions of it would make it
sound. I guess my description emphasized how I was trying to get a
handle on linear logic by relating it to classical logic. But there are
models of linear logic that are really different from any of the models
for classical or intuitionistic logic. (The paper by Blute I listed
starts going into this.) The main way I have of understanding this, to
the measly extent I do, is the slogan I quoted: intuitionistic logic is
to Cartesian closed categories as linear logic is to more general
monoidal categories. I sort of know how much, and in what ways,
monoidal categories are more general than Cartesian closed ones, so if
this slogan has any validity to it, linear logic should be quite a bit
different in flavor than intuitionistic (or classical) logic. This
sounds more revolutionary to me than worrying about the fine structure of
the recursive hierarchy, ineffable cardinals, and the like. Maybe my
enthusiasm is due to ignorance; maybe someone who really understands
linear logic well should post!!!
Bill Taylor
|> When I was an undergraduate I was quite interested in logic and the
|> foundations of mathematics --- I was always looking for the most
|> mind-blowing concepts I could get ahold of,
... ...
|> I remember feeling at the time
|> that logic had become less revolutionary than in it was in the early
|> part of the century. It seemed to me that logic had become a branch of
|> mathematics like any other,
Very well put! I remember feeling much the same; like a lot of folk, I expect.
|> I think Rota has said that the really interesting work in
|> logic now goes under the name of "computer science',
This sounds like a sensible view.
However, one thing puzzles me. The linear logic you describe sounds like fun
stuff. But whether you regard it as multi-set premised logic, or as computer
science with non-reusable inputs for sentence derivation, or whatever, it still
seems to me to be "a branch of mathematics like any other", and hardly the
"mind-blowing concept" or "revolutionary" approach to foundations that we all
yearned for as undergrads (and perhaps still do).
This is in no way meant to be a put-down, (and indeed I'm grateful for the tip
to read up on linear logic); but it seems there's no real connection between
your initial plaint and your later (clearly justified) enthusiasm.
Am I missing something here?
-------------------------------------------------------------------------------
Bill Taylor w...@math.canterbury.ac.nz
-------------------------------------------------------------------------------
Watch out for my definitive series of books on Prime Numbers.
Just coming into print now... volume I: "The Even Primes"
-------------------------------------------------------------------------------
Paul Budnik
: This Week's Finds in Mathematical Physics (Week 40)
: John Baez
[...]
: It seemed to me that logic had become a branch of
: mathematics like any other, studying obscure properties of models of the
: Zermelo-Fraenkel axioms, rather than questioning the basic presumptions
: implicit in those axioms and daring to pursue new, different approaches.
: I couldn't really get excited about the properties of super-huge
: cardinals. [...]
In discussing such issues it is important to distinguish between different
ways of extending logic. One is to extend the framework of logic with
large cardinal axioms or other attempts to make it more powerful. It
is clear from Godel's theorem that this will always be possible.
Another way is to modify the rules of the propositional
calculus. When people talk about contraractual definiteness they are
talking about logic at the level of the propositional calculus. It is
a kind of physicists version of intuitionism where the excluded middle
is denied for possible experiments that were never performed. There is
little reason to change logic in this way. The only motivation for
doing this is to avoid some of the implications of QM about locality
that trouble some physicists.
[...]
From your discussion I take it that linear logic as something embedded
in classical logic and not an intended as a replacement for it.
: 2) Linear logic for generalized quantum mechanics, by Vaughan Pratt,
: available in LaTeX format (compressed) by anonymous ftp from
: boole.stanford.edu, as the file pub/ql.dvi.Z,
: which relates linear logic and quantum logic, and which is part of a body
: of work relating linear logic and category theory, with the key idea
: being that "linear logic is a logic of monoidal closed categories in
: much the same way that intuitionistic logic is a logic of Cartesian
: closed categories" --- here I quote
Is any of what you are talking about an attempt at replacing the basic
laws of logic at the level of the propositional calculus with something
different?
Paul Budnik
Matthew P Wiener
>In article <380oa0$9...@netnews.upenn.edu> wee...@sagi.wistar.upenn.edu (Matthew P Wiener) writes:
>>In article <37vi3l$r...@galaxy.ucr.edu>, baez@guitar (john baez) writes:
>>The only thing I know of called linear logic is a system in between
>>classical and intuitionistic. Not all excluded middles are allowed
>>in, but I think "p=>q v q=>p" is, and that this characterizes linear
>>logic.
>While it's conceivable that there's something that I'm missing, my belief
>is that you're both wrong.
I'm perhaps totally wrong.
I'm thinking of a system of Dummett's from 30 some years ago. I have
heard *that* one called linear logic, but I don't think that was its
official name, but it is obviously not the stuff in the Girard book.
Jamie Andrews
In article <380oa0$9...@netnews.upenn.edu>,
Matthew P Wiener <wee...@sagi.wistar.upenn.edu> wrote:
>The only thing I know of called linear logic is a system in between
>classical and intuitionistic. Not all excluded middles are allowed
>in, but I think "p=>q v q=>p" is, and that this characterizes linear
>logic.
The linear logic I know of is a sequent calculus-based
logic which removes most of the classical connectives and
replaces them with much weaker versions and some new
connectives. We can show that there is a translation of
intuitionistic logic into linear logic in the same sense that
there is a translation (e.g. Goedel's) of classical logic into
intuitionistic logic.
Linear logic is basically a relevance logic devised by
Jean-Yves Girard. (_Theoretical Computer Science_ v.50 1987
pp.1-102) It weakens traditional relevance logic in ways that
relevance logicians hadn't explored much.
A more sociological description might be that linear logic
is to 1990s computer science what category theory is to 1990s
mathematics... make of that what you will. :-)
--Jamie.
ja...@cs.sfu.ca
"Make sure Reality is not twisted after insertion"
james dolan
>From your discussion I take it that linear logic as something embedded
>in classical logic and not an intended as a replacement for it.
...
>Is any of what you are talking about an attempt at replacing the basic
>laws of logic at the level of the propositional calculus with something
>different?
you can study many sorts of "alternative logic" quite deeply without
making any ultimate commitment as to whether the "alternative logic"
is supposed to be more or less (or equally or "non-comparably")
fundamental than the "standard logic", reserving for yourself the
flexibility to adopt different attitudes whenever they seem
convenient, and to perhaps eventually make some ultimate commitment if
the things you discover move you to.
Timothy Y. Chow
Bill Taylor <w...@math.canterbury.ac.nz> wrote:
>ba...@ucrmath.ucr.edu (John Baez) writes:
>|> I remember feeling at the time
>|> that logic had become less revolutionary than in it was in the early
>|> part of the century. It seemed to me that logic had become a branch of
>|> mathematics like any other,
>
>Very well put! I remember feeling much the same; like a lot of folk, I expect.
Actually, I have a slightly different view of this. IMO, making logic a
branch of mathematics *was* the revolutionary idea. That's perhaps stating
it too strongly, but the key behind the revolutionary ideas was making the
methods of mathematical investigation (i.e., proofs) themselves the objects
of mathematical investigation. (This gives more credit to Hilbert than to
Goedel than is usual, I realize.)
Perhaps logic is less revolutionary now than before, but I don't think
this has anything to do with its "becoming a branch of mathematics like
any other."
--
Tim Chow tyc...@math.mit.edu
Where a calculator on the ENIAC is equipped with 18,000 vacuum tubes and weighs
30 tons, computers in the future may have only 1,000 vacuum tubes and weigh
only 1 1/2 tons. ---Popular Mechanics, March 1949
john baez
>paul budnik writes:
>>From your discussion I take it that linear logic as something embedded
>>in classical logic and not an intended as a replacement for it.
It's not "embedded in it", in the sense that it's a "from scratch"
axiomatic system just like classical logic. I don't think anyone
expects it to "replace" classical logic, especially because - if I
understand it correctly - it's a conservative extension of classical
logic, meaning that any reasoning valid in classical logic is valid in
linear logic, and anything that's provable in linear logic which only
uses the connectives of classical logic is in fact provable in classical
logic. (I could be wrong about this, so if there are any linear
logicians out there, they should correct me if I've got it wrong.) So
the proper thing to say is that linear logic "subsumes" classical logic.
>>Is any of what you are talking about an attempt at replacing the basic
>>laws of logic at the level of the propositional calculus with something
>>different?
>you can study many sorts of "alternative logic" quite deeply without
>making any ultimate commitment as to whether the "alternative logic"
>is supposed to be more or less (or equally or "non-comparably")
>fundamental than the "standard logic", reserving for yourself the
>flexibility to adopt different attitudes whenever they seem
>convenient, and to perhaps eventually make some ultimate commitment if
>the things you discover move you to.
I think most of the people I was talking to take an attitude like that
which James describes here. I don't think these folks are moralizing
firebrands trying to convert the world to linear logic. That sort of
evangelical impulse seems to be confined to puritanical movements like
finitism and intuitionism, which would *restrict* our forms of
reasoning. I think people interested in linear logic are interested in
exploring various systems of logic and not too interested in picking one
system and decreeing it to be "fundamental".
Lee Rudolph
>The point is that in
>linear logic one should not think of S as a *set* of premisses, but
>rather as a *multiset*, meaning that the same premiss can appear twice.
>The idea is that if we use one premiss in S to deduce something, we *use
>it up*, and we can only use it again if S has several copies of that
>premiss in it. As they say, linear logic is "resource-sensitive" (which
>is apparently why computer scientists like it).
This sounds like what Yesenin-Volpin was talking about, 20 years ago
and more. Is it? (I plead ignorance.)
Lee Rudolph
Paul Budnik
: In article <37vecn$9...@ucrmath.ucr.edu> jdo...@ucrmath.ucr.edu (james dolan) writes:
[...]
: >>Is any of what you are talking about an attempt at replacing the basic
: >>laws of logic at the level of the propositional calculus with something
: >>different?
: >you can study many sorts of "alternative logic" quite deeply without
: >making any ultimate commitment as to whether the "alternative logic"
: >is supposed to be more or less (or equally or "non-comparably")
: >fundamental than the "standard logic", reserving for yourself the
: >flexibility to adopt different attitudes whenever they seem
: >convenient, and to perhaps eventually make some ultimate commitment if
: >the things you discover move you to.
: I think most of the people I was talking to take an attitude like that
: which James describes here. I don't think these folks are moralizing
: firebrands trying to convert the world to linear logic. That sort of
: evangelical impulse seems to be confined to puritanical movements like
: finitism and intuitionism, which would *restrict* our forms of
: reasoning. I think people interested in linear logic are interested in
: exploring various systems of logic and not too interested in picking one
: system and decreeing it to be "fundamental".
Of course to study a system is not to insist that it is the only valid
system. However the distinction I was asking about is valid regardless
of how little or much commitment you make to what you study. The
distinction is particularly important in this context because only a
change in logic at the level of the propositional calculus can deal
with the question of whether quantum mechanics predicts nonlocal
causal effects. I get the impression that none of the technical work
you are referring to changes logic at this level but I am still not sure.
Since I advocate a from of finitism I want to respond to your comment
about restricting our forms of reasoning. My goal is not restrict but
to expand the forms of our reasoning. Mathematics has had a historical
tendency to adopt goals that were overly ambitious. We have Frege's
set theory that produced Russell's paradox and Hilbert's program that
led to Godel's incompleteness theorem. It is reasonable to assume that
that there are other errors of this nature that do not lead to absolute
contradictions but still lead to overly ambitious programs. I think Zermelo
Frankel set theory and large cardinal axioms are an example of this.
They are a way of developing and extending mathematics
that *seem* enormously powerful but in fact limit ones ability to
extend mathematics because they put the focus on structures that we can
never understand. They are structures that have no connection to anything
in our universe and I think no connection to anything that exists. I believe
there are structures that can model ZF but these structures are not
what one wants to mean by ZF because among other things they are
countable. What we need to do is study those structures directly and
not study a phantom image of them in the form cardinal numbers.
Paul Budnik
james dolan
->paul budnik writes:
-
->>From your discussion I take it that linear logic as something embedded
->>in classical logic and not an intended as a replacement for it.
-
-It's not "embedded in it", in the sense that it's a "from scratch"
-axiomatic system just like classical logic. I don't think anyone
-expects it to "replace" classical logic, especially because - if I
-understand it correctly - it's a conservative extension of classical
-logic, meaning that any reasoning valid in classical logic is valid in
-linear logic, and anything that's provable in linear logic which only
-uses the connectives of classical logic is in fact provable in classical
-logic. (I could be wrong about this, so if there are any linear
-logicians out there, they should correct me if I've got it wrong.) So
-the proper thing to say is that linear logic "subsumes" classical logic.
even if it did "subsume" classical logic in some sense, that wouldn't
seem to rule out the possibility that it could also be "embedded in"
classical logic in some sense. (and furthermore, composing the
"subsuming" process with the "embedding" process, in either order,
need not, even if it makes sense, produce the identity
transformation.)
-I think most of the people I was talking to take an attitude like that
-which James describes here. I don't think these folks are moralizing
-firebrands trying to convert the world to linear logic. That sort of
-evangelical impulse seems to be confined to puritanical movements like
-finitism and intuitionism, which would *restrict* our forms of
-reasoning. I think people interested in linear logic are interested in
-exploring various systems of logic and not too interested in picking one
-system and decreeing it to be "fundamental".
in line with the idea that there can be lots of different ways of
embedding different logics inside of each other, it seems possible
that the question of which sorts of logical systems deserve to be
considered "restrictive" (and their advocates "puritanical") may be
Patrick Lincoln
> Date: 19 Oct 1994 06:38:51 GMT
> ...
> Hmm. Clearly (as various followup posts indicate) I don't understand
> linear logic very well. But I think it's more than just classical logic
> repackaged in a new way, as your two descriptions of it would make it
> sound.
First of all, when you say linear logic I assume that you are speaking
about Girard's linear logic, as described in the theoretical computer
science journal (vol 50 1987). This logic is closely related to
previous work, like *-autonomous categories (studied by M.Barr) and
the Lambek Calculus (developed by J.Lambek for natural language
parsing and understanding: a noncommutative precursor to LL).
Girard developed linear logic as part of his analysis of the
semantics of intuitionistic logic. In particular, Girard
found that intuitionistic implication A => B decomposes nicely
into two separate operations as !A -o B, where ! means
'reuse at will' and -o means 'linearly implies'.
Linear logic can be seen as a multiset logic, where
the multiplicity of formulas on both sides of the |- is
important (contraction and weakening are allowed everywhere in LK,
only on the left in LJ, and nowhere in LL).
In this setting conjunction separates into two
versions, one which shares context (the additive 'with' &)
and one which splits the context (the multiplicative 'tensor' *).
Two disjunctions also arise dual to the conjunctions: the additive
'plus' + and the multiplicative 'par' (upside-down &).
Linear implication A -o B is defined as (not A) par B.
The exponentials ('of course' ! and its dual 'why not' ?) complete
the set of propositional connectives of linear logic. One can
add the usual first and/or higher-order quantifier rules as well.
I posted a note to sci.logic in early sept giving informal readings of all
the linear connectives and giving some starting points for reading.
Linear logic is more detailed than classical or intuitionistic
logic. One can decompose LK or LJ connectives into several orthogonal
linear operations. Linear logic is very expressive: propositional
linear logic is undecidable. Surprisingly small fragments have
surprisingly huge complexity: validity of formulas written in just
{*,-o,1,bottom} (no propositional literals, no additives, no
exponentials, no quantifiers, just multiplicative connectives and
true and false, something like linear circuit evaluation) is NP-complete.
Intuitionistic logic embeds via !A -o B into linear logic preserving
most interesting proof-theoretic properties. Girard developed two
semantics for linear logic which give rise to semantics for
intuitionistic logic (seen through his embedding). One can
of course embed classical logic into intuitionistic logic using double
negation. One can use linear logic in the study of other logics:
propositional intuitionistic logic embeds into propositional linear
logic without exponentials: that is, the use of structural rules
(contraction and weakening) in prop LJ isn't always necessary. All these
embeddings preserve provability: eg. A => B in LJ iff !A -o B in LL,
but the classical and intuitionistic connectives do not appear
native in linear logic. One cannot easily translate formulas
the other way, from LL to LJ or LK, since LK forgets how many
copies of formulas you have, and so LL-unprovable formulas may
be translated to LK-provable formulas. Complexity considerations
also dictate the impossibility of such translations.
There are now many available semantics that can confer understanding
of the strange linear sequent calculus, some based on games (Abramsky
and Jagadeesan solved a long-standing open problem regarding full
completeness for PCF using game semantics from linear logic, see also
A.Blass,P.Curien), event spaces (Pratt), probabilities (see
file://ftp.cis.upenn.edu/pub/papers/scedrov/ip.dvi.Z), Lauchli
semantics (new work by Blute & Scott), and *-autonomous categories
(Seely &c), in addition to Girard's original two semantics,
As for why computer scientists have taken a liking to LL, there are
many reasons. Functional programming languages (S.Abramsky, P.Wadler,
P.Lincoln, J.Mitchell, N.Benton, G.Bierman, V.DePaiva, M.Hyland,
I.Mackie, J.Chirimar, C.Gunter, J.Riecke, &c) compilers (P.O'Hearn,
D.Wakeling, P.Lincoln, H.Baker, Y.Lafont, &c), constraint systems
(V.Saraswat, P.Lincoln, V.Gupta, M.Okada, A.Yonezawa, N.Kobayashi,&c),
inheritance (Girard), databases (N.Bidoit, S.Cerrito, C.Froidevaux,&c),
and other CS topics have been considered using linear logic
as a tool of analysis.
The proof theory is rich. Too many authors to list here.
Recently V.Pratt, P.Panangaden, and others have been exploring
connections between linear logic and some physics related things.
Pratt's 'linear logic for generalized quantum mechanics' and
other papers (see file://boole.stanford.edu/pub/ABSTRACTS), and
Panangaden's work on connections between linear proof nets and
Feynman diagrams are interesting, but are certainly in the very
early stages, and I'm not an expert on those things.
For some pointers to wwwebable and ftpable papers and bibliographies
see http://www.csl.sri.com/linear/sri-csl-ll.html.
pdl.
Henry G. Baker
>This Week's Finds in Mathematical Physics (Week 40)
>John Baez
>
>inkling of, is "linear logic". This was introduced in the following
>paper (which I haven't gotten around to looking at):
>
>1) Linear Logic, by Jean-Yves Girard, Theoretical Computer Science 50
>(1987) pp. 1-102.
Linear logic is also useful for thinking about (and performing)
computation. Linear logic leads directly into the concept of
'use-once' variables, which have to be explicitly copied to be used
more than once, and have to be explicitly deleted. Of course, certain
_types_ of these variables may have to be conserved, and may not be
deleted OR copied -- e.g., the I/O stream which talks to the user.
Thus, it is possible to start putting conservation laws into computer
software using some of the ideas behind linear logic. These conservation
laws are useful (among other things) the same way that strong typing and
physical units are useful -- as consistency checks on the software.
There are a number of papers in my ftp directory about using linear
logic ideas in computation.
Henry Baker
Read ftp.netcom.com:/pub/hbaker/README for info on ftp-able papers.
Bill Taylor
|> Bill Taylor <w...@math.canterbury.ac.nz> wrote:
|> >ba...@ucrmath.ucr.edu (John Baez) writes:
|> >|> I remember feeling at the time
|> >|> that logic had become less revolutionary than in it was in the early
|> >|> part of the century. It seemed to me that logic had become a branch of
|> >|> mathematics like any other,
|> >Very well put! I remember feeling much the same; like a lot of folk, I expect.
|> Actually, I have a slightly different view of this. IMO, making logic a
|> branch of mathematics *was* the revolutionary idea.
Very astute and pithy!
|> That's perhaps stating
|> it too strongly, but the key behind the revolutionary ideas was making the
|> methods of mathematical investigation (i.e., proofs) themselves the objects
|> of mathematical investigation. (This gives more credit to Hilbert than to
|> Goedel than is usual, I realize.)
As usual, Tim, you have got to the heart of it so simply and easily. I agree
with this view totally. (And if any others object that I also agreed with
John Baez totally, and that John and Tim say different things, then...
I will also agree with them totally!)
Thanks for your take on this one Tim.
-------------------------------------------------------------------------------
Bill Taylor w...@math.canterbury.ac.nz
-------------------------------------------------------------------------------
My opinion may have changed, but not the fact that I am right.
-------------------------------------------------------------------------------
Matthew P Wiener
>Is there some reason why intuitionism et al are singled out for gratuitous
>top-of-the-head commentary?
Yes. Its practitioners made strong universal claims at one point.
> I mean, you don't often hear disabusals of
>algebraic geometry as *restrictive* in its reliance on polynomials, or how
>combinatorics is a Luddite conspiracy to take away our toys.
These folks have just secretly tried to take over mathematics.
john baez
>Is there some reason why intuitionism et al are singled out for gratuitous
>top-of-the-head commentary?
Probably because some of them, like Bishop, attack classical mathematics
as "schizophrenic". The only intuitionist I know well personally,
Christer Hennix --- actually an "ultraintuitionist" follower of
Yesenin-Volpin --- seriously puts down classical mathematics as a bunch
of mistaken junk that's not worth learning. In short, there really
*are* puritanical intuitionists, finitists, constructivists and the
like, who think a kind of revolution is required to bring mathematics to
its senses. (I have no idea what Brouwer's exact opinion about this
was; while Hilbert said he was trying to expel us from the paradise
Cantor built, deprive mathematicians of proof by contradiction like
depriving a boxer of his gloves, etc. I don't know whether *Brouwer*
said explicitly that people should *stop doing* classical mathematics.)
After having argued with Hennix for a long time, I decided that in
certain cases the only sensible response to such positions was to make
fun of them. And I like joking around. This has *nothing* to do with
people who are interested in studying alternative forms of logic, or
even "restricted" forms of logic, as part of the general goal of
mathematics to understand everything in all possible ways. In fact,
right now I am busily struggling to understand Mac Lane and Moerdijk's
book on topoi in an effort to see how intuitionistic logic is related to
cartesian closed categories, and I think it's fascinating stuff.
Note also that as Dolan pointed out, some forms of logic are not really
as restrictive as they seem! One can prove not(not(P)) in
intuitionistic logic, and the distinction between not(not(P)) and P
makes it in a sense more expressive than classical logic.
"Restrictiveness" often has more to do with the emotional tone of a
certain body of work than with the mathematics itself. Thus, while I
have nothing against algebraic geometry (except a certain frustration at
my own ignorance of it), I would gladly make fun of algebraic geometers
who insisted that the only functions we can "really comprehend" are
polynomials.
Randall Holmes
Tal Kubo (ku...@brauer.harvard.edu) wrote:
: Is there some reason why intuitionism et al are singled out for gratuitous
: top-of-the-head commentary? I mean, you don't often hear disabusals of
: algebraic geometry as *restrictive* in its reliance on polynomials, or how
: combinatorics is a Luddite conspiracy to take away our toys. But with
: intuitionism there is somehow a recurring need to Cast Out The Heretics, or
: at least to paint them as crackpots (grumpy malcontents, as Baez put it in
: week 40's Finds). The review of van Stigt's book on Brouwer in the most
: recent American Mathematical Monthly, for example, refers to Bishop and
: Kronecker as "constructivist-fascists" -- this in an article with a
: *favorable* assessment of Brouwer and his philosophy. So who is
: puritanical, anyway?
Certainly there is a reason. Many intuitionists are not just studying a
particular class of mathematical models. They claim the mathematics
that other mathematicians know and love is not sound.
I suspect it is sound in the sense of being consistent and in the
stronger sense that the conclusions we can draw from it about recursive
processes are correct. On the other hand I think most of the objects
it aims to talk about do not exist. It is sound because those objects
have a countable model in a universe that talks only about properties
of Turing Machines (and thus properties of the integers). Even this model
does not exist as physical objects exist but all the properties of TMs
within this model have a objective meaning in a potentially infinite
universe.
It is not just taking away their toys that mathematicians resent.
Taking away their illusions about the metaphysical status of
those toys also draws their ire.
Paul Budnik
Holmes:
A case in point regarding my remark in a parallel post about
the incompatibility between a correct view of mathematical objects and
the spirit of the age. There is no coherent account of mathematics in
terms of properties of physical objects. There isn't even a coherent
account of physical objects in terms of the properties of physical
objects (alone): all actual accounts involve mathematical objects,
and the attempt to eliminate the fundamental role of these (and
possibly other universals) is generally not actually attempted in
practice; an appeal to prevailing prejudices is usually taken to be
sufficient.
--
The opinions expressed | --Sincerely,
above are not the "official" | M. Randall Holmes
opinions of any person | Math. Dept., Boise State Univ.
or institution. | hol...@math.idbsu.edu
Jamie Andrews
Paul Budnik <pa...@mtnmath.mtnmath.com> wrote:
> Many intuitionists are not just studying a
>particular class of mathematical models. They claim the mathematics
>that other mathematicians know and love is not sound.
I would say rather that they claim that some of the
mathematics that other mathematicians do is meaningless.
Brouwer, Weyl and so on were really just articulating
a discomfort with non-constructive proofs that was quite common
at the time. Proponents and opponents of non-constructive
proofs were equally dogmatic back then, I would say.
Over time, as with many minor traditions in academic
disciplines, some of the ideas of intuitionism got integrated
into the mainstream, and the minor tradition attracted its share
of crackpots that pushed it to the limits. That doesn't mean we
can dismiss any intuitionist as a crackpot.
90 years from now, I'm sure there will be people ranting
about category theory being the basis of all human thought,
but that doesn't mean we should dismiss it. Completely, at least. :-)
Ron Maimon
|> In article <1994Oct26.0...@hulaw1.harvard.edu> ku...@brauer.harvard.edu (Tal Kubo) writes:
|>
|> >Is there some reason why intuitionism et al are singled out for gratuitous
|> >top-of-the-head commentary?
|>
|> Probably because some of them, like Bishop, attack classical mathematics
|> as "schizophrenic"
Well, classical math is pretty schitzophrenic.
You have one theorem that says that the real numbers admit a well ordering,
and then you have another theorem that says that any ordering of the real
numbers you will be given ever in your entire life will _not_ be a well
ordering.
You have one theorem that says that you can chop up a grape into a finite
number of peices and rotate these peices and glue them together disjointly
to form a set as big as the sun, but you have another theorem that says
that no set of grape-peices that anyone will ever present to you will have
this property.
You have a theorem that says that every vector space has a basis, and you
have a theorem that says that no one will ever write down a basis for
the vector space of real valued functions on Z.
This is schitsophrenia with a vengence. The only way to sort these things
in your mind is to realize that it is a qualitatively different thing to
prove a statement that to prove it's contrapositive and it is a
qualitatively different thing to prove a theorem using finitistic axioms
vs. proving it using the axiom of choice.
How hard can it be to take these two facts into account?
--
Ron Maimon
! You're a star bellied sneetch, you suck like a leech
Jello ! you want everyone to act like you
Biafra ! kiss ass while you bitch so you can get rich
! but your boss gets richer off you
Matthew P Wiener
>|> Probably because some of them, like Bishop, attack classical mathematics
>|> as "schizophrenic"
>Well, classical math is pretty schitzophrenic.
>You have one theorem that says that the real numbers admit a well ordering,
>and then you have another theorem that says that any ordering of the real
>numbers you will be given ever in your entire life will _not_ be a well
>ordering.
There are finitistic theorems that are just as "schizophrenic". For
example, Goedel's first incompleteness theorem says--even constructs--
ought-to-be-true statements with no proofs.
A dyed-in-the-wool finite purist may perhaps not officially believe in
the ought-to-be-true part--but do any of them seriously try to prove
PA inconsistent?
Neil Rickert
>In article <38mic6$n...@galaxy.ucr.edu>, ba...@guitar.ucr.edu (john baez) writes:
>Well, classical math is pretty schitzophrenic.
>You have one theorem that says that the real numbers admit a well ordering,
Right.
>and then you have another theorem that says that any ordering of the real
>numbers you will be given ever in your entire life will _not_ be a well
>ordering.
There ain't no such theorem. "Ever in your entire life" is not
suitable mathematical terminology for use in a theorem.
>You have one theorem that says that you can chop up a grape into a finite
>number of peices and rotate these peices and glue them together disjointly
>to form a set as big as the sun,
Again, there is no such theorem. The Banach-Tarski paradox is not
about dissecting grapes.
> but you have another theorem that says
>that no set of grape-peices that anyone will ever present to you will have
>this property.
Again, there is no such theorem, although that is a plausible
consequence of various theorems. Theorems are not about grape
pieces. If intuitionists think that theorems are about grape pieces,
then they have been drinking too much fermented grape juice.
>You have a theorem that says that every vector space has a basis,
Right.
> and you
>have a theorem that says that no one will ever write down a basis for
>the vector space of real valued functions on Z.
Wrong again. Such statements are not the proper content of
theorems. The question of what a person will or will not actually
write down is a question of psychology or sociology, or perhaps
biology. It is not a question of mathematics.
>This is schitsophrenia with a vengence.
You may happen to be schizophrenic, but there is no need for you to
inappropriatly attribute your own schizophrenia to others.
> The only way to sort these things
>in your mind is to realize that it is a qualitatively different thing to
>prove a statement that to prove it's contrapositive and it is a
>qualitatively different thing to prove a theorem using finitistic axioms
>vs. proving it using the axiom of choice.
No. The way to sort this out is to realize that mathematics is not
about real world objects, such as grapes.
Paul Budnik
: A case in point regarding my remark in a parallel post about
: the incompatibility between a correct view of mathematical objects and
: the spirit of the age. There is no coherent account of mathematics in
: terms of properties of physical objects. There isn't even a coherent
: account of physical objects in terms of the properties of physical
: objects (alone): all actual accounts involve mathematical objects,
: and the attempt to eliminate the fundamental role of these (and
: possibly other universals) is generally not actually attempted in
: practice; an appeal to prevailing prejudices is usually taken to be
: sufficient.
All either mathematics or physics can ever accomplish is to describe
complex structures in terms of simpler structures. The most fundamental
elements in any such analysis can be equally well regarded as mathematical
or physical. Describing more complex physical structures in terms of more
fundamental ones is applied mathematics.
If you want to understand what the fundamental `building blocks of existance'
are you have to go outside of both mathematics and physics. My philosophcial
speculation is that the essense of everything that exists is a form of
consciousness or self awareness not in the sense of the complex structure
of human consciousness but in the sense of say a single point in a visual
field. Human consciousness and self awareness is what it means for a
physical object to exist and be structured as the human mind and body
is and to interact with the world as we do. There are no `building blocks'.
There is a diffuse form of unviersal consciouness out of which individuals
are carved as if by some cosmic stone mason.
These individual structures are finite because consciouness is
specific and finite. Unlike infinite sets if you add something to a conscious
gestalt it is always different. There may no fixed limit to the number of
conscious experiences that can evolve but each of them is finite. That
is what I mean by a potentially infinite universe and why I think most
of the objects mathematicians reason about do not exist although most
of them have an interpretation in terms of how structures in a potentially
infinite universe might evolve.
Paul Budnik
Matthew MacIntyre
: Is there some reason why intuitionism et al are singled out for gratuitous
: top-of-the-head commentary? I mean, you don't often hear disabusals of
: algebraic geometry as *restrictive* in its reliance on polynomials,
I would, if it were not for Chow's theorem.
Ramsay-MT
Ron Maimon writes:
|You have one theorem that says that the real numbers admit a well ordering,
|numbers you will be given ever in your entire life will _not_ be a well
|ordering.
No, there isn't a theorem that says that. One can give a formula F(x,y)
which defines a well-ordering of the reals, if a certain statement (known
as V=L) is true. By a result of Godel, there is no proof of V<>L in ZFC.
To show that there isn't an explicit well-ordering of the reals you will
at least have to disprove V=L, and I suspect quite a bit more (even if we
grant you that by "explicitly giving" a well-ordering we mean defining the
well-ordering in some fixed language like first-order set theory).
Keith Ramsay
Paul Budnik
: I believe that a more fundamental distinction (than that between complexity
: and simplicity) is that between informal and formal objects. The universe
: is ultimately ineffable in the sense that we can't give a complete formal
: description of it - it can't be reduced absolutely to the tidy world of
: discrete symbols; "The Tao that can be said is not the true Tao." Even
: mathematics is more than just the formal systems used to express it.
: Nonetheless, by some magic - which, I'm afraid, I cannot explain but must
: accept as an article of faith - it seems possible and useful to use formal
: symbols to give approximate expression to aspects of the informal real
: world. What physics accomplishes is to set up a formal system that we can
: (informally) relate to the real world and - if it is a successful physics -
: thereby know better what the real world does.
: Here's a simpler example: the true specification of a computer program is
: "ineffable" or informal. Fundamentally, it's quality and fitness for
: purpose, but these depend on users' needs and expectations, and these are
: incompletely understood and indeed change with time. A formal specification
: is good insofar as programs satisfying it (a formal relation) have quality
: and fitness for purpose (informal notions).
You seem to be saying that reality is not reducible to a formal description
and that is more fundamental than the difference between simplicity and
complexity. I certainly agree. In fact I agree so much that it would never
occur to me to make a posting about it.
This does not imply that it is impossible *even in theory* to give a
formal description that *models* physical reality in complete detail.
I suspect it is possible in theory (but not in practice) to fully
characterize any finite space time volume with a formal description that
will fully model what happens in the collapsing light cone for that volume.
However this is a very limited characterization. For example it says
nothing about what "user's needs and expectations are" even
thought it may be able to fully model their behavior.
Paul Budnik
Neil Rickert
>You seem to be saying that reality is not reducible to a formal description
>and that is more fundamental than the difference between simplicity and
>complexity. I certainly agree. In fact I agree so much that it would never
>occur to me to make a posting about it.
>This does not imply that it is impossible *even in theory* to give a
>formal description that *models* physical reality in complete detail.
Any formal model which models physical reality in complete detail
would have to include within that model, the existence of a modeler
modeling the model in complete detail. There would appear to be a
problem of an infinite chain of models and modelers.
>I suspect it is possible in theory (but not in practice) to fully
>characterize any finite space time volume with a formal description that
>will fully model what happens in the collapsing light cone for that volume.
One might imagine that one could escape from the universe, but this
can never be more than imagination. Then, in one's imagined
existence outside the universe, one might in theory model that
universe as an external observer. But any idea that one could model
the universe while remaining within that universe seems obviously
wrong.
unknown mail address
>From: wee...@aries.wistar.upenn.edu (Matthew P Wiener)
>Subject: Re: This Week's Finds in Mathematical Physics (Week 40)
>Date: 26 Oct 1994 14:43:15 GMT
hhu.forum Y 0
hhu.gibs Y 0
hhu.linux Y 0
hhu.mach Y 0
hhu.modem Y 0
hhu.netadmins Y 0
hhu.rzinfos Y 0
hhu.software Y 0
Lawrence McKnight
writes:
>Mind you, I don't buy it myself (I'm rather fond of measurable
cardinals).
>But I listen with respect.
>
Oh, no. Think how confusing things will get if those who cannot
understand finite induction start trying to understand Ulam
measureability.
--
----------------------------------------------------------
Larry McKnight...........
Tal Kubo
Even if you care only about smooth projective complex manifolds,
the odious finitistic considerations impose themselves. e.g., computing
Betti numbers of interesting analytic spaces by counting points on
the reduction mod p.