ProofWeb

Working with ProofWeb

Tips on First Ordem Logic


Require Import ProofWeb.

(* Exemplos na lógica proposicional *)

Variables A B C : Prop.

(*Primeiro uma demonstração usando apenas regras "Backward" 
(para trás - seguindo da conclusão às premissas) *)

Theorem example_01 : A /\ B -> B /\ A.
Proof.
imp_i H.
con_i.
con_e2 (A).

(* Insere um "A" numa conjunção com B *) 

ass H.
con_e1 (B).
ass H.
Qed.

(* mesma demonstração usando o máximo de regras "Forward" possíveis 
(para frente - seguindo das premissas à conclusão) *) 


Theorem example_02 : A /\ B -> B /\ A.
Proof.
imp_i H.
insert H1 (A).

(* insere a hipótese A para que ela possa ser usada na introdução da conjunção para frente *)

f_con_e1 H.
insert H2 (B).
f_con_e2 H.
f_con_i H2 H1.
Qed.

(* Utilizando táticas mistas  "Forward" e  "Backward" (para frente e para trás) *)

Theorem example_03 : A /\ B -> B /\ A.
Proof.
imp_i H.
con_i.
f_con_e2 H.
f_con_e1 H.
Qed.

(* Um exemplo com a eliminação da disjunção usando apenas táticas "Backward" *)

Theorem example_04 : A \/ B -> B \/ A.
Proof.
imp_i H.
dis_e (A \/ B) H1 H2.
ass H.
dis_i2.
ass H1.
dis_i1.
ass H2.
Qed.

(* ... e uma solução bem menor usando apenas táticas "Forward" *) 

Theorem example_05 : A \/ B -> B \/ A.
Proof.
imp_i H.
f_dis_e H H1 H2.

(* Para reduzir o tamanho da derivação, a eliminação da disjunção 
deve ser aplicada antes de outras regras... *)

f_dis_i2 H1.

(* Nesta caso, se a eliminação da disjunção fosse utilizada depois de outras regras, 
não se conseguiria demonstrar *)

f_dis_i1 H2.
Qed.

(* Exemplo de uma demonstração intuicionista com várias negações *)

Theorem example_06 : ~~(~~A -> A).
Proof.
neg_i H.
insert H1 (~~A -> A).
imp_i H2.
insert H3 (~A).
neg_i H4.
neg_e (~~A -> A).

(* Aplicada regra "Backward" em que surgem as duas fórmulas eliminadas pela negação *) 

ass H.
imp_i H5.
ass H4.
fls_e.
f_neg_e H2 H3.
f_neg_e H H1.
Qed.

(* Demonstrando a Lei do terceiro excluido *)

Theorem example_07 : A \/ ~A.
Proof.
PBC H0.

(*... assim como a Eliminação da Disjunção, deve-se usar o Absurdo Clássico antes 
de outras regras... *)

(* a idéia é ter o máximo de hipóteses para se trabalhar na demonstração, 
e as regras PBC e dis_e fazem isso... *)

neg_e (A \/ ~ A).
ass H0.

(* Observe que estamos com a mesma fórmula, mas agora temos uma hipótese H0 adicional *)

dis_i2.
neg_i H1.
neg_e (A \/ ~ A).
ass H0.

(* mais uma vez estamos com a mesma fórmula, mas agora temos duas hipóteses H0 e H1 *)

dis_i1.
ass H1.

(* Pronto!!! *)
Qed.