Verificação Formal de Software

1.3. Conectivos🔗

Conectivos constroem proposições compostas a partir de proposições mais simples.

Símbolo

Nome

Leitura

¬P

negação

não P

P ∧ Q

conjunção

P e Q

P ∨ Q

disjunção

P ou Q

P → Q

implicação

se P então Q

P ↔ Q

bicondicional

P se e somente se Q

O valor de verdade de uma proposição composta depende apenas dos valores de verdade das suas partes. A tabela abaixo define os cinco conectivos, com V para verdadeiro e F para falso.

P

Q

¬P

P ∧ Q

P ∨ Q

P → Q

P ↔ Q

V

V

F

V

V

V

V

V

F

F

F

V

F

F

F

V

V

F

V

V

F

F

F

V

F

F

V

V

Duas linhas da coluna da implicação merecem atenção. Quando P é falso, P → Q é verdadeira independentemente de Q. Uma implicação nada afirma sobre os casos em que o seu antecedente falha, então esses casos não podem refutá-la. A disjunção é inclusiva, então P ∨ Q é verdadeira quando os dois disjuntos o são.