Sistema Formal L para Lógica de Predicados

Prévia do material em texto

Resumos - Lógica - Prof. Ricardo P. Tassinari - Departamento de Filosofia - Unesp/Marília - 2009
NOSSA 2ª CONCEITOGRAFIA: O SISTEMA FORMAL L PARA A LÓGICA DE PREDICADOS DE 
PRIMEIRA ORDEM 
Nesta seção, vamos apresentar o desenvolvimento de uma conceitografia para a Lógica de Predi-
cado de Primeira Ordem (ou, como também chamamos aqui, Lógica Intra-sentencial), o Sistema 
Formal L; ou seja, apresentamos uma “linguagem” tal que a utilização de suas regras sintáticas 
apenas garante a validade dos argumentos nela desenvolvidos. Para tal, expomos a seguir, primei-
ramente, a noção de conseqüência semântica que e, logo em seguida, o sistema formal Formal L.
A NOÇÃO DE CONSEQÜÊNCIA SEMÂNTICA NA LÓGICA DE PREDICADOS DE PRIMEIRA ORDEM 
Assim como na Lógica Proposicional Clássica, podemos definir a noção de conseqüência semântica 
na Lógica de Predicados de Primeira Ordem a partir da noção de argumento válido como a seguir.
Definição. Uma fórmula B é uma conseqüência semântica de um conjunto Γ de fórmulas se, e so-
mente se, Γ|=B (isto é, sempre que todas as fórmulas de Γ são válidas, B também é válida). 
O SISTEMA FORMAL L 
O Sistema Formal L se baseia sobre a noção geral de sistema formal apresentada na primeira 
parte para introdução do sistema formal L para a Lógica Proposicional Clássica. Assim, para defi-
nir o Sistema Formal L, temos de introduzir seus símbolos, suas fórmulas, seus axiomas e suas 
regras de inferência. Para maiores detalhes a respeito de L, e de suas propriedades, consultar 
CASTRUCCI 1982, FEITOSA & PAUDOVICH 2005 e MENDELSON 1997
Os Símbolos (alfabeto de L)
Conectivos (condicional e negação): → ~
Símbolos auxiliares (parênteses e vírgula): ( ) ,
Variáveis individuais: xi
Constantes individuais: ai
Letras Predicativas: Ain (n e i são numerais representando números naturais, n é chamado de ari-
dade de Ain) 
Quantificador Universal: ∀
As Fórmulas de L
Se Ain é uma letra predicativa e α1, α2, ..., αn são termos (i.e., por definição, constantes individuais 
ou variáveis individuais), então:
a. Ainα1, α2, ..., αn é uma fórmula (chamada de fórmula atômica)*;
b. Se B eC são fórmulas, então ~B , ~C , (B →C ) são fórmulas;
c. Se B é uma fórmula e α é uma variável individual, então ∀αB é uma fórmula;
d. As fórmulas são apenas aquelas decorrentes dos itens a, b e c acima.
* Notar que A00, A10, A20, ..., etc. são fórmulas atômicas, que denominaremos de letras proposi-
cionais.
Os Axiomas de L
São axiomas as fórmulas que tem a seguinte forma (esquemas de axiomas): 
(B → (C → B ))
((B → (C →D )) → ((B → C ) → (B → D )))
((~C → ~B ) → (( ~C →B ) → C )))
(∀xB(x) → B(t)), se t é um termo livre para x em B(x) (IU)1;
(∀x(B→C ) → (B→∀xC )), se x não ocorre livre em B ; 
As Regras de Inferência de L
Modus Ponens: Generalização Universal:
B , (B →C ) B 
C ∀xB
As outras constantes lógicas (∨, ∧, ↔ e ∃) são definidas por:
(B ∨ C ) :=def. (~B →C )
(B ∧ C ) :=def. ~(B →~C )
(B ↔C ) :=def. ((B →C )∧(C →B )), ou seja, ~((B →C )→~(C →B ))
∃xB :=def. ~∀x~B 
As definições de demonstração, teorema, dedução, conseqüência sintática e uso do Símbolo de 
Dedução |–L , são exatamente como em A NOÇÃO DE SISTEMA FORMAL E A NOSSA 1ª CONCEITOGRAFIA: O 
SISTEMA FORMAL L. 
INDEPENDÊNCIA DOS AXIOMAS, CONSISTÊNCIA, DEDUÇÃO E L COMO EXTENSÃO DE L 
Metateorema da Independência dos Axiomas
Os esquemas de axiomas e regras de inferência de L são independentes. 
Metateorema da Consistência
L é consistente (i.e., por definição, não existe uma fórmula B tal que |–L B e |–L ~B). 
Metateorema da Dedução
Seja Γ um conjunto de fórmulas e sejam B eC fórmulas, se Γ, B |–L C e nessa dedução não se 
aplica Generalização Universal em uma fórmula que depende de B 2, então: Γ |–L B →C . 
1 Este esquema de axiomas expressa a Instanciação Universal, abreviada por IU. Para maiores 
detalhes e para as definições de “termo livre para uma variável em uma fórmula” e de “ocorrên-
cia livre de uma variável em uma fórmula”, que entram, respectivamente, nas definições dos es-
quemas de axiomas 4 e 5, veja as referências bibliográficas.
2 Em particular, isso ocorre se B é fechada, i.e., não tem variáveis livres. Para as definições de 
“fórmula fechada” e “fórmula que depende de uma fórmula” em uma demonstração e para mais 
detalhes, veja as referências bibliográficas.
Resumos - Lógica - Prof. Ricardo P. Tassinari - Departamento de Filosofia - Unesp/Marília - 2009
Definição. Uma fórmula B é da Lógica Proposicional se todas as suas letras predicativas são le-
tras proposicionais. 
Metateorema de L como Extensão da Lógica Proposicional
Todo teorema de L que é da Lógica Proposicional pode ser demonstrado utilizando apenas os es-
quemas de axiomas 1, 2 e 3 e a regra de inferência Modus Ponens. 
CORREÇÃO, COMPLETUDE E DECIDIBILIDADE DO SISTEMA FORMAL L 
Os metateoremas a seguir dependem de definições semânticas (interpretação, fórmula verdadei-
ra em uma interpretação e tautologia) que não daremos aqui e que podem ser encontradas nas re-
ferências bibliográficas. Lembremos apenas a definição de fórmula válida. 
Definição. Uma fórmula B é válida se é verdadeira em toda interpretação. 
Em particular, temos que se uma fórmula B é da Lógica Proposicional, então: 
B é válida se, e somente se, B é uma tautologia. 
Metateorema da Correção
Todo teorema de L é uma fórmula válida. Em particular, todo teorema que é da Lógica Proposi-
cional é uma tautologia. 
Metateorema da Completude
Toda fórmula válida é teorema de L. Em particular, toda tautologia pode ser demonstrada utili-
zando apenas os esquemas de axiomas 1, 2 e 3 e a regra de inferência Modus Ponens
Metateorema da Decidibilidade da Lógica Proposicional
Dada uma fórmula B da Lógica Proposicional, existe um método efetivo para se determinar se B 
é, ou não, teorema de L. 
Em particular, as Tabelas-Verdade e o Método das Ramificações (ou Método dos Tableaux) são 
métodos que permitem determinar se B é, ou não, uma tautologia, logo, pelos Metateoremas da 
Correção e Completude, as Tabelas-Verdade e o Método das Ramificações podem determinar se 
B é, ou não, um teorema de L.. 
Metateorema da Indecidibilidade da Lógica de Primeira Ordem 
Não existe um método efetivo para determinar se uma fórmula B qualquer de L é, ou não, teor-
ema de L. 3
Porém, existe um método efetivo M tal que: 
se B é teorema de L, então M determina que B é teorema de L ; 
se B não é teorema de L , então M não determina que B não é teorema de L . 
Metateorema da Indecidibilidade da Validade em Primeira Ordem
3 Porém, para algumas classes de fórmulas, o problema de se determinar se as fórmulas são, ou 
não, teoremas de L (e, conseqüentemente, pelo Metateorema da Completude, se são ou não váli-
das) é decidível, por exemplo: para as classes das fórmulas apenas com letras sentenciais (Lógica 
Proposicional), como vimos; para as classes das fórmulas apenas com letras sentenciais e letras 
predicativas Ain, com n = 1 (Lógica de Primeira Ordem Monádica); para a classe das fórmulas sem 
quantificadores; ou, ainda, para a classe das fórmulas apenas com quantificadores universais.
Não existe um método efetivo para determinar se uma fórmula B qualquer de L é, ou não, válida. 
Porém, existe um método efetivo M tal que: 
se B é válida, então M determina que B é válida; 
se B não é válida, M não determina que B não é válida.
Em particular, podemos considerar o Método das Ramificações como sendo o método M citado 
nos metateoremas acima, ou seja: se uma fórmula é válida (ou teorema de L), então o Método das 
Ramificações permite verificar que ela é válida (ou teorema de L); porém, se a fórmula não é váli-
da (ou não é teorema de L), o Método das Ramificações nem sempre mostra que ela não é válida 
(ou não é teorema de L). Notemos, então, que, para uma fórmula qualquer, o método não permite 
saber se a fórmula é, ou não, válida ou teorema de L, pois, se até um certo momento, a aplicação 
do método não forneceuresposta, não sabemos se é porque a fórmula é válida (e teorema de L) e 
o método não terminou o computo, ou se nunca retornará resposta, pois a fórmula não é válida (e 
não é teorema de L).
Por fim, temos os seguintes metateoremas fundamentais para nossa questão aqui.
Metateorema da Correção Forte
Se Γ |–L B , então Γ|=B . Em particular, quando Γ é vazio temos o Metateorema da Correção: se |–L 
B , então |=B
Metateorema da Completude Forte
Se Γ|=B , então Γ |–L B . Em particular, quando Γ é vazio temos o Metateorema da Completude: se|
=B , então |– L B
Notemos que: todas as regras de inferência derivadas de L são regras de inferência válidas (pelo 
Metateorema da Correção Forte) e que todas as regras de inferência válidas da Lógica Proposi-
cional são regras derivadas no sistema L (pelo Metateorema da Completude Forte).
Temos assim estabelecida as bases para nossa conceitografia tal que uma fórmula é válida, ou 
seja, é verdadeira em qualquer interpretação, se e somente se, é teorema de L, ou seja, existe 
uma demonstração dessa fórmula a partir dos axiomas. Mais ainda, pelo metateoremas da corre-
ção forte e da completude forte, chegamos a conceitografia proposta no início da disciplina:
Significados  Signos Que, Proposições  Sentenças
  em nosso caso,  
Operações 
sobre
 significados

Operações
sobre
signos
 torna-se: Conseqüência 
semântica

Conseqüência
Sintática
(Demonstrações)
Γ|=B Γ |–L B
Vamos, a partir daqui, ver algumas definições e alguns resultados sobre teorias formais que usam 
o sistema formal L como sua lógica subjacente.