Dê uma prova formal para cada argumento:
Questão-06.
Premissas:
(forall x)(Ax Bx vee Cx),
(forall x)(Bx Cx)
Conclusão: (forall x)(Ax Cx)

Passo 1

O enunciado fornece as premissas
forall x,(A(x)to (B(x)lor C(x)))
forall x,(B(x)to C(x))
e pede para provar
forall x,(A(x)to C(x))
O conteúdo usado será lógica de predicados de primeira ordem, com as regras de eliminação e introdução do quantificador universal, introdução da implicação e eliminação da disjunção (prova por casos).

Passo 2

Seja c um indivíduo arbitrário do domínio. Vamos mostrar primeiro
A(c)to C(c),
para então aplicar generalização universal e obter forall x,(A(x)to C(x)).

Passo 3

Assuma provisoriamente
A(c)

Passo 4

Da premissa
forall x,(A(x)to (B(x)lor C(x)))
por eliminação do quantificador universal, obtém-se
A(c)to (B(c)lor C(c))

Passo 5

Da premissa
forall x,(B(x)to C(x))
por eliminação do quantificador universal, obtém-se
B(c)to C(c)

Passo 6

De A(c) e A(c)to (B(c)lor C(c)), por modus ponens, segue
B(c)lor C(c)

Passo 7

Para extrair C(c) de B(c)lor C(c), fazemos prova por casos:
  1. Suponha B(c). Então, de B(c) e B(c)to C(c) por modus ponens, vem C(c)
  2. Suponha C(c). Imediatamente obtemos C(c)

Passo 8

Pela eliminação da disjunção (prova por casos) com os dois subproofs acima, concluímos
C(c)

Passo 9

Descarregando a suposição de A(c) pela introdução da implicação, temos
A(c)to C(c)

Passo 10

Finalmente, como c foi arbitrário, aplicamos a introdução do quantificador universal e obtemos
forall x,(A(x)to C(x)),
que é a conclusão desejada.

Resposta

forall x,(A(x)to C(x))

Exercícios relacionados