% -*- TeX -*- BR -*-

\documentclass[portuguese]{pracjourn}

\usepackage{turnstile}
%\usepackage{english}
\usepackage[latin1]{inputenc}
\usepackage[T1]{fontenc}

\TPJrevision{2007}{08}{18}
\TPJissue{2007}{3}

%%% Changing the name of the info labels:
\renewcommand\abstractname{Resumo}
\renewcommand\emailname{Contacto}
\renewcommand\websitename{S\'itio}
%%%

\title{Uma Ferramenta para Lógicos}
\author{Arthur Buchsbaum e Francisco Reinaldo}
\email{arthur@inf.ufsc.br, reinaldo.opus@gmail.com}  
\website{http://www.inf.ufsc.br/~arthur}

\abstract{\textsf{turnstile} é um estilo baseado em \texttt{article.cls}, usado para composição de artigos. Entre outros usos, a barra de Frege é usada pelos lógicos para denotar a relação de conseqüência, com respeito a uma dada lógica, entre coleções de fórmulas e fórmulas. Pesquisadores em Lógica têm sentido falta de uma rotina em \LaTeX\ para obter a barra de Frege, em alguma das diversas formas em que esta é utilizada.}

\bibliographystyle{plain}

\begin{document}

\maketitle

\section{Introdução}

A Lógica é uma ciência cuja motivação inicial foi a análise do raciocínio correto. Hoje em dia ela está muito além do estudo do raciocínio, ela tem muitas ligações com áreas de pesquisa tais como Matemática, Filosofia, Informática, Lingüística, Física e Inteligência Artificial. Um dos sinais de maior utilização na Lógica é a barra de Frege\footnote{Gottlob Frege (1848--1925) é considerado por muitos o pai da lógica quantificacional e da moderna filosofia da linguagem, e adotou em sua obra o símbolo que é o tema deste artigo. Maiores detalhes estão em \cite{Frege1978}.}, da qual existem versões tais como ``$\,\vdash$'' e~``$\,\models$'', obtidas respectivamente pelos comandos de \LaTeX\ \begin{verb}=\vdash=\end{verb} e \begin{verb}=\models=\end{verb}.

\section{O Projeto turnstile}
\label{sec:turnstile_project}

A barra de Frege\footnote{\url{http://tug.ctan.org/tex-archive/macros/latex/contrib/turnstile}} é um sinal muito utilizado pelos lógicos para denotar a relação de conseqüência, em uma dada lógica, entre coleções de fórmulas e fórmulas. A existência de uma rotina em \LaTeX\ que desenhe adequadamente este símbolo tem feito falta, na composição de artigos que utilizam este sinal, em diversas das formas em que este aparece, incluindo a colocação de dados nas posições corretas acima e abaixo deste sinal. Comandos de \LaTeX\ tais como \begin{verb}=\vdash=\end{verb} e~\begin{verb}=\models=\end{verb}, embora resultem em versões da barra de Frege, não são capazes de colocar nos lugares adequados eventuais dados acima ou abaixo da mesma. Por exemplo, algumas vezes é necessário colocar abaixo da barra de Frege o nome de um determinado sistema lógico, e algumas vezes é preciso colocar acima desta alguma informação adicional.

\vspace{0.2em}

Se queremos dizer que uma fórmula $P$ é conseqüência lógica de uma coleção $\Gamma$ de fórmulas em uma lógica $\mathrm{L}$, poderíamos tentar obter isto por \begin{verbatim}\Gamma \vdash_\mathrm{L} P,\end{verbatim} obtendo $\Gamma \vdash_\mathrm{L} P$.

\medskip

Note que ``$\mathrm{L}$'' não foi bem posicionado com respeito à barra de Frege, ``$\mathrm{L}$'' deveria ser colocado bem abaixo e centralizado. Com \texttt{turnstile.sty} podemos obter isto por \begin{verbatim}\Gamma \sststile{\mathrm{L}}{} P,\end{verbatim} resultando em $\Gamma \sststile{\mathrm{L}}{} P$.

\medskip

Além disto, se quisermos dizer que uma fórmula $P$ é conseqüência lógica de uma coleção $\Gamma$ de fórmulas em uma lógica $\mathrm{L}$, pela variação de $x$ e $y$\footnote{Em \cite{BuchsbaumBeziau2004,BuchsbaumPequeno1997,BuchsbaumPequeno1998} objetos variantes são apresentados.}, poderíamos tentar obter isto por \begin{verbatim}\Gamma \models_\mathrm{L}^{x,y} P,\end{verbatim} resultando em $\Gamma \models_\mathrm{L}^{x,y} P$.

\medskip

Também neste caso, ``$\mathrm{L}$'' e ``$x,y$'' não foram posicionados corretamente com respeito à barra de Frege, estas expressões deveriam ser centralizadas e colocadas, respectivamente, logo abaixo e logo acima deste sinal. Com \texttt{turnstile.sty} podemos obter isto por \begin{verbatim}\Gamma \sdtstile{\mathrm{L}}{x,y} P,\end{verbatim} resultando em $\Gamma \sdtstile{\mathrm{L}}{x,y} P$.

\medskip

Os comandos deste estilo são formados pela samblagem ``tstile'', precedida por uma samblagem com duas ou três letras. Estas letras indicam o tipo das linhas a serem desenhadas sucessivamente; elas podem ser ``n'', ``s'', ``d'' ou ``t''. A letra ``n'' informa que a linha correspondente é vazia, a letra ``s'' que a linha é simples, a letra ``d'' que é dupla, e finalmente a letra ``t'' que é tripla. Os comandos correspondentes às samblagens de duas letras resultam nas barras de Frege mais utilizadas, nas quais não é desenhada uma segunda linha vertical seguindo a linha horizontal. A primeira letra destas samblagens indica o tipo da linha vertical, enquanto que a segunda o tipo da linha horizontal a ser desenhada após a linha vertical. As samblagens de três letras podem conter qualquer uma das letras ``n'', ``s'', ``d'' ou ``t'', com a restrição de que a derradeira letra seja distinta de ``n'', porque o caso no qual a terceira linha é vazia já foi tratado pelos comandos com samblagens de duas letras precedendo ``tstile''. A primeira letra informa o tipo da primeira linha vertical, a segunda o tipo da linha horizontal e, finalmente, a terceira o tipo da segunda linha vertical.

Estes comandos possuem três argumentos, onde o primeiro é opcional.

O primeiro argumento é opcional, este informa o tamanho em que as expressões internas na barra de Frege devem ser exibidas, ``d'' para expressões (normalmente) em linhas exclusivas, ``t'' para expressões (normalmente) inseridas no texto corrente, ``s'' para expressões subscritas ou sobrescritas, e ``ss'' para expressões ainda menores, subscritas ou sobrescritas com respeito às do tipo anterior. O valor predeterminado é ``s''. O resultado de aplicar ``d'' ou ``t'' é o mesmo, a não ser que haja um sinal matemático no segundo ou terceiro argumento exibido de formas distintas, dependendo se este está em expressões (normalmente) de linhas exclusivas, ou em expressões (normalmente) inseridas no texto corrente.

O segundo e o terceiro argumento fornecem as expressões a serem colocadas abaixo e acima da barra de Frege, onde ambas são convertidas para o tamanho especificado no primeiro argumento. Por outro lado, se o segundo ou o terceiro argumento foram vazios, então nada é colocado abaixo ou acima deste sinal.

\section{Exemplos}
\label{sec:examples}

Damos a seguir alguns exemplos, onde, à guisa de ilustração, $\Gamma$ é uma coleção de fórmulas e $P$ é uma fórmula de uma lógica. Naturalmente, os sinais ``$\Gamma$'' e ``$P$'' apenas servem para dar um possível contexto no qual a barra de Frege pode aparecer, entre outros.

\begin{verbatim}
\Gamma \sststile{}{} P
\end{verbatim}
\begin{equation}\Gamma \sststile{}{} P \end{equation}\vspace{0.4em}

\begin{verbatim}
\Gamma \sststile{\mathrm{LPD}}{} P
\end{verbatim}
\begin{equation}\Gamma \sststile{\mathrm{LPD}}{} P\end{equation}\vspace{0.4em}

\begin{verbatim}
\Gamma \sststile{}{x,y} P
\end{verbatim}
\begin{equation}\Gamma \sststile{}{x,y} P\end{equation} \vspace{0.4em}

Se o argumento opcional não é usado, então o resultado é o mesmo no qual ``s'' é o argumento opcional:

\begin{verbatim}
\Gamma \sststile{\mathrm{LPD}}{x,y} P
\end{verbatim}
\begin{equation}\Gamma \sststile{\mathrm{LPD}}{x,y} P\end{equation} \vspace{0.4em}

\begin{verbatim}
\Gamma \sststile[d]{\mathrm{LPD}}{x,y} P
\end{verbatim}
\begin{equation}\Gamma \sststile[t]{\mathrm{LPD}}{x,y} P\end{equation}\vspace{0.4em}
\enlargethispage{-2\baselineskip}

\begin{verbatim}
\Gamma \sststile[t]{\mathrm{LPD}}{x,y} P
\end{verbatim}
\begin{equation}\Gamma \sststile[d]{\mathrm{LPD}}{x,y} P\end{equation} \vspace{0.4em}


\begin{verbatim}
\Gamma \sststile[s]{\mathrm{LPD}}{x,y} P
\end{verbatim}
\begin{equation}\Gamma \sststile[s]{\mathrm{LPD}}{x,y} P\end{equation} \vspace{0.4em}

\begin{verbatim}
\Gamma \sststile[ss]{\mathrm{LPD}}{x,y} P
\end{verbatim}
\begin{equation}\Gamma \sststile[ss]{\mathrm{LPD}}{x,y} P\end{equation} \vspace{0.4em}

\begin{verbatim}
\Gamma \sststile{\mathrm{LPDEFGH}}{x,y} P
\end{verbatim}
\begin{equation}\Gamma \sststile{\mathrm{LPDEFGH}}{x,y} P\end{equation} \vspace{0.4em}

\begin{verbatim}
\Gamma \sststile{\mathrm{LC}}{x,y,z,w} P
\end{verbatim}
\begin{equation}\Gamma \sststile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}

\begin{verbatim}
\Gamma \sdtstile{\mathrm{LC}}{x,y,z,w} P
\end{verbatim}
\begin{equation}\Gamma \sdtstile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}
     
\pagebreak

\begin{verbatim}
\Gamma \dststile{\mathrm{LC}}{x,y,z,w} P
\end{verbatim}
\begin{equation}\Gamma \dststile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}

\begin{verbatim}
\Gamma \ddtstile{\mathrm{LC}}{x,y,z,w} P
\end{verbatim}
\begin{equation}\Gamma \ddtstile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}

\begin{verbatim}
\Gamma \dttstile{\mathrm{LC}}{x,y,z,w} P
\end{verbatim}
\begin{equation}\Gamma \dttstile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}

\begin{verbatim}
\Gamma \nsststile{\mathrm{LC}}{x,y,z,w} P
\end{verbatim}
\begin{equation}\Gamma \nsststile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}

\begin{verbatim}
\Gamma \ndststile{\mathrm{LC}}{x,y,z,w} P
\end{verbatim}
\begin{equation}\Gamma \ndststile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}

\begin{verbatim}
\Gamma \nsdtstile{\mathrm{LC}}{x,y,z,w} P
\end{verbatim}
\begin{equation}  \nsdtstile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}
     
\pagebreak

\begin{verbatim}
\Gamma \nddtstile{\mathrm{LC}}{x,y,z,w} P
\end{verbatim}
\begin{equation}\Gamma \nddtstile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}

\begin{verbatim}
\Gamma \ndttstile{\mathrm{LC}}{x,y,z,w} P
\end{verbatim}
\begin{equation}\Gamma \ndttstile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}

\begin{verbatim}
\Gamma \ssststile{\mathrm{LC}}{x,y,z,w} P
\end{verbatim}
\begin{equation}\Gamma \ssststile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}

\begin{verbatim}
\Gamma \stststile{\mathrm{LC}}{x,y,z,w} P
\end{verbatim}
\begin{equation}\Gamma \stststile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}

\begin{verbatim}
\Gamma \stttstile{\mathrm{LC}}{x,y,z,w} P
\end{verbatim}
\begin{equation}\Gamma \stttstile{\mathrm{LC}}{x,y,z,w} P\end{equation} \vspace{0.4em}

São dados a seguir alguns exemplos de expressões matemáticas abaixo e acima da barra de Frege que mudam bastante, dependendo do argumento opcional. Se nenhum argumento opcional for dado, então este é considerado ``s''.

O leitor pode observar que as linhas verticais não crescem de acordo com a altura das expressões localizadas abaixo e acima da barra de Frege, isto porque consideramos que este sinal deve ter uma altura padrão, pois entendemos que este símbolo aparece principalmente inserido no texto corrente.
          
\pagebreak

\begin{verbatim}
\Gamma \sststile{\sum_0^\infty 1/2^n}{\int_a^b f} P
\end{verbatim}
\begin{equation}\Gamma \sststile{\sum_0^\infty 1/2^n}{\int_a^b f} P\end{equation} \vspace{0.4em}

\begin{verbatim}
\Gamma \sststile[d]{\sum_0^\infty 1/2^n}{\int_a^b f} P
\end{verbatim}
\begin{equation}\Gamma \sststile[d]{\sum_0^\infty 1/2^n}{\int_a^b f} P\end{equation} \vspace{0.4em}

\begin{verbatim}
\Gamma \sststile[t]{\sum_0^\infty 1/2^n}{\int_a^b f} P
\end{verbatim}
\begin{equation}\Gamma \sststile[t]{\sum_0^\infty 1/2^n}{\int_a^b f} P\end{equation} \vspace{0.4em}

\begin{verbatim}
\Gamma \sststile[s]{\sum_0^\infty 1/2^n}{\int_a^b f} P
\end{verbatim}
\begin{equation}\Gamma \sststile[s]{\sum_0^\infty 1/2^n}{\int_a^b f} P\end{equation} \vspace{0.4em}

\begin{verbatim}
\Gamma \sststile[ss]{\sum_0^\infty 1/2^n}{\int_a^b f} P
\end{verbatim}
\begin{equation}\Gamma \sststile[ss]{\sum_0^\infty 1/2^n}{\int_a^b f} P\end{equation} \vspace{0.4em}

\section{Conclusões}
\label{sec:conclusions}

O estilo \texttt{turnstile.sty} parece ser adequado para a obtenção da barra de Frege, em muitas das formas em que esta aparece, e coloca corretamente expressões adicionais abaixo e acima desta, se necessário, bem como a largura deste sinal cresce tanto quanto for preciso, quando uma ou ambas as expressões são largas.

Para uma versão futura deste pacote, pretendemos examinar a conveniência de mudar também a altura da barra de Frege, levando assim em conta as alturas das expressões eventualmente colocadas abaixo ou acima deste sinal, além das suas larguras, como já procedemos.

\begin{thebibliography}{1}

\bibitem{BuchsbaumBeziau2004}
Arthur Buchsbaum e Jean-Yves Béziau.
\newblock Introduction of implication and generalization in axiomatic calculi.
\newblock Em Jean-Yves Béziau, Alexandre~Costa Leite, e Alberto Facchini,
  editores, {\em Aspects of Universal Logic}, número 17 em Travaux de Logique,
  página 231. Centre de Recherches Sémiologiques, Université de Neuchâtel, Dezembro de 2004.

\bibitem{BuchsbaumPequeno1997}
Arthur Buchsbaum e Tarcisio Pequeno.
\newblock A general treatment for the deduction theorem in open calculi.
\newblock {\em Logique et Analyse}, 157:9--29, janeiro--março de 1997.

\bibitem{BuchsbaumPequeno1998}
Arthur Buchsbaum e Tarcisio Pequeno.
\newblock A introdução da implicação em cálculos axiomáticos abertos.
\newblock Em {\em Anais do IV Encontro de Filosofia Analítica}, páginas~61--75, 1998.

\bibitem{Frege1978}
Gottlob Frege.
\newblock {\em Lógica e Filosofia da Linguagem}.
\newblock Editora Cultrix e Editora da Universidade de São Paulo, 1978.

\bibitem{KopkaDaly1999}
Helmut Kopka and Patrick~W. Daly.
\newblock {\em A Guide to \LaTeX}.
\newblock Addison-Wesley, 1999.

\bibitem{Lamport1994}
Leslie Lamport.
\newblock {\em \LaTeX\ -- A Document Preparation System -- User's Guide and Reference Manual}.
\newblock Addison-Wesley, 1994.

\bibitem{NerodeShore1997}
Anil Nerode and Richard~A. Shore.
\newblock {\em Logic for Applications}.
\newblock Springer, 1997.

\bibitem{Nolt1996}
John Nolt.
\newblock {\em Logics}.
\newblock Wadsworth, 1996.

\end{thebibliography}

\end{document}