Usando o pacote fitch (1)


Warning: preg_replace(): The /e modifier is no longer supported, use preg_replace_callback instead in /home/storage/9/61/5d/alessandroduarte/public_html/wp-content/plugins/latex/latex.php on line 47

Warning: preg_replace(): The /e modifier is no longer supported, use preg_replace_callback instead in /home/storage/9/61/5d/alessandroduarte/public_html/wp-content/plugins/latex/latex.php on line 49

Há pelo menos dois pacotes para produzir provas em dedução natural usando o estilo Fitch (modelo Fitch): o primeiro é o de Johan Klüwer (infelizmente, o seu site está fora do ar); o segundo, de Peter Selinger.

Para instalar os pacotes, copie os .sty para a pasta de instalação do texlive e faça o update do banco de dados dos pacotes instalados (como fazer isso poder ser visto aqui). Como os dois pacotes têm o mesmo nome, é possível renomear um deles (talvez para fitch2.sy), no caso de instalar ambos pacotes. Para quem usa debian (ubuntu), empacotei ambos:

fitch (Johan Klüwer)

fitch2 (Peter Selinger) - para instalá-los, entre na pasta onde foram "baixados" e digite (como root):

dpkg -i fitch.deb fitch2.deb

Vamos começar com o fitch (Johan Klüwer). Infelizmente, esse pacote não foi muito bem documentado. Em primeiro lugar, é necessário introduzir o seguinte comando no preâmbulo

\usepackage{fitch}

Exemplo de preâmbulo:

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Classe de documento
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\documentclass[10pt,a4paper]{article}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacotes de língua e fontes
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage[utf8]{inputenc}
\usepackage[brazil]{babel}
\usepackage[T1]{fontenc}
%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote matemático
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote Fitch
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{fitch}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Dados 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\author{Alessandro Duarte}
\title{Pacote Fitch}

Os comandos do pacote devem ser inseridos dentro do ambiente fitch, iniciado com comando \begin{fitch} e terminado com o comando \end{fitch}. Nesse ambiente, as linhas de dedução são numeradas. Há outra opção de ambiente em que as linhas não são numeradas: fitch*, iniciado com \begin{fitch*} e terminado com \end{fitch*}.

Há dois comandos básicos:

\fh - para introduzir nova hipótese

\fa - para introduzir linha vertical

Suponha que desejamos derivar o seguinte: p\vdash q \supset p

A prova consistirá em assumirmos como premissa: p. Depois, assumir como hipótese q e, finalmente, derivar p na linha da hipótese q para aplicar a regra do condicional e sair da linha de hipótese.

Assim, em primeiro lugar adicionaremos o comando:

\fh p

dentro do ambiente fitch.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Classe de documento
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\documentclass[10pt,a4paper]{article}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacotes de língua e fontes
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage[utf8]{inputenc}
\usepackage[brazil]{babel}
\usepackage[T1]{fontenc}
%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote matemático
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote Fitch
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{fitch}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Dados 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\author{Alessandro Duarte}
\title{Pacote Fitch}

\begin{document}
\maketitle

Derivação de: $p \vdash q\supset p$

\begin{fitch}
\fh p

\end{fitch}

\end{document}

Isso produz:

Captura de tela de 2013-09-09 22:46:19

Agora, temos de introduzir a nova hipótese q. A regra é clara: a toda hipótese sempre se adiciona uma nova linha vertical (da hipótese) à direita. Assim, devemos introduzir o comando:

\fa\fh q

Observação importante: o pacote fitch tem o ambiente fitch que é produzido, usando o ambiente tabular. Portanto, para iniciar nova linha de dedução, deve-se dar o comando \\. Caso contrário, acontecerá o seguinte:

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Classe de documento
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\documentclass[10pt,a4paper]{article}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacotes de língua e fontes
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage[utf8]{inputenc}
\usepackage[brazil]{babel}
\usepackage[T1]{fontenc}
%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote matemático
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote Fitch
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{fitch}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Dados 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\author{Alessandro Duarte}
\title{Pacote Fitch}

\begin{document}
\maketitle

Derivação de: $p \vdash q\supset p$

\begin{fitch}
\fh p
\fa\fh q

\end{fitch}

\end{document}

Captura de tela de 2013-09-09 22:53:32

Introduzindo \\ no código:

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Classe de documento
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\documentclass[10pt,a4paper]{article}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacotes de língua e fontes
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage[utf8]{inputenc}
\usepackage[brazil]{babel}
\usepackage[T1]{fontenc}
%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote matemático
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote Fitch
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{fitch}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Dados 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\author{Alessandro Duarte}
\title{Pacote Fitch}

\begin{document}
\maketitle

Derivação de: $p \vdash q\supset p$

\begin{fitch}
\fh p\\
\fa\fh q

\end{fitch}

\end{document}

Captura de tela de 2013-09-09 22:55:25

No comando

\fa\fh q

\fa prolonga a linha vertical da premissa p, enquanto \fh q introduz em nova linha (de hipótese) q.

Depois, podemos introduzir p na linha de hipótese de q por meio da regra de repetição. Para isso, usamos o comando

\fa\fa p

O primeiro \fa prolongará a linha vertical da premissa p; o segundo, a da hipótese q

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Classe de documento
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\documentclass[10pt,a4paper]{article}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacotes de língua e fontes
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage[utf8]{inputenc}
\usepackage[brazil]{babel}
\usepackage[T1]{fontenc}
%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote matemático
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote Fitch
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{fitch}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Dados 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\author{Alessandro Duarte}
\title{Pacote Fitch}

\begin{document}
\maketitle

Derivação de: $p \vdash q\supset p$

\begin{fitch}
\fh p\\
\fa\fh q\\
\fa\fa p

\end{fitch}

\end{document}

Captura de tela de 2013-09-09 23:03:19

Ora, uma vez que da hipótese q deduzimos  p, podemos aplicar a regra do condicional e sair da linha de hipótese de q. Para isso, introduzimos o comando:

\fa q\supset p

Nesse caso, \fa só prolongará a linha vertical da premissa p

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Classe de documento
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\documentclass[10pt,a4paper]{article}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacotes de língua e fontes
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage[utf8]{inputenc}
\usepackage[brazil]{babel}
\usepackage[T1]{fontenc}
%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote matemático
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote Fitch
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{fitch}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Dados 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\author{Alessandro Duarte}
\title{Pacote Fitch}

\begin{document}
\maketitle

Derivação de: $p \vdash q\supset p$

\begin{fitch}
\fh p\\
\fa\fh q\\
\fa\fa p\\
\fa q\supset p
\end{fitch}

\end{document}

Captura de tela de 2013-09-09 23:09:24

que é o que queríamos demonstrar.

Podemos melhorar a demonstração introduzindo os passos usados. Lembrando que o ambiente fitch é baseado no ambiente tabular, podemos usar o símbolo & para separar a prova em colunas: na primeira coluna, a prova em si; na segunda, os passos da prova.

Vimos que na linha 1 foi introduzida uma premissa. Assim:

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Classe de documento
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\documentclass[10pt,a4paper]{article}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacotes de língua e fontes
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage[utf8]{inputenc}
\usepackage[brazil]{babel}
\usepackage[T1]{fontenc}
%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote matemático
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote Fitch
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{fitch}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Dados 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\author{Alessandro Duarte}
\title{Pacote Fitch}

\begin{document}
\maketitle

Derivação de: $p \vdash q\supset p$

\begin{fitch}
\fh p & Premissa\\
\fa\fh q\\
\fa\fa p\\
\fa q\supset p
\end{fitch}

\end{document}

Captura de tela de 2013-09-09 23:15:03

Na linha 2, introduzimos uma nova hipótese. Logo:

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Classe de documento
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\documentclass[10pt,a4paper]{article}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacotes de língua e fontes
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage[utf8]{inputenc}
\usepackage[brazil]{babel}
\usepackage[T1]{fontenc}
%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote matemático
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote Fitch
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{fitch}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Dados 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\author{Alessandro Duarte}
\title{Pacote Fitch}

\begin{document}
\maketitle

Derivação de: $p \vdash q\supset p$

\begin{fitch}
\fh p & Premissa\\
\fa\fh q & Hipótese\\
\fa\fa p\\
\fa q\supset p
\end{fitch}

\end{document}

Captura de tela de 2013-09-09 23:17:47

Na linha 3, p foi introduzida por repetição da premissa na linha 1. Portanto:

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Classe de documento
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\documentclass[10pt,a4paper]{article}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacotes de língua e fontes
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage[utf8]{inputenc}
\usepackage[brazil]{babel}
\usepackage[T1]{fontenc}
%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote matemático
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote Fitch
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{fitch}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Dados 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\author{Alessandro Duarte}
\title{Pacote Fitch}

\begin{document}
\maketitle

Derivação de: $p \vdash q\supset p$

\begin{fitch}
\fh p & Premissa\\
\fa\fh q & Hipótese\\
\fa\fa p & 1, Repetição\\
\fa q\supset p
\end{fitch}

\end{document}

Captura de tela de 2013-09-09 23:20:14

Finalmente, a linha 4 foi obtida das linhas 2 e 3 por meio da regra do condicional. Destarte

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Classe de documento
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\documentclass[10pt,a4paper]{article}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacotes de língua e fontes
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage[utf8]{inputenc}
\usepackage[brazil]{babel}
\usepackage[T1]{fontenc}
%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote matemático
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote Fitch
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{fitch}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Dados
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\author{Alessandro Duarte}
\title{Pacote Fitch}

\begin{document}
\maketitle

Derivação de: $p \vdash q\supset p$

\begin{fitch}
\fh p & Premissa\\
\fa\fh q & Hipótese\\
\fa\fa p & 1, Repetição\\
\fa q\supset p & 2,3 Regra do condicional
\end{fitch}

\end{document}

Captura de tela de 2013-09-09 23:22:11

Para uma demonstração não-numerada, use os comandos: \begin{fitch*} e \end{fitch*}

Observação1: O pacote fitch é definido a partir de um tabular de duas colunas. Se introduzir mais de um & ocorrerá um erro.

Código errado:

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Classe de documento
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\documentclass[10pt,a4paper]{article}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacotes de língua e fontes
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage[utf8]{inputenc}
\usepackage[brazil]{babel}
\usepackage[T1]{fontenc}
%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote matemático
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote Fitch
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{fitch}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Dados 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\author{Alessandro Duarte}
\title{Pacote Fitch}

\begin{document}
\maketitle

Derivação de: $p \vdash q\supset p$

\begin{fitch}
\fh p & Premissa &\\
\fa\fh q & Hipótese\\
\fa\fa p & 1, Repetição\\
\fa q\supset p & 2,3 Regra do condicional
\end{fitch}

\end{document}

Captura de tela de 2013-09-09 23:42:48

 

Observação2: A primeira coluna (a coluna da prova em si) foi definida em modo matemático, portanto não é necessário o uso de $ $ ou . Se introduzir o modo matemático na primeira coluna ocorrerá um erro.

Código com erro

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Classe de documento
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\documentclass[10pt,a4paper]{article}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacotes de língua e fontes
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage[utf8]{inputenc}
\usepackage[brazil]{babel}
\usepackage[T1]{fontenc}
%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote matemático
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote Fitch
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{fitch}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Dados 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\author{Alessandro Duarte}
\title{Pacote Fitch}

\begin{document}
\maketitle

Derivação de: $p \vdash q\supset p$

\begin{fitch}
\fh p & Premissa \\
\fa\fh q & Hipótese\\
\fa\fa p & 1, Repetição\\
\fa $q\supset p$ & 2,3 Regra do condicional
\end{fitch}

\end{document}

Captura de tela de 2013-09-09 23:47:22

Observação3:  A segunda coluna não é definida em modo matemático. Assim, é necessário introduzir $ $.

Código com erro:

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Classe de documento
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\documentclass[10pt,a4paper]{article}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacotes de língua e fontes
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage[utf8]{inputenc}
\usepackage[brazil]{babel}
\usepackage[T1]{fontenc}
%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote matemático
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote Fitch
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{fitch}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Dados 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\author{Alessandro Duarte}
\title{Pacote Fitch}

\begin{document}
\maketitle

Derivação de: $p \vdash q\supset p$

\begin{fitch}
\fh p & Premissa \\
\fa\fh q & Hipótese\\
\fa\fa p & 1, Repetição\\
\fa q\supset p & 2,3 \supset-introdução
\end{fitch}

\end{document}

Captura de tela de 2013-09-09 23:50:49

 

Código correto

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Classe de documento
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\documentclass[10pt,a4paper]{article}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacotes de língua e fontes
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage[utf8]{inputenc}
\usepackage[brazil]{babel}
\usepackage[T1]{fontenc}
%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote matemático
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote Fitch
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{fitch}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Dados 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\author{Alessandro Duarte}
\title{Pacote Fitch}

\begin{document}
\maketitle

Derivação de: $p \vdash q\supset p$

\begin{fitch}
\fh p & Premissa \\
\fa\fh q & Hipótese\\
\fa\fa p & 1, Repetição\\
\fa q\supset p & 2,3 $\supset$-introdução
\end{fitch}

\end{document}

Captura de tela de 2013-09-09 23:52:18

 

Depois, falaremos do pacote fitch2. Abaixo, exemplos mais complexos:

%% LyX 2.0.3 created this file.  For more info, see http://www.lyx.org/.
%% Do not edit unless you really know what you are doing.
\documentclass[brazil]{article}
\usepackage[T1]{fontenc}
\usepackage[utf8x]{inputenc}

\makeatletter
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% User specified LaTeX commands.
\usepackage{fitch}

\makeatother

\usepackage{babel}
\begin{document}

\title{Exercícios de Dedução Natural (Não vale Ponto)}

\maketitle

\section{Prove}
\begin{enumerate}
\item $p\vdash(q\rightarrow p)$\\\begin{equation*}
\begin{fitch}
\fh p & Premissa\\
\fa\fh q & Hipótese\\
\fa\fa p & 1, Repetição\\
\fa (q\rightarrow p) & 2,3, Prova do condicional\\
\end{fitch}
\end{equation*}
\item $p,(\sim p)\vdash q$\\\begin{equation*}
\begin{fitch}
\fa p & Premissa\\
\fa (\sim p) & Premissa\\
\fa\fh (\sim q) & Hipótese\\
\fa\fa p & 1, Repetição\\
\fa\fa (\sim p) & 2, Repetição\\
\fa\fa (p\ \&\ (\sim p)) & 4,5, Introdução da conjunção\\
\fa (\sim(\sim q)) & 3,6, Redução ao absurdo\\
\fa q & 7, Eliminação da dupla negação\\
\end{fitch}
\end{equation*}
\item $((p\rightarrow q)\rightarrow p)\vdash p$\\\begin{equation*}
\begin{fitch}
\fh (p\rightarrow q)\rightarrow p) & Premissa\\
\fa\fh (\sim p) & Hipótese\\
\fa\fa\fh p & Hipótese\\
\fa\fa\fa (\sim p) & 2, repetição\\
\fa\fa\fa q & Derivação anterior\\
\fa\fa (p\rightarrow q) & Prova do condicional\\
\fa\fa (p\rightarrow q)\rightarrow p) & 1, repetição\\
\fa\fa p & 6,7, Modus Ponens\\
\fa\fa (p\ \&\ (\sim p)) & 2,8, Introdução da conjunção\\
\fa (\sim(\sim p)) & 2,9, Redução ao absurdo\\
\fa p & 10, eliminação da dupla negação\\
\end{fitch}
\end{equation*}
\item $p\vdash p$\\\begin{equation*}
\begin{fitch}
\fh p & Premissa\\
\fa p & 1, repetição\\
\end{fitch}
\end{equation*}
\item $\vdash(p\rightarrow p)$\\\begin{equation*}
\begin{fitch}
\fh p & Premissa\\
\fa p & 1, repetição\\
(p\rightarrow p) & 1,2, Prova do condicional\\
\end{fitch}
\end{equation*}
\item $\vdash((p\&q)\equiv(q\&p))$\\\begin{equation*}
\begin{fitch}
\fh (p\ \&\ q) & Hipótese\\
\fa q & 1, eliminação da conjunção\\
\fa p & 1, eliminação da conjunção\\
\fa (q\ \&\ p) & introdução da conjunção\\
((p\ \&\ q)\rightarrow(q\ \&\ p)) & 1,4, Prova do condicional\\
\fh (q\ \&\ p) & Hipótese\\
\fa p & 6, eliminação da conjunção\\
\fa q & 6, eliminação da conjunção\\
\fa (p\ \&\ q) & 7,8, introdução da conjunção\\
((q\ \&\ p)\rightarrow(p\ \&\ q)) & 6,9, Prova do condicional\\
((p\ \&\ q)\equiv(q\ \&\ p)) & 5,10, Introdução da equivalência\\
\end{fitch}
\end{equation*}
\item $(p\equiv q),(\sim q)\vdash(\sim p)$\\\begin{equation*}
\begin{fitch}
\fa (p\equiv q) & Premissa\\
\fa (\sim q) & Premissa\\
\fa (p\rightarrow q)& 1, eliminação da equivalência\\
\fa (\sim p) & 2,3, Modus Tolens \\
\end{fitch}
\end{equation*}
\item $(p\equiv q),(\sim p)\vdash(\sim q)$\\\begin{equation*}
\begin{fitch}
\fa (p\equiv q) & Premissa\\
\fa (\sim p) & Premissa\\
\fa (q\rightarrow p)& 1, eliminação da equivalência\\
\fa (\sim q) & 2,3, Modus Tolens \\
\end{fitch}
\end{equation*}
\item $(p_{1}\rightarrow p_{2})\vdash((p_{1}\vee p_{3})\rightarrow(p_{2}\vee p_{3}))$\\\begin{equation*}
\begin{fitch}
\fh (p_1\rightarrow p_2) & Premissa\\
\fa\fh (p_1\vee p_3) & Hipótese\\
\fa\fa\fh (\sim(p_2\vee p_3)) & Hipótese\\
\fa\fa\fa ((\sim p_2)\ \&\ (\sim p_3)) & 3, De Morgan \\
\fa\fa\fa (\sim p_2) & 4, eliminação da conjunção\\
\fa\fa\fa (p_1\rightarrow p_2) & 1, repetição\\
\fa\fa\fa (\sim p_1) & 5,6, Modus Tolens\\
\fa\fa\fa (p_1\vee p_3) & 2, repetição\\
\fa\fa\fa p_3 & 7,8, Silogismo disjuntivo\\
\fa\fa\fa (p_2\vee p_3) & 9, introdução da disjunção\\
\fa\fa\fa ((p_2\vee p_3)\ \& \ (\sim(p_2\vee p_3))) & 3,10, introdução da conjunção\\
\fa\fa (\sim(\sim(p_2\vee p_3))) & 3,11, Redução ao absurdo\\
\fa\fa (p_2\vee p_3) & 12, eliminação da dupla negação\\
\fa ((p_{1}\vee p_{3})\rightarrow(p_{2}\vee p_{3}))& 2,13, Prova do condicional\\ 
\end{fitch}
\end{equation*}
\item $(p_{1}\rightarrow(p_{2}\rightarrow p_{3}))\vdash((p_{1}\&p_{2})\rightarrow p_{3})$\\\begin{equation*}
\begin{fitch}
\fh (p_{1}\rightarrow(p_{2}\rightarrow p_{3})) & Premissa\\
\fa\fh (p_{1}\&p_{2}) & Hipótese\\
\fa\fa p_1 & 2, eliminação da conjunção\\
\fa\fa (p_{1}\rightarrow(p_{2}\rightarrow p_{3})) & 1, repetição\\
\fa\fa (p_{2}\rightarrow p_{3}) & 3,4, Modus Ponens\\
\fa\fa p_2 & 2, eliminação da conjunção\\
\fa\fa p_3 & 5,6, Modus ponens\\
\fa ((p_{1}\&p_{2})\rightarrow p_{3})&2,7, Prova do condicional\\
\end{fitch}
\end{equation*}\end{enumerate}

\end{document}

 Código

Captura de tela de 2013-09-09 23:37:30

Observação Final: para usar o fitch no LyX, é só adicionar o comando \usepackage{fitch} no preambulo do LyX (veja aqui), depois apertar Ctrl + L (ou clicar no ícone TeX) e inserir os códigos na caixa do TeX.