Verificação Formal de Software

1.3. Conectivos🔗

Conectivos constroem proposições compostas a partir de proposições mais simples, e a Tabela 1.3.1 nomeia os cinco.

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

Tabela 1.3.1. Os cinco conectivos, com os seus símbolos e leituras.

O valor de verdade de uma proposição composta depende apenas dos valores de verdade das suas partes. A Tabela 1.3.2 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

Tabela 1.3.2. Os valores de verdade dos cinco conectivos.

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 coluna da disjunção merece a mesma atenção. A disjunção é inclusiva, então P ∨ Q é verdadeira quando os dois disjuntos o são.