... Haha, Tem um detalhe sutil aí na prova que o Petrúcio apresentou,
Apesar de ser "raciocínio calculacional", pra provar o que ela quer provar, digamos assim, precisa do Axioma da Escolha, No sentido de que o argumento essencialmente diz que: "Dada uma funcao de X em Partes de X, ela nao tem inversa à direita" Só que a implicacao "não ter inversa à direita" --> "não é sobrejetora" é equivalente a "a função é sobrejetora" ----> "tem inversa à direita" e esta última é uma equivalência do Axioma da Escolha !!!! Gostei hehe... Atés, bom final de semana, []s Samuel Em sexta-feira, 5 de março de 2021 às 17:29:22 UTC-4, Petrucio Viana escreveu: > Oi João, > acredito que o artigo ao qual ele está se referindo seja este aqui: > > On calculational proofs > <https://www.sciencedirect.com/science/article/pii/S0168007201000598> > > 1. Vladimir Lifschitz > > Annals of Pure and Applied Logic > <https://www.sciencedirect.com/science/journal/01680072> > Volume 113, Issues 1–3 > <https://www.sciencedirect.com/science/journal/01680072/113/1>, 27 > December 2001, Pages 207-224 > > > Em sex., 5 de mar. de 2021 às 17:04, Joao Marcos <boto...@gmail.com> > escreveu: > >> Belo exemplo do "raciocínio calculacional" de Dijkstra, Petrucio! >> >> Em um post recente na FOM (do qual eu tirei o link que enviei aqui na >> lista esta semana para o arquivo do Dijkstra) o Vladik Kreinovich >> escreveu: >> "Examples of calculational proofs in Edsger’s writings were so >> impressive that I even asked myself whether every possible use of >> natural deduction in classical logic can be replaced, in principle, by >> calculational reasoning. The answer turned out to be yes (published in >> the Annals of Pure and Applied Logic in 2002)." >> https://cs.nyu.edu/pipermail/fom/2021-March/022524.html >> >> Você saberia dizer a qual paper no APAL ele se refere? >> >> Abraços, >> Joao Marcos >> >> On Fri, Mar 5, 2021 at 3:16 PM Petrucio Viana <petruci...@id.uff.br> >> wrote: >> > >> > Boa tarde, >> > segue uma maneira "intuitiva" (construtiva?), devida a Dijkstra e >> Misra, de provar o teorema de Cantor. >> > Ela condensa a ideia usada na prova que o Samuel apresentou, exibindo >> de maneira natural o conjunto que "estraga" a bijeção. >> > >> > Teorema: Para todas as funções F de X em P(X) e g de P(X) em X, Fog =/= >> Id. >> > >> > Prova: >> > Sejam F e g tais funções. >> > >> > Temos que: >> > >> > Fog =/= Id >> > >> > é equivalente a >> > >> > existe Y em P(X) tal que Y =/= F(g(Y)) >> > >> > é consequência de >> > >> > existe Y em P(X) tal que [g(Y) pertence a Y não é equivalente a g(Y) >> pertence a F(g(Y)] >> > >> > é consequência de >> > >> > existe Y em P(X) tal que para todo x {[x pertence a Y] é equivalente a >> [x não pertence a F(x)]} >> > >> > tomando (o candidato natural exposto pela passagem acima) Y = { x : x >> não pertence a F(x) } isto é equivalente a >> > >> > verdadeiro. >> > QED >> > >> > Em qui., 4 de mar. de 2021 às 17:52, Joao Marcos <boto...@gmail.com> >> escreveu: >> >> >> >> > Aí que vem a única análise de casos ("uso do Terceiro Excluído", >> concordo...) >> >> >> >> E por falar em Terceiro Excluído, Samuel, você saberia explicar em >> >> termos pedestres até onde conseguiríamos levar o argumento da >> >> diagonalização, digamos, em *CZF*, se assumirmos o axioma segundo >> >> o qual todo conjunto é subcontável? >> >> >> >> []s, Joao Marcos >> >> >> >> >> >> -- >> >> http://sequiturquodlibet.googlepages.com/ >> >> >> >> -- >> >> 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+u...@dimap.ufrn.br. >> >> Para ver esta discussão na web, acesse >> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LghbEJLz_key_MLrks16WSXx%3D4NeYsj%3D08d2NO44HQKdA%40mail.gmail.com >> . >> >> >> >> -- >> http://sequiturquodlibet.googlepages.com/ >> >> -- >> 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+u...@dimap.ufrn.br. >> > Para ver esta discussão na web, acesse >> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LigzB4LaC3G8h_HtijEHP2-3%3D-wfO03tjETohpEnUir4g%40mail.gmail.com >> . >> > -- 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 ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/4f1998a2-2bcf-40ee-9114-976144297ccan%40dimap.ufrn.br.
