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 [email protected].
Para postar neste grupo, envie um e-mail para [email protected].
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-2avC%2BvjpF9Zx1hivqvup6xNDx0_GHaaQrrz2bsv9EqyQ%40mail.gmail.com.
