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
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 "invariânc
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
https://
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 u
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
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 permanec
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 com a negação definida
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 informal ou
> justificativa fi
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*.
>>
>> Por
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 ser
> um operador *lógi
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ê, Hermógenes?
Bem, o
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 computação
12 matches
Mail list logo
