Fernando Yamauti <fgyama...@gmail.com> escreveu:
> Não. A minha sugestão é diferente. \neg A deve ser definido como A
> \cong empty := \sum_{f: A --> empty} isequ (f) . Já iseq (f) é um
> pouco mais complicado de escrever via email, portanto vou pedir que
> olhe a pagina 78 do HoTT book
Isso não faz muito sentido para mim. Em primeiro lugar, o termo sendo
definido, ¬A, não aparece na definição (estou usando "0" para o seu
"empty"): A≅0 := ∑(f: A→0) isequiv(f). A não ser que você já esteja
tomando A→0 como definição de ¬A, mas aí a coisa fica ainda mais
confusa. Em segundo lugar, não me parece muito conveniente, para se
dizer o mínimo, uma abordagem que defina a negação em termos de tipos
mais complexos como a soma ∑ (também conhecido como quantificador
existencial) e tipos de igualdades (uma vez que isequiv(f) é definido de
acordo com os tipos idA e idB para f: A→B).
> Mas isso é considerado quando se usa tipos dependentes. De uma prova
> hipotética \Gamma \vdash A e outra \Delta \vdash \Gamma se
> concatenarmos tudo temos \Delta \vdash \Gamma \vdash A, ou seja, outra
> prova hipotética, não?
Sim. Mas esse não era o ponto.
> [...]
>
> A introdução de 'A prop' como proposição até onde eu entenda serve
> para evitar em falar de um domínio (onde as expressões variam)
> contendo objetos de caráter semânticos e não puramente formais. Em
> contrapartida em Analytic and Synthetic Judgements in Type Theory, ML,
> inspirado por Church, introduz um tipo 'prop' (que é igual a 'set') e
> usa 'A : prop' ao invés de 'A prop' . Além disso, ele introduz um tipo
> 'type' e termos 'i (A) : prop' para cada tipo A.
>
> Portanto, de acordo com a sua afirmação, ML não estaria sendo
> consistente?
Não, não foi isso que eu quis dizer (eu acho). Você está trazendo mais
e mais elementos para a discussão, e eu não estou conseguindo ver a
relação deles com os meus comentários iniciais (isto não significa que
não haja relação, somente que *eu* não estou conseguindo vê-la). Isso
não é ruim, *em si*, mas eu já estou ficando meio velho e não tenho mais
fôlego intelectual para discussões assim. Você poderia, por gentileza,
tentar se focar naquilo que eu escrevi e responder ponto-a-ponto para
que eu possa identificar exatamente aquilo que não ficou claro.
> Desculpe-me, mas ainda estou falhando em entender o que vai para o
> espaço. Creio eu que você esteja pensando em um problema diferente do
> que eu mencionei acima : criar uma estratégia para A variar em
> expressões completas ao invés de proposições, que tem um caráter
> semântico.
Espero que você tenha compreendido, pelo menos, que, com a introdução
*irrestrita* de universos (i.e. com a introdução completa da hierarquia
infinita de universos), nós perdemos a distinção entre os juízos "A é um
tipo" e "x tem o tipo A" (i.e. "x é um termo do tipo A" ou "A é
habitado"). Você poderia dizer: "Tá bem. E daí?" Bem, para
compreender o tamanho da perda, é preciso apreciar o valor da distinção.
Para isso, eu sugeri uma leitura atenta e *reflexiva* dos escritos mais
*filosóficos* do Martin-Löf, com uma mente voltada para fundamentação.
Não fornecerei uma explicação detalhada disso aqui na lista para não
encher ainda mais o saco do pessoal que, a este ponto, já deve estar
lotado de doutrina martin-löfiana. :-)
--
Hermógenes Oliveira
--
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+unsubscr...@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logica-l@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/87lgrbkxd6.fsf%40camelot.oliveira.
