Prova de dedução natural com quantificadores

Question

Aqui está uma prova de dedução natural onde minhas respostas estão no vermelho.

Tenho dúvidas nas seguintes linhas:

Linha 8: podemos apresentar um $\lor$operadora aqui? Nós temos$\exists xQ(x)$ então com $\lor$ introdução podemos dizer tem ou qualquer coisa certa, porque já é verdade?

Linha 12 e 13: Nós eliminamos $\exists x (P(x) \rightarrow Q(x))$na linha 1 porque há mais de um elemento nesta instrução. E nós apresentamos$\exists$ em 13 porque provamos que há apenas um elemento que satisfaz isso.

Mais alguma coisa no vermelho parece incorreta?

O acima parece correto? Estou lutando com o$\exists$ parte deste tipo de provas.

Answer 1

A linha 8 está correta, exatamente pelo motivo que você disse. Mas existem outros erros na sua prova, a maioria deles está relacionada à forma de gerenciar o quantificador existencial.

A grande caixa externa (linhas 3-12) é o que você faz para eliminar o quantificador existencial $\exists x$ da premissa 1 ($\exists x (P(x) \to Q(x))$) Portanto, as fórmulas nas linhas 12 e 13 devem coincidir e a linha 13 , não a linha 12, é a regra$\exists_\text{elim}$ que fecha a caixa.

Então, na linha 13, a fórmula está correta, mas a regra de inferência é $\exists_\text{elim}$ (1, 3-12).

A linha 3 abre a caixa para eliminar o quantificador existencial $\exists x$ da premissa 1 ($\exists x (P(x) \to Q(x))$), portanto, a fórmula na linha 3 (a suposição) deve ser aquela na linha 1 sem o quantificador existencial e com um termo genérico $c$ ao invés de $x$, ie $P(c) \to Q(c)$.

Na linha 6, você não pode aplicar $\to_\text{elim}$ a uma fórmula que não é da forma $A \to B$ (a premissa 1 tem a forma $\exists x (A \to B)$, que não é o necessário). O problema é que na sua tentativa de prova você não tinha essa fórmula. Mas agora nós temos (linha 3), então a regra de inferência correta é$\to_\text{elim}$ (3, 5).

Na linha 9 a suposição no início da regra para eliminar a disjunção $P(c) \lor \lnot P(c)$ deve ser exatamente uma das duas fórmulas na disjunção, neste caso $\lnot P(c)$, e não $\lnot P(x)$.

Na linha 12, a fórmula está correta, mas a regra de inferência é $\lor_\text{elim}$(4, 5-11). Na verdade, as duas caixas internas são o que você faz para eliminar a disjunção na linha 4, e a linha 12 é a regra$\lor_\text{elim}$ que fecha as duas caixas (e a fórmula na linha 12 é a mesma que as últimas nas duas caixas internas, linhas 8 e 11).

Answer 2

Suponha que:
existe x com (p (x) implica q (x)).
Prove:
(p (x) implica q (x)) implica
(não-p (x) ou q (x)).
Assim:
existe x com (not-p (x) ou q (x)).
Como discutido anteriormente, onde
existe x com não-p (x) ou
existe x com q (x).