[Prev][Next][Index][Thread]

Linear logic question



Date: Wed, 10 Jun 92 14:56:31 BST

Define the formulae of linear logic as usual:

	atoms			X
	linear formulae		A, B ::=  X | (A -o B) | !A

Define also two subsets of formulae:

	standard formulae	A*, B* ::=  X | (A$ -o B*)
	lax standard formulae	A$     ::=  A* | !A*

Standard form only allows ! to the left of -o, while lax standard form
optionally allows ! at the beginning.  Let Gamma$ range over sequences
of lax standard formulae.

I conjecture that the following is the case:

	If Gamma$ |- A$ and A$ begins with !
	then each formula in Gamma$ begins with !

I'd be grateful if anyone could verify or disprove this conjecture,
or point me to related work.  Thanks,  -- Phil

-----------------------------------------------------------------------
Philip Wadler                                  wadler@dcs.glasgow.ac.uk
Department of Computing Science                    tel: +44 41 330 4966
University of Glasgow                              fax: +44 41 330 4913
Glasgow G12 8QQ, SCOTLAND