1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
|
% -*- 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}
|