--
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+unsubscribe@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logi...@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/87wpb1tpz7.fsf%40camelot.oliveira.
Muito obrigado!
Em 3 de abril de 2017 13:28, Hermógenes Oliveira <hermogene...@student.uni-tuebingen.de> escreveu:
Fernando Yamauti <fgya...@gmail.com> escreveu:
> Oi,
>
> Será que alguém teria acesso ao paper
>
> 1 Ladyman, J., Presnell, S.: Identity in Homotopy Type Theory, Part I:
> The Justification of Path Induction. Philosophia Mathematica (2015) ?
Coincidência. Eu li esse artigo recentemente. A versão que eu li está
disponível em
http://philsci-archive.pitt.edu/11079/1/Identity_in_HTT_public.pdf
Sem contar o selinho da Oxford University Press, não sei se há muitas
diferenças entre a versão acima e a versão oficial.
Além das páginas tradicionais,
https://homotopytypetheory.org/links/
https://ncatlab.org/nlab/show/homotopy+type+theory#References
mais referências interessantes para quem estiver estudando Teoria
Homotópica dos Tipos podem ser encontradas no repositório do grupo de
estudos que estamos organizando aqui em Tübingen:
https://github.com/BinderDavid/HoTT-StudyGroup
--
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+u...@dimap.ufrn.br.
--
Você recebeu essa mensagem porque está inscrito 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+u...@dimap.ufrn.br.
Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
Acesse esse grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/28e4c785-a336-4b64-989f-42e3de6a9f6f%40dimap.ufrn.br.
--
Você recebeu essa mensagem porque está inscrito 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+unsubscribe@dimap.ufrn.br.
Um outro caso que me incomoda muito e o Martin-Löf sempre joga em baixo do tapete: o porquê de " 'A true' infere 'B true' " ser correto, onde A é falso (onde o "falso" é clássico, ou seja, existe uma prova de \neg A) , para um construtivista. Como se constrói uma prova, a partir de uma prova de que o falso é verdadeiro?
Ou ainda, outro problema que leva ao regresso infinito e a identificação de um objeto do conhecimento com o conhecimento desse objeto (que o Rodrigo havia comentado a um tempo atras de maneira diferente). Um juízo do tipo 'A true' pode virar uma proposição onde '(A true) true' se torna um juízo. E, mais. No ponto de vista epistemico, essas duas coisas são equivalentes (saber que vc sabe é igual a saber). Acho que o ponto de vista epistemico não bate com a teoria, já que garantir que o tipo "A é habitado" não é equivalente a A (em um dado universo), ou será que é? Ou seja, a justificativa do ML não é adequada e só a teoria funciona.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+u...@dimap.ufrn.br.
Porque o meu povo se perde por falta de conhecimento...
Oséias 4:6--
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+u...@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logi...@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/87a87tof1w.fsf%40camelot.oliveira.
--
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+unsubscribe@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logi...@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/87shllitep.fsf%40camelot.oliveira.
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*. Uma exceção interessante é o caso da "Core Logic" de
Tennant, onde a negação é dada um caráter lógico, mesmo sem ECQ, pela
admissão de modus tollendo ponens (ou silogismo disjuntivo) e uma regra
especial para a implicação que permite obter ¬A,A⊢B. Muitos, porém,
acham o preço a se pagar muito salgado: falha da transitividade
(monotonicidade, regra de corte).
b) Um outro problema é que Martin-Löf explica (reduz) o conceito de
"prova hipotética" ao conceito de "prova categórica" (sem hipóteses
abertas).
Martin-Löf, no artigo de fundamentação filosófica da sua Teoria dos
Tipos[7], assume que as regras de introdução dão o significado das
constantes lógicas e, a partir daí, justifica as regras de eliminação.
Isto demonstra, em terminologia corrente, a correção da lógica
intuicionista (como sistema formal) com respeito a uma fundamentação
baseada nas introduções (estilo BHK). Contudo, a contrapartida (a
questão se todos os princípios de raciocínio justificáveis são de fato
deriváveis intuicionisticamente), isto é, completude, em terminologia
corrente, permanece em aberto no artigo, pois Martin-Löf não oferece
nenhum argumento em seu favor. Os resultados mencionados
anteriormente mostram que, sob certas condições que parecem razoáveis
de um ponto de vista construtivo, uma fundamentação estilo BHK, quando
formulada precisamente (uma vez que BHK é uma espécia de fundamentação
(semântica) informal), justificaria inferências que não são
intuicionisticamente deriváveis.
Na minha opinião, o potencial explanatório e de fundamentação da
Teoria Intuicionista de Tipos (TIT) se estraçalha a partir do momento
que se introduz universos. A partir daí, me parece, a TIT assume um
caráter fortemente ad hoc e muitas da intuições iniciais vão para o
espaço. 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. Por outro lado, os argumentos de que ZF seria
filosoficamente mais robusta e conceitualmente mais coerente (ver, por
exemplo, Harvey Friedman na FOM) não me convencem. Acontece que, dado
que ZF é a doutrina ortodoxa, estamos acostumados a fazer vista grossa
para as aberrações em ZF e maldizer excessivamente qualquer
idiossincrasia de propostas alternativas, como TIT.
De qualquer maneira, mesmo num contexto muito elementar, abordar o
intuicionismo, ou construtivismo, de um ponto de vista epistemológico,
tal como Martin-Löf faz, me parece um equívoco. Concordo ainda que a
discussão epistemológica de Martin-Löf em conexão com a fundamentação
da sua Teoria de Tipos é muito confusa, para se dizer o mínimo.
[...] 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.
Me parece que em ambos os quesitos, a) e b), a posição construtivista
de vertente intuicionista, conforme tradicionalmente concebida, deixa
muito a desejar. Confesso que, às vezes, me pergunto se o
intuicionismo tradicional, como exemplificado pela tradição BHK, seria
mesmo uma posição filosoficamente coerente.
Contudo, a contrapartida (a
questão se todos os princípios de raciocínio justificáveis são de fato
deriváveis intuicionisticamente), isto é, completude, em terminologia
corrente, permanece em aberto no artigo, pois Martin-Löf não oferece
nenhum argumento em seu favor.
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.
Eu entendo a objeção que faz ao meu uso do *termo* "completude" no
contexto de Martin-Löf, mas espero que tenha conseguido deixar claro que
o uso que fiz de "completude" e "correção" naquele contexto se referia à
*adequação* das explicações semânticas de Martin-Löf ao sistema de
regras de inferência dedutivas que conhecemos como lógica intuicionista.
Esta questão da adequação é legítima, não importa o quão informal seja a
sua fundamentação (explicação, semântica).
[...] Confesso que, às vezes, me pergunto se o
intuicionismo tradicional, como exemplificado pela tradição BHK, seria
mesmo uma posição filosoficamente coerente.
--
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+u...@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logi...@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/874ly0e5sz.fsf%40camelot.oliveira.
> 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 é exatamente a definição padrão de
¬A como A→⊥. Como você observou, meu comentário acima realmente não diz
respeito a universos. Estava comentando o seu incômodo com o fato de
A→B ser construtivamente válido quando A é falso (quando temos ¬A). Eu
havia observado que esse seu incômodo também aparece na literatura
construtivista, especialmente em conexão com objeções à ECQ.
Note que a definição ¬A≡A→⊥ não é suficiente para definir a negação, mas
apenas define a negação em termos de ⊥. É necessário ainda caracterizar
⊥. O princípio construtivista padrão que caracteriza ⊥ é ECQ. A
inferência que incomodava (¬A,A⊢B) é obtida por modus ponens e ECQ. Um
construtivista que queira rejeitá-la, portanto, teria que rejeitar modus
ponens ou ECQ. O candidato mais óbvio é ECQ. Daí, eu comentei sobre
algumas propostas "construtivas" que rejeitam ECQ.
Espero que agora tenha ficado mais claro (há alguns detalhes adicionais
na minha resposta ao João Marcos).
Em poucas palavras, o que quero dizer é o seguinte: Por que o mapa
transfere, necessariamente, provas *categóricas* das hipóteses? Por que
não mapear provas *hipotéticas* das hipóteses, isto é, por que não
considerar também deduções baseadas em hipóteses, das quais as provas
categóricas (fechadas) são apenas um caso particular?
Agora, poderia uma proposta assim ser considerada "construtivista" ou
"intuicionista"? Depende do que se entende por "construtivismo" ou
"intuicionismo". Se o critério aqui é BHK juntamente com o ponto de
vista epistemológico de Martin-Löf, é provável que a resposta seja
"Não". Mas, se abordamos o intuicionismo por meio de um inferencialismo
apoiado tecnicamente nos trabalhos de Gentzen, a resposta talvez seja
"Sim".
BHK está morta! Longa vida ao inferencialismo gentzeniano! :-)
> O problema que citei ('A true' =' 'A true' true' do ponto de vista
> epistêmico) não tem relação com universos (eu não devia ter citado
> universo no meu comentário) , apesar de ser mais fácil de internalizar
> o juízo 'A true' nas proposições usando universos, i.e., enche o saco
> escrever a definição de uma equivalência homotópica para definir 'A é
> habitado'.
Hum... Não consigo ver uma maneira de fazê-lo sem universos. Poderia me
fornecer detalhes? Pode ser em privado, se você preferir.
> Também acho que a definição de universo univalente é bem intuitiva e
> consistente com a pratica matemática. O universo é só um objeto a mais
> na teoria que mostra a compatibilidade da identidade com a
> equivalência homotópica. Eles fazem o mesmo papel dos V_{\kappa}. E
> como a TIT deve ser semântica e sintática ao mesmo tempo, acho natural
> colocar um universo (ou melhor, uma estratificação em universos) na
> teoria. Gostaria, portanto, de entender o que gera essa tal destruição
> do potencial explanatório da TIT.
O principal problema com os universos é que eles borram a distinção
entre os juízos "A é um tipo" e "x tem o tipo A" (i.e. A é habitado).
Na presença de universos, o juízo "B é um tipo" se reduz a um juízo da
forma "x tem o tipo A" ou "x é um termo do tipo A", onde A é um
universo. Tecnicamente, isso pode até ser muito conveniente, mas,
filosoficamente, é desastroso.
Sem me alongar muito, creio que a gravidade do problema pode ser
depreendida de uma leitura atenta e refletiva do artigo de fundamentação
do Martin-Löf[1]. Ali, ele discorre sobre a importância em se
distinguir entre os juízos "A prop" ("A é um tipo", pois ali o único
tipo tratado é o tipo das proposições) e "A true" ("x tem o tipo A", "o
tipo proposicional A é habitado", "x é uma prova de A"). Esta distinção
me parece importantíssima para o funcionamento da teoria como
fundamentação filosófica. Quando se introduz universos, toda as
intuições e coerência filosófica que estavam apoiadas nesta distinção
vão para o espaço.
Brouwer não fazia a mesma coisa. Fazia muito pior!
> 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.
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
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. :-)