discussão animada sobre "What is a Formal Proof?"

[Joao Marcos]

Eis um blog post fascinante, seguido de uma interessante discussão
(que ainda não acabou) --- particularmente recomendado para aqueles
que confundem "demonstrações formais" com "derivações em sistemas
dedutivos", ou para aqueles interessados na distinção entre
"argumentações", "representações de demonstrações", e "demonstrações"
de fato:

What is a Formal Proof?
-- Mike Shulman
https://golem.ph.utexas.edu/category/2016/08/what_is_a_formal_proof.html

O que segue é uma resposta para o post acima, que propõe critérios a
serem satisfeitos por "demonstrações formais" e colabora para a
discussão sobre se as demonstrações seriam "termos / objetos / dados"
ou mais propriamente "processos", sobre a relação entre a
"demonstração" e o "conhecimento" de fatos matemáticos, e sobre como
"demonstrações completas" seriam demasiado grandes para serem
armazenadas ou mesmo comunicadas:

What is a Formal Proof?
-- Andrzej Bauer
http://math.andrej.com/2016/08/09/what-is-a-formal-proof/


JM

[Joao Marcos]

Corrigindo:

> Andrzej Bauer

deveria ser "Andrej Bauer". Sorry.

JM

[Bruno Lopes]

A quem se interessar pelo tema, o artigo "Informal proof, formal proof, formalism" de Alan Weir pode ser de interesse.

http://dx.doi.org/10.1017/S1755020315000234

Abraços,

Bruno.

JM

--
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+unsubscribe@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logi...@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/CAO6j_LiEWSxYhz5_9LVYamX48W6X7d_2BaSkjPxHx5pP%3DzkCiQ%40mail.gmail.com.

--

Bruno Lopes

http://www.ic.uff.br/~bruno