Formulas of Classical Linear Logic

%%% Classical Linear Logic
%%% Language of formulas
%%% Author: Frank Pfenning
%%%
%%% Some of the classically redundant connectives have been
%%% commented out, but negation remains.

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

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

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

% Involution
perp   : o -> o.

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

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

Frank Pfenning