Lógica

CARLOS CALEIRO, PAULA GOUVEIA E JOÃO RASGA 
SECÇÃO DE LÓGICA E COMPUTAÇÃO
DEPARTAMENTO DE MATEMÁTICA
INSTITUTO SUPERIOR TÉCNICO

Aplicação motivadora: Verificação da correção parcial e total de programas imperativos

No decurso da sua actividade um informático irá ter de escrever programas que realizem uma certa tarefa pretendida. Mas como poderá ele ter a certeza que o programa faz o que se pretende? Ou sequer que o programa termina? Responder a estas questões é fundamental não só para quem faz o programa mas também para quem vai utilizar o código feito. 

Usando o cálculo de Hoare é possível comprovar através de uma demonstração que um programa imperativo termina ou realiza um certo cálculo.

Considere o programa correspondente ao corpo da seguinte função:

Function[{w, x}, 
        Module[{i, n}, 
i = 1; 
n = 
            0; 
While[
            i ≠ Length[w] + 1, 
If[
              w[[i]] > x, n = n + 1]; 
i = 
              i + 1]; 
n]]

será que o programa termina quaisquer que sejam os valores dos dados de entrada? E no caso de terminar, será que a variável n termina com o valor do número de elementos da lista w maiores que x, isto é, será que

                n == # {j : (w[[j]] > x)⋀(1 ≤ 
                    j ≤ Length[w])}?

Sendo o cálculo de Hoare não mais do que um sistema dedutivo de uma lógica convém perceber um pouco mais alguns conceitos importantes de lógica tais como, o que é um sistema dedutivo, o que é uma demonstração, o que é consequência dedutiva, o que é a semântica de uma lógica, o que é consequência semântica, entre outros aspectos importantes. Para este fim iremos começar por estudar lógica de primeira ordem, começando pelo seu fragmento proposicional. De seguida estudar-se-á então o cálculo de Hoare.

Lógica de primeira ordem

Um dos objectivos da lógica é o estudo dos mecanismos associados aos raciocínios válidos. Em que condições se pode dizer que uma certa afirmação é consequência de um certo conjunto de factos?  Será possível definir algoritmos que possam ser usados para comprovar que é um raciocínio válido dizer que uma certa afirmação é consequências de um certo conjunto de hipóteses? Será possível definir algoritmos que possam ser usados para construir consequências de um certo conjunto de hipóteses?

A linguagem natural é demasiado complexa e ambígua para poder ser directamente utilizada para estes propósitos. Para levar a cabo estas tarefas há que começar por definir uma linguagem formal que nos permita representar simbolicamente de uma forma precisa, sem ambiguidades, e tão simples quanto possível as hipóteses e as conclusões envolvidas. Esta linguagem formal inclui um conjunto de expressões com sintaxe bem definida, as fórmulas da linguagem. 

Por si só, as fórmulas são apenas sequências de caracteres. Só passam a representar um determinado facto ou propriedade,  após se lhes ter atribuído um certo significado, uma certa semântica. Como se verá adiante, os conceitos semânticos vão permitir definir o conceito de raciocínio válido.

Para construir algoritmos que permitam construir raciocínios válidos é frequentemente bastante complicado, se não mesmo impossível, manipular directamente os conceitos semânticos que os definem. É importante nessas situações ser capaz de desenvolver tais algoritmos recorrendo apenas à manipulação simbólica das fórmulas envolvidas. Obtêm-se assim os chamados sistemas dedutivos.

Existem muitas e diferentes lógicas. Como exemplos podem referir-se: a lógica proposicional, a lógica de primeira ordem, a lógica modal proposicional, lógica modal de primeira ordem, a lógica temporal linear (proposicional e de primeira ordem), a lógica temporal ramificada  (proposicional e de primeira ordem), a lógica dinâmica, a lógica (ou cálculo) de Hoare, a lógica epistémica e a lógica paraconsistente.  Elas diferem entre si na linguagem formal adoptada e/ou estruturas semânticas envolvidas. A escolha de uma ou outra lógica depende do tipo de propriedades e raciocínios que se pretendem representar.  Quanto mais complexos forem, mais complexas terá de ser a linguagem e/ou estruturas semânticas envolvidas.

A lógica de primeira ordem permite raciocinar e expressar propriedades sobre objectos ou indivíduos bem como exprimir conceitos como existência e universalidade.

Linguagem

No caso de uma linguagem da lógica de primeira ordem estão envolvidos dois tipos de expressões: expressões que denotam indivíduos ou objectos do domínio em causa (designadas por termos) e expressões às quais se pode atribuir o valor verdade ou falso (as fórmulas).  De seguida define-se a sintaxe dessas expressões.

Termos

A linguagem dos termos pode ser definida usando uma gramática. O alfabeto dessa gramática, isto é, o conjunto dos símbolos que podem aparecer nesses termos é constituído por símbolos de pontuação, símbolos de função e símbolos de variáveis. Os símbolos de função e de variáveis constituem a assinatura do sistema lógico.

Definição Uma assinatura de termos é um tuplo
						<F, τ, X>
em que
 • F é um conjunto, cujos elementos se designam por símbolos de função
 • τ : 
        F → (Subscript[ℕ, 0]), indica a aridade dos símbolos de funções
 • X é um conjunto numerável, cujos elementos se designam por variáveis.

Dada uma assinatura e um natural n denota-se por (Subscript[F, n]) o conjunto {f ∈ F :  τ(f) = n}. Os elementos de (Subscript[F, n]) representam-se por (Subscript[f, n, 1]), (Subscript[f, n, 2]), …. Os símbolos de função de aridade 0 designam-se símbolos de constante. Os símbolos de função de aridade 1 são também designados símbolos de função unários (ou de um argumento), os símbolos de função de aridade 2 são também designados símbolos de função binários (ou de dois argumento), etc.

EXEMPLOS

EXEMPLO 1

Considere-se a assinatura de termos <F, τ, X> em que

 • (Subscript[F, 0]) = ℤ
 • (Subscript[F, 1]) = {abs}
 • (Subscript[F, 2]) = {+,×}
 • (Subscript[F, n]) = ⌀ para n > 2
 • X = {(Subscript[x, 1]), (Subscript[x, 2]), …}.
 
Os símbolos de constante são 0, 1, -1, 2, -2,.... Existe um símbolo de função de aridade 1, o símbolo abs. Existem dois símbolos de função de aridade 2, os símbolos + e ×.

Note-se que, para já, os símbolos introduzidos na assinatura acima são apenas isso mesmo: símbolos. Nenhum significado está a ser, de momento, atribuído a estes símbolos. Só quando se considerarem estruturas semânticas é que se associa  a cada um desses símbolos um certo significado (uma função, neste caso).

EXEMPLO 2

Considere-se a assinatura de termos <F, τ, X> em que

 • (Subscript[F, 0]) = ℝ
 • (Subscript[F, 1]) = {sqrt, abs, sen, cos}
 • (Subscript[F, 2]) = {+,×}
 • (Subscript[F, n]) = ⌀ para n > 2
 • X = {(Subscript[x, 1]), (Subscript[x, 2]), …}.
 
Os símbolos de constante são os números reais,.... Existem 4 símbolos de função de aridade 1: sqrt, abs, sen, cos. Existem dois símbolos de função de aridade 2, + e ×.

Observe-se de novo que nenhum significado está ainda a ser tribuído aos símbolos introduzidos na assinatura anterior.

EXEMPLO 3

Considere-se a assinatura de termos <F, τ, X> em que

 • (Subscript[F, 0]) = {○}
 • (Subscript[F, 1]) = {▼}
 • (Subscript[F, 2]) = {◼}
 • (Subscript[F, n]) = ⌀ para n > 2
 • X = {(Subscript[x, 1]), (Subscript[x, 2]), …}.
 
Só há um símbolo de constante, o símbolo ○. Existe um símbolo de função de aridade 1, o símbolo ▼, e um símbolo de função de aridade 2, o símbolo ◼.

Com vista a definir rigorosamente a sintaxe dos termos, introduz-se agora a gramática que gera os termos de uma lógica associada a uma assinatura.

Definição A linguagem dos termos baseada na assinatura <F, τ, X> é o conjunto das sequências geradas pela gramática
						<V, I, P, S>
em que
 • V é o conjunto formado pelos símbolos não terminais TERMO, VAR, SF0,  SF1, SF2, …
 • I=X⋃F⋃{(, ), , }
 • S é o símbolo não terminal TERMO
 • P consiste nas produções
		TERMO → VAR | SF0 | SF1(TERMO) | 
        SF2(TERMO, TERMO) | …
		VAR → (Subscript[x, 1]) | (Subscript[x, 2]) | …
		SF0 → (Subscript[f, 0, 1]) | 
        (Subscript[f, 0, 2]) | … 
		SF1 → (Subscript[f, 1, 1]) | 
        (Subscript[f, 1, 2]) | …
		SF2 → (Subscript[f, 2, 1]) | 
        (Subscript[f, 2, 2]) | …
		⋮

As variáveis são termos, os símbolos de constante são termos e f((Subscript[t, 1]),...,(Subscript[t, n])) é um termo qualquer que seja o símbolo de função  f de aridade n>0 e quaisquer que sejam os termos (Subscript[t, 1]),...,(Subscript[t, n]).

A linguagem dos termos baseada numa assinatura de termos <F, τ, X> denota-se por Term(<F, τ, X>) ou então por Term quando não houver ambiguidade sobre qual a assinatura associada. Um termo diz-se fechado se nele não ocorrem variáveis.

EXEMPLOS

EXEMPLO 1

Considere-se a assinatura de termos <F, τ, X> em que (Subscript[F, 0]) = ℤ, (Subscript[F, 1]) = {abs}, (Subscript[F, 2]) = {+,×}, (Subscript[F, n]) = ⌀ para n > 2
e X = {(Subscript[x, 1]), (Subscript[x, 2]), …}. Alguns dos elementos pertencentes à linguagem dos termos baseada nesta assinatura são:
 
• 0
• -1
• (Subscript[x, 10])
• abs(-1)
• +(abs((Subscript[x, 10])),3)
• ×(abs(-1),+(abs((Subscript[x, 10])),3))

Os termos 0, -1 e abs(-1) são fechados. Os outros não são fechados.

Os termos acima referidos são, para já, apenas sequências de símbolos obedecendo à sintaxe definida pela gramática apresentada. Os termos são expressões construídas com o propósito de denotar indivíduos de um dado universo, mas só quando se considerarem estruturas semânticas e se aasociar a cada símbolo um certo significado é que se pode dizer qual é o indivíduo que é denotado por um certo termo.

EXEMPLO 2

Considere-se a assinatura de termos <F, τ, X> em que (Subscript[F, 0]) = ℝ, (Subscript[F, 1]) = {sqrt, abs, sen, cos}, (Subscript[F, 2]) = {+,×}, (Subscript[F, n]) = ⌀ para n > 2 e X = {(Subscript[x, 1]), (Subscript[x, 2]), …}. Alguns dos elementos pertencentes à linguagem dos termos baseada nesta assinatura são:
 
• 0
• π
• (Subscript[x, 1])
• sqrt(2)
• sin(π)
• +(×(sin((Subscript[x, 1])), 
              sin((Subscript[x, 1]))), ×(cos((Subscript[x, 1])), 
              cos((Subscript[x, 1]))))

Os termos  0, π, sqrt(2) e sin(π) são fechados. Os outros não são.

EXEMPLO 3

Considere-se a assinatura de termos <F, τ, X> em que (Subscript[F, 0]) = {○},  (Subscript[F, 1]) = {▼}, (Subscript[F, 2]) = {◼}, (Subscript[F, n]) = ⌀ para n > 2 e X = {(Subscript[x, 1]), (Subscript[x, 2]), …}. Alguns dos elementos pertencentes à linguagem dos termos baseada nesta assinatura são:
 
 • ○
 • (Subscript[x, 10])
 • ▼(○)
 • \(TraditionalForm\`◼(▼(○), ▼(○))\)
 • ▼(◼(
          (Subscript[x, 1]), ▼(○)))

Exercício Seja Σ uma assinatura. Mostre que o conjunto {E∈M:E é um termo sobre a assinatura Σ} é decidível.

Fórmulas

Para definir a sintaxe das fórmulas pode de novo utilizar-se uma gramática. O alfabeto dessa gramática, isto é, o conjunto dos símbolos que podem aparecer nas fórmulas da linguagem, é constituído por conectivos lógicos, símbolos de pontuação, símbolos de função e símbolos de predicados. Os símbolos de função e de predicado constituem a assinatura da lógica.

Definição Uma assinatura de primeira ordem é um tuplo
						<F, P, τ, X>
em que
 • \(TraditionalForm\`\(\(<\)\(F\)\), τ\_\(\(|\)\(F\)\), \(\(X\)\(>\)\)\) é uma assinatura de termos
 • P é um conjunto não vazio, disjunto de F, cujos elementos se designam por símbolos de predicado
 • τ : 
        F ⋃ P → (Subscript[ℕ, 0]) indica a aridade de funções e predicados.

Dada uma assinatura de primeira ordem e um natural n denota-se por (Subscript[P, n]) o conjunto {p ∈ P :  τ(p) = n}. Os elementos de (Subscript[P, n]) representam-se por (Subscript[p, n, 1]), (Subscript[p, n, 2]), …. Os elementos de (Subscript[P, 0]), os símbolos de predicado de aridade 0, são por vezes também  designados símbolos proposicionais. Os símbolos de predicado de aridade 1 são também designados símbolos de predicado unários (ou de um argumento), os símbolos de predicado de aridade 2 são também designados símbolos de predicado binários (ou de dois argumento), etc.

EXEMPLOS

EXEMPLO 1

Considere-se a assinatura de primeira ordem <F, P, τ, X> em que

 • (Subscript[F, 0]) = ℤ
 • (Subscript[F, 1]) = {abs}
 • (Subscript[F, 2]) = {+,×}
 • (Subscript[F, n]) = ⌀ para n > 2
 • (Subscript[P, 1]) = {Par,  Imp,  Prim}
 • (Subscript[P, 2]) = {=,>}
 • (Subscript[P, n]) = ⌀ para n ∉ {1, 2}
 • X = {(Subscript[x, 1]), (Subscript[x, 2]), …}.
 
Para além dos símbolos de função e variáveis já referidos, esta assinatura inclui três símbolos de predicado unários, os símbolos Par, Imp e Prim, e dois símbolos de predicado binários, os símbolos = e >.

Do mesmo modo que anteriormente, os símbolos de predicado introduzidos na assinatura são, para já, apenas símbolos. Nenhum significado lhes está a ser, de momento, atribuído. Só quando se considerarem estruturas semânticas é que se asocia a cada um desses símbolos um certo significado (um predicado, neste caso). Pode no entanto perceber-se que esta assinatura poderá ser apropriada para expressar algumas propriedades dos números inteiros.

EXEMPLO 2

Considere-se a assinatura de primeira ordem <F, P, τ, X> em que

 • (Subscript[F, 0]) = ℝ
 • (Subscript[F, 1]) = {sqrt, abs, sen, cos}
 • (Subscript[F, 2]) = {+,×}
 • (Subscript[F, n]) = ⌀ para n > 2
 • (Subscript[P, 2]) = {=,>}
 • (Subscript[P, n]) = ⌀ para n ≠ 2
 • X = {(Subscript[x, 1]), (Subscript[x, 2]), …}.

EXEMPLO 3

Considere-se a assinatura de primeira ordem <F, P, τ, X> em que

 • (Subscript[F, 0]) = {○}
 • (Subscript[F, 1]) = {▼}
 • (Subscript[F, 2]) = {◼}
 • (Subscript[F, n]) = ⌀ para n > 2
 • (Subscript[P, 1]) = {q, r}
 • (Subscript[P, 2]) = {p}
 • (Subscript[P, n]) = ⌀ para n ≠ 2
 • X = {(Subscript[x, 1]), (Subscript[x, 2]), …}.
 
Para além dos símbolos de função e variáveis já referidos, esta assinatura inclui dois símbolos de predicado unários, os símbolos q e r, e um símbolos de predicado binário, o símbolo p.

EXEMPLO 4

Considere-se a assinatura de primeira ordem <F, P, τ, X> em que

 • (Subscript[F, n]) = ⌀ para n ≥ 0
 • (Subscript[P, 0]) = {(Subscript[p, 1]), (Subscript[p, 2]), (Subscript[p, 3]), (Subscript[q, 1]), (Subscript[q, 2]), (Subscript[q, 3])}
 • (Subscript[P, n]) = ⌀ para n ≠ 0
 • X = {(Subscript[x, 1]), (Subscript[x, 2]), …}.
 
Esta assinatura tem apenas símbolos de predicado de aridade 0, isto é, símbolos proposicionais.

Pode-se agora definir linguagem de primeira ordem baseada numa assinatura de primeira ordem.

Definição A linguagem de primeira ordem baseada na assinatura <F, P, τ, X> é o conjunto das sequências geradas pela gramática
						<V, I, P, S>
em que
 • V é o conjunto formado pelos símbolos não terminais FORM, FORMATOMICA, TERMO, VAR, SF0, SP0, SF1, SP1, SF2, SP2, …
 • I=X⋃F⋃P⋃{ ¬,∧,∨,→,∀,∃}⋃{(, ), , } onde ¬ , ⋀, ⋁,  → , ∀  e ∃  são os símbolos para a negação, conjunção, disjunção, implicação, quantificação universal e quantificação existencial, respectivamente
 • S é o símbolo não terminal FORM
 • P consiste nas produções
		\(TraditionalForm\`FORM → 
          FORMATOMICA | \((¬ FORM)\) | \((FORM⋀FORM)\) | \((FORM⋁FORM)\) | \((FORM → 
            FORM)\) | \((∀ VAR\ FORM)\) | \((∃ VAR\ FORM)\) | …\)
		FORMATOMICA → SP0 | SP1(TERMO) | 
        SP2(TERMO, TERMO) | …
		SP0 → (Subscript[p, 0, 1]) | 
        (Subscript[p, 0, 2]) | …
		SP1 → (Subscript[p, 1, 1]) | 
        (Subscript[p, 1, 2]) | …
		SP2 → (Subscript[p, 2, 1]) | 
        (Subscript[p, 2, 2]) | …
		⋮ 
		TERMO → VAR | SF0 | SF1(TERMO) | 
        SF2(TERMO, TERMO) | …
		VAR → (Subscript[x, 1]) | (Subscript[x, 2]) | …
		SF0 → (Subscript[f, 0, 1]) | 
        (Subscript[f, 0, 2]) | …
		SF1 → (Subscript[f, 1, 1]) | 
        (Subscript[f, 1, 2]) | …
		SF2 → (Subscript[f, 2, 1]) | 
        (Subscript[f, 2, 2]) | …
		⋮

Os símbolos de predicado de aridade 0 são fórmulas,  p((Subscript[t, 1]),...,(Subscript[t, n])) é uma fórmula. qualquer que seja o símbolo de predicado p de aridade n>0 e quaisquer que sejam os termos (Subscript[t, 1]),...,(Subscript[t, n]), e (¬φ), (φ∧ψ),  (φ∨ψ),  (φ->ψ), (∀xφ), (∃xφ) são fórmulas quaisquer que sejam as fórmulas φ e ψ e variável x.

Sempre que não exista ambiguidade é usual omitirem-se os parênteses mais exteriores das fórmulas. Para simplificar, é também usual escrever  φ∧ψ∧γ em vez de  (φ∧ψ)∧γ ou de  φ∧(ψ∧γ). O mesmo se passa relativamente à disjunção.

A linguagem de primeira ordem baseada numa assinatura de primeira ordem <F, P, τ, X> denota-se por Form(<F, P, τ, X>) ou então por Form quando não houver ambiguidade sobre qual a assinatura associada.

EXEMPLOS

EXEMPLO 1

Considere-se a assinatura de primeira ordem <F, P, τ, X> em que (Subscript[F, 0]) = ℤ, (Subscript[F, 1]) = {abs}, (Subscript[F, 2]) = {+,×}, (Subscript[F, n]) = ⌀, para n > 2, (Subscript[P, 1]) = {Par,  Imp,  Prim}, (Subscript[P, 2]) = {=,>}, (Subscript[P, n]) = ⌀ para n ∉ {1, 2} e X = {(Subscript[x, 1]), (Subscript[x, 2]), …}. Algumas fórmulas pertencentes a esta linguagem são:

 • Par(2)
 • Prim(5)
 • Par((Subscript[x, 1]))∨Imp((Subscript[x, 1]))
 • >(abs((Subscript[x, 1])),(Subscript[x, 2]))
 • ∀(Subscript[x, 1])(Par((Subscript[x, 1]))->Imp(+((Subscript[x, 1]),1)))
 • ∀(Subscript[x, 1])((Prim((Subscript[x, 1]))∧ >((Subscript[x, 1]),2))->Imp((Subscript[x, 1])))
 • ∀(Subscript[x, 1])(∃(Subscript[x, 2]) >((Subscript[x, 1]),(Subscript[x, 2])))

As fórmulas, por si só, e tal como os termos, são apenas sequências de caracteres, construídas segundo certas regras. As fórmulas são construídas com o propósito de expressar certos factos ou propriedades dos indivíduos, que tanto podem ser verdadeiros como podem ser falsos, dependendo do contexto. Mas, de novo, só quando se considerarem as estruturas semânticas e se atribuir significado aos símbolos que ocorrem nas fórmulas, se pode dizer qual o facto ou propriedade que uma fórmula representa e se esse facto ou propriedade é verdadeiro ou falso.

EXEMPLO 2

Considere-se a assinatura de primeira ordem <F, P, τ, X> em que (Subscript[F, 0]) = ℝ, (Subscript[F, 1]) = {sqrt, abs, sen, cos}, (Subscript[F, 2]) = {+,×}, (Subscript[F, n]) = ⌀ para n > 2, (Subscript[P, 2]) = {=,>}, (Subscript[P, n]) = ⌀ para n ≠ 2 e  X = {(Subscript[x, 1]), (Subscript[x, 2]), …}. Algumas fórmulas pertencentes a esta linguagem são:

 • >(1,cos((Subscript[x, 1])))
 • >(cos((Subscript[x, 1])),-1)
 • ∀ (Subscript[x, 1])=((+(×(sin((Subscript[x, 1])), 
              sin((Subscript[x, 1]))), ×(cos((Subscript[x, 1])), 
              cos((Subscript[x, 1]))))),0)

EXEMPLO 3

Considere-se a assinatura de primeira ordem <F, P, τ, X> em que (Subscript[F, 0]) = {○}, (Subscript[F, 1]) = {▼}, (Subscript[F, 2]) = {◼}, (Subscript[F, n]) = ⌀ para n > 2, (Subscript[P, 1]) = {q, r}, (Subscript[P, 2]) = {p}, (Subscript[P, n]) = ⌀ para n ≠ 2 e X = {(Subscript[x, 1]), (Subscript[x, 2]), …}.Algumas fórmulas pertencentes a esta linguagem são:

 • p(○, (Subscript[x, 10]))
 • \(TraditionalForm\`∀ \(x\_1\) \(p(▼(○), ▼(◼(
                x\_1, ▼(○))))\)\)
 • \(TraditionalForm\`\((∀ \(x\_1\) \(p(▼(○), ▼(◼(
                    x\_1, ▼(○))))\))\)⋀\(p(○, x\_10)\)\).

EXEMPLO 4

Considere-se a assinatura de primeira ordem <F, P, τ, X> em que (Subscript[F, n]) = ⌀ para n ≥ 0,  (Subscript[P, 0]) = {(Subscript[p, 1]), (Subscript[p, 2]), (Subscript[p, 3]), (Subscript[q, 1]), (Subscript[q, 2]), (Subscript[q, 3])}, (Subscript[P, n]) = ⌀ para n ≠ 0 e X = {(Subscript[x, 1]), (Subscript[x, 2]), …}. Algumas fórmulas pertencentes a esta linguagem são:

•  (Subscript[p, 1])
•  (Subscript[q, 2])
• \(TraditionalForm\`p\_1 ∧ \((¬ p\_2)\) ∧ \((¬ p\_3)\)\)
• ((Subscript[q, 2]) -> (Subscript[p, 1]))∧ ((Subscript[p, 1]) -> (Subscript[q, 2]))

Exercício Seja Σ uma assinatura. Mostre que o conjunto {E∈M:E é uma fórmula de primeira ordem sobre a assinatura Σ} é decidível.

Podem identificar-se vários fragmentos relevantes de uma linguagem de primeira ordem:
  - o fragmento constituído apenas pelas fórmulas que incluem variáveis, símbolos de função e predicado, o quantificador universal, ∀, e os conectivos ¬ e ∧
  - o fragmento constituído apenas pelas fórmulas que incluem variáveis, símbolos de função e predicado, o quantificador universal, ∀, e os conectivos ¬ e ->
  - o fragmento constituído apenas pelas fórmulas que incluem variáveis, símbolos de função e predicado e os conectivos ¬ , ∧, ∨ e ->.
  
Um fragmento a que se dará particular destaque neste texto é o fragmento proposicional.

Definição: Fragmento proposicional
O  fragmento proposicional de uma linguagem de primeira ordem é constituído pelas fórmulas que incluem apenas os símbolos de predicado de aridade 0 (os símbolos proposicionais) e os conectivos ¬ , ∧, ∨ e ->. As fórmulas do fragmaento proposicional são fórmulas proposicionais.

Para o fragmento proposicional de uma linguagem de primeira ordem baseada numa assinatura <F, P, τ, X> só é relevante o conjunto (Subscript[P, 0]) (o conjunto dos símbolos de predicado de aridade 0). Por isso, de agora em diante, quando se fizer referência a um fragmento proposicional baseado num dado conjunto SP tal deverá ser entendido como o fragmento proposicional de uma linguagem de primeira ordem baseada numa assinatura na qual  o conjunto dos símbolos de predicado de aridade 0 é SP. O fragmento proposicional de uma linguagem de primeira ordem será então denotado por FProp(SP) ou, simplesmente FProp, quando não existirem dúvidas sobre o conjunto de símbolos proposicionais em causa.

Exercício Construa uma gramática que gere apenas as fórmulas do fragmento proposicional

Exercício Mostre que o conjunto {E ∈ M : 
            E é uma fórmula proposicional} é decidível.

Exercício: Em cima de uma mesa existem três caixas de madeira fechadas. Sabe-se que uma delas tem dentro 100 000euros e as outras estão vazias. Cada uma delas tem uma mensagem escrita na tampa. A mensagem da caixa 1 é "Não estão aqui". A mensagem da caixa 2 é "Estão na caixa 1". A mensagem da caixa 3 é "Não estão aqui". Sabe-se que uma das mensagem é verdadeira é as outras duas são falsas. Sem abrir as caixas, pretende-se saber em qual delas está o dinheiro. 

Modele este problema através de fórmulas proposicionais.

Resolução:  Pode usar-se o conjunto SP={(Subscript[p, 1]), (Subscript[p, 2]), (Subscript[p, 3]), (Subscript[q, 1]), (Subscript[q, 2]), (Subscript[q, 3])} de símbolos proposicionais, assumindo que (Subscript[p, 1])é uma abreviatura da afirmação "o dinheiro está na caixa 1", que (Subscript[q, 1])é uma abreviatura da afirmação "a mensagem da caixa 1 é verdadeira", e que os outros símbolos abreviam afirmação semelhantes relativas às caixas 2 e 3.

• a fórmula ((Subscript[p, 1])∧(¬ (Subscript[p, 2]))∧(¬ (Subscript[p, 3]))) ∨ ((¬ (Subscript[p, 1]))∧ (Subscript[p, 2]) ∧ (¬ (Subscript[p, 3]))) ∨ ((¬ (Subscript[p, 1]))∧ (¬ (Subscript[p, 2])) ∧ (Subscript[p, 3]))
adiante designada por ψ,  permite modelar o facto de uma das caixas ter dentro o dinheiro e as outras estarem vazias

• a fórmula ((Subscript[q, 1])∧(¬ (Subscript[q, 2]))∧(¬ (Subscript[q, 3]))) ∨ ((¬ (Subscript[q, 1]))∧ (Subscript[q, 2]) ∧ (¬ (Subscript[q, 3]))) ∨ ((¬ (Subscript[q, 1]))∧ (¬ (Subscript[q, 2])) ∧ (Subscript[q, 3]))
adiante designada por ψ',  permite modelar o facto de uma das mensagens ser verdadeira e as outras serem falsas

• a fórmula ((Subscript[q, 1])->(¬ (Subscript[p, 1]))) ∧  ((¬ (Subscript[p, 1]))-> (Subscript[q, 1]))
adiante designada por φ\(TraditionalForm\`\_1\), permite modelar o facto de a mensagens escrita na caixa 1 ser verdadeira se e só se a caixa 1 não tem o dinheiro

• a fórmula ((Subscript[q, 2])-> (Subscript[p, 2])) ∧  ((Subscript[p, 2])-> (Subscript[q, 1]))
adiante designada por φ\(TraditionalForm\`\_2\), permite modelar o facto de a mensagens escrita na caixa 2 ser verdadeira se e só se a caixa 2 tem o dinheiro

• a fórmula ((Subscript[q, 3])->(¬ (Subscript[p, 3]))) ∧  ((¬ (Subscript[p, 3]))-> (Subscript[q, 3]))
adiante designada por φ\(TraditionalForm\`\_3\), permite modelar o facto de a mensagens escrita na caixa 3 ser verdadeira se e só se a caixa 3 não tem o dinheiro.

Seguem-se alguns conceitos técnicos sobre a sintaxe das fórmulas que serão usados mais adiante.

Definição: Cada subsequência de uma fórmula φ que seja ela própria uma fórmula diz-se subfórmula de φ.

EXEMPLO

As subfórmulas de ∀x((Prim((Subscript[x, 1]))∧ >((Subscript[x, 1]),2))->Imp((Subscript[x, 1]))) são

 • Prim((Subscript[x, 1]))
 •  >((Subscript[x, 1]),2)
 • (Prim((Subscript[x, 1]))∧ >((Subscript[x, 1]),2)
 • Imp((Subscript[x, 1]))
 • (Prim((Subscript[x, 1]))∧ >((Subscript[x, 1]),2))->Imp((Subscript[x, 1]))
 • ∀(Subscript[x, 1])((Prim((Subscript[x, 1]))∧ >((Subscript[x, 1]),2))->Imp((Subscript[x, 1])))

Definição: Uma ocorrência da variável (Subscript[x, i]) numa fórmula φ está no alcance de uma quantificação ∀ (Subscript[x, j]) se essa ocorrência está numa subfórmula de φ do tipo ∀ (Subscript[x, j]) ψ. Uma ocorrência da variável (Subscript[x, i]) numa fórmula φ está no alcance de uma quantificação ∃ (Subscript[x, j]) se essa ocorrência está numa subfórmula de φ do tipo ∃ (Subscript[x, j]) ψ. 

Uma ocorrência da variável (Subscript[x, i]) numa fórmula φ é uma ocorrência muda se está no alcance de uma quantificação ∀(Subscript[x, i]) ou ∃(Subscript[x, i]) . Uma ocorrência da variável (Subscript[x, i]) numa fórmula φ que não é muda diz-se ocorrência livre.

A fórmula φ diz-se fechada se nenhuma variável tem ocorrências livres em φ. Caso contrário diz-se fórmula aberta.

Note-se que uma dada variável pode ocorrer várias vezes numa fórmula ou num termo. Na fórmula  
∀(Subscript[x, 1])((Prim((Subscript[x, 1]))∧ >((Subscript[x, 1]),2))->Imp((Subscript[x, 1]))), por exemplo, existem quatro ocorrências da variável (Subscript[x, 1]).

Observe-se ainda que numa mesma fórmula podem existir ocorrências mudas e ocorrências livres de uma dada variável.

EXEMPLO

Na fórmula Prim((Subscript[x, 2])) ∧ (∀(Subscript[x, 1])(Par((Subscript[x, 1]))->(¬Imp((Subscript[x, 1]))))) 
 • todas as ocorrências da variável (Subscript[x, 1]) estão no alcance de uma quantificação ∀(Subscript[x, 1])
 • a variável (Subscript[x, 2]) não está no alcance de uma quantificação
 • todas as ocorrências da variável (Subscript[x, 1]) são mudas
 • a ocorrência de (Subscript[x, 2]) é livre
 
Na fórmula Prim((Subscript[x, 1])) ∧ (∀(Subscript[x, 1])(Par((Subscript[x, 1]))->(¬Imp((Subscript[x, 1]))))) 
 • existem três ocorrências mudas de (Subscript[x, 1]) e uma ocorrência livre de (Subscript[x, 1.]) 
 
 As fórmulas 
 • Prim((Subscript[x, 2])) ∧ (∀(Subscript[x, 1])(Par((Subscript[x, 1]))->(¬Imp((Subscript[x, 1]))))) 
 • Prim((Subscript[x, 1])) ∧ (∀(Subscript[x, 1])(Par((Subscript[x, 1]))->(¬Imp((Subscript[x, 1])))))  
são abertas.
 
A fórmula ∀(Subscript[x, 1])(Par((Subscript[x, 1]))->(¬Imp((Subscript[x, 1])))) é fechada.

As ocorrências de variáveis em termos podem ser substituídas por outros termos. As ocorrências livres de variáveis em fórmulas podem ser substituídas por termos.

Definição O termo que se obtém por substituição da variável x pelo termo t' no termo t denota-se por (Subscript[((t)), t']^x) e define-se indutivamente como se segue:

 • (Subscript[((f((Subscript[t, 1]), …,  (Subscript[t, n])))), t']^x) = 
        f((Subscript[(((Subscript[t, 1]))), t']^x), …, (Subscript[(((Subscript[t, n]))), t']^x)) se (Subscript[t, 1]), …, (Subscript[t, n]) e f ∈ (Subscript[F, n]).

A fórmula que se obtém por substituição da variável x pelo termo t na fórmula φ denota-se por (Subscript[((φ)), t]^x) e define-se indutivamente como se segue.

 • (Subscript[(p((Subscript[t, 1]), …,  (Subscript[t, n]))), t]^x) = 
        p((Subscript[(((Subscript[t, 1]))), t]^x), …, (Subscript[(((Subscript[t, n]))), t]^x)) se (Subscript[t, 1]), …, (Subscript[t, n]) ∈ Term e p ∈ (Subscript[P, n])
 • \(TraditionalForm\`\((∀ x\ φ)\)\_t\%x\  = ∀ x\ φ\)
 • \(TraditionalForm\`\((∀ v\ φ)\)\_t\%x\  = ∀ v\ \((φ)\)\_t\%x\) se v ∈ X∖{x}
 • \(TraditionalForm\`\((∃ x\ φ)\)\_t\%x\  = ∃ x\ φ\)
 • \(TraditionalForm\`\((∃ v\ φ)\)\_t\%x\  = ∃ v\ \((φ)\)\_t\%x\) se v ∈ X∖{x}
 • \(TraditionalForm\`\((¬ φ)\)\_t\%x\  = ¬ \((φ)\)\_t\%x\)
 • \(TraditionalForm\`\((φ'⋀φ'')\)\_t\%x\  = \((φ')\)\_t\%x⋀\((φ'')\)\_t\%x\) 
 • \(TraditionalForm\`\((φ'⋁φ'')\)\_t\%x\  = \((φ')\)\_t\%x⋁\((φ'')\)\_t\%x\)
 • \(TraditionalForm\`\((φ' → φ'')\)\_t\%x\  = \((φ')\)\_t\%x → \((φ'')\)\_t\%x\)

Note-se que ao substituir uma variável x por um termo numa fórmula, só nas ocorrências livres de x são efectivamente realizadas as substituições. Deste modo, se uma variável só ocorre muda numa fórmula, a sua substituição por um qualquer termo não modifica a fórmula de partida.

EXEMPLO

Substituição em termos
 • abs((Subscript[x, 2]))\(TraditionalForm\`\_\(-1\)\%\(x\_2\)\) = abs(-1)
 • abs((Subscript[x, 2]))\(TraditionalForm\`\_\(x\_1\)\%\(x\_2\)\) = abs((Subscript[x, 1]))
 • +((Subscript[x, 1]),(Subscript[x, 2]))\(TraditionalForm\`\_\(-1\)\%\(x\_2\)\) =  +((Subscript[x, 1]),-1)

Substituição em fórmulas
Na fórmula Prim((Subscript[x, 1])) ∧ (∀(Subscript[x, 1])(Par((Subscript[x, 1]))->(¬Imp((Subscript[x, 1]))))) 
 • existem três ocorrências mudas de (Subscript[x, 1]) e uma ocorrência livre de (Subscript[x, 1.]) 
 
 As fórmulas 
 • Prim((Subscript[x, 2])) ∧ (∀(Subscript[x, 1])(Par((Subscript[x, 1]))->(¬Imp((Subscript[x, 1]))))) 
 • Prim((Subscript[x, 1])) ∧ (∀(Subscript[x, 1])(Par((Subscript[x, 1]))->(¬Imp((Subscript[x, 1])))))  
são abertas.
 
A fórmula ∀(Subscript[x, 1])(Par((Subscript[x, 1]))->(¬Imp((Subscript[x, 1])))) é fechada.

Existem situações em que não é desejável que certas ocorrências livre de variáveis sejam substituídas por determinados termos pois tal pode alterar de modo não desejado a interpretação da fórmula. Por exemplo quando se substitui (Subscript[x, 1]) por s((Subscript[x, 2])) na fórmula ∃ (Subscript[x, 2]) p((Subscript[x, 2]), (Subscript[x, 1])) obtém-se a fórmula ∃ (Subscript[x, 2]) p((Subscript[x, 2]), s((Subscript[x, 2]))). Se se interpretar p como um predicado que exprima a usual relação "maior que" no conjunto dos números naturais, a fórmula ∃ (Subscript[x, 2]) p((Subscript[x, 2]), (Subscript[x, 1])) exprime que existe um natural maior que o representado por (Subscript[x, 1]). Se se interpretar s como a função que a cada natural faz corresponder o seu sucessor, ∃ (Subscript[x, 2]) p((Subscript[x, 2]), s((Subscript[x, 2]))) exprime que existe um natural que é maior que o seu sucessor (o que não é verificado no conjunto dos naturais).

Situações indesejadas na substituição como a que se acabou de descrever estão relacionadas com o facto de numa fórmula φ, uma ocorrência livre da variável x estar no alcance de uma quantificação sobre uma variável que ocorre no termo t que vai substituir x. No caso do exemplo acima, existe uma ocorrência livre de \(TraditionalForm\`\(\(x\_1\)\(\ \)\(na\)\(\ \)\(fórmula\)\(\ \)\)\)∃ (Subscript[x, 2]) p((Subscript[x, 2]), (Subscript[x, 1])) que está no alcance da quantificação ∃ (Subscript[x, 2]) e no termo que vai substituir (Subscript[x, 1]),o termo s((Subscript[x, 2])), ocorre a variável (Subscript[x, 2]). Assim em muitas situações só se permitem substituições quando tal problema não ocorre, caso em que se diz que o termo t é livre para x em φ.

Definição O termo t é livre para x em φ se nenhuma ocorrência livre de x em φ está no alcance de uma quantificação ∀y ou ∃y em que y é uma variável que ocorre em t.

EXEMPLO

Tem-se que:

 • s((Subscript[x, 2])) não é livre para (Subscript[x, 1]) em ∃ (Subscript[x, 2]) p((Subscript[x, 2]), (Subscript[x, 1]))
 • s((Subscript[x, 1])) e  s((Subscript[x, 3])) são livres para (Subscript[x, 1]) em  ∃ (Subscript[x, 2]) p((Subscript[x, 2]), (Subscript[x, 1]))
 • s((Subscript[x, 1])), s((Subscript[x, 2])) e s((Subscript[x, 3])) são livres para (Subscript[x, 2]) em  ∃ (Subscript[x, 2]) p((Subscript[x, 2]), (Subscript[x, 1]))

De agora em diante usa-se a notação
						(Subscript[([φ]), t]^x)
para representar a fórmula que resulta de substituir a variável x pelo termo t em φ com t livre para x em φ.

Semântica

Tratam-se agora os aspectos semânticos da lógica de primeira ordem. Ao considerar uma estrutura semântiva, juntamente com uma atribuição de valores às variáveis, associa-se um significado aos símbolos de função e de predicado da assinatura, bem assim como um valor a cada uma das variáveis. Pode calcular-se então o indivíduo denotado por cada termo e determinar se uma fórmula é verdadeira ou falsa (nessa estrutura).

Estuda-se em primeiro lugar o caso mais simples correspondente ao fragmento proposicional e depois trata-se do caso mais geral.

De agora em diante assume-se fixada uma assinatura de primeira ordem  <F, P, τ, X> e designa-se por SP o seu conjunto de símbolos de predicado de aridade 0.

Fragmento proposicional

Recorde-se que o fragmento proposicional de uma linguagem de primeira ordem inclui apenas fórmulas construídas à custa de símbolos proposicionais (símbolos de predicado de aridado 0) e dos conectivos ¬, ∧, ∨ e ->.

O objectivo da semântica consiste em atribuir um significado às expressões que fazem parte da linguagem. No caso da semântica do fragmento proposicional, é suficiente atribuir um valor de verdade aos símbolos proposicionais da lógica, uma vez que qualquer fórmula nessa linguagem se obtém através destes usando conectivos lógicos cuja interpretação é fixa.

Definição Uma valoração ou estrutura de interpretação para o fragmento proposicional baseado no conjunto de símbolos proposicionais SP é uma função total
						V : SP → {0, 1}.
						
A extensão a FProp de uma valoração V é a função total
						(Subscript[V, F]) : FProp → {0, 1}
definida indutivamente da seguinte forma:

 • (Subscript[V, F])(p) = V(p) para cada p ∈ SP
 
 • (Subscript[V, F])(φ ∧ φ')={({{\(1\ \ \ \ \ \ se\ \(\(V\_F\)(φ)\)\)=1 e (Subscript[V, F])(φ')=1}, {\(0\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ caso\ contrário\)}})
 
 • (Subscript[V, F])(φ ∨ φ')={({{\(1\ \ \ \ \ \ se\ \(\(V\_F\)(φ)\) = \(1\ ou\ \(\(V\_F\)(φ')\) = 1\)\)}, {\(0\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ caso\ contrário\)}})
 
 • (Subscript[V, F])(φ → φ')={({{\(1\ \ \ \ \ \ se\ \(\(V\_F\)(φ)\) = \(0\ ou\ \(\(V\_F\)(φ')\) = 1\)\)}, {\(0\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ caso\ contrário\)}})
 
 • (Subscript[V, F])(¬ φ)={({{1       se (Subscript[V, F])(φ) = 0}, {0     caso contrário}})

Para simplificar a notação é usual escrever apenas V(φ) em vez de (Subscript[V, F])(φ).

Sendo já possível considerar o valor lógico de uma fórmula proposicional pode-se então definir satisfação de fórmula por valoração.

Definição Uma valoração V satisfaz uma fórmula φ, o que se denota por
						V ⊨ φ
se V(φ) = 1.
Usa-se V / ⊨φ como abreviatura de V não satisfaz φ, isto é, V(φ) = 0. 

Uma estrutura de interpretação V satisfaz um conjunto de fórmulas Φ, o que se denota por
		 				V ⊨ Φ
se V ⊨  φ para toda a fórmula φ ∈ Φ. 
Usa-se V / ⊨Φ como abreviatura de V não satisfaz Φ, isto é, V(φ) = 0 para alguma fórmula φ ∈ Φ.

EXEMPLO

Seja SP= {(Subscript[p, 1]), (Subscript[p, 2]), (Subscript[p, 3,]) (Subscript[q, 1]), (Subscript[q, 2]), 
        (Subscript[q, 3])} e V uma valoração baseada em SP tal que
	 V((Subscript[p, 1])) = 1, V((Subscript[p, 2]))=V((Subscript[p, 3])) = 0 e V((Subscript[q, 1])) = V((Subscript[q, 2])) = V((Subscript[q, 3])) = 1. 
	
Tem-se que
 • V ⊨  (Subscript[p, 1]) pois V((Subscript[p, 1])) = 1
 • V / ⊨(Subscript[p, 2]) pois V((Subscript[p, 2])) = 0 
 • V ⊨  
        (Subscript[p, 2]) ∨ ((Subscript[p, 1]) ∧ (Subscript[q, 1])) pois V((Subscript[p, 1])) = 1 e V((Subscript[q, 1])) = 1, logo V((Subscript[p, 1]) ∧ (Subscript[q, 1])) = 1
 • V ⊨  
        (Subscript[q, 2]) ∧ ((Subscript[p, 1]) ∨ (Subscript[p, 3])) pois V((Subscript[q, 2]))=1  e , como V((Subscript[p, 1])) = 1,  V((Subscript[p, 1]) ∨ (Subscript[p, 3])) = 1
 • V / ⊨ (Subscript[p, 1]) → (Subscript[p, 2]) pois V((Subscript[p, 1])) = 1 e V((Subscript[p, 2])) = 0 
 • V ⊨  (Subscript[p, 1]) → (Subscript[q, 2]) pois V((Subscript[q, 2])) = 1
 • V ⊨  
        (Subscript[p, 2]) → ((Subscript[q, 2]) ∧ (Subscript[p, 3])) pois V((Subscript[p, 2])) = 0

É importante caracterizar uma fórmula proposicional em termos de ser verdadeira ou não face não só a uma valoração mas face a alguma ou a todas as estruturas de interpretação de um conjunto de valorações.

Definição Uma fórmula proposicional diz-se
 • possível se existe uma valoração que a satisfaz;
 • contraditória (ou impossível) se nenhuma valoração a satisfaz;
 • válida, o que se denota por ⊨φ, se todas as valorações a satisfazem.

As fórmulas proposicionais válidas são também designadas por tautologias. Algumas destas noções podem ser estendidas a conjuntos de fórmulas.

Definição Um conjunto de fórmulas proposicionais diz-se
 • possível se existe uma valoração que satisfaz todas as fórmulas do conjunto;
 • contraditório (ou impossível) se para cada valoração existe sempre uma fórmula no conjunto que não é satisfeita.

Pode-se agora definir a noção fundamental de consequência semântica. É a noção de consequência semântica que define raciocínio válido.

Definição Uma fórmula φ é consequência semântica de um conjunto de fórmulas Φ, s, o que se denota por

					Φ ⊨ φ

se para cada valoração V se tem que  V ⊨ φ sempre que V ⊨ Φ.

Sendo SP= {(Subscript[p, 1]), (Subscript[p, 2]), (Subscript[p, 3,]) (Subscript[q, 1]), (Subscript[q, 2]), 
        (Subscript[q, 3,])}

 • fórmulas possíveis
 	- (Subscript[p, 1])
 	- (Subscript[p, 1])⋀(Subscript[p, 2])
 	- (Subscript[p, 3])⋁((Subscript[p, 1])⋀(Subscript[p, 2]))
 • fórmulas contraditórias
 	- (Subscript[p, 1])⋀(¬ (Subscript[p, 1]))
 	- ((Subscript[p, 3]) → 
            (Subscript[q, 2]))⋀((Subscript[p, 3])⋀(¬ (Subscript[q, 2])))
 • fórmulas válidas, ou tautologias
 	- (Subscript[p, 1])⋁(¬ (Subscript[p, 1]))
 	- ((Subscript[p, 1])⋀(Subscript[p, 2])) → (Subscript[p, 2])
 • consequência semântica
 	- {(Subscript[p, 1]) → (Subscript[p, 2]), (Subscript[p, 2]) → (Subscript[p, 3]),  
          (Subscript[p, 1])} ⊨ (Subscript[p, 3])

Decidibilidade do problema da satisfação

A proposição seguinte mostra que para determinar se uma fórmula proposicional é ou não satisfeita por uma dada valoração V, basta saber qual o valor que V atribui aos símbolos proposicionais presentes em φ.

Proposição:
Seja φ uma fórmula proposicional e V e V' duas valorações. Se para cada símbolo proposicional p que ocorre em φ se tem que V(p) = V' (p) então 

						V ⊨ φ se e só se V' ⊨ φ.

Uma consequência deste resultado é que, para determinar se uma fórmula é ou não válida, basta considerar um número finito de valorações. Mais precisamente, basta considerar (2^n) valorações, onde n é o número de símbolos proposicionais distintos que ocorrem na fórmula. Pode-se então concluir que o seguinte conjunto, correspondente ao Problema da verificação da satisfação, é decidível.

Proposição O conjunto {((Subscript[E, 1]), 
                (Subscript[E, 2])) ∈ (ℳ^2) :  
                (Subscript[E, 1]) é uma valoração, (Subscript[E, 2]) é uma fórmula e (Subscript[E, 1])⊨(Subscript[E, 2])} é decidível.

Prova (esboço)
Seja ((Subscript[E, 1]), (Subscript[E, 2])) um par de expressões Mathematica. Pela proposição acima pode-se assumir sem perda de generalidade que se (Subscript[E, 1]) for uma valoração e (Subscript[E, 2]) uma fórmula então (Subscript[E, 1]) atribui valores de verdade apenas aos símbolos proposicionais presentes na fórmula (Subscript[E, 2]). Assume-se também que uma valoração é representada como uma lista de regras de valoração da seguinte forma: se os únicos símbolos proposicionais que aparecem numa fórmula são (Subscript[p, 1]) e (Subscript[p, 2]) e a valoração atribui a (Subscript[p, 1]) o valor True e a (Subscript[p, 2]) o valor False então essa valoração será representado pela lista {(Subscript[p, 1]) -> True, (Subscript[p, 2]) -> False} (esta lista é interpretada pelo Mathematica como uma regra de reescrita). 

Assume-se ainda que uma fórmula é representada por uma string. Por exemplo, "(p∧q)->r".

A seguinte expressão calcula a função característica do conjunto dado

Function[{s1,s2},If[valoracaoPropQ[s1]=="0" || formulaPropQ[s2]=="0",
                             "0",
                              If[ReplaceAll[ToExpression[s2],ToExpression[s1]],"1","0"]]]

mostrando então que o conjunto é decidível. A expressão formulaPropQ decide se uma expressão é uma fórmula proposicional. A expressão valoracaoPropQ decide se uma expressão é uma valoração proposicional. Deixa-se como exercício ao leitor implementar estas expressões. A função do Mathematica ReplaceAll aplica uma lista de regras de reescrita a uma expressão.

Para representar valorações em Mathematica  tira-se partido da possibilidade de definir regras de reescrita em Mathematica. O leitor interessado em saber mais sobre regras de reescrita pode consultar o manual disponível no sistema.

Exercício: Mostre que
 • \(TraditionalForm\`{E ∈ \(M : 
            E\ é\ uma\ fórmula\ proposicional\ possível\)}\) é decidível (problema da satisfação - SAT).
 • \(TraditionalForm\`{E ∈ \(M : 
            E\ é\ uma\ fórmula\ proposicional\ válida\)}\) é decidível (problema da validade).
 • \(TraditionalForm\`{E ∈ \(M : 
            E\ é\ uma\ fórmula\ proposicional\ contraditória\)}\) é decidível (problema da impossibilidade).
 • {((Subscript[E, 1]), (Subscript[E, 2])) ∈ (M^2) :  
                (Subscript[E, 1]) representa um conjunto de fórmulas,(Subscript[E, 2]) é uma fórmula proposicional e (Subscript[E, 1])⊨(Subscript[E, 2])} 
 é decidível (problema da consequência semântica).

Lógica de primeira ordem

Um alfabeto de primeira ordem refere símbolos de função e de predicado, isto é, nomes de funções e de predicados. Esses símbolos ou nomes podem vir a ser interpretados de muitas formas diferentes, no sentido em que a cada um desses nomes de função se pode fazer corresponder uma certa função (total),  e a cada um desses nomes de predicado se pode fazer corresponder um certo  predicado (relação). Quando se faz corresponder a cada símbolo de função uma certa função e a cada símbolo de predicado um certo predicado está a definir-se uma estrutura de interpretação. As funções e predicados são definidos à custa de conjuntos.Cada estrutura de interpretação inclui apenas um conjunto, designado domínio ou universo de interpretação. 

A interpretação de um símbolo de função de aridade n por uma estrutura com domínio U é então uma função de (U^n)para U. A interpretação de um símbolo de predicado de aridade n é uma relação n-ária sobre esse conjunto (isto é, um subconjunto de (U^n) ou uma função de  (U^n)para {0,1}).

A interpretação de um termo nessa estrutura é um elemento desse domínio. Cada fórmula exprime uma certa afirmação sobre os elementos desse domínio e a sua interpretação é  0 ou 1. Se a interpretação é 1 tal significa que a afirmação é verdadeira e se é 0 a 
a afirmação é falsa (no contexto dessa interpretação).

Definição Uma estrutura de interpretação sobre uma assinatura de primeira ordem <F, P, τ, X> é um par
						<U, I>
onde
 • U é um conjunto não vazio, designado universo, domínio ou suporte da estrutura
 
 • I é uma função total, designada função de interpretação, que a cada símbolo em F ⋃ P associa uma função total do seguinte modo

 	- para cada símbolo de função f de aridade n, I(f) é uma função total
 				I(f) : (U^n) → U

 	- para cada símbolo de predicado p de aridade n, I(p) é uma função total
 				I(p) : (U^n) → {0, 1}.

Para cada símbolo de função f de aridade 0, ou seja, para cada símbolo de constante f, I(f) é uma aplicação que ao elemento do conjunto singular (U^0) faz corresponder um elemento u ∈ U. De modo semelhante, para cada símbolo de predicado p de aridade 0, I(p) denota um elemento de {0, 1}.

EXEMPLO

Considere-se a assinatura de primeira ordem <F, P, τ, X> em que (Subscript[F, 0]) = ℤ, (Subscript[F, 1]) = {abs}, (Subscript[F, 2]) = {+,×}, (Subscript[F, n]) = ⌀ para n > 2, (Subscript[P, 1]) = {Par,  Imp,  Prim}, (Subscript[P, 2]) = {=,>}, (Subscript[P, n]) = ⌀ para n ∉ {1, 2}, X = {(Subscript[x, 1]), (Subscript[x, 2]), …}. 

Um exemplo de estrutura de interpretação sobre esta assinatura é o par
						\(TraditionalForm\`\(\(<\)\(ℤ\)\), \(\(I\)\(>\)\)\)
com
 • I(k)=k para cada constante k
 • \(TraditionalForm\`I(
          abs) : ℤ → ℤ\) associa a cada inteiro n o seu valor absoluto
 • \(TraditionalForm\`I(+) : ℤ\^\(\(\ \)\(2\)\) → ℤ\) associa a cada par de inteiros (n,m) a sua soma m+m
 • \(TraditionalForm\`I(×) : ℤ\^\(\(\ \)\(2\)\) → ℤ\) associa a cada par de inteiros (n,m) a seu produto m×m
 • I(
          Par) : ℤ → {0, 1} a cada inteiro n associa 1 se n é par e associa 0 caso contário
 • I(
          Imp) : ℤ → {0, 1} a cada inteiro n associa 1 se n é ímpar e associa 0 caso contário
 • I(
          Prim) : ℤ → {0, 1} a cada inteiro n associa 1 se n é primo e associa 0 caso contário
 • \(TraditionalForm\`I( = ) : ℤ\^\(\(\ \)\(2\)\) → ℤ\) a cada par de inteiros (n,m)  associa 1 se n é igual a m e 0 caso comtrário
 • \(TraditionalForm\`I( > ) : ℤ\^\(\(\ \)\(2\)\) → ℤ\) a cada par de inteiros (n,m)  associa 1 se n é maior que  m e 0 caso comtrário

Observe-se que uma estrutura de interpretação não associa nenhum valor às variáveis em X. A associação de valores às variáveis é realizada através de uma atribuição.

Definição Uma atribuição sobre uma assinatura de primeira ordem <F, P, τ, X> e uma estrutura de interpretação <U, I> é uma função total
						ρ : X → U.
						
Sendo ρ : X→U uma atribuição, x∈X e u∈U,  ρ[
          x := u] : X→U é a atribuição tal que   ρ[x := u] (x) = u e  ρ[x := u] (y) = ρ(y) para cada y∈X\{x}.

Pode-se agora interpretar fórmulas e termos.

Definição: A interpretação de termos sobre uma estrutura de interpretação <U, I> e uma atribuição ρ sobre uma assinatura de primeira <F, P, τ, X> é uma função
						\(TraditionalForm\`\(\([[\)\(]]\)\)\_\(\(\(<\)\(U\)\), \(\(I\)\(>\)\)\)\%ρ\): Term -> U
definida indutivamente como se segue:

 • \(TraditionalForm\`\(\([[\)\(x\)\(]]\)\)\_\(\(\(<\)\(U\)\), \(\(I\)\(>\)\)\)\%ρ = ρ(x)\) se x ∈ X
 
 • \(TraditionalForm\`\(\([[\)\(f(t\_1, …, t\_n)\)\(]]\)\)\_\(\(\(<\)\(U\)\), \(\(I\)\(>\)\)\)\%ρ = \(I(
            f)\) \((\(\([[\)\(t\_1\)\(]]\)\)\_\(\(\(<\)\(U\)\), \(\(I\)\(>\)\)\)\%ρ, …, \(\([[\)\(t\_n\)\(]]\)\)\_\(\(\(<\)\(U\)\), \(\(I\)\(>\)\)\)\%ρ)\)\) se f é um símbolo de função de aridade n e (Subscript[t, 1]), …, (Subscript[t, n]) são termos.

Definição: A interpretação de fórmulas sobre uma estrutura de interpretação <U, I> e uma atribuição ρ sobre uma assinatura de primeira <F, P, τ, X> é uma função
						\(TraditionalForm\`\(\([[\)\(]]\)\)\_\(\(\(<\)\(U\)\), \(\(I\)\(>\)\)\)\%ρ\):Form -> {0,1}
definida indutivamente como se segue:

 • \(TraditionalForm\`\(\([[\)\(p(t\_1, …, t\_n)\)\(]]\)\)\_\(\(\(<\)\(U\)\), \(\(I\)\(>\)\)\)\%ρ = \(I(
            p)\) \((\(\([[\)\(t\_1\)\(]]\)\)\_\(\(\(<\)\(U\)\), \(\(I\)\(>\)\)\)\%ρ, …, \(\([[\)\(t\_n\)\(]]\)\)\_\(\(\(<\)\(U\)\), \(\(I\)\(>\)\)\)\%ρ)\)\) se p é um símbolo de predicado de aridade ne (Subscript[t, 1]), …, (Subscript[t, n]) são termos
 
 • \(\(\([[\)\(φ ∧ φ'\)\(]]\)\)\_\(\(\(<\)\(U\)\), \(\(I\)\(>\)\)\)\%ρ\)={({{\(1\ \ \ \ \ \ \(se\ [[φ]]\)\_\(\(\(<\)\(U\)\), \(\(I\)\(>\)\)\)\%ρ\)=1 (Subscript[e [[φ']], <U, I>]^ρ)=1}, {\(0\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ caso\ contrário\)}})
 
 • \(\(\([[\)\(φ ∨ φ'\)\(]]\)\)\_\(\(\(<\)\(U\)\), \(\(I\)\(>\)\)\)\%ρ\)={({{\(1\ \ \ \ \ \ \(se\ [[φ]]\)\_\(\(\(<\)\(U\)\), \(\(I\)\(>\)\)\)\%ρ = \(1\ \(ou\ [[φ']]\)\_\(\(\(<\)\(U\)\), \(\(I\)\(>\)\)\)\%ρ = 1\)\)}, {\(0\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ caso\ contrário\)}})
 
 • \(\(\([[\)\(φ -> φ'\)\(]]\)\)\_\(\(\(<\)\(U\)\), \(\(I\)\(>\)\)\)\%ρ\)={({{\(1\ \ \ \ \ \ \(se\ [[φ]]\)\_\(\(\(<\)\(U\)\), \(\(I\)\(>\)\)\)\%ρ = \(0\ \(ou\ [[φ']]\)\_\(\(\(<\)\(U\)\), \(\(I\)\(>\)\)\)\%ρ = 1\)\)}, {\(0\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ caso\ contrário\)}})
 
 • \(\(\([[\)\(¬ φ\)\(]]\)\)\_\(\(\(<\)\(U\)\), \(\(I\)\(>\)\)\)\%ρ\)={({{\(\(1\ \ \ \ \ \ \(se\ [[φ]]\)\_\(\(\(<\)\(U\)\), \(\(I\)\(>\)\)\)\%ρ\)\(=\)\(0\)\(\ \)\)}, {0            caso contrário}})
 
 • \(\(\([[\)\(∀ x\ φ\)\(]]\)\)\_\(\(\(<\)\(U\)\), \(\(I\)\(>\)\)\)\%ρ\)={({{\(1\ \ \ \ \ \ \(se\ [[φ]]\)\_\(\(\(<\)\(U\)\), \(\(I\)\(>\)\)\)\%\(ρ[x := u]\) = \(\(1\ para\ cada\ u\)\(∈\)\(U\)\(\ \)\)\)}, {\(0\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ caso\ contrário\)}})
 
 • \(\(\([[\)\(∃ x\ φ\)\(]]\)\)\_\(\(\(<\)\(U\)\), \(\(I\)\(>\)\)\)\%ρ\)={({{\(1\ \ \ \ \ \ \(se\ [[φ]]\)\_\(\(\(<\)\(U\)\), \(\(I\)\(>\)\)\)\%\(ρ[x := u]\) = \(\(1\ para\ algum\ u\)\(∈\)\(U\)\(\ \)\)\)}, {\(0\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ caso\ contrário\)}})

Análogamente ao fragmento proposicional uma fórmula de primeira ordem é satisfeita por uma estrutura de interpretação e uma valoração se a sua interpretação nessa estrutura e atribuição for verdadeira.

Definição Uma estrutura de interpretação <U, I> e uma atribuição ρ satisfazem uma fórmula φ, o que se denota por
						\(TraditionalForm\`\(\(<\)\(U\)\), \(\(I\)\(>\)\), ρ ⊨ φ\)
se \(TraditionalForm\`\(\([[\)\(φ\)\(]]\)\)\_\(\(\(<\)\(U\)\), \(\(I\)\(>\)\)\)\%ρ = 
        1\).

EXEMPLO

Considere-se a assinatura de primeira ordem <F, P, τ, X> em que (Subscript[F, 0]) = ℤ, (Subscript[F, 1]) = {abs}, (Subscript[F, 2]) = {+,×}, (Subscript[F, n]) = ⌀ para n > 2, (Subscript[P, 1]) = {Par,  Imp,  Prim}, (Subscript[P, 2]) = {=,>}, (Subscript[P, n]) = ⌀ para n ∉ {1, 2}, X = {(Subscript[x, 1]), (Subscript[x, 2]), …} e a estrutura de interpretação \(TraditionalForm\`\(\(<\)\(ℤ\)\), \(\(I\)\(>\)\)\) referida acima. Considere-se uma atribuição ρ tal que ρ((Subscript[x, 1]))=3. Tem-se que				
 •  \(TraditionalForm\`\(\([[\)\(Par(2)\)\(]]\)\)\_\(\(\(<\)\(U\)\), \(\(I\)\(>\)\)\)\%ρ = 
        I\)(Par)(2) = 1
  • \(TraditionalForm\`\(\([[\)\(Par(x\_1)\)\(]]\)\)\_\(\(\(<\)\(U\)\), \(\(I\)\(>\)\)\)\%ρ = I\)(Par)(\(TraditionalForm\`\(\([[\)\(ρ(x\_1)\)\(]]\)\)\_\(\(\(<\)\(U\)\), \(\(I\)\(>\)\)\)\%ρ\)) = I(Par)(3) = 1
 •  \(TraditionalForm\`\(\([[\)\(Par(x\_1) -> Imp(x + 1)\)\(]]\)\)\_\(\(\(<\)\(U\)\), \(\(I\)\(>\)\)\)\%ρ = \ 1\)

Uma vez definida a noção de satisfação pode-se definir de um modo análogo ao fragmento proposicional as noções de fórmula possível, contraditória e válida, conjunto possível e impossível, e a noção de consequência semântica.

Definição: Uma fórmula de primeira ordem φ diz-se
 • possível se existe uma estrutura de interpretação e uma atribuição que a satisfaz.
 • contraditória (ou impossível) se nenhuma estrutura de interpretação e atribuição a satisfazem.
 • válida, o que se denota por ⊨ φ, se qualquer estrutura de interpretação e atribuição sobre essa estrutura a satisfazem.

EXEMPLO

Considere-se a assinatura de primeira ordem <F, P, τ, X> em que (Subscript[F, 0]) = ℤ, (Subscript[F, 1]) = {abs}, (Subscript[F, 2]) = {+,×}, (Subscript[F, n]) = ⌀ para n > 2, (Subscript[P, 1]) = {Par,  Imp,  Prim}, (Subscript[P, 2]) = {=,>}, (Subscript[P, n]) = ⌀ para n ∉ {1, 2}, X = {(Subscript[x, 1]), (Subscript[x, 2]), …} Tem-se que				
 • \(TraditionalForm\`\(\([[\)\(Par(2)\)\(]]\)\)\_\(\(\(<\)\(U\)\), \(\(I\)\(>\)\)\)\%ρ = 
        I\)(Par)(2) = 1
 • Par((Subscript[x, 1]))]] é fórmula possível
 • \(TraditionalForm\`\(\(Par(x\_1) -> 
            Imp(x + 1)\)\(]]\)\)\ \ é\ fórmula\ possível\)

Definição: Um conjunto de fórmulas de primeira ordem diz-se
 • possível se existe uma estrutura de interpretação e uma atribuição que satisfazem todas as fórmulas do conjunto
 • contraditório (ou impossível) se para cada estrutura de interpretação e atribuição sobre essa estrutura existe sempre uma fórmula no conjunto que não é satisfeita.

Definição: Uma fórmula φ é consequência semântica de um conjunto de fórmulas Φ,  o que se denota por Φ ⊨ φ se para cada estrutura de interpretação <U, I> e atribuição ρ sobre essa estrutura, se \(TraditionalForm\`\(\(<\)\(U\)\), \(\(I\)\(>\)\), ρ ⊨ Φ\) então \(TraditionalForm\`\(\(<\)\(U\)\), \(\(I\)\(>\)\), ρ ⊨ φ\).

Sistema dedutivo

Adopta-se como sistema dedutivo para a lógica de primeira ordem o sistema dedutivo T, também designado sistema de tableaux ou sistema ou cálculo de Smullyan. Neste sistema dedutivo as derivações são árvores etiquetadas por conjuntos de fórmulas. A estas árvores dá-se o nome de tableaux. Assim vamos começar esta secção por descrever o que é uma árvore etiquetada.

Árvores etiquetadas

Informalmente, uma árvore é uma estrutura constituída por um conjunto de elementos, designados nós, ordenados de um modo particular. Quando se faz a representação gráfica desses nós seguindo a ordem referida obtém-se uma imagem que lembra uma árvore.

Definição Uma relação binária ⋄ em N é um subconjunto de N×N. Usa-se (Subscript[n, 1])⋄(Subscript[n, 2]) como abreviatura de ((Subscript[n, 1]), (Subscript[n, 2])) ∈ ⋄. Uma relação binária ⋄ em N 
 • é reflexiva se n⋄n para cada n ∈ N
 • é transitiva se quaisquer que sejam n, n' e n'' em N se n⋄n' e n'⋄n'' então n⋄n''.
 • é anti-simétrica se quaisquer que sejam n e n' em N se n⋄n' e n'⋄n então n = n'.
 • tem elemento mínimo se existe n em N tal que n⋄n' para cada n' em N.

Definição Uma árvore é um par (N, ⋄) em que
 • N é um conjunto finito, cujos elementos são designados nós
 • ⋄ é uma relação binária em N tal que
 	- ⋄ é reflexiva, transitiva, anti-simétrica, com elementos mínimo
 	- se n'⋄n e n''⋄n então n'⋄n'' ou n''⋄n', para quaisquer nós n, n' e n''.

Neste contexto, se (Subscript[n, 1])⋄(Subscript[n, 2]), diz-se que (Subscript[n, 2]) é sucessor do nó (Subscript[n, 1]), ou que (Subscript[n, 1]) é predecessor de (Subscript[n, 2]). Mais ainda, (Subscript[n, 2]) diz-se sucessor directo de (Subscript[n, 1]) se (Subscript[n, 2]) ≠ (Subscript[n, 1]) e não existe (Subscript[n, 3]) distinto de (Subscript[n, 1]) e de (Subscript[n, 2]) que seja simultaneamente sucessor de (Subscript[n, 1]) e predecessor de (Subscript[n, 2]). O elemento mínimo é designado por raiz da árvore. Os nós que não têm sucessores directos são as folhas da árvore. O conjunto dos nós que são predecessores de uma folha n, designa-se por ramo da árvore. Cada ramo inclui o nó raiz e uma única folha.

EXEMPLO

Tem-se que o par (M, ◼) em que
 • M = {(Subscript[n, 0]),  (Subscript[n, 1]),  (Subscript[n, 2]),  (Subscript[n, 3]),  (Subscript[n, 4]),  (Subscript[n, 5]),  
          (Subscript[n, 6])}
 • ◼ é o conjunto composto pelos pares:
   {(Subscript[n, i]) ◼ (Subscript[n, i]): i∈{1,2,3,4,5,6}} ⋃ {(Subscript[n, 1]) ◼ (Subscript[n, 3]), (Subscript[n, 1]) ◼ (Subscript[n, 5]), (Subscript[n, 2]) ◼ (Subscript[n, 4]), (Subscript[n, 2]) ◼ (Subscript[n, 6]), (Subscript[n, 4]) ◼ (Subscript[n, 6])}   
é uma árvore.

O nó raiz é (Subscript[n, 0]). Os sucessores directos de (Subscript[n, 0]) são (Subscript[n, 1]) e (Subscript[n, 2]). As folhas são (Subscript[n, 3]), (Subscript[n, 5]) e (Subscript[n, 6]). Existem assim 3 ramos. O ramo associado à folha (Subscript[n, 3]), constituido pelo conjunto {(Subscript[n, 0]), (Subscript[n, 1]), (Subscript[n, 3])}, o ramo associado à folha (Subscript[n, 5]), constituido pelo conjunto {(Subscript[n, 0]), (Subscript[n, 1]), (Subscript[n, 5])} e o ramo associado à folha (Subscript[n, 6]), constituido pelo conjunto  {(Subscript[n, 0]), (Subscript[n, 2]), (Subscript[n, 4]), (Subscript[n, 6])}. 

Representando graficamente esta árvore, dispondo os nós de modo a respeitarem a ordenação induzida por ◼, com a raiz em baixo e as folhas no topo, e com uma linha horizontal separando cada nó dos seus sucessores directos, obtém-se o seguinte diagrama.

						(Subscript[n, 6])
										--
					(Subscript[n, 3])		(Subscript[n, 5])			(Subscript[n, 4])
					---------------------			--
						(Subscript[n, 1])				(Subscript[n, 2])
						-----------------------------------------
								(Subscript[n, 0])
								
Ou adoptando a representação em que a raiz se encontra no topo:	

								(Subscript[n, 0])
						---------------------------------------
						(Subscript[n, 1])				(Subscript[n, 2])
					---------------------			--
					(Subscript[n, 3])		(Subscript[n, 5])			(Subscript[n, 4])
										--
										(Subscript[n, 6])

É muitas vezes relevante associar informação aos nós de uma árvore o que pode ser conseguido através de uma função cujo domínio é o conjunto dos nós da árvore.

Definição Uma árvore etiquetada é um triplo (N, ⋄,etq) em que (N, ⋄) é uma árvore e etq : N → E é uma função. O conjunto E é o conjunto de etiquetas.

EXEMPLO

Considere-se a linguagem FProp baseada em SP= {(Subscript[p, 1]), (Subscript[p, 2]), (Subscript[p, 3,]) (Subscript[q, 1]), (Subscript[q, 2]), 
        (Subscript[q, 3,])}, a árvore (M, ◼) referida no exemplo anterior e a função f : M → ℘ Form tal que
 •f(
          (Subscript[n, 0])) = {((Subscript[p, 1]) -> 
                (Subscript[p, 2])) ∨ ((Subscript[p, 3]) ∧ (¬ ((Subscript[q, 1]) -> 
                        (Subscript[q, 2]))))}
 •f((Subscript[n, 1])) = {(Subscript[p, 1]) -> (Subscript[p, 2])}
 •f(
          (Subscript[n, 2])) = {(Subscript[p, 3]) ∧ (¬ ((Subscript[q, 1]) -> (Subscript[q, 2])))}
 •f((Subscript[n, 3])) = {¬ (Subscript[p, 1])}
 •f(
          (Subscript[n, 4])) = {(Subscript[p, 3,])(¬ ((Subscript[q, 1]) -> 
                  (Subscript[q, 2])))}
 •f((Subscript[n, 5])) = {(Subscript[p, 2])} 
 •f((Subscript[n, 6])) = {(Subscript[q, 1]), ¬ (Subscript[q, 2])}.
Tem-se então que a tuplo (N, ◼, f) constitui uma árvore etiquetada. O conjunto das etiquetas é neste caso a conjunto formado pelos conjuntos de fórmulas em FProp. Representando graficamente esta árvore obtém-se:

					{((Subscript[p, 1]) -> 
              (Subscript[p, 2])) ∨ ((Subscript[p, 3]) ∧ (¬ ((Subscript[q, 1]) -> 
                      (Subscript[q, 2]))))}
					-------------------------------------------
				       {(Subscript[p, 1]) -> (Subscript[p, 2])}			{(Subscript[p, 3]) ∧ (¬ ((Subscript[q, 1]) -> 
                  (Subscript[q, 2])))}
				---------------------		-------------------------
				¬ (Subscript[p, 1])		(Subscript[p, 2])		{(Subscript[p, 3,]) (¬ ((Subscript[q, 1]) -> 
                  (Subscript[q, 2])))}
								------------------------
								       {(Subscript[q, 1]), ¬ (Subscript[q, 2])}

O conjunto das etiquetas é neste caso a conjunto formado pelos conjuntos de fórmulas sobre uma certa assinatura.

Fragmento proposicional - sistema dedutivo (Subscript[T, p])

Antes de apresentar o sistema dedutivo T na sua generalidade, começa-se por estudar o seu fragmento proposicional. Este fragmento proposicional é aqui designado (Subscript[T, p]). Recorde-se que as derivações de T em são árvores etiquetadas por conjuntos de fórmulas, os tableaux.  No caso de (Subscript[T, p]) as fórmulas envolvidas são fórmulas proposicionais. 

Uma derivação inicia-se a partir de um tableau singular (uma árvore com um único nó) e prossegue por aplicação sucessiva de regras de inferência do sistema. Dado um tableau, se o conjunto de fórmulas Φ é a etiqueta do nó raiz do tableau, diz-se que este é um tableau para Φ. Cada ramo de um tableau t pode ser visto como correspondendo a uma tentativa de construir uma valoração que satisfaça o conjunto Φ associado à raiz de t. Em certos casos essas tentativas falham porque a valoração deveria satisfazer simultaneamente uma dada fórmula e a sua negação. Quando todas as tentativas falham prova-se que não existe nenhum valoração que satisfaça Φ.

No sistema (Subscript[T, p]) existem sete regras de inferência, duas regras por cada conectivo, com a excepção do conectivo ¬ :

 • regra ⋀
 • regra ¬ ⋀
 • regra ⋁
 • regra ¬ ⋁
 • regra  → 
 • regra ¬  → 
 • regra ¬ ¬ 

A aplicação de uma regra a um tableau t vai dar origem a um novo tableau. Este novo tableau é obtido a partir de t acrescentando um ou dois nós sucessores directos a alguma folha de t, de acordo com a regra em causa. A etiqueta de cada um desses novos nós é um conjunto de fórmulas que depende da regra em causa. Quando se aplica a regra ¬ ⋀, a regra ⋁ ou a regra  →  são acrescentados dois nós sucessores a uma folha de t. Por isso estas regras são designadas por regras binárias. No caso da aplicação de cada uma das outras regras é acrescentado apenas um nó sucessor. Essas outras regras são assim designadas regras unárias.

Uma dada regra só pode ser aplicada a um tableau t se na etiqueta de algum nó de t existir uma fórmula com a sintaxe adequada. Por exemplo, para aplicar a regra ⋀ a t tem de existir em algum nó de t uma fórmula do tipo φ⋀ψ e para aplicar a regra ¬ ⋀ tem de existir uma fórmula do tipo ¬ (φ⋀ψ). Escolhidas a fórmula com a sintaxe adequada, o nó a que pertence, e um ramo r contendo esse nó, acrescenta-se então apenas à folha desse ramo o(s) novo(s) nó(s). Pode também dizer-se que o novo tableau é obtido a partir de t por aplicação da regra de inferência à formula em causa, relativamente ao ramo r.

Apresentam-se agora as regras de inferência do sistema dedutivo (Subscript[T, p]). Na representação usada a fórmula acima da linha horizontal estabelece a sintaxe da fórmula que deve estar presente na etiqueta de algum nó do tableau para se poder aplicar a regra.  As fórmulas abaixo representam as fórmulas que vão estar presentes nas etiquetas do(s) novo(s) nó(s) acrescentado(s) por aplicação da regra. O símbolo | ocorre nas regras binárias, caso em que são acrescentados a uma folha dois nós sucessores directos. A fórmula à esquerda do símbolo | constitui a etiqueta de um dos nós e a fórmula à direita a do outro. Se estão presentes duas fórmulas separadas por uma vírgula, a etiqueta do novo nó é constituída por essas duas fórmulas. A designação da regra está presente à direita da linha horizontal.

Definição As regras de inferência do sistema (Subscript[T, p]) são as seguintes:

 φ⋀ψ		 ¬ (φ⋀ψ)		  φ⋁ψ		¬ (φ⋁ψ)
-------- ⋀	-------------- ¬ ⋀	---------	⋁	------------- ¬ ⋁
 φ, ψ		 ¬ φ | ¬ ψ		  φ | ψ		 ¬ φ , ¬ ψ


  φ → ψ	 ¬ (φ → ψ)		  ¬ ¬ φ	
-----------  → 	-------------- ¬  → 	---------- ¬ ¬ 
 ¬ φ | ψ	    φ , ¬ ψ		     φ

Para simplificar a notação é usual omitir as chavetas dos conjuntos que etiquetam os nós dos tableaux. Ao construir um tableau é também usual incluir a designação das regras que são aplicadas na sua construção.

EXEMPLO

Considere-se o conjunto \(TraditionalForm\`Φ = {ψ\_1⋀ψ\_2, ¬ \((¬ \((ψ\_1⋀ψ\_2)\) → ψ\_3)\)}\). Comece-se por considerar o tableau singular para Φ, isto é, a árvore com um único nó cuja etiqueta é este conjunto:

				\(TraditionalForm\`ψ\_1⋀ψ\_2, ¬ \((¬ \((ψ\_1⋀ψ\_2)\) → ψ\_3)\)\)
				
Tendo em conta a fórmulas do conjunto podem aplicar-se duas regras a este tableau: a regra ¬  →  à fórmula \(TraditionalForm\`¬ \((ψ\_1⋀ψ\_2)\) → ψ\_3\) e a regra ⋀ à fórmula (Subscript[ψ, 1])⋀(Subscript[ψ, 2]). Aplicando a regra ⋀ obtém-se o tableau seguinte:

				\(TraditionalForm\`ψ\_1⋀ψ\_2, ¬ \((¬ \((ψ\_1⋀ψ\_2)\) → ψ\_3)\)\)
				-------------------------------------  ⋀
				           	(Subscript[ψ, 1]), (Subscript[ψ, 2])

A este novo tableau pode-se continuar a aplicar a regra ¬  →  à fórmula \(TraditionalForm\`¬ \((ψ\_1⋀ψ\_2)\) → ψ\_3\). Aplicando esta regra obtém-se:

				\(TraditionalForm\`ψ\_1⋀ψ\_2, ¬ \((¬ \((ψ\_1⋀ψ\_2)\) → ψ\_3)\)\)
				---------------------------------------- ⋀
					      (Subscript[ψ, 1]), (Subscript[ψ, 2])
				 	--------------- ¬  → 
				         ¬ ((Subscript[ψ, 1])⋀(Subscript[ψ, 2])), ¬ (Subscript[ψ, 3])
				         

Aplica-se agora a regra ¬ ⋀ à fórmula ¬ ((Subscript[ψ, 1])⋀(Subscript[ψ, 2])) obtendo-se:

				\(TraditionalForm\`ψ\_1⋀ψ\_2, ¬ \((¬ \((ψ\_1⋀ψ\_2)\) → ψ\_3)\)\)
				---------------------------------------- ⋀
					      (Subscript[ψ, 1]), (Subscript[ψ, 2])
				 	--------------- ¬  → 
				         ¬ ((Subscript[ψ, 1])⋀(Subscript[ψ, 2])), ¬ (Subscript[ψ, 3])
				----------------------------------------- ¬ ⋀
				   ¬ (Subscript[ψ, 1])			¬ (Subscript[ψ, 2])

Foram acrescentados dois nós, ambos sucessores directos da folha do tableau anterior. O tableau obtido tem assim dois ramos. Recorde-se que todos os tableaux obtidos até agora são tableaux para o conjunto Φ, pois a etiqueta da raiz de cada um destes tableaux é Φ. Por vezes, para além de se indicar a regra usada, pode ser relevante indicar explicitamente qual é o nó e a fórmula que permitiram a aplicação dessa regra. No caso que tem vindo a ser ilustrado neste exemplo ter-se-á:

				\(TraditionalForm\`ψ\_1⋀ψ\_2\^\((1)\), ¬ \((¬ \((ψ\_1⋀ψ\_2)\) → ψ\_3)\)\^\((2)\)\)
				---------------------------------------- ⋀,(1)
					      (Subscript[ψ, 1]), (Subscript[ψ, 2])
				 	--------------- ¬  → ,(2)
				         \(TraditionalForm\`¬ \((ψ\_1⋀ψ\_2)\)\^\((3)\)\), ¬ (Subscript[ψ, 3])
				----------------------------------------- ¬ ⋀,(3)
				   ¬ (Subscript[ψ, 1])			¬ (Subscript[ψ, 2])

Apresentam-se de seguida mais alguns exemplos de tableaux:

EXEMPLOS

O tableau 

				\(TraditionalForm\`\((ψ\_1 ∨ ψ\_2)\) -> ψ\_3\^\((1)\), ψ\_1 ∧ ψ\_2\^\((2)\)\), ¬ (Subscript[ψ, 3])
				-----------------------------------------  ∧ , (2)
				         		(Subscript[ψ, 1]), (Subscript[ψ, 2])
				   -----------------------------------------  -> , (1)
				 ((¬ ((Subscript[ψ, 1]) ∨ (Subscript[ψ, 2])))^((3)))			 (Subscript[ψ, 3])
				------------------ ¬  ∨ , (3)
 				  ¬(Subscript[ψ, 1]), ¬ (Subscript[ψ, 2])
 
é um tableau para \(TraditionalForm\`{\((ψ\_1 ∨ ψ\_2)\) -> ψ\_3, ψ\_1 ∧ ψ\_2, \ ¬ ψ\_3}\).

O tableau 

				\(TraditionalForm\`¬ \((ψ\_1 → \((¬ ψ\_2)\))\)\^\((1)\), ψ\_1⋁\((¬ ψ\_2)\)\^\((3)\)\)
				----------------------------------------- ¬  → , (1)
				         (Subscript[ψ, 1]), ¬ (((¬ (Subscript[ψ, 2])))^((2)))
				       --------------------- ¬ ¬ , (2)
					      (Subscript[ψ, 2])
				------------------------------------ ⋁, (3)
				   (Subscript[ψ, 1])			¬ (Subscript[ψ, 2])

é um tableau para \(TraditionalForm\`{¬ \((ψ\_1 → \((¬ ψ\_2)\))\), ψ\_1⋁\((¬ ψ\_2)\)}\).

O tableau 
	  			\(TraditionalForm\`¬ \((\((ψ\_1 → \((ψ\_2 → ψ\_3)\))\) → \((\((ψ\_1 → ψ\_2)\) → \((ψ\_1 → ψ\_3)\))\))\)\^\((1)\)\)
				---------------------------------------------------------------- ¬  → , (1)
				              \(TraditionalForm\`ψ\_1 → \((ψ\_2 → ψ\_3)\)\^\((2)\)\),
				         \(TraditionalForm\`¬ \((\((ψ\_1 → ψ\_2)\) → \((ψ\_1 → ψ\_3)\))\)\^\((3)\)\)
				       -------------------------------------- ¬  → , (3)
					       (Subscript[ψ, 1]) → ((Subscript[ψ, 2])^((4))),
					      \(TraditionalForm\`¬ \((ψ\_1 → ψ\_3)\)\^\((5)\)\)
					    --------------------- ¬  → , (5)
					    	(Subscript[ψ, 1]),¬ (Subscript[ψ, 3])
					------------------------------------------  → , (2)
				 	  ¬ (Subscript[ψ, 1])			(Subscript[ψ, 2]) → ((Subscript[ψ, 3])^((6)))
							--------------------------------  → , (4)
						 	  ¬ (Subscript[ψ, 1])			(Subscript[ψ, 2])
										--------------------------------  → , (6)
								 	  ¬ (Subscript[ψ, 2])			(Subscript[ψ, 3])
 é um tableaux para o conjunto constituído pela fórmula \(TraditionalForm\`¬ \((\((ψ\_1 → \((ψ\_2 → ψ\_3)\))\) → \((\((ψ\_1 → ψ\_2)\) → \((ψ\_1 → ψ\_3)\))\))\)\).

Como referido, cada ramo de um tableau t pode ser visto como correspondendo a uma tentativa de construir uma interpretação que satisfaça o conjunto Φ associado à raiz de t. Em certos casos essas tentativas falham porque a interpretação deveria satisfazer simultaneamente uma dada fórmula e a sua negação. Quando todas as tentativas falham prova-se que não existe nenhum interpretação que satisfaça Φ.

O sistema dedutivo (Subscript[T, p]) é um sistema de refutação. Como se provará adiante (ver secção Correcção do sistema (Subscript[T, p])), para determinar se uma fórmula φ é válida, pode considerar-se um tableau para Φ = {¬ φ}. Cada ramo de t corresponde então a uma tentativa de encontrar uma valoação que satisfaça ¬ φ, ou seja, corresponde a uma tentativa de refutar a asserção representada por φ. Se todas as tentativas falham não existe uma tal interpretação e portanto φ é válida.

No caso de um tableau para \(TraditionalForm\`Φ = {φ\_1, …, φ\_n, ¬ φ}\), cada ramo pode ser visto como correspondendo a uma tentativa de construir uma valoração que satisfaça (Subscript[φ, 1]), …, (Subscript[φ, n]) e não satisfaça φ. Se todas as tentativas falham prova-se que não existe uma tal valoração. Assim, todas as valorações que satisfaçam  (Subscript[φ, 1]), …, (Subscript[φ, n]) não satisfazem¬ φ e , portanto, satisfazem necessariamente φ. Pode então concluir-se que  φ é consequência semântica de (Subscript[φ, 1]), …, (Subscript[φ, n]).

Convém então introduzir as noções de ramo fechado, de tableau fechado, de ramo aberto, de conjunto confutado, de teorema de (Subscript[T, p]) e de derivação em (Subscript[T, p]).

Definição 
Um ramo r de um tableau é ramo fechado se existe uma fórmula φ tal que φ e ¬ φ aparecem ambas no ramo r. Um ramo r de um tableau é ramo aberto se não é fechado.

Definição
Um tableau t diz-se tableau fechado se todos os ramos de t são ramos fechados e diz-se tableau aberto se não é fechado.

Definição
Um conjunto de fórmulas Φ diz-se confutado se existe um tableau fechado para Φ.
A fórmula φ diz-se confutada se o conjunto {φ} é confutado.

EXEMPLOS

EXEMPLO 1

O tableau

				\(TraditionalForm\`\((ψ\_1 ∨ ψ\_2)\) -> ψ\_3\^\((1)\), ψ\_1 ∧ ψ\_2\^\((2)\)\), ¬ (Subscript[ψ, 3])
				-----------------------------------------  ∧ , (2)
				         		(Subscript[ψ, 1]), (Subscript[ψ, 2])
				   -----------------------------------------  -> , (1)
				 ((¬ ((Subscript[ψ, 1]) ∨ (Subscript[ψ, 2])))^((3)))			 (Subscript[ψ, 3])
				------------------ ¬  ∨ , (3)
 				  ¬(Subscript[ψ, 1]), ¬ (Subscript[ψ, 2])
 

para {((Subscript[ψ, 1]) ∨ (Subscript[ψ, 2])) -> (Subscript[ψ, 3]),(Subscript[ψ, 1]) ∧ (Subscript[ψ, 2]),¬ (Subscript[ψ, 3])} tem os seus dois ramos fechados. É assim um tableau fechado e o conjunto {((Subscript[ψ, 1]) ∨ (Subscript[ψ, 2])) -> (Subscript[ψ, 3]),(Subscript[ψ, 1]) ∧ (Subscript[ψ, 2]),¬ (Subscript[ψ, 3])} é um conjunto confutado.

Por vezes é útil indicar explicitamente no tableau quais são os ramos fechados. Para esse propósito usa-se o símbolo ×. No caso do tableau anterior tem-se então

				\(TraditionalForm\`\((ψ\_1 ∨ ψ\_2)\) -> ψ\_3\^\((1)\), ψ\_1 ∧ ψ\_2\^\((2)\)\), ¬ (Subscript[ψ, 3])
				-----------------------------------------  ∧ , (2)
				         		(Subscript[ψ, 1]), (Subscript[ψ, 2])
				   -----------------------------------------  -> , (1)
				 ((¬ ((Subscript[ψ, 1]) ∨ (Subscript[ψ, 2])))^((3)))			 (Subscript[ψ, 3])
				------------------ ¬  ∨ , (3)	  ×
 				  ¬(Subscript[ψ, 1]), ¬ (Subscript[ψ, 2])
				        ×

EXEMPLO 2

O tableau

				\(TraditionalForm\`¬ \((ψ\_1 → \((¬ ψ\_2)\))\)\^\((1)\), ψ\_1⋁\((¬ ψ\_2)\)\^\((3)\)\)
				----------------------------------------- ¬  → , (1)
				         (Subscript[ψ, 1]), ¬ (((¬ (Subscript[ψ, 2])))^((2)))
				       --------------------- ¬ ¬ , (2)
					      (Subscript[ψ, 2])
				------------------------------------ ⋁, (3)
				   (Subscript[ψ, 1])			¬ (Subscript[ψ, 2])
						         ×

para \(TraditionalForm\`{¬ \((ψ\_1 → \((¬ ψ\_2)\))\), ψ\_1⋁\((¬ ψ\_2)\)}\) tem um ramo fechado e um aberto. É um tableau aberto.

EXEMPLO 3

O tableau
	  			\(TraditionalForm\`¬ \((\((ψ\_1 → \((ψ\_2 → ψ\_3)\))\) → \((\((ψ\_1 → ψ\_2)\) → \((ψ\_1 → ψ\_3)\))\))\)\^\((1)\)\)
				---------------------------------------------------------------- ¬  → , (1)
				              \(TraditionalForm\`ψ\_1 → \((ψ\_2 → ψ\_3)\)\^\((2)\)\),
				         \(TraditionalForm\`¬ \((\((ψ\_1 → ψ\_2)\) → \((ψ\_1 → ψ\_3)\))\)\^\((3)\)\)
				       -------------------------------------- ¬  → , (3)
					       (Subscript[ψ, 1]) → ((Subscript[ψ, 2])^((4))),
					      \(TraditionalForm\`¬ \((ψ\_1 → ψ\_3)\)\^\((5)\)\)
					    --------------------- ¬  → , (5)
					    	(Subscript[ψ, 1]),¬ (Subscript[ψ, 3])
					------------------------------------------  → , (2)
				 	  ¬ (Subscript[ψ, 1])			(Subscript[ψ, 2]) → ((Subscript[ψ, 3])^((6)))
					   ×		--------------------------------  → , (4)
						 	  ¬ (Subscript[ψ, 1])			(Subscript[ψ, 2])
								    ×		--------------------------------  → , (6)
								 	  ¬ (Subscript[ψ, 2])			(Subscript[ψ, 3])
								 	    ×				  ×	
é um tableaux para {\(TraditionalForm\`\(\(¬ \((\((ψ\_1 → \((ψ\_2 → ψ\_3)\))\) → \((\((ψ\_1 → ψ\_2)\) → \((ψ\_1 → ψ\_3)\))\))\)\)\(}\)\)\). Tem todos os seus ramos fechados e portanto é um tableau fechado. A fórmula \(TraditionalForm\`¬ \((\((ψ\_1 → \((ψ\_2 → ψ\_3)\))\) → \((\((ψ\_1 → ψ\_2)\) → \((ψ\_1 → ψ\_3)\))\))\)\) é portanto confutada.

Pode definir-se agora a noção de teorema e consequência no sistema (Subscript[T, p]) imediata e simples.

Definição
Uma fórmula φ é teorema de (Subscript[T, p]), o que se representa por
					 (Subscript[⊢ , (Subscript[T, p])])φ
se ¬ φ é fórmula confutada.

Uma fórmula φ é consequência de um conjunto de fórmulas Φ em (Subscript[T, p]), o que se representa por
					\(TraditionalForm\`Φ\( ⊢ \_\(T\_p\)\)φ\)
se Φ ⋃ {¬ φ} é conjunto confutado.

Quando uma fórmula é consequência no sistema (Subscript[T, p]) de um conjunto de fórmulas também se diz que existe uma derivação no sistema (Subscript[T, p]) dessa fórmula a partir desse conjunto de fórmulas.

EXEMPLO

Tendo em conta os exemplos apresentados anteriormente tem-se que
 • {\(\(\((ψ\_1 ∨ ψ\_2)\) -> ψ\_3, ψ\_1 ∧ ψ\_2\)\(}\)\)   (Subscript[⊢ , (Subscript[T, p])]) (Subscript[ψ, 3])
 •\(TraditionalForm\`\(\( ⊢ \_\(T\_p\)\)\((\((ψ\_1 → \((ψ\_2 → ψ\_3)\))\) → \((\((ψ\_1 → ψ\_2)\) → \((ψ\_1 → ψ\_3)\))\))\)\)\)

Exercício: Recorde o problema das caixas referido anteriormente e as fórmulas ψ, ψ', φ1, φ2, φ3 aí consideradas. Mostre que 
						{ ψ, ψ', φ1, φ2, φ3, ¬ p3}
é um conjunto confutado.

Correcção do sistema (Subscript[T, p])

Como tem vindo a ser referido, cada ramo de um tableau para um conjunto pode ser visto como correspondendo a uma tentativa de encontrar uma interpretação que satisfaça esse conjunto. Um ramo fechado corresponde a uma tentativa falhada porque obrigaria a que a interpretação satisfizesse uma certa fórmula e a sua negação.  Se todos os ramos de um tableau são fechados isso vai significar que todas as tentativas falharam e portanto o conjunto dado não é possível.
 
 Se o conjunto é {¬ φ} então todas as valorações falsificam a fórmula ¬ φ e portanto todas as valorações satisfazem a sua negação, isto é, satisfazem φ. Logo φ é uma fórmula válida.
 
Se conjunto é Φ ⋃ {¬ φ} então qualquer que seja a valoração ela falsifica sempre uma fórmula desse conjunto. Assim qualquer valoração que satisfaça Φ tem necessáriamente que satisfazer φ, pelo que φ é consequência semântica de Φ.

Mas para se poder fazer este tipo de análise é necessário que as regras do sistema em causa, neste caso o sistema (Subscript[T, p]), sejam correctas. Isto é, se após aplicar uma regra num tableau todos os conjuntos de fórmulas correspondentes aos ramos que resultam da regra, são impossíveis, então o conjunto de fórmulas do ramo original já era impossível (ou, o que é o mesmo, se o conjunto de fórmulas do ramo original é possível então pelo menos um dos conjuntos de fórmulas correspondentes aos ramos que resultam da regra é também possível).

Definição Uma regra do sistema (Subscript[T, p]) diz-se correcta se verifica a seguinte condição:
	 se t é um tableau com um ramo r tal que as fórmulas desse ramo constituem um conjunto possível 
	  então qualquer tableau t' obtido a partir de t por aplicação dessa regra tem também um ramo r' 
	  cujo conjunto de fórmulas é um conjunto possível.

Todas as regras do sistema T são correctas. Este resultado é estabelecido na proposição seguinte.

Proposição Todas as regras do sistema (Subscript[T, p]) são correctas.

Prova
A prova tem que ser feita para cada regra do sistema (Subscript[T, p]).
Regra ⋀:
Seja t um tableau e r um ramo de t cujo conjunto de fórmulas, (Subscript[F, r,]) é possível. Seja t' o tableau obtido de t por aplicação da regra ⋀ a uma fórmula φ⋀ψ pertence a um ramo \(TraditionalForm\`r\&_\) de t. Designe-se por \(TraditionalForm\`r\&_'\) o ramo em t' correspondente a \(TraditionalForm\`r\&_\). O conjunto de fórmulas neste ramo, \(TraditionalForm\`F\_\(\(r\&_'\)\(,\)\)\) é  constituído pelas fórmulas em \(TraditionalForm\`r\&_\) e por φ e ψ. 

Considere-se os dois casos possíveis:

 1. O ramo r não é \(TraditionalForm\`r\&_\). 
    Neste caso r é também um ramo de t' e portanto t' tem também um ramo que é possível.
 
 2. O ramo r é \(TraditionalForm\`r\&_\). 
     Seja V uma estrutura de interpretação que satisfaz todas as fórmulas em (Subscript[F, r]). Então em particular V satisfaz φ ∧ ψ. Logo V satisfaz φ e V satisfaz ψ. Assim ,V satisfaz todas as fórmulas em \(TraditionalForm\`F\_r\&_\). Logo t' tem um ramo cuj conjunto de fórmulas é possível como pretendíamos demonstrar.

Os outros casos ficam como exercícios para o leitor.

Relaciona-se agora o conceito dedutivo de conjunto confutado com o conceito semântico de esse conjunto de fórmulas ser impossível.

Proposição: Correcção do sistema dedutivo (Subscript[T, p])
Se o conjunto de fórmulas Φ é confutado então Φ é contraditório.

Prova:
Se  Φ  é conjunto confutado, existe um tableau fechado t para Φ. Assuma-se, com vista a um absurdo, que Φ é possível. 

O tableau t é obtido a partir de um tableau (Subscript[t, 0 ])para Φ com único nó, por aplicação sucessiva de regras de inferência. O tableau (Subscript[t, 0 ]) tem um único ramo e o conjunto de fórmulas desse ramo é precisamente Φ e portanto (Subscript[t, 0 ])tem um ramo cujo conjunto de fórmulas é possível. Pela proposição anterior,  t tem também um ramo cujo conjunto de fórmulas é possível. Esse ramo não pode ser fechado e portanto t tem um ramo que não é fechado.
Chega-se assim a uma contradição pois t é tableau fechado.

Conclui-se então que se t é fechado então Φ não é possível, ou seja, é contraditório.

Assim, é agora possível relacionar a noção dedutiva de teorema do cálculo (Subscript[T, p]) com a noção semântica de fórmula válida (no fragmento proposicional da lógica de primeira ordem). De modo semelhante relaciona-se consequência com consequência semântica e conjunto confutado com conjunto impossível.

Corolário 
• Se {¬φ} é confutado então ⊨φ.
• Se {(Subscript[φ, 1]),  ... , (Subscript[φ, n]),¬φ} é confutado então \(TraditionalForm\`{φ\_1, …, φ\_n} ⊨ φ\).

Observe-se que este corolário enuncia os resultados que tinham vindo a ser referidos sobre a relação entre conjuntos confutados e consequência semântica e
entre conjuntos confutados e validade.  A partir de conclusões dedutivas extraem-se conclusões semânticas. Este facto constitui a correcção do sistema em causa, neste caso do fragmento proposicional da lógica de primeira ordem. Correcção porque garante que todas as conclusões que se tirem por via dedutivas estão correctas semânticamente

EXEMPLO

Tendo em conta os exemplos apresentados anteriormente, usando a correcção do sistema (Subscript[T, p]) pode concluir-se que
 • {\(\(\((ψ\_1 ∨ ψ\_2)\) -> ψ\_3, ψ\_1 ∧ ψ\_2\)\(\ \)\(}\)\)⊨ (Subscript[ψ, 3])
 ou seja,  (Subscript[ψ, 3]) é consequência semântica de \(TraditionalForm\`\((ψ\_1 ∨ ψ\_2)\) -> ψ\_3, ψ\_1 ∧ ψ\_2\)
 • \(TraditionalForm\`\(\(⊨\)\((\((ψ\_1 → \((ψ\_2 → ψ\_3)\))\) → \((\((ψ\_1 → ψ\_2)\) → \((ψ\_1 → ψ\_3)\))\))\)\)\)
 ou seja \(TraditionalForm\`\((\((ψ\_1 → \((ψ\_2 → ψ\_3)\))\) → \((\((ψ\_1 → ψ\_2)\) → \((ψ\_1 → ψ\_3)\))\))\)\) é fórmula válida

Exercício: Recorde o problema das caixas referido anteriormente e as fórmulas ψ, ψ', φ1, φ2, φ3 aí consideradas. Conclua que
						{ ψ, ψ', φ1, φ2, φ3} ⊨ p3
e portanto o dinheiro está na caixa 3, recorrendo ao sistema (Subscript[T, p]) e á sua correcção.

Corolário 
• Se  (Subscript[⊢ , (Subscript[T, p])])φ então ⊨φ.
• Se \(TraditionalForm\`{φ\_1, …, φ\_n}\( ⊢ \_\(T\_p\)\)φ\) então \(TraditionalForm\`{φ\_1, …, φ\_n} ⊨ φ\).

A partir de conclusões dedutivas extraem-se conclusões semânticas. A correcção do sistema (Subscript[T, p]) é assim designada porque garante que todas as conclusões que se tirem por via dedutivas estão correctas semânticamente.

Completude do sistema (Subscript[T, p])

Dizer que um sistema dedutivo é completo, significa, em termos intuitivos, que todas as conclusões sobre fórmulas e conjuntos (finitos) de fórmulas que se possam tirar semanticamente também se podem tirar dedutivamente. 

No caso particular do sistema (Subscript[T, p]), prova-se que se um conjunto é contraditório então ele é também um conjunto confutado. Como consequência prova-se que se uma fórmula φ é válida então ¬φ é fórmula confutada, e prova-se que se φ é consequência semântica de {(Subscript[φ, 1]), …, (Subscript[φ, n])} então {(Subscript[φ, 1]),  ... , (Subscript[φ, n]),¬φ} é conjunto confutado.

Para se mostrar que (Subscript[T, p]) é completo é necessário definir-se primeiro quando é que um ramo de um tableau é esgotado.

Definição Um ramo r de um tableau está esgotado se para cada fórmula φ nesse ramo se tem que:

 • se φ é ¬ ¬ (Subscript[φ, 1]) então (Subscript[φ, 1]) está em r
 • se φ é (Subscript[φ, 1]) ∧ (Subscript[φ, 2]) então (Subscript[φ, 1]) e (Subscript[φ, 2]) estão em r
 • se φ é \(TraditionalForm\`¬ \((φ\_1 ∧ φ\_2)\)\) então ¬ (Subscript[φ, 1]) ou ¬ (Subscript[φ, 2]) estão em r
 • se φ é (Subscript[φ, 1]) ∨ (Subscript[φ, 2]) então (Subscript[φ, 1]) ou (Subscript[φ, 2]) estão em r
 • se φ é \(TraditionalForm\`¬ \((φ\_1 ∨ φ\_2)\)\) então ¬ (Subscript[φ, 1]) e ¬ (Subscript[φ, 2]) estão em r
 • se φ é (Subscript[φ, 1]) -> (Subscript[φ, 2]) então ¬ (Subscript[φ, 1]) ou (Subscript[φ, 2]) estão em r
 • se φ é \(TraditionalForm\`¬ \((φ\_1 -> φ\_2)\)\) então (Subscript[φ, 1]) e ¬ (Subscript[φ, 2]) estão em r.

Intuitivamente, na maior parte dos casos, um ramo está esgotado se, relativamente a esse ramo, já foram aplicadas regras de inferência a todas as fórmulas do ramo a que se possam aplicar regras (isto é, fórmulas que não sejam símbolos proposicionais nem negação de símbolos proposicionais).

EXEMPLOS

O tableau 

				\(TraditionalForm\`¬ \((ψ\_1 → \((¬ ψ\_2)\))\)\^\((1)\), ψ\_1⋁\((¬ ψ\_2)\)\^\((3)\)\)
				----------------------------------------- ¬  → , (1)
				         (Subscript[ψ, 1]), ¬ (((¬ (Subscript[ψ, 2])))^((2)))
				       --------------------- ¬ ¬ , (2)
					      (Subscript[ψ, 2])
				------------------------------------ ⋁, (3)
				   (Subscript[ψ, 1])			¬ (Subscript[ψ, 2])

tem todos os seus ramos esgotados.

O tableau 
	  			\(TraditionalForm\`¬ \((\((ψ\_1 → \((ψ\_2 → ψ\_3)\))\) → \((\((ψ\_1 → ψ\_2)\) → \((ψ\_1 → ψ\_3)\))\))\)\^\((1)\)\)
				---------------------------------------------------------------- ¬  → , (1)
				              \(TraditionalForm\`ψ\_1 → \((ψ\_2 → ψ\_3)\)\^\((2)\)\),
				         \(TraditionalForm\`¬ \((\((ψ\_1 → ψ\_2)\) → \((ψ\_1 → ψ\_3)\))\)\^\((3)\)\)
				       -------------------------------------- ¬  → , (3)
					       (Subscript[ψ, 1]) → ((Subscript[ψ, 2])^((4))),
					      \(TraditionalForm\`¬ \((ψ\_1 → ψ\_3)\)\^\((5)\)\)
					    --------------------- ¬  → , (5)
					    	(Subscript[ψ, 1]),¬ (Subscript[ψ, 3])
					------------------------------------------  → , (2)
				 	  ¬ (Subscript[ψ, 1])			(Subscript[ψ, 2]) → ((Subscript[ψ, 3])^((6)))
							
tem um ramo (o ramo do lado direito) não esgotado. Com efeito, a fórmula (Subscript[ψ, 1]) → (Subscript[ψ, 2]) pertence ao ramo mas nem ¬ (Subscript[ψ, 1]) nem (Subscript[ψ, 2]) pertencem ao ramo em causa.

Prova-se agora o resultado que descreve como a partir de ramos esgotados de um tableau de (Subscript[T, p]) se obtém uma valoração que satisfaz o conjunto associado à raiz do tableau.

Proposição Seja r um ramo aberto e esgotado de um tableau para um conjunto Φ. 
A valoração V tal que V(p) = 0 se ¬ p está no ramo r e V(p) = 1 caso contrário satisfaz o conjunto Φ.

Prova (esboço)
Mostra-se por indução na complexidade das fórmulas no ramo r que qualquer fórmula presente nesse ramo é satisfeita por V. A complexidade de uma fórmula é o comprimento da fórmula (recorde-se que cada fórmula é uma sequência de símbolos).

Base: Fórmulas de complexidade 1 (ou seja, símbolos proposicionais)
Seja p um símbolo proposicional presente em r. Por definição da valoração V tem-se então que V(p) = 1.

Passo: Fórmulas de complexidade n>1. Há que considerar 4 casos.
Caso 1: a fórmula  (Subscript[φ, 1]) ∧ (Subscript[φ, 2]) está em r. Como o ramo r é esgotado tem-se que (Subscript[φ, 1]) e (Subscript[φ, 2]) também estão em r. Logo por hipótese de indução V((Subscript[φ, 1])) = 1 e V((Subscript[φ, 2])) = 1. Logo V((Subscript[φ, 1]) ∧ (Subscript[φ, 2])) = 1 como se pretendia demonstrar.

Deixa-se como o exercício ao leitor provar os restantes casos, correspondentes a fórmulas  (Subscript[φ, 1]) ∨ (Subscript[φ, 2]),  (Subscript[φ, 1]) -> (Subscript[φ, 2]) e  ¬ φ.

Assim, se existe um tableau com um ramo aberto e esgotado para um conjunto Φ então o conjunto é possível e pode construi-se a partir do tableau uma valoração que comprova que o conjuto é possível.  

Em particular, se existe um tableau com um ramo aberto e esgotado para {¬φ} pode, a partir dele, construir-se uma valoração que comprova que φ não é fórmula válida. Por outro lado, se existe um tableau com um ramo aberto e esgotado para {(Subscript[φ, 1]),  ... , (Subscript[φ, n]),¬φ} pode, a partir dele, construir-se uma valoração que comprova que φ não é consequência semântica de (Subscript[φ, 1]),  ... , (Subscript[φ, n]).

EXEMPLOS

EXEMPLO 1

O tableau

				        \(TraditionalForm\`¬ \((p\_1 → \((p\_1 ∧ p\_2)\))\)\^\((1)\)\)
				   ----------------------------------- ¬  → , (1)
				              (Subscript[p, 1]), ¬ ((((Subscript[p, 1]) ∧ (Subscript[p, 2])))^((2)))
				     	 ------------------------ ¬  ∧ , (2)
				    	 ¬ (Subscript[p, 1])		¬ (Subscript[p, 2])
				 	 ×

tem um ramo esgotado e aberto (o ramo da direita). Tendo em conta a proposição anterior, é possível construir uma valoração V que satisfaz a fórmula da raiz. Essa valoração é construída observando que ¬ (Subscript[p, 2]) e  (Subscript[p, 1]) estão no ramo e portanto V((Subscript[p, 2]))=0 e V((Subscript[p, 1]))=1. Deixa-se como exercício, confirmar que de facto esta valoração satisfaz ¬ ((Subscript[p, 1]) → ((Subscript[p, 1]) ∧ 
                (Subscript[p, 2]))).

Dado que existe um tableau com um ramo aberto e esgotado para ¬ ((Subscript[p, 1]) → ((Subscript[p, 1]) ∧ 
                (Subscript[p, 2]))) pode concluir-se que (Subscript[p, 1]) → ((Subscript[p, 1]) ∧ (Subscript[p, 2])) não é fórmula válida  e  valoração acima comprova-o.

EXEMPLO 2

O tableau

				¬ ((((Subscript[p, 1]) → (Subscript[p, 2])))^((1))), 
      (Subscript[p, 1])⋁(((¬ (Subscript[p, 2])))^((2)))
				----------------------------------------- ¬  → , (1)
				              (Subscript[p, 1]), ¬ (Subscript[p, 2])
				------------------------------------ ⋁, (2)
				   (Subscript[p, 1])			¬ (Subscript[p, 2])
						         ×

tem um ramo esgotado e aberto (o ramo da esquerda). Tendo em conta a proposição anterior, é possível construir uma valoração V que satisfaz as duas fórmulas da raiz: uma valoração com V((Subscript[p, 2]))=0 e V((Subscript[p, 1]))=1. Deixa-se como exercício, confirmar que de facto esta valoração satisfaz ¬ ((Subscript[p, 1]) → (Subscript[p, 2])) e (Subscript[p, 1])⋁(¬ (Subscript[p, 2])).

Dado que existe um tableau com um ramo aberto e esgotado para {(Subscript[p, 1])⋁(¬ (Subscript[p, 2])), ¬ ((Subscript[p, 1]) → 
            (Subscript[p, 2]))} pode concluir-se que (Subscript[p, 1]) → (Subscript[p, 2]) não é consequência semântica de (Subscript[p, 1])⋁(¬ (Subscript[p, 2])) e  valoração acima comprova-o.

Pode-se agora provar que o fragmento proposicional é completo.

Proposição: Completude do sistema dedutivo (Subscript[T, p])
Se o conjunto finito de fórmulas Φ é contraditório então  Φ é confutado.

Prova (esboço)
Note-se que para cada conjunto finito de fórmulas é possível construir um tableau em que todos os ramos são esgotados. 

Considere-se então um tableau para  Φ com todos os seus ramos esgotados. Se existisse um ramo aberto, seria possível construir uma valoração que satisfaz todas as fórmulas em Φ. Tal não é possível porque, por hipótese, Φ é contraditório. Assim, todos os ramos do tableau são necessariamente fechados. Logo o tableau é fechado e consequentemente Φ é confutado.

Como corolário tem-se que se uma fórmula φ é válida então ¬φ é confutada e se φ é consequência semântica de (Subscript[φ, 1]), …, (Subscript[φ, n]) então {(Subscript[φ, 1]),  ... , (Subscript[φ, n]),¬φ} é confutado.

Corolário 
• Se  ⊨φ então {¬φ} é confutado.
• Se  \(TraditionalForm\`{φ\_1, …, φ\_n} ⊨ φ\) então {(Subscript[φ, 1]),  ... , (Subscript[φ, n]),¬φ} é confutado.

Corolário 
• Se  ⊨φ então   (Subscript[⊢ , (Subscript[T, p])])φ.
• Se  \(TraditionalForm\`{φ\_1, …, φ\_n} ⊨ φ\) então \(TraditionalForm\`{φ\_1, …, φ\_n}\( ⊢ \_\(T\_p\)\)φ\).

Sistema dedutivo T

O sistema dedutivo T é uma extensão do sistema (Subscript[T, p]). Os tableaux são agora árvores etiquetadas por conjuntos de fórmulas de primeira  ordem e, para além das regras de (Subscript[T, p]), o sistema T inclui também regras para os quantificadores. Existem onze regras de inferência, duas regras por cada conectivo, com a excepção do conectivo ¬ :

 • regra ⋀
 • regra ¬ ⋀
 • regra ⋁
 • regra ¬ ⋁
 • regra  → 
 • regra ¬  → 
 • regra ¬ ¬ 
 • regra ∀ 
 • regra ¬ ∀ 
 • regra ∃ 
 • regra ¬ ∃

Definição As regras de inferência do sistema T são as seguintes:

 φ⋀ψ		 ¬ (φ⋀ψ)		  φ⋁ψ		¬ (φ⋁ψ)
-------- ⋀	-------------- ¬ ⋀	---------	⋁	------------- ¬ ⋁
 φ, ψ		 ¬ φ | ¬ ψ		  φ | ψ		 ¬ φ , ¬ ψ


  φ → ψ	 ¬ (φ → ψ)		  ¬ ¬ φ	
-----------  → 	-------------- ¬  → 	---------- ¬ ¬ 
 ¬ φ | ψ	    φ , ¬ ψ		     φ


  ∀ x φ			 ¬ (∀ x φ)
-------- ∀ 		------------ ¬ ∀ 
  (Subscript[([φ]), t]^x)			  ¬ (Subscript[([φ]), y]^x)
t é um termo		y é uma variável que não ocorre no tableau


  ∃ x φ							 ¬ (∃ x φ)
-------- ∃ 						------------ ¬ ∃ 
   (Subscript[([φ]), y]^x)						 	  ¬ (Subscript[([φ]), t]^x)
y é uma variável que não ocorre no tableau	      t é um termo

Observe-se que nas regras ¬ ∀  e ∃  para além de ter de existir no tableau uma fórmula com a sintaxe indicada, exige-se ainda que a variável y não exista em nenhuma das fórmulas do tableau a que se aplica a regra. 

Recorde-se que a notação (Subscript[([φ]), t]^x) corresponde à fórmula que se obtém a partir da fórmula φ substituindo todas as ocorrências livres de  x em φ pelo termo t,  sendo  t termo livre para a variável x em φ  (isto é, nenhuma ocorrência livre de x em φ está no alcance de uma quantificação ∀y ou  ∃y em que y seja uma variável que ocorra em t).

As noções de ramo aberto, ramo fechado, tableau aberto, tableau fechado e fórmula e conjunto confutado são, naturalmente, tal como apresentado no caso do sistema (Subscript[T, p]).

EXEMPLOS

EXEMPLO 1

O tableau 
				\(TraditionalForm\`¬ \((\((∃ x\ \(q(x)\))\) → \((¬ \((∃ x(¬ \((q(x))\)))\))\))\)\^\((1)\)\)
				----------------------------------------------- ¬  → , (1)
				              ∃ x ((q(x))^((2))),
				         \(TraditionalForm\`¬ \((¬ \((∃ x(¬ \((q(x))\)))\))\)\^\((3)\)\)
				       -------------------------------------- ¬ ¬ , (3)
					       ∃ ((x(¬ (q(x))))^((4)))
					    --------------------- ∃ , (2)
					    	q(y)
					        ------------- ∃ , (4)
					 	¬ q(z)

é um tableau para o conjunto constituído pela fórmula \(TraditionalForm\`¬ \((\((∃ x\ \(q(
                    x)\))\) → \((¬ \((∃ x(¬ \((q(x))\)))\))\))\)\) onde q é um símbolo de predicado unário. Recorde-se que ao aplicar a regra ∃  há que utilizar variáveis que não ocorrem nas fórmulas presentes no tableau.

Este é um tableau aberto pois o seu único ramo é um ramo aberto.

EXEMPLO 2

O tableau 		
				\(TraditionalForm\`¬ \((\((∃ x\ \((∀ y\ \(p(x, y)\))\))\) → \((∀ y\ \((∃ x\ \(p(x, y)\))\))\))\)\^\((1)\)\)
				--------------------------------------------------------- ¬  → , (1)
				              \(TraditionalForm\`∃ x\ \ \((∀ y\ \(p(x, y)\))\)\^\((2)\)\),
				         \(TraditionalForm\`¬ \((∀ y\ \((∃ x\ \(p(x, y)\))\))\)\^\((3)\)\)
				       -------------------------------------- ∃ , (2)
					       ∀ y ((p(z, y))^((4)))
					    --------------------- ¬ ∀ , (3)
					     \(TraditionalForm\`\(\(\ \)\(¬ \((∃ x\ \(p(x, w)\))\)\^\((5)\)\)\)\)
					   ------------------------- ∀ , (4)
					 	p(z, w)
					        ----------------- ¬ ∃ , (5)
					 	¬ p(z, w)
					 	      ×

é um tableau para o conjunto constituído pela fórmula \(TraditionalForm\`¬ \((\((∃ x\ \((∀ y\ \(p(x, 
                          y)\))\))\) → \((∃ x\ \((∀ y\ \(p(x, y)\))\))\))\)\) onde p é um símbolo de predicado binário. 

Este é um tableau fechado pois o seu único ramo é um ramo fechado. A fórmula \(TraditionalForm\`¬ \((\((∃ x\ \((∀ y\ \(p(x, 
                          y)\))\))\) → \((∃ x\ \((∀ y\ \(p(x, y)\))\))\))\)\) é assim fórmula confutada.

EXEMPLO 3

O tableau 		
				      \(TraditionalForm\`∀ \(x(q(x) → r(x))\)\^\((1)\)\),
				  \(TraditionalForm\`¬ \((\((\(q(a)\)⋀\(q(b)\))\) → \((\(r(a)\)⋀\(r(b)\))\))\)\^\((2)\)\)
				---------------------------------------------- ¬  → , (2)
				             q(a)⋀((q(b))^((3))),
				           ¬ (((r(a)⋀r(b)))^((4)))
				         ------------------------ ⋀, (3)
					      q(a), q(b)
					    ------------------ ∀ , (1)
					     q(a) → ((r(a))^((5)))
				    ----------------------------------------  → , (5)
				     ¬ q(a)			r(a)
				         ×	    	------------------------------------------ ¬ ⋀, (4)
						     ¬ r(b)			¬ r(a)
						------------------ ∀ , (1)	   	    ×
					     	q(b) → ((r(b))^((6)))
				  ----------------------------------------  → , (5)
				   ¬ q(b)			r(b)
				   ×				 ×
é um tableau para o conjunto {∀ x(
            q(x) → 
              r(x)), ¬ ((q(a)⋀q(
                    b)) → (r(a)⋀r(
                    b)))} onde q e r são símbolos de predicado unários. Note-se que na construção deste tableau se aplicou duas vezes a regra ∀  à fórmula (1). Numa das vezes, substituiu-se a variável x pela constante a e na outra pela constante b.

Este é um tableau fechado pois todos os seus ramos são fechados. O conjunto {∀ x(
            q(x) → 
              r(x)), ¬ ((q(a)⋀q(
                    b)) → (r(a)⋀r(
                    b)))} é portanto conjunto confutado.

Naturalmente, a noção de teorema e consequência no sistema T é como apresentada no caso do fragmento proposicional:
 • uma fórmula φ é teorema de T, o que se representa por (Subscript[⊢ , T])φ, se ¬ φ é fórmula confutada
 • uma fórmula φ é consequência de um conjunto de fórmulas Φ em T, o que se representa por Φ (Subscript[⊢ , T])φ se Φ ⋃ {¬ φ} é conjunto confutado.

Correcção e completude do sistema T

Proposição: Correcção do sistema dedutivo
Se o conjunto de fórmulas Φ é confutado então Φ é contraditório.

Corolário 
• Se {¬φ} é confutado então ⊨φ.
• Se {(Subscript[φ, 1]),  ... , (Subscript[φ, n]),¬φ} é confutado então \(TraditionalForm\`{φ\_1, …, φ\_n} ⊨ φ\).

EXEMPLO

Tendo em conta os exemplos apresentados anteriormente, usando a correcção do sistema T pode concluir-se que
 • \(TraditionalForm\`\(\(⊨\)\(\((∃ x\ \((∀ y\ \(p(x, 
                        y)\))\))\) → \((∃ x\ \((∀ y\ \(p(x, y)\))\))\)\)\)\)
 ou seja \(TraditionalForm\`\((∃ x\ \((∀ y\ \(p(x, 
                      y)\))\))\) → \((∃ x\ \((∀ y\ \(p(x, y)\))\))\)\) é fórmula válida	
 
 • {∀ x(q(x) → r(x)) }⊨ (q(a)⋀q(b)) → (r(
                    a)⋀r(b))
 ou seja,  (q(a)⋀q(b)) → (r(
                    a)⋀r(b)) é consequência semântica de ∀ x(q(x) → r(x))

Proposição: Completude do sistema dedutivo T
Se o conjunto finito de fórmulas Φ é contraditório então  Φ é confutado.

Tal como no caso do fragmento proposicional, é também possível definir neste contexto a noção de ramo esgotado e é possível provar que a partir de um ramo esgotado se pode construir uma estrutura de interpretação que satisfaz todas as fórmulas na raiz do tableau. No entanto, ao contrário do que acontecia no fragmento proposicional, pode acontecer que um ramo esgotado seja um ramo com um número infinito de nós.

Cálculo de Hoare

O cálculo de Hoare permite mostrar propriedades de pequenos programas imperativos.

Essas propriedades podem ser de dois tipos: 
1. verificação de que o programa quando iniciado num estado que satisfaz uma certa condição, designada por pré-condição ou condição inicial, se terminar, termina num estado em que as variáveis satisfazem uma condição designada por pós-condição ou condição final.
2. verificação de que o programa termina quando iniciado num estado que satisfaz uma pré-condição. Consideram-se apenas programas em que a não terminação provém unicamente de ciclos em que a guarda tem sempre o valor True. Não se consideram programas que não terminem devido à invocação de funções com argumentos inapropriados. Assume-se que as funções são invocadas com os argumentos correctos.

A primeira propriedade designa-se por correcção parcial uma vez que não é provada a terminação do programa e a segunda por propriedade de terminação dos programas. Por correcção total de um programa entende-se a prova de correcção parcial e de terminação desse programa.

Correcção parcial

Como se fez para lógica de primeira ordem, começa-se por definir a linguagem da lógica.

Linguagem

A linguagem da lógica é o conjunto das expressões sintaticamente correctas no âmbito da lógica em causa. No caso do cálculo de Hoare para correcção parcial essas expressões são triplos da forma
							{(Subscript[C, i])} P {(Subscript[C, f])}
em que (Subscript[C, i]) e (Subscript[C, f]) são condições e P é um programa Mathematica construído a partir de um número limitado de operações.  

Designa-se por Id o conjunto dos identificadores do Mathematica, isto é, das sequências de caracteres que podem corresponder a nomes correctos para variáveis (tipicamente sequências de letras e dígitos começando por uma letra).

Considera-se um subconjunto  \(TraditionalForm\`M\&_\) de ℳ construído a partir de um conjunto de expressões básicas e de operações escolhidas de modo a que a avaliação das expressões em \(TraditionalForm\`M\&_\) termina. De modo semelhante considera-se o subconjunto \(TraditionalForm\`M\&_\_B\) de \(TraditionalForm\`M\&_\) constituído pelas expressões Mathematica com valor booleano. Devido a não ser o tópico deste módulo omite-se a definição de \(TraditionalForm\`M\&_\_B\) e \(TraditionalForm\`M\&_\) assumindo-se que contêm todas as expressões que intuitivamente satisfazem os requisitos descritos atrás.

Definição: O conjunto Imp de programas imperativos em Mathematica é definido indutivamente como se segue

 • Null ∈ Imp

 • I = E ∈ Imp, em que I ∈ Id e \(TraditionalForm\`E ∈ M\&_\)

 • If[G, (Subscript[P, 1]), (Subscript[P, 2])] ∈ Imp, em que \(TraditionalForm\`G ∈ M\&_\_B\) e (Subscript[P, 1]), (Subscript[P, 2]) ∈ Imp

 • While[G, P] ∈ Imp, em que \(TraditionalForm\`G ∈ M\&_\_B\) e P ∈ Imp

 • (Subscript[P, 1]); (Subscript[P, 2]) ∈ Imp, em que (Subscript[P, 1]), (Subscript[P, 2]) ∈ Imp.

Seguindo a terminologia usual de programação imperativa designaremos Null como o comando vazio, I = E como o comando (atómico) de atribuição, If[G, (Subscript[P, 1]), (Subscript[P, 2])] como o comando (composto) de alternativa, While[G, P] como o comando (composto) de iteração e (Subscript[P, 1]); (Subscript[P, 2]) como o comando (composto) de sequenciação.

Note-se que nos programas considerados a interacção com o utilizador, a ter sido realizada, é expressa nos valores das variáveis no inicio da computação.

Como resultado  das restrições impostas na sintaxe dos programas em Imp, tem-se que nos comandos de atribuição I = E, de composição alternativa If[G, (Subscript[P, 1]), (Subscript[P, 2])]  e de composição iterativa While[G, P] em Imp a avaliação da expressão E e da expressão G termina sempre.

Fica assim garantida, através da imposição destas restrições, que a única causa de não terminação dos programas que serão considerados são ciclos infinitos.

Mais ainda, note-se que nos comandos de composição alternativa If[G, (Subscript[P, 1]), (Subscript[P, 2])]  e de composição iterativa While[G, P] em Imp a avaliação da expressão G tem como resultado um valor booleano.

Fica assim garantida, através da imposição desta restrição, que a lógica das expressões booleanas consideradas em Imp é clássica.

Note-se que a limitação a esta classe de programas é computacionalmente completa no sentido em que é sempre possível encontrar um programa construído unicamente a partir destas operações com o mesmo comportamento que um outro programa qualquer escrito em Mathematica.

O programa P correspondente ao corpo da função 

Function[{w, x}, 
        Module[{i, n}, 
i = 1; 
n = 
            0; 
While[
            i ≠ Length[w] + 1, 
If[
              w[[i]] > x, n = n + 1, Null]; 
i = 
              i + 1]; 
n]]

é o seguinte programa:

i = 1;
n = 0;
While[
        i ≠ Length[w] + 1, 
If[w[[i]] > x, 
          n = n + 1, Null]; 
i = i + 1]

Definição: Uma condição é uma fórmula fechada pertencente a uma linguagem de primeira ordem que
 • inclui como termos as expressões em \(TraditionalForm\`M\&_\)
 • inclui como fórmulas as expressões em \(TraditionalForm\`M\&_\_B\).

Assume-se que o conjunto das variáveis de primeira ordem que podem aparecer nas condições é disjunto do conjunto Id dos identificadores do Mathematica. 

Pode-se então agora definir a linguagem do Cálculo de Hoare para correcção parcial.

Definição A linguagem do Cálculo de Hoare para correcção parcial é o conjunto dos triplos

					{(Subscript[C, i])} P {(Subscript[C, f])}
em que
 • P ∈ Imp
 • (Subscript[C, i]) e (Subscript[C, f]) são condições.

É usual designar os elementos {(Subscript[C, i])} P {(Subscript[C, f])} da linguagem do Cálculo de Hoare para correcção parcial como asserções.

Exemplos de asserções  na linguagem do Cálculo de Hoare para correcção parcial:

 • {n == 3}    n = 
        n + 1    {n == 4}
 
 • {True}  x = x + 1  {x > 0}

 • {(n == 3) ∧ (a < 2)}  n = 
        n + a  {n < 5}
 
 • {(n == 3) ∧ (a < 2)}  If[
          n == 4, n = n - a, n = n + a]  {n < 5}
 
 • {x < 3}  x = x*x  {x < 9}
  
 • {x == -3}  x = x*x  {x < 9}
  
 • {True}   n = 3; a = -1; 
      If[n == 4, n = n - a, n = n + a]   {n < 5}
  
  • {True}
i = 1; n = 0;
While[
        i ≠ Length[w] + 1, 
If[w[[i]] > x, 
          n = n + 1, Null]; 
i = i + 1]
{n == # {j : (w[[j]] > 
                      x) ∧ (1 ≤ j ≤ 
                      Length[w])}}

Naturalmente, algumas destas asserções serão interpretadas como verdadeiras e outras como falsas.

O significado que se pretende atribuir à asserção {(Subscript[C, i])} P {(Subscript[C, f])} é que o programa P quando iniciado num estado que satisfaça a condição (Subscript[C, i]), se terminar, termina num estado que satisfaz a condição (Subscript[C, f]). Mas o que é um estado? E o que é a denotação de um programa? Para se entender estas noções aborda-se agora a semântica do Cálculo de Hoare para a correcção parcial.

Semântica

Definição Um estado é uma aplicação \(TraditionalForm\`σ : Id → M\&_\).

O conjunto dos estados designa-se por Est.

Um estado possível pode ser uma função 
			\(TraditionalForm\`\(σ\_0\) : Id → M\&_\) 
em que
 • (Subscript[σ, 0])(x) = 3
 • (Subscript[σ, 0])(i) = 9
 • (Subscript[σ, 0])(n) = 8
 • (Subscript[σ, 0])(m) = 4
 • (Subscript[σ, 0])(w) = {5, 1, -5, 4}

Após ser executado o primeiro comando do programa P

i = 1;
n = 0;
While[
        i ≠ Length[w] + 1, 
If[w[[i]] > x, 
          n = n + 1, Null]; 
i = i + 1]

isto é
			i = 1
o estado muda de (Subscript[σ, 0]) para (Subscript[σ, 1]) em que (Subscript[σ, 1]) é tal que 

 • (Subscript[σ, 1])(z) = (Subscript[σ, 0])(z) para qualquer z ∈ Id diferente de i

 • (Subscript[σ, 1])(i) = 1

A interpretação de expressões Mathematica depende obviamente do estado.

A denotação de uma expressão E em \(TraditionalForm\`M\&_\) num estado σ 
					\(TraditionalForm\`\(\([[\)\(E\)\(]]\)\)\_σ\)
é o resultado de
				avalia(σ,E)
isto é, é o resultado de avaliar a expressão E assumindo que os identificadores Mathematica têm o valor atribuído por σ.

Note-se que devido às restrições impostas \(TraditionalForm\`\(\([[\)\(E\)\(]]\)\)\_σ\) está sempre definida.

Considere-se um estado σ tal que
σ(i) = 2
σ(w) = {12, 45, 32, 0, 4, 5} 

Tem-se então que 

 • \(TraditionalForm\`\(\([[\)\(i ≤ Length[w]\)\(]]\)\)\_σ = True\)
 
 • \(TraditionalForm\`\(\([[\)\(i + 1\)\(]]\)\)\_σ = 3\)

Semanticamente um programa pode ser interpretado como uma função de estados para estados, isto é uma função que dado um estado é tal que, ou não está definida para esse estado, significando que o programa não termina para esses valores dos identificadores, ou se está definida, tem como resultado o estado que resulta da execução do programa a partir do estado inicial dado.

Definição A denotação de programas é uma função

					D : Imp×Est → Est

definida indutivamente como se segue:

 • D(Null, σ) = σ


 • D(I = E, σ) = σ' 
   em que σ' é igual a σ excepto que \(TraditionalForm\`σ' \((I)\) = \(\([[\)\(E\)\(]]\)\)\_σ\)


 • D(If[G, (Subscript[P, 1]), (Subscript[P, 2])], σ)={({{\(\(\(D(
                              P\_1, σ)\)\ \ \ \ \ \ \ \ \ \ \(se\ [[G]]\)\_σ\)\(=\)\(True\)\(\ \)\)}, {\(\(D(
                              P\_2, σ)\)\ \ \ \ \ \ \ \ \ \ \(se\ [[G]]\)\_σ = False\)}}) 
 
 
 • D((Subscript[P, 1]); (Subscript[P, 2]), σ)={({{\(indefinida\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ se\ \(\(D(P\_1, σ)\)\(↑\)\)\)}, {\(\(D(P\_2, 
                            D(P\_1, σ))\)\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ se\ \(\(D(
                              P\_1, σ)\)\(↓\)\)\)}}) 

 
 • D(While[G, P], σ)={({{\(\(σ\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \(se\ [[G]]\)\_σ\)\(=\)\(False\)\(\ \)\)}, {\(indefinida\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \(se\ [[G]]\)\_σ = True\ e\ \ \(\(D(P, σ)\)\(↑\)\)\)}})
                                      D(While[G, P], D(P, σ))           \(\(se\ [[G]]\)\_σ\)=True e D(P, σ)↓.

Considere-se um estado σ em que
 • σ(x) = 4
 • σ(i) = 9
 • σ(n) = 10
 • σ(m) = 4
 • σ(a) = 3
 • σ(w) = {5, 1, -5, -4}

 • D(n = n - 6, σ) = σ' em que 
   - σ' (n) = 4
   - σ' (z) = σ(z), para qualquer z ∈ Id diferente de n
 
 • D(
          If[n == 4, i = i - a, x = x + a], σ) = σ' em que 
   - σ' (x) = 6
   - σ' (z) = σ(z), para qualquer z ∈ Id diferente de x

 • D(n = n - 6; a = a*m; 
          If[n == 4, i = i - a, x = x + a], σ) = σ' em que 
   - σ' (n) = 4
   - σ' (a) = 12
   - σ' (i) = -3
   - σ' (z) = σ(z), para qualquer z ∈ Id diferente de n, a, i
 
  • D(   i = 1; 
n = 
            0; 
While[
            i ≠ Length[w] + 1, 
If[
              w[[i]] > x, n = n + 1, Null]; 
i = 
              i + 1], 
σ) = σ' em que 
   - σ' (i) = 5
   - σ' (n) = 1
   - σ' (m) = 3
   - σ' (z) = σ(z), para qualquer z ∈ Id diferente de n, m, i

Para se poder verificar se uma asserção é válida no âmbito do Cálculo de Hoare para correcção parcial, é necessário verificar se uma condição é ou não satisfeita num certo estado σ.

Definição A estrutura de interpretação para a lógica de primeira ordem das condições induzida pelo estado σ é o tuplo
					\(TraditionalForm\`\(\(<\)\(M\&_\)\), \(\(I\_σ\)\(>\)\)\)
é tal que

 • \(TraditionalForm\`\(I\_σ\)(
          E) = \(\([[\)\(E\)\(]]\)\)\_σ\) para cada termo \(TraditionalForm\`E ∈ M\&_\)
 
 • (Subscript[I, σ])(E)={({{\(1\ \ \ \ \ \ \ \ \(se\ [[E]]\)\_σ = True\)}, {\(0\ \ \ \ \ \ \ \ \(se\ [[E]]\)\_σ = False\)}}), para cada termo \(TraditionalForm\`E ∈ M\&_\_B\).

Uma condição C é satisfeita no estado σ, o que se representa por
 						σ ⊨ C
 se \(TraditionalForm\`\(\(<\)\(M\&_\)\), \(\(I\_σ\)\(>\)\) ⊨ C\).

Pode-se agora definir quando uma asserção pertencente à linguagem do Cálculo de Hoare para correcção parcial é válida.

Definição Uma asserção {(Subscript[C, i])} P {(Subscript[C, f])} é válida no Cálculo de Hoare para correcção parcial, o que se denota por

					⊨{(Subscript[C, i])} P {(Subscript[C, f])}

se D(P, σ) ⊨ (Subscript[C, f]) sempre que D(P, σ)↓, para qualquer que seja o estado σ tal que σ ⊨ (Subscript[C, i]).

Note-se que

 • ⊨{n == 3}  n = 
        n + 1 {n == 4}
 
 • ⊨{(n == 
                    3) ∧ (a < 2)}   n = 
        n + a   {n < 5}
 
 • {(n == 3) ∧ (a < 2)} If[
          n == 4, i = i - a, x = x + a] {x < 5} não é válida.
 
 Considere-se o estado σ tal que σ(n) = 3, σ(a) = 1, σ(x) = 6.
 
 Tem-se que
 
  - D(
          If[n == 4, i = i - a, 
            x = x + a], σ)↓
  
  - σ ⊨ (n == 
              3) ∧ (a < 2)
  
  mas
  
  - D(
            If[n == 4, i = i - a, 
              x = x + a], σ)/ ⊨ x < 5

Sistema dedutivo

Nesta secção vamos mostrar como provar a correcção parcial de um programa face a uma condição inicial e condição final. As asserções correspondentes a esses triplos designam-se por teoremas do Cálculo de Hoare para correcção parcial. Usando os resultados de correcção e completude será possível estabelecer uma equivalência entre asserções que são teoremas segundo o sistema dedutivo e as asserções que são válidas semânticamente.

O sistema dedutivo para o Cálculo de Hoare para correcção parcial é composto pelas seguintes regras.

Definição As regras de inferência do Cálculo de Hoare para correcção parcial são as seguintes

RN:  \(\/\({C} Null {C}\)\)

RA:  \(\/\(\(\ \)\({C\_e\%x} x = \(\(e\) \({C}\)\(\ \ \)\)\)\)\) 
em que (Subscript[C, e]^x) se obtém de C substituindo uniforme e simultaneamente todas as ocorrências de x pela expressão e

RS:\(\({C\_1} \(P\_1\) {C}\ \ \ \ \ \ \ \ \ \ \ \ {C} \(P\_2\) {C\_2}\)\/\({C\_1} P\_1; \(P\_2\) {C\_2}\)\)

RI:\(\({C\_1\  ∧ \ 
                    G} \(P\_1\) {C\_2}\ \ \ \ \ \ {C\_1\  ∧ \((¬ G)\)} \(P\_2\) {C\_2}\)\/\({C\_1} If[G, P\_1, P\_2] {C\_2}\)\)

RW:(({I  ∧  G} P {I}  )/({I} 
                While[G, P] {I  ∧  (¬  G)}))

RC1:(((Subscript[C, 1])⇒C         {C} 
                P {(Subscript[C, 2])})/({(Subscript[C, 1])} P {(Subscript[C, 2])}))

RC2:(({(Subscript[C, 1])} P {C}       C⇒(Subscript[C, 2]))/({(Subscript[C, 1])} P {(Subscript[C, 2])}))

RV:     \(\/\(\(\ \ \ \ \ \ \)\(C\)\(\ \ \ \ \ \)\)\) 
em que C é uma condição válida.

É usual chamar às regras de inferência RN, RA e RV axiomas do Cálculo de Hoare para correcção parcial.

Define-se agora o que é uma asserção {(Subscript[C, i])} P {(Subscript[C, f])} ser teorema do Cálculo de Hoare para correcção parcial.

Definição Uma asserção {(Subscript[C, i])} P {(Subscript[C, f])} é teorema do Cálculo de Hoare para a correcção parcial, o que se denota por

						⊢{(Subscript[C, i])} P {(Subscript[C, f])}

se existe uma sequência de asserções (Subscript[F, 1]), …, (Subscript[F, n]) tal que

 • (Subscript[F, i]) é um axioma ou obtém-se de asserções anteriores por aplicação de uma regra de inferência
 
 • (Subscript[F, n]) é {(Subscript[C, i])} P {(Subscript[C, f])}.

Considere-se o programa Fact correspondente ao corpo da seguinte função:

Function[{n}, 
        Module[{j, r}, 
j = 1; 
r = 
            1; 
While[
            j ≠ n + 1, 
r = 
              r*j; 
j = j + 1]; 
r]]

Mostra-se agora que o programa Fact é parcialmente correcto face à condição inicial True e face à condição final r == n!.
Por outras palavras, mostra-se que o triplo

				{True}Fact{r == n!}

é teorema do Cálculo de Hoare para a correcção parcial.

Para estabelecer a correcção parcial de Fact face a estas condições há que começar por escolher uma condição invariante I apropriada para o ciclo central do programa Fact. 

A condição invariante deve ser escolhida de modo a ser estabelecida pela inicialização do programa  a partir de um estado que satisfaça a condição inicial, isto é,  de modo a ser estabelecida pela composição sequencial j = 1; r = 1.

A condição invariante deve também ser escolhida de modo a que em conjunção com a negação da guarda do ciclo garanta a condição final.

Proposta: I = (r == (j - 1)!)

Demonstração:

Parte I [inicialização estabelece a condição invariante]:

1:{1 == 0!}   j=1   {1 == (j - 1)!}    (RA)

2:{1 == (j - 1)!}  r=1  {r == (j - 1)!}    (RA)

3:{1 == 0!}  j=1;r=1  {r == (j - 1)!}    (RS[1, 2])

4:True⇒(1 == 0!)    (RV)

5:{True}  j=1;r=1  {r == (j - 1)!}    (RC1[3, 4])



Parte II [corpo do ciclo guardado preserva a condição invariante]

6:{r *j == j!}  r=r* j  {r == j!}   (RA)

7:{r == j!}   j=j+1   {r == (j - 1)!}     (RA)

8:{r *j == j!}   r=r *j;j=j+1    {r == (j - 1)!}    (RS[6, 7])

9:((r == (j - 
                          1)!) ∧ (j ≠ n + 1))⇒(r *j == j!)    (RV)

10:{(r == (j - 
                              1)!) ∧ (j ≠ n + 1)}    r=r* j;j=j+1    {r == (j - 1)!}    (RC1[8, 9])



Parte III [programa estabelece condição final]:

11:{r == (j - 1)!}   While[j ≠ n + 1, 
            r = r *j; j = j + 1]{(r == (j - 1)!) ∧ (j == 
                    n + 1)}    (RW[10])

12:((r == (j - 1)!) ∧ (j == 
                    n + 1))⇒(r == n!)    (RV)

13:{r == (j - 1)!}     While[j ≠ n + 1, r = r j; 
            j = j + 1]     {r == n!}    (RC2[11, 12])

14:{True}     j=1;r = 1;While[j ≠ n + 1, r = r j; j = j + 1]     {r == n!}    (RS[5, 13])

Correcção total

A correcção parcial garante que quando um programa se inicia num estado que satisfaz a condição inicial, se terminar, termina num estado que satisfaz a condição objectivo. Existe muitas vezes a necessidade de assegurar que um programa termina. Também para este caso o Cálculo de Hoare pode ajudar. Nesta secção apresenta-se uma lógica baseada no Cálculo de Hoare que pode ser utilizada para provar quer a correcção parcial de programas quer a não existência de ciclos cuja guarda é sempre verdadeira (ciclos cuja guarda é sempre verdadeira é a mais importante causa de não terminação de programas). Essa lógica designa-se por Cálculo de Hoare para corecção total.

Linguagem

A linguagem do Cálculo de Hoare para correcção total é um enriquecimento da linguagem do Cálculo de Hoare para correcção parcial com os pares
							Ω[C, P]
denotados por asserções de convergência, em que C é uma condição e P ∈ Imp. O significado intuitivo destas asserções é que a execução do programa P quando iniciada num estado em que a condição C seja verdadeira não tem ciclos infinitos, isto é ciclos cuja guarda seja sempre verdadeira. Como ciclos infinitos são a única causa de não terminação dos programas que se está a considerar provar que um programa não tem ciclos infinitos é equivalente neste contexto a provar que o programa termina.

Pode-se então agora definir a linguagem do Cálculo de Hoare para correcção total.

Definição A linguagem do Cálculo de Hoare para correcção total é o conjunto formado por

 • triplos {(Subscript[C, 1])} P {(Subscript[C, 2])} em que (Subscript[C, 1]) e (Subscript[C, 2]) são condições e P ∈ Imp
 
 • pares Ω[C, P] em que C é uma condição e P ∈ Imp.

Exemplos de asserções na linguagem do Cálculo de Hoare para correcção total

  • {x == -3}   x = x*x   {x < 9}
  
  • Ω[x == -3, x = x*x]
  
 • {True}   n = 3; a = -1; 
      If[n == 4, n = n - a, n = n + a]   {n < 5}
 
 • Ω[True,  n = 3; a = -1; 
        If[n == 4, n = n - a, n = n + a]]
 
  • {True}
 i = 1;
n = 0;
While[
        i ≠ Length[w] + 1, 
If[w[[i]] > x, 
          n = n + 1, Null]; 
i = i + 1]
{n == # {j :  (w[[j]] > 
                      x)⋀(1 ≤ j ≤ 
                      Length[w])}}

  • Ω[True, 
i = 1; 
        n = 0; While[i ≠ Length[w] + 1, 
          If[w[[i]] > x, n = n + 1, Null]; i = i + 1]]

Semântica

A interpretação das asserções {(Subscript[C, 1])} P {(Subscript[C, 2])} de correcção parcial mantém-se no Cálculo de Hoare para correcção total. Remete-se o leitor para a respectiva secção do módulo sobre Cálculo de Hoare para correcção parcial. A interpretação das asserções de convergência é indicada de seguida.

Definição Uma asserção Ω[C, P] é válida, o que se denota por
					⊨Ω[C, 
          P]
se D(P, σ)↓ qualquer que seja o estado σ tal que σ ⊨ C.

Assim a asserção Ω[C, P] é válida se o programa P terminar quando iniciado num estado que satisfaz a condição C.

Note-se que

 • ⊨Ω[
          n == 3,  n = n + 1]

 • ⊨Ω[True,  
          n = n + 1]

 • /⊨{(n == 
                    3) ∧  (a < 2)} If[n == 4, i = i - a, 
              x = x + a] {x < 5}

      
   \(TraditionalForm\`\(\(⊨\)\(Ω[\((n == 3)\) ∧ \((a < 2)\), \ \ If[n == 4, i = i - a, 
            x = x + a]]\)\)\)

 • ⊨Ω[
          True, 
   i = 1; 
          n = 0; 
  While[i ≠ Length[w] + 1, 
            If[w[[i]] > x, n = n + 1, Null]; i = i + 1]]

 • ⊨Ω[
          True, 
   i = 
            1; 
   While[i ≠ Length[w] + 1, 
            If[w[[i]] > x, n = n + 1, Null]; i = i + 1]]    

 • /⊨Ω[
            True, 
   i = 
              2; 
   While[i ≠ Length[w] + 1, 
              If[w[[i]] > x, n = n + 1, Null]; i = i + 1]]

Sistema dedutivo

O sistema dedutivo para o Cálculo de Hoare para correcção total é composto pelas regras para correcção parcial já apresentadas e por regras que caracterizam o comportamento das asserções de convergência.

Definição As regras de inferência do Cálculo de Hoare para correcção total são 

RCN:   \(\/Ω[True, Null]\)

RCA:   \(\/Ω[True, x = e]\)

RCS:\(\(Ω[C, 
                  P\_1]\ \ \ \ \ \ \ \ {C} \(P\_1\) {C\_1}\ \ \ \ \ \ \ \ Ω[C\_1, P\_2]\)\/Ω[C, P\_1; 
                P\_2]\)

RCI:((Ω[C  ∧  G, 
                  (Subscript[P, 1])]         Ω[
                  C  ∧  (¬ G), (Subscript[P, 2])])/Ω)[C, 
                If[G, (Subscript[P, 1]), (Subscript[P, 2])]]

RCW:\(\(\(\ \ \)\(I ⇒ \((τ ≥ 
                      0)\)\ \ \ \ \ \ \ \ \ \ \ \ \ \ {I\  ∧ \ \((τ == N)\) ∧ \ G} 
                  P {I\  ∧ \ \((τ < 
                          N)\)}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Ω[I\  ∧ \ G, P]\)\)\/Ω[I, While[G, P]]\)

RC3:((C ⇒ 
                (Subscript[C, 1])            Ω[(Subscript[C, 1]), 
                    P])/Ω)[C, P]

mais as regras de inferência do Cálculo de Hoare para correcção parcial.

É usual chamar às regras de inferência RN, RA, RV, RCN e RCA axiomas do Cálculo de Hoare para correcção total, e às regras específicas do Cálculo de Hoare para correcção total regras de convergência.

Define-se agora o que é uma asserção ser teorema do Cálculo de Hoare para correcção total.

Definição Uma asserção F é teorema do Cálculo de Hoare para correcção total, o que se denota por
						⊢F
se existe uma sequência de asserções (Subscript[F, 1]), …, (Subscript[F, n]) tal que

 • (Subscript[F, i]) é um axioma ou obtém-se de asserções anteriores por aplicação de uma regra de inferência do Cálculo de Hoare para correcção total 
 
 • F é (Subscript[F, n]).

Considere-se o programa P correspondente ao corpo da seguinte função:

Function[{w, x}, 
        Module[{i, n, m}, 
i = 1; 
n = 
            0; 
While[
            i ≠ Length[w] + 1, 
If[
              w[[i]] > x, n = n + 1, Null]; 
i = 
              i + 1]; 
n]]


Mostra-se agora que

1. A asserção 
			Ω[ListQ[w], P]
é teorema do Cálculo de Hoare para correcção total


2. A asserção 
			{True} 
        P {n == # {j : (w[[j]] > x)⋀(1 ≤ 
                        j ≤ Length[w])}}
é teorema do Cálculo de Hoare para correcção parcial




PROVA de 1., isto é, que a asserção Ω[ListQ[w], P] é teorema do Cálculo de Hoare para correcção total:

Expressão variante τ: (Length[w] + 1 - i)
Invariante I: (ListQ[w] ∧ 
          IntegerQ[i] ∧ (Length[w] + 1 - i ≥ 0))

Parte I [inicialização termina]:

1: Ω[True,i = 1]        (RCA)

2: Ω[True,n = 0]        (RCA)

3: {True}i=1{True}        (RA)

4:Ω[True,i = 1; n = 0]    (RCS[1, 2, 3])

5:ListQ[w]⇒True    (RV)

6:Ω[ListQ[w],i = 1; n = 0]    (RC3[5, 4])


Parte II [inicialização estabelece condição invariante]:

5: {ListQ[w] ∧ 
                IntegerQ[
                  1] ∧ (Length[w] + 1 - 1 ≥ 0)}     
	i = 1
       {I}   (RA)

6: {I}
	n = 0
       {I}        (RA)

7:{ListQ[w] ∧ 
              IntegerQ[1] ∧ (Length[w] + 1 - 1 ≥ 0)}
	i = 1; n = 0
      {I}    (RCS[5, 6])

8:ListQ[w]⇒(ListQ[w] ∧ 
                  IntegerQ[
                    1] ∧ (Length[w] + 1 - 1 ≥ 0))    (RV)

9:{ListQ[w]}
	i = 1; n = 0
      {I}    (RC1[7, 8])



Parte III [corpo do ciclo guardado preserva condição invariante e reduz expressão variante]

10 : {ListQ[w] ∧ 
              IntegerQ[
                i + 1] ∧ (Length[w] - i ≥ 
                  0) ∧ (Length[w] - i < N)}  
	Null  
	{ListQ[w] ∧ 
                IntegerQ[
                  i + 1] ∧ (Length[w] - i ≥ 
                    0) ∧ (Length[w] - i < N)}   (RN)

11 : (I ∧ (τ == N) ∧ (i ≠ 
                  Length[w] + 1) ∧ (w[[i]] ≤ 
                  x))
   ⇒
(ListQ[w] ∧ 
                  IntegerQ[
                    i + 1] ∧ (Length[w] - i ≥ 
                      0) ∧ (Length[w] - i < N))   (RV)

12 : {I ∧ (τ == N) ∧ (i ≠ 
                  Length[w] + 1) ∧ (w[[i]] ≤ 
                  x)}  
	Null  
      {ListQ[w] ∧ 
                IntegerQ[
                  i + 1] ∧ (Length[w] - i ≥ 
                    0) ∧ (Length[w] - i < N)}   (RC1[10, 11])

13:{ListQ[w] ∧ 
                IntegerQ[
                  i + 1] ∧ (Length[w] - i ≥ 
                    0) ∧ (Length[w] - i < N)}  
	n = n + 1  
      {ListQ[w] ∧ 
                IntegerQ[
                  i + 1] ∧ (Length[w] - i ≥ 
                    0) ∧ (Length[w] - i < N)}   (RA)

14 : (I ∧ (τ == N) ∧ (i ≠ 
                  Length[w] + 1) ∧ (w[[i]] > x))
   ⇒
(ListQ[w] ∧ 
                  IntegerQ[
                    i + 1] ∧ (Length[w] - i ≥ 
                      0) ∧ (Length[w] - i < N))   (RV)

15:{I ∧ (τ == N) ∧ (i ≠ 
                    Length[w] + 1) ∧ (w[[i]] > x)}  
	n = n + 1  
      {ListQ[w] ∧ 
                IntegerQ[
                  i + 1] ∧ (Length[w] - i ≥ 
                    0) ∧ (Length[w] - i < N)}   (RC1[13, 14])

16:{I ∧ (τ == N) ∧ (i ≠ 
                    Length[w] + 1)}  
	If[w[[i]] > x, n = n + 1, Null]  
	{ListQ[w] ∧ 
                IntegerQ[
                  i + 1] ∧ (Length[w] - i ≥ 
                    0) ∧ (Length[w] - i < N)}   (RI[12, 15])

17:{ListQ[w] ∧ 
                IntegerQ[
                  i + 1] ∧ (Length[w] - i ≥ 
                    0) ∧ (Length[w] - i < N)}   
	i = i + 1   
	{I ∧ (τ < N)}     (RA)

18:{I ∧ (τ == N) ∧ (i ≠ 
                    Length[w] + 1)}   
	If[w[[i]] > x, n = n + 1, Null]; i = i + 1    
	{I ∧ (τ < N)}    (RS[16, 17])


Parte IV [corpo do ciclo guardado termina]

19:Ω[True,n = n + 1]    (RCA)

20:(True ∧ (w[[i]] > x))⇒True    (RV)

21:Ω[True ∧ (w[[i]] > x),n = n + 1]    (RC3[19, 20])

22:Ω[True,Null]    (RCN)

23:(True ∧ (w[[i]] ≤ x))⇒True    (RV)

24:Ω[True ∧ (w[[i]] ≤ x),Null]    (RC3[22, 23])

25:Ω[True,If[w[[i]] > x, n = n + 1, 
                Null]]    (RCI[21, 24])

26:Ω[True,i = i + 1]    (RCA)

27:{True}If[w[[i]] > x, n = n + 1, Null]{True}    (LEMA)

28:Ω[True,   
	If[w[[i]] > x, n = n + 1, Null]; i = i + 1]    (RCI[25, 26, 27])

29:(I ∧ G)⇒True    (RV)

30:Ω[I ∧ G,   
	If[w[[i]] > x, n = n + 1, Null]; i = i + 1]    (RC3[28, 29])


Parte V [programa termina]:

31:I⇒(τ ≥ 0)   (RV)

32:Ω[I,While[i ≠ Length[w] + 1, 
                If[w[[i]] > x, n = n + 1, Null]; i = i + 1]]   (RCW[30, 18, 31])

33:Ω[ListQ[w],
	i = 1; n = 0; 
              While[i ≠ Length[w] + 1, 
                If[w[[i]] > x, n = n + 1, Null]; i = i + 1]]    (RCS[4, 9, 32])




PROVA de 2.,  isto é, que a asserção {True} 
        P {n == # {j : (w[[j]] > x)⋀(1 ≤ 
                        j ≤ Length[w])}} é teorema do Cálculo de Hoare para correcção parcial:


Invariante: (n == # {j : (w[[j]] > x)⋀(1 ≤ 
                      j ≤ i - 1)})

Parte I [inicialização estabelece a condição invariante]:

1:{0 == # {j : (w[[j]] > 
                            x)⋀(1 ≤ j ≤ 
                            1 - 1)}}   
	i = 1   
      {0 == # {j : (w[[j]] > 
                            x)⋀(1 ≤ j ≤ 
                            i - 1)}}    (RA)

2:{0 == # {j : (w[[j]] > 
                            x)⋀(1 ≤ j ≤ 
                            i - 1)}}  
	n = 0 
      {n == # {j : (w[[j]] > 
                            x)⋀(1 ≤ j ≤ 
                            i - 1)}}    (RA)

3:{0 == # {j : (w[[j]] > 
                            x)⋀(1 ≤ j ≤ 
                            1 - 1)}}  
	i = 1; n = 0  
      {n == # {j : (w[[j]] > 
                            x)⋀(1 ≤ j ≤ 
                            i - 1)}}    (RS[1, 2])

4:True⇒(0 == # {j : (w[[j]] > 
                              x)⋀(1 ≤ j ≤ 
                              1 - 1)})    (RV)

5:{True}  
	i = 1; n = 0  
      {n == # {j : (w[[j]] > 
                            x)⋀(1 ≤ j ≤ 
                            i - 1)}}    (RC1[3, 4])



Parte II [corpo do ciclo guardado preserva a condição invariante]

6:{n + 
                  1 == # {j : (w[[j]] > 
                            x)⋀(1 ≤ j ≤ 
                            i)}}  
	n = n + 1  
      {n == # {j : (w[[j]] > 
                            x)⋀(1 ≤ j ≤ 
                            i)}}   (RA)

7:((n == # {j : (w[[j]] > 
                                x)⋀(1 ≤ j ≤ 
                                i - 1)}) ∧ (w[[i]] > x))⇒(n + 
                    1 == # {j : (w[[j]] > 
                              x)⋀(1 ≤ j ≤ 
                              i)})   (RV)

8:{(n == # {j : (w[[j]] > 
                                x)⋀(1 ≤ j ≤ 
                                i - 1)}) ∧ (w[[i]] > x)}  
	n = n + 1  
      {n == # {j : (w[[j]] > 
                            x)⋀(1 ≤ j ≤ 
                            i)}}   (RC1[6, 7])

9 : {n == # {j : (w[[j]] > 
                          x)⋀(1 ≤ j ≤ 
                          i)}}  
	Null  
      {n == # {j : (w[[j]] > 
                            x)⋀(1 ≤ j ≤ 
                            i)}}   (RN)

10:\((\((n == # {j : \((w[\([j]\)] > 
                                x)\)⋀\((1 ≤ j ≤ 
                                i - 1)\)})\) ∧ \((w[\([i]\)] ≤ x)\))\)⇒(n == # {j : (w[[j]] > 
                              x)⋀(1 ≤ j ≤ 
                              i)})   (RV)

11 : {(n == # {j : (w[[j]] > 
                              x)⋀(1 ≤ j ≤ 
                              i - 1)}) ∧ (w[[i]] ≤ 
                  x)}  
	Null  
	{n == # {j : (w[[j]] > 
                            x)⋀(1 ≤ j ≤ 
                            i)}}   (RC1[9, 10])

12:{n == # {j : (w[[j]] > 
                            x)⋀(1 ≤ j ≤ 
                            i - 1)}}  
	If[w[[i]] > x, n = n + 1, Null]  
	{n == # {j : (w[[j]] > 
                            x)⋀(1 ≤ j ≤ 
                            i)}}   (RI[8, 11])

13:{n == # {j : (w[[j]] > 
                            x)⋀(1 ≤ j ≤ 
                            i)}}   
	i = i + 1   
	{n == # {j : (w[[j]] > 
                            x)⋀(1 ≤ j ≤ 
                            i - 1)}}     (RA)

14:{n == # {j : (w[[j]] > 
                            x)⋀(1 ≤ j ≤ 
                            i - 1)}}   
	If[w[[i]] > x, n = n + 1, Null]; i = i + 1    
	{n == # {j : (w[[j]] > 
                            x)⋀(1 ≤ j ≤ 
                            i - 1)}}    (RS[12, 13])

15:((n == # {j : (w[[j]] > 
                                x)⋀(1 ≤ j ≤ 
                                i - 1)}) ∧ (i ≠ 
                    Length[w] + 1))⇒(n == # {j : (w[[j]] > 
                              x)⋀(1 ≤ j ≤ 
                              i - 1)})    (RV)

16:{(n == # {j : (w[[j]] > 
                                x)⋀(1 ≤ j ≤ 
                                i - 1)}) ∧ (i ≠ 
                    Length[w] + 1)}   
	If[w[[i]] > x, n = n + 1, Null]; i = i + 1    
	{n == # {j : (w[[j]] > 
                            x)⋀(1 ≤ j ≤ 
                            i - 1)}}    (RC1[14, 15])



Parte III [programa estabelece condição final]:

17:{n == # {j : (w[[j]] > 
                            x)⋀(1 ≤ j ≤ 
                            i - 1)}}   
	While[i ≠ Length[w] + 1, 
          If[w[[i]] > x, n = n + 1, Null]; i = i + 1]  
	{(n == # {j : (w[[j]] > 
                                x)⋀(1 ≤ j ≤ 
                                i - 1)}) ∧ (i == 
                    Length[w] + 1)}    (RW[16])

18:{True}   
	i = 1; n = 0; 
        While[i ≠ Length[w] + 1, 
          If[w[[i]] > x, n = n + 1, Null]; i = i + 1]  
	{(n == # {j : (w[[j]] > 
                                x)⋀(1 ≤ j ≤ 
                                i - 1)}) ∧ (i == 
                    Length[w] + 1)}    (RS[5, 17])

19:((n == # {j : (w[[j]] > 
                                x)⋀(1 ≤ j ≤ 
                                i - 1)}) ∧ (i == 
                    Length[w] + 1))⇒(n == # {j : (w[[j]] > 
                              x)⋀(1 ≤ j ≤ 
                              Length[w])})    (RV)

20:{True}   
	i = 1; n = 0; 
        While[i ≠ Length[w] + 1, 
          If[w[[i]] > x, n = n + 1, Null]; i = i + 1]  
	{n == # {j : (w[[j]] > 
                            x)⋀(1 ≤ j ≤ 
                            Length[w])}}    (RC2[18, 19])

Exercício
Considere-se o programa SquareEMultiply correspondente ao corpo da seguinte função:

Function[{x, y}, 
        Module[{n, m, r}, 
n = x; 
m = 
            y; 
r = 1; 
While[
            m ≠ 0, 
If[
              OddQ[m], 
r = r×n; 
              m = m - 1, 
n = (n^2); 
              m = (m/2)]]; 
r]]

1. Mostre que {True}SquareEMultiply{r == (x^y)} é teorema do Cálculo de Hoare para correcção parcial.

2. Mostre que Ω[IntegerQ[x] ∧ IntegerQ[y] ∧ 
              y ≥ 0,SquareEMultiply] é teorema do Cálculo de Hoare para correcção total.