Valeria de Paiva <valeria.depa...@gmail.com> escreveu:
[... ] (¬φ → ¬χ) → (χ → φ) (Law of contraposition) mas essa ultima assercao nao 'e o que eu chamaria de contraposicao. Contraposicao usual 'e valida em logical intuicionista. o que acontece e' que essa assercao combina contraposicao com eliminacao da negacao dupla, ou seja: contraposicao devia ser (A → B) → (¬B → ¬A) mas quem escreveu o artigo em vez de dizer (¬A → ¬B) → (¬¬B → ¬¬A), removeu a dupla negacao, ficando com (¬A → ¬B) → (B → A) dai que isso 'e mesmo nao-derivavel em IL, pois inclui double negation elimination, junto com a contraposicao. voces concordam? ou eu estou "esquecendo" alguma coisa importante?
Eu concordo contigo, Valéria. Tradicionalmente, "contraposição" é o nome dado à (A → B) → (¬B → ¬A). Curiosamente, a primeira vez que eu vi a "contraposição" apresentada como divisora de águas entre lógica clássica e intuicionista foi no vídeo da palestra da Elaine Pimentel, "A semantical view of proof systems", no Filomena 2017 (divulgado recentemente nesta lista). Na ocasião, pensei "Peraí...", pausei o vídeo e raciocinei basicamente o que você apresentou acima. A Elaine apresentou o negócio como uma regra de inferência que permitiria estabelecer A → B por meio de derivação de ¬A a partir de ¬B. Devo admitir, contudo, que apresentado assim, como regra de inferência, o nome "contraposição" não me parece *tão* estranho. Eu não sei porque (¬A → ¬B) → (B → A), com o nome "contraposição", tem sido usado como diferenciador entre lógica clássica e intuicionista, mas isso parece ser um desenvolvimento recente (a palestra da Elaine e o artigo da Wikipédia sendo os únicos casos que me lembro até agora). Talvez tenha aparecido em algum livro ou artigo e as pessoas passaram a adotar essa caracterização. Eu não gosto muito, pois tem grande potencial para causar confusão.
tem mais alguma coisa errada no artigo? eu estou querendo me lembrar da relacao entre implicacao e disjuncao. essas estao certas? Disjunction versus implication: (φ ∨ ψ) → (¬φ → ψ)
Esta está correta. Basta aplicar ∨E com premissa menor ψ, obtida, respectivamente, (1, [φ]) por ECQ a partir de φ (descartado) e ¬φ, e (2, [ψ]) ψ (descartado). Daí é só introdizir as implicações.
(¬φ ∨ ψ) → (φ → ψ)
Esta tambeḿ está correta. Basta substituir φ por ¬φ na justificativa acima. Mas talvez a relação mais interessante entre disjunção e implicação seja dada por φ ∨ ψ ⇔ ∀χ (φ → χ) → ((ψ → χ) → χ)) que é, basicamente, uma tradução da regra de eliminação em segunda ordem (com quantificação sobre sentenças), também chamado de sistema Fₐₜ na literatura recente. Essa relacão é inclusive usada no artigo da Wikipédia que você mencionou para oferecer um *esquema* axiomático alternativo para a lei do terceiro excluído (φ ∨ ¬φ): (φ → χ) → ((¬φ →χ) → χ). -- Hermógenes Oliveira -- Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google. Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscr...@dimap.ufrn.br. Para postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br. Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/. Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/20171024103907.Horde.StcBDM_NGGFij6cUvk478_N%40webmail.uni-tuebingen.de.
