Usando o pacote fitch(2)

Tratarei agora do pacote fitch escrito por Peter Selinger. Aqui tem a documentação do pacote.

Aqui tem o empacotamento que fiz do fitch (2) (debian wheezy e ubuntu)

Para usar o pacote, deve-se adicionar o comando

\usepackage{fitch2)

no preâmbulo. Exemplo de preâmbulo:

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Classe de documento
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\documentclass[10pt,a4paper]{article}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Fontes e lingua
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage[utf8]{inputenc}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacotes matemáticos
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote Fitch2
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{fitch2}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Titulo e autor
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\author{Alessandro Duarte}
\title{Pacote Fitch(2)}

Iremos produzir a mesma derivação que há na postagem do fitch(1). Para isso, precisamos entender os comandos atrelados ao pacote. Ele são:

\hypo - usado para introduzir uma premissa ou nova hipótese

\open - usado antes do comando \hypo para introduzir a hipótese em nova linha à direita.

\have - usado para introduzir fórmulas que são obtidas pelas regras de dedução

\close - usado quando a linha da hipótese é descartada (prova do condicional, redução ao absurdo)

Além desses comandos, há comandos que introduzem indicações das regras utilizadas:

\r - reiteração

\ii - introdução da implicação (regra do condicional)

\ie - eliminação da implicação (modus ponens)

\ai - introdução da conjunção

\ae - eliminação da conjunção

\oi - introdução da disjunção

\oe - eliminação da disjunção

\ni - introdução da negação

\ne - eliminação da negação

\be - eliminação do bottom

\nne - eliminação da dupla negação

\Ai - introdução do quantificador universal

\Ae - eliminação do quantificador universal

\Ei - introdução do quantificador existencial

\Ee - eliminação do quantificador existencial

Em fitch(2), a derivação de é como se segue. Em primeiro lugar, iniciamos o modo matemático. Depois, iniciamos o ambiente fitch com os comandos \begin{nd} e \end{nd}. O ambiente fitch deve ficar dentro do ambiente matemático.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote Fitch2
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{fitch2}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Titulo e autor
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\author{Alessandro Duarte}
\title{Pacote Fitch(2)}
\begin{document}
\maketitle
$p\vdash q\supset p$

$
\begin{nd}

\end{nd}
$

\end{document}

Dentro do ambiente fitch, introduzimos os comandos listados acima. Para introduzir a premissa , devemos inserir o comando

\hypo {1} {p}

É necessário introduzir a numeração das linhas em sequência.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Classe de documento
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\documentclass[10pt,a4paper]{article}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Fontes e lingua
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage[utf8]{inputenc}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacotes matemáticos
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote Fitch2
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{fitch2}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Titulo e autor
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\author{Alessandro Duarte}
\title{Pacote Fitch(2)}
\begin{document}
\maketitle
$p\vdash q\supset p$

$
\begin{nd}
\hypo{1} {p}

\end{nd}
$

\end{document}

Compilando

Depois, será introduzida a hipótese . Para isso, precisamos introduzir nova linha de hipótese. Isso é feito com o comando \open. A seguir, inserimos o comando

\hypo{2} {q}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Classe de documento
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\documentclass[10pt,a4paper]{article}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Fontes e lingua
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage[utf8]{inputenc}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacotes matemáticos
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote Fitch2
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{fitch2}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Titulo e autor
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\author{Alessandro Duarte}
\title{Pacote Fitch(2)}
\begin{document}
\maketitle
$p\vdash q\supset p$

$
\begin{nd}
\hypo{1} {p}
\open
\hypo{2} {q}
\end{nd}
$

\end{document}

Compilando

Agora repetimos a premissa na linha de hipótese de . Isso é feito com a regra de repetição (reiteração). Nesse caso, usamos o comando

\have{3} {p}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Classe de documento
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\documentclass[10pt,a4paper]{article}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Fontes e lingua
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage[utf8]{inputenc}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacotes matemáticos
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote Fitch2
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{fitch2}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Titulo e autor
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\author{Alessandro Duarte}
\title{Pacote Fitch(2)}
\begin{document}
\maketitle
$p\vdash q\supset p$

$
\begin{nd}
\hypo{1} {p}
\open
\hypo{2} {q}
\have{3} {p}
\end{nd}
$

\end{document}

Compilando

Como a fórmula foi derivada na linha de hipótese de , podemos aplicar a regra do condicional e eliminar essa linha. Para isso, usamos o comando \close e em seguida o comando

\have{4} {q\supset p}

Código final

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Classe de documento
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\documentclass[10pt,a4paper]{article}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Fontes e lingua
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage[utf8]{inputenc}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacotes matemáticos
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote Fitch2
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{fitch2}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Titulo e autor
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\author{Alessandro Duarte}
\title{Pacote Fitch(2)}
\begin{document}
\maketitle
$p\vdash q\supset p$

$
\begin{nd}
\hypo{1} {p}
\open
\hypo{2} {q}
\have{3} {p}
\close
\have{4} {q\supset p}
\end{nd}
$

\end{document}

Podemos incrementar o código indicando as regras usadas. Na linha 3, a regra de reiteração (repetição) e na linha 4, a regra de introdução da implicação (condicional). Assim, temos o seguinte código:

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Classe de documento
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\documentclass[10pt,a4paper]{article}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Fontes e lingua
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage[utf8]{inputenc}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacotes matemáticos
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Pacote Fitch2
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{fitch2}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Titulo e autor
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\author{Alessandro Duarte}
\title{Pacote Fitch(2)}
\begin{document}
\maketitle
$p\vdash q\supset p$

$
\begin{nd}
\hypo{1} {p}
\open
\hypo{2} {q}
\have{3} {p} \r{1}
\close
\have{4} {q\supset p} \ii{2,3}
\end{nd}
$

\end{document}