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 <[email protected]> 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 <[email protected]> > 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 [email protected]. >> 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 [email protected]. 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.
