Abstract: Mostramos no presente artigo que a fórmula ¬¬ A ≡ A e análogos do Axioma IV e Teorema IVa de Grundgesetze der Arithmetik não são demonstráveis em Begriffsschrift.
Sumário
1 O Cálculo BS-Prop
A linguagem de Begriffsschrift (BS) é inteiramente diferente da linguagem dos sistemas lógicos formais contemporâneos. De fato, poderia ser sem sentido e anacrônico tentar apresentar o conteúdo de BS como um sistema formal. Porém, é possível interpretar a linguagem de BS em uma linguagem formalizada contemporânea. Foi assim que Lukasiewicz mostrou que os axiomas (1), (2), (28), (31) e (41) são independentes uns dos outros e que o axioma (8) de BS não é independente, sendo provável a partir dos axiomas (1) e (2). Neste sentido, iremos propor um cálculo, que será chamado BS-Prop, no qual tentaremos interpretar os axiomas (1), (2), (28), (31), (41), (52) e (54) de BS. A linguagem de BS-Prop é diferente da linguagem usual dos sistemas lógicos formais proposicionais contemporâneos, uma vez que, além de variáveis proposicionais, do conectivo unário ‘¬’ (a negação) e do conectivo binário ‘⊃’ (a implicação), há um conectivo binário ‘≡’ que será chamado identidade de conteúdo.
A base axiomática para BS-prop é dada pelos seguintes esquemas de axiomas:
A regra de inferência utilizada é modus ponens: A, A⊃ B ⊢ B
No Axioma 7, ‘C[A/B]′ é a notação para a fórmula que resulta de C pela substituição de uma ou mais ocorrências de A por uma ou mais ocorrência de B. Este axioma pretende ser um substituto da proposição (52) de BS, quando ‘≡’ é aplicado a fórmulas.
Chamaremos de CPC (Cálculo Proposicional Clássico) o sub-cálculo de Prop-BS que tem os axiomas de (1) a (5) expressáveis na linguagem clássica (LC) contendo apenas variáveis proposicionais, a negação, implicação e Modus Ponens. Os seguintes fatos são válidos em CPC e LC:
- CPC é uma base axiomática completa para a lógica clássica das funções bivalentes em LC, ou seja, o conjunto dos teoremas de CPC é o mesmo que o das sentenças tautológicas clássicas de LC;
- LC é funcionalmente completa, isto quer dizer, todas as funções bivalentes de verdade podem ser expressas em LC
A prova de independência de (IV*), (BB) e (NN) mostra que BS-Prop não é um cálculo clássico, caso contrário, ‘≡’ teria de expressar uma função de verdade bivalente. Neste caso, alguma fórmula de LC deveria ser dedutivamente equivalente a ‘A≡ B’1.
Mas que função de verdade poderia ser expressa por ‘(A≡ B)’? Vamos considerar todas as possibilidades de distribuição dos valores de verdade V e F nas variáveis A e B:
| ≡ | V | F |
| V | 1 | 2 |
| F | 3 | 4 |
Como temos o axioma 6 (A≡ A), então nas posições 1 e 4 temos de ter o Verdadeiro. Por outro lado, uma vez que ((A≡ B)⊃(A⊃ B)) é demonstrável a partir do axioma (7) e, portanto, esta fórmula tem de ser verdadeira, então quando (A⊃ B) é falsa (na posição 2), (A≡ B) também deve ser. Por outro lado, ((A⊃ B)⊃(B⊃ A)) é demonstrável no sistema (a partir de 57 de BS) e uma vez que (B⊃ A) é falsa na posição 3, então (A≡ B) deveria ser obrigatoriamente falsa nesta posição também. Portanto, em BS-Prop, as únicas candidatas que restariam para expressar (A≡ B) como uma função de verdade bivalente seriam todas as fórmulas equivalentes a: ¬ ((A⊃ B)⊃ ¬ (B⊃ A))2.
Destarte, se ‘≡’ expressasse uma função de verdade bivalente, (A≡ B) deveria ser dedutivamente equivalente a :¬ ((A⊃ B)⊃ ¬ (B⊃ A)). Mas, pela nossa hipótese, em BS-Prop, o teorema da dedução teria de ser válido e, portanto, o esquema (¬ ((A⊃ B)⊃ ¬ (B⊃ A))⊃ (A≡ B)) deveria ser demonstrável.
Contudo, recorrendo-se a uma matriz com três valores, mostraremos que um esquema dedutivamente equivalente a (¬ ((A⊃ B)⊃ ¬ (B⊃ A))⊃ (A≡ B)) não é demonstrável em BS-Prop.
Portanto, ‘A≡ B’ não expressa a equivalência material e, assim, não expressa nenhuma função de verdade bivalente. Disto, podemos concluir que BS-Prop não é um cálculo clássico.
2 Matriz Trivalente para BS-Prop
Seja M=<{1,2,3}, {1},¬, ⊃, ≡ > uma matriz trivalente com o valor distinguido 1. Sejam também as tabelas abaixo para os conectivos de BS-Prop:
Table 1: Negação
A ¬ A 1 2 2 1 3 1
Table 2: Implicação
⊃ 1 2 3 1 1 2 2 2 1 1 1 3 1 1 1
Table 3: Identidade de Conteúdo
≡ 1 2 3 1 1 3 3 2 3 1 3 3 3 3 1
3 M-Validade dos Axiomas de BS-Prop
Dizemos que uma fórmula é M-válida se ela recebe valor distinguido 1 para qualquer atribuição dada às suas variáveis proposicionais.
Agora, verificaremos se os axiomas de (1) a (7) recebem valor 1 para todas as atribuições, mostrando que todos são M-válidos.
Table 4: Axioma 1 – (A⊃(B⊃ A))
A B B ⊃ A (A⊃(B⊃ A)) 1 1 1 1 1 2 1 1 1 3 1 1 2 1 2 1 2 2 1 1 2 3 1 1 3 1 2 1 3 2 1 1 3 3 1 1
Table 5: Axioma 2 – ((A⊃(B⊃ C))⊃ ((A⊃ B)⊃ (A⊃ C)))
A B C (B⊃C) (A⊃(B⊃C)) (A⊃B) (A⊃C) ((A⊃B)⊃(A⊃C)) Ax. 2 1 1 1 1 1 1 1 1 1 1 1 2 2 2 1 2 2 1 1 1 3 2 2 1 2 2 1 1 2 1 1 1 2 1 1 1 1 2 2 1 1 2 2 1 1 1 2 3 1 1 2 2 1 1 1 3 1 1 1 2 1 1 1 1 3 2 1 1 2 2 1 1 1 3 3 1 1 2 2 1 1 2 1 1 1 1 1 1 1 1 2 1 2 2 1 1 1 1 1 2 1 3 2 1 1 1 1 1 2 2 1 1 1 1 1 1 1 2 2 2 1 1 1 1 1 1 2 2 3 1 1 1 1 1 1 2 3 1 1 1 1 1 1 1 2 3 2 1 1 1 1 1 1 2 3 3 1 1 1 1 1 1 3 1 1 1 1 1 1 1 1 3 1 2 2 1 1 1 1 1 3 1 3 2 1 1 1 1 1 3 2 1 1 1 1 1 1 1 3 2 2 1 1 1 1 1 1 3 2 3 1 1 1 1 1 1 3 3 1 1 1 1 1 1 1 3 3 2 1 1 1 1 1 1 3 3 3 1 1 1 1 1 1
Table 6: Axioma 5– ((A ⊃ B)⊃ (¬ B ⊃ ¬ A))
A B ¬A ¬B (A⊃B) (¬B⊃¬A) Ax. 5 1 1 2 2 1 1 1 1 2 1 2 2 2 1 1 3 1 2 2 2 1 2 1 2 1 1 1 1 2 2 1 1 1 1 1 2 3 1 1 1 1 1 3 1 2 1 1 1 1 3 2 1 1 1 1 1 3 3 1 1 1 1 1
Table 7: Axioma 6 – (A ≡ A)
A (A ≡ A) 1 1 2 1 3 1
O axioma 7 tem a forma implicativa, portanto ele só poderia receber um valor diferente de 1 no caso do antecedente receber o valor 1. Mas, (A≡ B) só receberá valor 1, quando A e B receberem o mesmo valor. Ora, se A e B tiverem o mesmo valor, C e C[A/B] terão necessariamente o mesmo valor, qualquer que seja C. Mas, pela tabela da implicação, quando o antecedente e o consequente recebem o mesmo valor, a implicação receberá o valor 1. Assim, sempre que (A≡ B) tiver valor 1, (C⊃ C[A/B]) terá o valor 1 também. Portanto, o axioma 7 é M-válido.
Se chamarmos grotescas todas as fórmulas que recebem o valor 1 para todas as atribuições, então:
O próximo passo é mostrar que (IV*), (NN) e (BB) não são grotescos. Para isto, basta mostrar apenas a existência de uma M-valoração que dá um valor diferente de 1 para cada uma destas fórmulas.
4 Independência de (IV*), (NN) e (BB)
Independência de IV*: (¬(A ≡ ¬ B)⊃ (A ≡ B))
Há três possibilidades nas quais (IV*) não recebe valor 1. Estas são:
Table 8: IV* - (¬(A ≡ ¬ B)⊃ (A ≡ B))
A B ¬B (A≡¬B) ¬(A≡¬B) (A≡B) (¬(A≡¬B)⊃(A≡B)) 2 3 1 3 1 3 2 3 1 2 3 1 3 2 3 2 1 3 1 3 2
Independência de (BB): ((A⊃ B)⊃((B⊃ A)⊃(A≡ B)))
Há duas possibilidades nas quais (BB) não recebe valor 1
Table 9: BB – ((A⊃ B)⊃((B⊃ A)⊃(A≡ B)))
A B (A⊃B) (B⊃A) (A≡B) ((B⊃A)⊃(A≡B)) BB 2 3 1 1 3 2 2 3 2 1 1 3 2 2
Independência de (NN): ¬¬ A ≡ A
Há uma possibilidade na qual (NN) não recebe valor 1.
Table 10: NN – ¬¬ A ≡ A
A ¬ A ¬¬ A (A ≡ ¬¬ A) 3 1 2 3
- *
-
Esta prova foi-nos sugerida pela Prof(a) Andrea Loparic.
- 1
-
Obviamente, BS-Prop seria uma base, na sua linguagem (LC + ≡), para a lógica das funções de verdade bivalentes.
- 2
-
Esta fórmula expressa a equivalência material.
This document was translated from LATEX by HEVEA.
Código:
\documentclass[10pt,a4paper]{article}
\usepackage[latin1]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
%\usepackage[usenames,dvipsnames]{pstricks}
%\usepackage{epsfig}
%\usepackage{pst-grad} % For gradients
%\usepackage{pst-plot} % For axes
\usepackage[brazil]{babel}
\title{Provas de Independência\footnote{Esta prova foi-nos sugerida pela Prof(a) Andrea Loparic.}}
\begin{document}
\maketitle
\begin{abstract}
Mostramos no presente artigo que a fórmula $\neg\neg A \equiv A$ e análogos do Axioma IV e Teorema IVa de \textit{Grundgesetze der Arithmetik} não são demonstráveis em \textit{Begriffsschrift}.
\tableofcontents
\listoftables
\end{abstract}
\section{O Cálculo BS-Prop}
A linguagem de \textit{Begriffsschrift} (\textbf{BS}) é inteiramente diferente da linguagem dos sistemas lógicos formais contemporâneos. De fato, poderia ser sem sentido e anacrônico
tentar apresentar o conteúdo de \textbf{BS} como um sistema formal. Porém, é possível
interpretar a linguagem de \textbf{BS} em uma linguagem formalizada contemporânea.
Foi assim que Lukasiewicz mostrou que os axiomas (1), (2), (28), (31) e (41) são
independentes uns dos outros e que o axioma (8) de \textbf{BS} não é independente, sendo
provável a partir dos axiomas (1) e (2). Neste sentido, iremos propor um cálculo,
que será chamado \textbf{BS-Prop}, no qual tentaremos interpretar os axiomas (1), (2),
(28), (31), (41), (52) e (54) de \textbf{BS}. A linguagem de \textbf{BS-Prop} é diferente da linguagem usual dos sistemas lógicos formais proposicionais contemporâneos, uma vez
que, além de variáveis proposicionais, do conectivo unário `$\neg$' (a negação) e do
conectivo binário `$\supset$' (a implicação), há um conectivo binário `$\equiv$' que será chamado identidade de conteúdo.
A base axiomática para BS-prop é dada pelos seguintes esquemas de axiomas:
\newtheorem{axiom}{Axioma}
\begin{axiom}
$(A \supset (B \supset A))$
\end{axiom}
\begin{axiom}
$((A\supset(B\supset C))\supset ((A \supset B)\supset (A \supset B)))$
\end{axiom}
\begin{axiom}
$(\neg\neg A \supset A)$
\end{axiom}
\begin{axiom}
$(A \supset \neg\neg A)$
\end{axiom}
\begin{axiom}
$((A\supset B)\supset (\neg B \supset \neg A))$
\end{axiom}
\begin{axiom}
$(A \equiv A)$
\end{axiom}
\begin{axiom}
$((A \equiv B)\supset(C\supset C[A/B]))$
\end{axiom}
\noindent
A regra de inferência utilizada é \textit{modus ponens}: $A, A\supset B \vdash B$
No Axioma 7, `$C[A/B]'$ é a notação para a fórmula que resulta de $C$ pela substituição de uma ou mais ocorrências de $A$ por uma ou mais ocorrência de $B$. Este axioma pretende ser um substituto da proposição (52) de \textbf{BS}, quando `$\equiv$' é aplicado a fórmulas.
Chamaremos de CPC (Cálculo Proposicional Clássico) o sub-cálculo de Prop-BS que tem os axiomas de (1) a (5) expressáveis na linguagem clássica (LC) contendo apenas variáveis proposicionais, a negação, implicação e Modus Ponens. Os seguintes fatos são válidos em CPC e LC:
\begin{enumerate}
\item[I] CPC é uma base axiomática completa para a lógica clássica das funções bivalentes em LC, ou seja, o conjunto dos teoremas de CPC é o mesmo que o das sentenças tautológicas clássicas de LC;
\item[II] LC é funcionalmente completa, isto quer dizer, todas as funções bivalentes de verdade podem ser expressas em LC
\end{enumerate}
A prova de independência de (IV*), (BB) e (NN) mostra que BS-Prop não é um cálculo clássico, caso contrário, `$\equiv$' teria de expressar uma função de verdade bivalente. Neste caso, alguma fórmula de LC deveria ser dedutivamente equivalente a `$A\equiv B$'\footnote{Obviamente, BS-Prop seria uma base, na sua linguagem (LC +\ $\equiv$), para a lógica das funções de verdade bivalentes.}.
Mas que função de verdade poderia ser expressa por `$(A\equiv B)$'? Vamos considerar todas as possibilidades de distribuição dos valores de verdade V e F nas variáveis $A$ e $B$:
\begin{center}
\begin{tabular}{|c|c|c|}
\hline
$\equiv$ & V & F\\
\hline
V & 1 & 2\\
\hline
F & 3 & 4\\
\hline
\end{tabular}
\end{center}
Como temos o axioma 6 $(A\equiv A)$, então nas posições 1 e 4 temos de ter o Verdadeiro. Por outro lado, uma vez que $((A\equiv B)\supset(A\supset B))$ é demonstrável a partir do
axioma (7) e, portanto, esta fórmula tem de ser verdadeira, então quando $(A\supset B)$ é falsa (na posição 2), $(A\equiv B)$ também deve ser. Por outro lado, $((A\supset B)\supset(B\supset A))$ é demonstrável no sistema (a partir de 57 de BS) e uma vez que $(B\supset A)$ é falsa na posição 3, então $(A\equiv B)$ deveria ser obrigatoriamente falsa nesta posição também. Portanto, em BS-Prop, as únicas candidatas que restariam para expressar $(A\equiv B)$ como uma função de verdade bivalente seriam todas as fórmulas equivalentes a: $\neg ((A\supset B)\supset \neg (B\supset A))$\footnote{Esta fórmula expressa a equivalência material.}.
Destarte, se `$\equiv$' expressasse uma função de verdade bivalente, $(A\equiv B)$ deveria ser dedutivamente equivalente a :$\neg ((A\supset B)\supset \neg (B\supset A))$. Mas, pela nossa
hipótese, em BS-Prop, o teorema da dedução teria de ser válido e, portanto, o esquema $(\neg ((A\supset B)\supset \neg (B\supset A))\supset (A\equiv B))$ deveria ser demonstrável.
Contudo, recorrendo-se a uma matriz com três valores, mostraremos que um esquema dedutivamente equivalente a $(\neg ((A\supset B)\supset \neg (B\supset A))\supset (A\equiv B))$ não é demonstrável em BS-Prop.
Portanto, `$A\equiv B$' não expressa a equivalência material e, assim, não expressa nenhuma função de verdade bivalente. Disto, podemos concluir que BS-Prop não é um cálculo clássico.
\section{Matriz Trivalente para BS-Prop}
Seja $M=<\{1,2,3\}, \{1\},\neg, \supset, \equiv >$ uma matriz trivalente com o valor distinguido 1. Sejam também as tabelas abaixo para os conectivos de BS-Prop:
\begin{table}[!htp]
\caption{Negação}
\begin{center}
\begin{tabular}{|c|c|}
\hline
$A$ & $\neg A$\\
\hline
1 & 2\\
\hline
2 & 1\\
\hline
3 & 1\\
\hline
\end{tabular}
\end{center}
\end{table}
\begin{table}[!htp]
\caption{Implicação}
\begin{center}
\begin{tabular}{|c|c|c|c|}
\hline
$\supset$ & 1 & 2 & 3\\
\hline
1 & 1 & 2 & 2\\
\hline
2 & 1 & 1 & 1\\
\hline
3 & 1 & 1 & 1\\
\hline
\end{tabular}
\end{center}
\end{table}
\begin{table}[!htp]
\caption{Identidade de Conteúdo}
\begin{center}
\begin{tabular}{|c|c|c|c|}
\hline
$\equiv$ & 1 & 2 & 3\\
\hline
1 & 1 & 3 & 3\\
\hline
2 & 3 & 1 & 3\\
\hline
3 & 3 & 3 & 1\\
\hline
\end{tabular}
\end{center}
\end{table}
\section{M-Validade dos Axiomas de BS-Prop}
Dizemos que uma fórmula é M-válida se ela recebe valor distinguido 1 para qualquer atribuição dada às suas variáveis proposicionais.
Agora, verificaremos se os axiomas de (1) a (7) recebem valor 1 para todas as atribuições, mostrando que todos são M-válidos.
\begin{table}[!htp]
\caption{Axioma 1 -- $(A\supset(B\supset A))$}
\begin{center}
\begin{tabular}{|c|c|c|c|}
\hline
$A$ & $B$ & $B \supset A$ & $(A\supset(B\supset A))$\\
\hline
1 & 1 & 1 & 1\\
\hline
1 & 2 & 1 & 1\\
\hline
1 & 3 & 1 & 1\\
\hline
2 & 1 & 2 & 1\\
\hline
2 & 2 & 1 & 1\\
\hline
2 & 3 & 1 & 1\\
\hline
3 & 1 & 2 & 1\\
\hline
3 & 2 & 1 & 1\\
\hline
3 & 3 & 1 & 1\\
\hline
\end{tabular}
\end{center}
\end{table}
\begin{table}[!htp]
\caption{Axioma 2 -- $((A\supset(B\supset C))\supset ((A\supset B)\supset (A\supset C)))$}
\begin{center}
\begin{tabular}{|c|c|c|c|c|c|c|c|c|}
\hline
$A$ & $B$ & $C$ & $(B\supset C)$ & $(A\supset(B\supset C))$ & $(A\supset B)$ & $(A\supset C)$ & $((A\supset B)\supset (A\supset C))$ & Ax. 2\\
\hline
1 & 1 & 1 & 1 & 1 & 1 &1 & 1 & 1\\
\hline
1 & 1 & 2 & 2 & 2 & 1 & 2 & 2 & 1\\
\hline
1 & 1 & 3 & 2 & 2 & 1 & 2 & 2 & 1 \\
\hline
1 & 2 & 1 & 1 & 1 & 2 & 1 & 1 & 1\\
\hline
1 & 2 & 2 & 1 & 1 & 2 & 2 & 1 & 1\\
\hline
1 & 2 & 3 & 1 & 1 & 2 & 2 & 1 & 1\\
\hline
1 & 3 & 1 & 1 & 1 & 2 & 1 & 1 & 1\\
\hline
1 & 3 & 2 & 1 & 1 & 2 & 2 & 1 & 1\\
\hline
1 & 3 & 3 & 1 & 1 & 2 & 2 & 1 & 1\\
\hline
2 & 1 & 1 & 1 & 1 & 1 & 1 & 1 & 1\\
\hline
2 & 1 & 2 & 2 & 1 & 1 & 1 & 1 & 1\\
\hline
2 & 1 & 3 & 2 & 1 & 1 & 1 & 1 & 1\\
\hline
2 & 2 & 1 & 1 & 1 & 1 & 1 & 1 & 1\\
\hline
2 & 2 & 2 & 1 & 1 & 1 & 1 & 1 & 1\\
\hline
2 & 2 & 3 & 1 & 1 & 1 & 1 & 1 & 1\\
\hline
2 & 3 & 1 & 1 & 1 & 1 & 1 & 1 & 1\\
\hline
2 & 3 & 2 & 1 & 1 & 1 & 1 & 1 & 1\\
\hline
2 & 3 & 3 & 1 & 1 & 1 & 1 & 1 & 1\\
\hline
3 & 1 & 1 & 1 & 1 & 1 & 1 & 1 & 1\\
\hline
3 & 1 & 2 & 2 & 1 & 1 & 1 & 1 & 1\\
\hline
3 & 1 & 3 & 2 & 1 & 1 & 1 & 1 & 1\\
\hline
3 & 2 & 1 & 1 & 1 & 1 & 1 & 1 & 1\\
\hline
3 & 2 & 2 & 1 & 1 & 1 & 1 & 1 & 1\\
\hline
3 & 2 & 3 & 1 & 1 & 1 & 1 & 1 & 1\\
\hline
3 & 3 & 1 & 1 & 1 & 1 & 1 & 1 & 1\\
\hline
3 & 3 & 2 & 1 & 1 & 1 & 1 & 1 & 1\\
\hline
3 & 3 & 3 & 1 & 1 & 1 & 1 & 1 & 1\\
\hline
\end{tabular}
\end{center}
\end{table}
\begin{table}[!htp]
\caption{Axioma 5-- $((A \supset B)\supset (\neg B \supset \neg A))$}
\begin{center}
\begin{tabular}{|c|c|c|c|c|c|c|}
\hline
$A$ & $B$ & $\neg A$ & $\neg B$ & $(A \supset B)$ & $(\neg B \supset \neg A)$ & Ax. 5\\
\hline
1 & 1 & 2 & 2 & 1 & 1 & 1\\
\hline
1 & 2 & 1 & 2 & 2 & 2 & 1\\
\hline
1 & 3 & 1 & 2 & 2 & 2 & 1\\
\hline
2 & 1 & 2 & 1 & 1 & 1 & 1\\
\hline
2 & 2 & 1 & 1 & 1 & 1 & 1\\
\hline
2 & 3 & 1 & 1 & 1 & 1 & 1\\
\hline
3 & 1 & 2 & 1 & 1 & 1 & 1\\
\hline
3 & 2 & 1 & 1 & 1 & 1 & 1\\
\hline
3 & 3 & 1 & 1 & 1 & 1 & 1\\
\hline
\end{tabular}
\end{center}
\end{table}
\begin{table}[!htp]
\caption{Axioma 6 -- $(A \equiv A)$}
\begin{center}
\begin{tabular}{|c|c|}
\hline
$A$ & $(A \equiv A)$\\
\hline
1 & 1\\
\hline
2 & 1\\
\hline
3 & 1\\
\hline
\end{tabular}
\end{center}
\end{table}
\newpage
O axioma 7 tem a forma implicativa, portanto ele só poderia receber um valor diferente de 1 no caso do antecedente receber o valor 1. Mas, ($A\equiv B$) só receberá valor 1, quando $A$ e $B$ receberem o mesmo valor. Ora, se $A$ e $B$ tiverem o mesmo valor, $C$ e $C[A/B]$ terão necessariamente o mesmo valor, qualquer que seja $C$. Mas, pela tabela da implicação, quando o antecedente e o consequente recebem o mesmo valor, a implicação receberá o valor 1. Assim, sempre que $(A\equiv B)$ tiver valor 1, $(C\supset C[A/B])$ terá o valor 1 também. Portanto, o axioma 7 é M-válido.
\newtheorem{teorema}{Teorema}
\begin{teorema}
Todos os axiomas de BS-Prop são M-válidos.
\end{teorema}
Se chamarmos grotescas todas as fórmulas que recebem o valor 1 para todas as
atribuições, então:
\newtheorem{lema}{Lema}
\begin{lema}
\textbf{Modus Ponens} (\textbf{MP}) preserva a propriedade de ser grotesca.
\end{lema}
\newtheorem{esbocodeprova}{Esboço de Prova}
\begin{esbocodeprova}
Assuma que $A$ e $A\supset B$ são grotescas. Assuma, por contradição, que $B$ (inferida por \textbf{MP}) não é grotesca. Ou seja, $B$ recebe valor 2 ou 3. Mas, uma vez que $A$ é grotesco, ele recebe valor 1 sempre. Assim, existiria alguma atribuição tal que $A$ é 1 e $B$ é 2 ou 3. Mas, nestes casos, seguindo a tabela de implicação, $A\supset B$ receberia valor 2, contradizendo o fato inicial de que $A\supset B$ tem a propriedade de ser grotesca.
\end{esbocodeprova}
\newtheorem{corolario}{Corolário}
\begin{corolario}
Todos os teoremas de BS-Prop são grotescos, portanto sempre recebem valor 1, ou seja, são M-válidos.
\end{corolario}
O próximo passo é mostrar que (\textbf{IV*}), (\textbf{NN}) e (\textbf{BB}) não são grotescos. Para isto, basta mostrar apenas a existência de uma M-valoração que dá um valor diferente de 1 para cada uma destas fórmulas.
\section{Independência de (\textbf{IV*}), (\textbf{NN}) e (\textbf{BB})}
\noindent
\textbf{Independência de IV*}: $(\neg(A \equiv \neg B)\supset (A \equiv B))$\\
Há três possibilidades nas quais (\textbf{IV*}) não recebe valor 1. Estas são:
\begin{table}[!htp]
\caption{IV* - $(\neg(A \equiv \neg B)\supset (A \equiv B))$}
\begin{center}
\begin{tabular}{|c|c|c|c|c|c|c|}
\hline
$A$ & $B$ & $\neg B$ & $(A\equiv\neg B)$ & $\neg(A\equiv\neg B)$ & $(A \equiv B)$ & $(\neg(A \equiv \neg B)\supset (A \equiv B))$\\
\hline
2 & 3 & 1 & 3 & 1 & 3 & 2\\
\hline
3 & 1 & 2 & 3 & 1 & 3 & 2\\
\hline
3 & 2 & 1 & 3 & 1 & 3 & 2\\
\hline
\end{tabular}
\end{center}
\end{table}
\newpage
\noindent
\textbf{Independência de (BB)}: $((A\supset B)\supset((B\supset A)\supset(A\equiv B)))$\\
Há duas possibilidades nas quais (\textbf{BB}) não recebe valor 1
\begin{table}[!htp]
\caption{\textbf{BB} -- $((A\supset B)\supset((B\supset A)\supset(A\equiv B)))$}
\begin{center}
\begin{tabular}{|c|c|c|c|c|c|c|c|}
\hline
$A$ & $B$ & $(A\supset B)$ & $(B \supset A)$ & $(A \equiv B)$ & $((B \supset A)\supset(A \equiv B))$ & \textbf{BB}\\
\hline
2 & 3 & 1 & 1 & 3 & 2 & 2\\
\hline
3 & 2 & 1 & 1 & 3 & 2 & 2\\
\hline
\end{tabular}
\end{center}
\end{table}
\noindent
\textbf{Independência de (NN)}: $\neg\neg A \equiv A$
\noindent
Há uma possibilidade na qual (\textbf{NN}) não recebe valor 1.
\begin{table}[!htp]
\caption{\textbf{NN} -- $\neg\neg A \equiv A$}
\begin{center}
\begin{tabular}{|c|c|c|c|}
\hline
$A$ & $\neg A$ & $\neg\neg A$ & $(A \equiv \neg\neg A)$\\
\hline
3 & 1 & 2 & 3\\
\hline
\end{tabular}
\end{center}
\end{table}
\end{document}