Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

Oi Hermógenes, > Existe uma maneira mais construtiva de se definir a negação. Basta > > tomar \neg A como 'A não é habitado', usando tipos isso seria dado por > > uma equivalência homotopica entre A e empty (não precisa de universos > > para fazer isso). > > Sim, claro. Em termos lógicos, essa

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

Viva, Valeria: > gostaria de entender melhor o que JM quer dizer com: >>note com efeito que a regra de substituição uniforme não se aplica ao >> símbolo de absurdo, como um *conectivo* nulário, tal como se aplica a >> sentenças atômicas. > > da' pra repetir a ideia aqui? Vou tentar. A

[Logica-l] [OFF] sobre o valor da pesquisa fundamental

Nestes tempos sombrios de drásticos cortes públicos no fomento da pesquisa brasileira, alguns colegas podem achar interesssante ler este artigo curtinho do Helmut Schwarz, presidente da Fundação Humboldt (entrando agora no último ano do seu mandato): On the usefulness of useless knowledge

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

ok mais 2 centavos daqui de longe: gostaria de entender melhor o que JM quer dizer com: >note com efeito que a regra de substituição uniforme não se aplica ao símbolo de absurdo, como um *conectivo* nulário, tal como se aplica a sentenças atômicas. da' pra repetir a ideia aqui? como eu passei

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

Oi JM e Hermógenes, Um breve comentário sobre o top. Em uma mensagem anterior, JM escreveu: Hummm... Dualmente, qual seria a regra de eliminação do top? A regra > de que "sob nenhuma circunstância podemos eliminar o top"? Parece-me > um simples forçação de barra. Podemos eliminá-lo sim e

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

Salve, Hermógenes: Obrigado pela resposta. >>> Bem, o problema é o que colocar no lugar de ECQ que, ao mesmo tempo, >>> (1) seja razoável se chamar de "negação" (ou, melhor, "absurdo", no >>> caso da negação definida pelo absurdo), e (2) seja construtivamente >>> justificável. >>> >>> Se

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

Joao Marcos escreveu: >> Bem, o problema é o que colocar no lugar de ECQ que, ao mesmo tempo, >> (1) seja razoável se chamar de "negação" (ou, melhor, "absurdo", no >> caso da negação definida pelo absurdo), e (2) seja construtivamente >> justificável. >> >> Se permanecemos

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

Bruno Bentzen escreveu: > Oi Hermógenes, Olá, Bruno. > [...] > > PS: Posso estar enganado, mas acho um pouco equivocado e confuso usar > a palavra “completude” (um termo de cunho técnico ou meta-matemático) > neste caso quando estamos nos tratando de uma semântica

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

Viva, Hermógenes: Obrigado pela resposta. >>> Eu, pessoalmente, acho ECQ um princípio *muito* suspeito. O >>> difícil é que, sem ECQ, um construtivista ficaria basicamente sem >>> negação (ao estilo do cálculo mínimo de Johansson), ou a negação >>> cessaria de ser um operador *lógico*. >> >>

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

Fernando Yamauti escreveu: > Oi Hermógenes, Olá, Fernando. > Eu, pessoalmente, acho ECQ um princípio *muito* suspeito. O difícil é > que, sem ECQ, um construtivista ficaria basicamente sem negação (ao > estilo do cálculo mínimo de Johansson), ou a negação cessaria de

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

Joao Marcos escreveu: >> Eu, pessoalmente, acho ECQ um princípio *muito* suspeito. O >> difícil é que, sem ECQ, um construtivista ficaria basicamente sem >> negação (ao estilo do cálculo mínimo de Johansson), ou a negação >> cessaria de ser um operador *lógico*. > > Por quê,

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

Oi Hermógenes, [...] Neste ponto, a única vantagem de TIT em comparação à ZF (sua > concorrente igualmente ad hoc), principalmente se você é um computeiro > ou matemático preocupado com computabilidade, é o fato de TIT ser > construtiva. Retomando um pouco o ponto da Valéria sobre a