Introdução bicondicional

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa

Em lógica proposicional, introdução bicondicional é uma regra de inferência válida. Ele permite inferir uma bicondicional de duas declarações condicionais. A regra torna possível introduzir uma declaração bicondicional em uma prova lógica. Se é verdade, e se é verdade, então pode-se inferir que é verdade. Por exemplo, da declaração "se eu estou respirando, então eu estou vivo" e "se eu estou vivo, então eu estou respirando", pode-se inferir que "eu estou respirando se e somente se eu estiver vivo". Introdução bicondicional é o inverso de eliminação bicondicional. A regra pode ser indicada formalmente como:

onde a regra é que sempre que as instâncias de "" e "" aparecer nas linhas de prova, "" pode substituí-la na linha seguinte.

Notação formal[editar | editar código-fonte]

A regra da introdução bicondicional pode ser escrita em notação sequente:

onde é um símbolo da metateoria da lógica que significa que é um acarretamento quando e estão ambos em uma prova;

ou como uma declaração de uma verdade tautologica ou teorema da lógica proposicional:

onde , e são proposições expressas em algum sistema formal.

References[editar | editar código-fonte]