Formulas of Minimal Linear Logic

%%% Minimal linear logic
%%% Author: Frank Pfenning
%%%
%%% Some connectives which are only meaningful in intuitionistic
%%% or classical linear logic are commented out.

i : type.  % terms
o : type.  % formulas
%name i T S
%name o A B C

% Multiplicative connectives
imp    : o -> o -> o.  %infix right 10 imp
times  : o -> o -> o.  %infix right 11 times
one    : o.
% par    : o -> o -> o.  %infix right 11 par
% bot    : o.

% Additive connectives
% wave   : o -> o -> o.  %infix right 10 wave
with   : o -> o -> o.  %infix right 11 with
top    : o.
plus   : o -> o -> o.  %infix right 11 plus
zero   : o.

% Involution
% perp   : o -> o.

% Quantifiers
forall : (i -> o) -> o.
exists : (i -> o) -> o.

% Modals
!      : o -> o.
% ?      : o -> o.

Frank Pfenning