Hermógenes,
Desculpe-me. Por favor, desconsidere o inicio da minha mensagem anterior.
De fato, A \cong empty é terrível. Além de ter os mesmos problemas que A
---> empty (por exemplo, ser justificado por contra-positiva, afinal esse é
o único jeito de justificar uma prova de inexistência), com essa definição
se deriva ECQ. Não sei da onde tirei essa idéia maluca de que essa
definição seria correta.
Abs,
Fernando
Em 8 de abril de 2017 13:30, Fernando Yamauti <fgyama...@gmail.com>
escreveu:
> Oi Hermógenes
>
> > 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).
>>
>
> Desculpe-me, não entendi a sua objeção. A minha intenção inicial era
> de transformar o juízo 'A false' = 'A não é habitado' em uma proposição e
> definir \neg A como tal proposição. Nesse caso os juízos '\neg A true' e 'A
> false' expressariam a mesma coisa. Ou seja, eu gostaria que ter uma prova
> de \neg A fosse a mesma coisa que dizer que existe uma prova de que A não
> tem uma prova.
>
> Além disso, a negação passa a ser algo menos primitivo e passará a
> depender de outras operações lógicas (identidade e quantificador
> existencial dependente).
>
>
>> > 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.
>>
>
> Acho que então não entendi o seu ponto. Gostaria de entender, caso você
> esteja motivado a escrever.
>
>
>> > [...]
>> >
>> > 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.
>>
>
> Eu quis compactar uma mensagem para evitar mais mensagens, mas parece
> que isso gerou mais confusão. Desculpe-me. Eu costumo a ser meio apressado.
> Poderia citar a parte em que o ML justifica a importância de incluir dois
> juízos distintos: 'A true' e 'A prop'? A única passagem que me recordo é a
> que mencionei (um pouco implicitamente) na minha mensagem anterior. Mais
> explicitamente, achei que você se referia ao trecho
>
> "... A and B should range over arbitrary propositions, another
> difficulty arises, because, whereas the notion of formula is a syntactic
> notion, a formula being defined as an expression that can be formed by
> means of certain formation rules, the notion of proposition is a semantic
> notion, which means that the rule is no longer completely formal in the
> strict sense of formal logic. That a rule of inference is completely formal
> means precisely that there must be no semantic conditions involved in the
> rule: it may only put conditions on the forms of the premises and
> conclusion. The only way out of this second difficulty seems to be to say
> that, really, the rule has not one but three premises, so that, if we were
> to write them all out, it would read
>
> A prop B prop A true
>
> ------------------------
>
> A∨B true
>
> that is, from A and B being propositions and from the truth of A, we are
> allowed to conclude the truth of A ∨ B. Here I am using A prop as an
> abbreviated way of saying that
> A is a proposition. "
>
> Seria essa a parte que você se referindo?
>
> 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. :-)
>
>
> Infelizmente, eu não consigo compreender a sua objeção enquanto eu
> não entender a que parte você está se referindo (assim como mencionei
> acima).
>
> Abs,
> Fernando Yamauti
>
--
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/CAJGvw-1kX%3DkdwRvo29Qo%2Bmugb2UM%2B0Qnwy1kKuLYfqrXxJK4EA%40mail.gmail.com.
