Observe que (-)⊥ é uma involução, isto é, A⊥⊥ = A para todas as proposições. A⊥ também é chamada de negação linear de A.
As colunas da tabela sugerem outra maneira de classificar os conectivos da lógica linear, denominada polaridade: os conectivos negados na coluna da esquerda (⊗, ⊕, 1, 0,!) são chamados de positivos, enquanto seus duais na coluna da direita (⅋, &, ⊥, ⊤,?) são chamados de negativos; cf. Tabela à direita.
A implicação linear não está incluída na gramática de conectivos, mas é definível em LLC usando a negação linear e a disjunção multiplicativa, por A ⊸ B := A┴ ⅋ B. O conectivo ⊸ às vezes é pronunciado "pirulito", devido à sua forma.
Uma maneira de definir a lógica linear é como um cálculo sequente. Usamos as letras Γ e Δ para variar sobre a lista de proposições A1,..., An, também chamadas de contextos. Um sequente coloca um contexto à esquerda e à direita da catraca, escrito Γ Predefinição:Tee Δ. Intuitivamente, o sequente afirma que a conjunção de Γ implica a disjunção de Δ (embora queiramos dizer a conjunção e a disjunção "multiplicativas", como explicado abaixo). Girard descreve a lógica linear clássica usando apenas sequências unilaterais (onde o contexto esquerdo está vazio), e seguimos aqui essa apresentação mais econômica. Isso é possível porque qualquer local à esquerda de uma catraca pode sempre ser movido para o outro lado e duplamente.
Primeiro, para formalizar o fato de que não nos importamos com a ordem das proposições dentro de um contexto, adicionamos a regra estrutural de troca:
Note que nós não adicionamos regras estruturais de enfraquecimento e de contração, porque nos preocupamos com a ausência de proposições em uma sequência, e o número de cópias presentes.
A regra de corte pode ser vista como uma maneira de compor provas, e seqüências iniciais servem como as unidades de composição. Em certo sentido, essas regras são redundantes: à medida que introduzimos regras adicionais para a construção de provas abaixo, manteremos a propriedade de que seqüências iniciais arbitrárias podem ser derivadas de seqüências atômicas iniciais, e que sempre que um sequente é provável, pode ser dado um prova livre de cortes. Em última instância, esta propriedade de forma canônica (que pode ser dividida na completude das sequências iniciais atômicas e do teorema de eliminação de corte, induzindo uma noção de prova analítica) está por trás das aplicações da lógica linear na ciência da computação, pois permite que a lógica seja usada na pesquisa de prova e como um lambda-cálculo calculado com recurso.
Agora, explicamos os conectivos dando regras lógicas. Tipicamente, no cálculo sequente, é dada uma "regra-direita" e uma "regra-esquerda" para cada conectivo, descrevendo essencialmente dois modos de raciocínio sobre proposições envolvendo esse conectivo (por exemplo, verificação e falsificação). Em uma apresentação unilateral, uma vez que faz uso da negação: as regras certas para um conectivo (digamos ⅋) efetivamente desempenham o papel de regras-esquerda para o seu dual (⊗). Portanto, devemos esperar uma certa "harmonia" entre a(s) regra(s) para um conectivo e a(s) regra(s) para o seu dual.
Observe que as regras para conjunção e disjunção multiplicativa são admissíveis paraconjunção e disjunção simples sob uma interpretação clássica (isto é, são regras admissíveis no LK).
Observar que as regras para a conjunção e a disjunção aditivas são novamente admissíveis sob uma interpretação clássica. Mas agora podemos explicar a base para a distinção multiplicativa / aditiva nas regras para as duas versões diferentes da conjunção: para o conectivo multiplicativo (⊗), o contexto da conclusão (Γ, Δ) é dividido entre as premissas, enquanto que para o caso do conectivo aditivo (&), o contexto da conclusão (Γ) é transportado inteiro para ambas as premissas.