Provas de Independência*

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:

Axioma 1   (A ⊃ (B ⊃ A))
Axioma 2   ((A⊃(B⊃ C))⊃ ((A ⊃ B)⊃ (A ⊃ B)))
Axioma 3   (¬¬ A ⊃ A)
Axioma 4   (A ⊃ ¬¬ A)
Axioma 5   ((A⊃ B)⊃ (¬ B ⊃ ¬ A))
Axioma 6   (A ≡ A)
Axioma 7   ((A ≡ B)⊃(C⊃ C[A/B]))

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:

  1. 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;
  2. 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.

Teorema 1   Todos os axiomas de BS-Prop são M-válidos.

Se chamarmos grotescas todas as fórmulas que recebem o valor 1 para todas as atribuições, então:

Lema 1   Modus Ponens (MP) preserva a propriedade de ser grotesca.
Esboço de Prova 1   Assuma que A e A⊃ B são grotescas. Assuma, por contradição, que B (inferida por 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⊃ B receberia valor 2, contradizendo o fato inicial de que A⊃ B tem a propriedade de ser grotesca.
Corolário 1   Todos os teoremas de BS-Prop são grotescos, portanto sempre recebem valor 1, ou seja, são M-válidos.

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}