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 <[email protected]> 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 <[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 > . > -- 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/CACRvmVTPUvRWCjLJL52%3D4dQSpMroxys7HfcXXCiJAjziEgT16Q%40mail.gmail.com.
