Prezados Hermógenes e Valéria, Em matemática, quando você quer provar A => B por "contrapositivo", você prova \neg B => \neg A. Ou seja, você usa que
\neg B => \neg A => (A => B) é válida. Isso é equivalente a adicionar a dupla negação ao seu sistema lógico. Eu aprendi assim: que a "lei do contrapositivo" era \neg B => \neg A \equiv (A => B) sendo que a recíproca é obviamente válida em lógica intuicionista. Nunca, entretanto, pensei a respeito da terminologia. Longe de mim querer "make a point" ou etc. Não tenho problema em deixar de usar o termo na próxima palestra :) Obrigada por assistir, btw. Abraços, Elaine. 2017-10-24 5:39 GMT-03:00 Hermógenes Oliveira < hermogenes.olive...@student.uni-tuebingen.de>: > 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/di > map.ufrn.br/group/logica-l/. > Para ver esta discussão na web, acesse https://groups.google.com/a/di > map.ufrn.br/d/msgid/logica-l/20171024103907.Horde.StcBDM_NG > GFij6cUvk478_N%40webmail.uni-tuebingen.de. > -- Elaine. ------------------------------------------------- Elaine Pimentel - DMAT/UFRN Address: Departamento de Matemática Universidade Federal do Rio Grande do Norte Campus Universitário - Av. Senador Salgado Filho, s/nº Lagoa Nova, CEP: 59.078-970 - Natal - RN Phone: +55 84 3215-3820 http://sites.google.com/site/elainepimentel/ Lattes: http://lattes.cnpq.br/3298246411086415 -------------------------------------------------------- -- 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/CAHQVs%2BVNVSj_NEZHiFF%2BcqXOhw0sU58HD9KMoJXJRptOusTE1A%40mail.gmail.com.
