Comando: Instantiate

Parte I - Uso do instante para eliminar quantificador existencial da conclusão.

Problema:

As vezes, para concluir uma prova (teorema da inicialização, por exemplo), pode ser necessário resolver um problema com o formato:

[set of premiss \implies] \exist variable : TYPE @ predicate

Nesta situação, o quantificador existencial precisa ser eliminado. Para realizar isto, o especificador precisa encontrar uma witness para eliminar o quantificador existencial utilizando o comando instantiate. Em alguns casos, é necessário definir a witness para depois poder utilizá-la. Na notação acima, o que está entre colchetes é opcional.


Uma vez em posse da witness, utiliza-se o comando instantiate para instrui o provador a aplicar a one-point-rule e transformar o predicado para o predicado.

[set of premiss \implies] witness \in TYPE \land predicate[witness/variable]
\lor \exist variable : TYPE @predicate

O segundo passo da transformação é mostrado a seguir e é aplicado se a parte opcional destaca entre colchetes estiver presente no predicado.

set of premiss \land (\not (witness \in TYPE \land predicate[witness/predicate])) \implies \exist variable @predicate

Seja C um predicado contendo um quantificador existencial. Seja A um conjunto de premissas. Então, o resultado de um comando de instanciação da variável declarada em C resulta nos seguintes passos de prova:

1. A => C
2. A => B or C
3. A and NOT(B) => C

Do passo 1 para o 2 é aplicado a One-Point-Rule:

Do passo 2 para o passo 3 é aplicado transformação lógica.