...onde os superscritos e subscritos nas setas indicam qual é o contexto: “α ⇒^{1} β”

é “Γ_{1}, α ⇒ Δ_{1}, β”; “α ⇒^{1,2} β” é “Γ_{1}, Γ_{2}, α ⇒ Δ_{1}, Δ_{2}, β”; e “α ⇒^{!/?} β” é “!Γ_{1}, α ⇒

?Δ_{1}, β”, onde esses ‘!’s e ‘?’s indicam que cada membro de !Γ_{1} é precedido por um ‘!’ e cada de ?Δ_{1} por um ‘?’.

{⇒^{1} A \atop ∼A ⇒_{1}} ^{L∼}  {A ⇒^{1} \atop ⇒_{1} ∼A} ^{R∼}

{A ⇒^{1} \atop A ⊓ B ⇒_{1}} L⊓_{1}  {B ⇒^{1} \atop A ⊓ B ⇒_{1}} L⊓_{2}  \begin{matrix}⇒^{1} A & ⇒^{1} B \\ ⇒_{1} A ⊓ B \end{matrix} R⊓

{⇒^{1} A \atop ⇒_{1} A ⊔ B} R⊔_{1}  {⇒^{1} B \atop ⇒_{1} A ⊔ B} R⊔_{2}  \begin{matrix}A ⇒^{1} & B ⇒^{1} \\ A ⊔ B ⇒_{1} \end{matrix} L⊔

{A, B ⇒^{1} \atop A ⋆ B ⇒_{1}} L⋆  \begin{matrix}⇒^{1} A & ⇒^{2} B \\ ⇒_{1,2} A ⋆ B \end{matrix} R⋆

{⇒^{1} A, B \atop ⇒_{1} A + B} R+  \begin{matrix}A ⇒^{1} & B ⇒^{2} \\ A + B ⇒_{1,2} \end{matrix} L+

{A ⇒^{1} B \atop ⇒_{1} A ⊸ B} ^{R⊸}  \begin{matrix}⇒^{1} A & B ⇒^{2} \\ A ⊸ B ⇒_{1,2} \end{matrix} ^{L⊸}

⇒^{1} ; 1 ⇒_{1} L1  ⇒ 1 R1  ⊤ ⇒_{1} R⊤

⇒^{1} ; ⇒_{1} 0 R0  0 ⇒ L0  ⊥ ⇒_{1} L⊥

⇒^{1} ; !A ⇒_{1} W!  {!A,!A ⇒^{1} \atop !A ⇒_{1}} C!  {A ⇒^{1} \atop !A ⇒_{1}} L!  {⇒^{!/?} A \atop ⇒_{!/?}!A} R!

⇒^{1} ; ⇒^{1}?A W?  {⇒^{1}?A,?A \atop ⇒_{1}?A} C?  {⇒^{1} A \atop ⇒_{1}?A} R?  {A ⇒^{!/?} \atop ?A ⇒_{!/?}} L?

⇒^{1} A A ⇒^{2} ; ⇒_{1,2} Cut

Numa semântica de espaços vetoriais o ⋆ e o + viram ⊗, o ⊓ e o ⊔ viram ⊕, 1 e 0 viram ℝ^{1} e ⊤ e ⊥ viram ℝ^{0}.

99sep25 (typeset 2000jan05 08:44) edrx@mat.puc-rio.br