Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

[Fernando Yamauti]

  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 
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

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

[Joao Marcos]

Viva, Hermógenes:

> Se é que eu entendi bem o "conectivo" que você apresentou, minha
> hesitação inicial diz respeito exatamente ao fato dele ser apenas
> *parcialmente* determinado, isto é, sua semântica (valor semântico)
> estaria fixada apenas com relação a uma parte das sentenças da
> linguagem.

Na realidade, no caso da negação definida como \neg A := A\to\botop, a
semântica de \neg *não* é parcial, mas simplesmente
não-determinística.  De fato, se v é uma valoração tendo como
contradomínio o conjunto {F,T}, podemos neste caso impor o "axioma":

  v(A)=F implica v(\neg A)=T

e mais nada.  Em particular, se v(A)=T então v(\neg A) pode tomar um
valor qualquer, F ou T.

> Além disso, só para deixar registrado, eu, pessoalmente, não vejo nenhum
> problema com "pregações com caráter puramente ideológico".

Eu também não tenho nenhum problema com isso, desde que o pregador
esteja consciente do caráter ideológico da sua pregação --- ao invés
de dizer, digamos, que "estou apenas fazendo matemática (em uma
vertente intuicionista, ou construtiva, ou dummettiana, ou
martinlöfiana, ou prawitziana, ou...)".

>> Moral: um conectivo não é uma proposição atômica --- nem quando ambos
>> se parecem.
>
> Você poderia elaborar mais?  Em particular, no caso de IL⁺ e hJ, dado
> que você admite[3] que este é extensão conservativa daquele, qual seria
> a diferença entre ⊥ e uma sentença atômica qualquer? O fato de que um
> deles eu escrevo assim "⊥" e o outro eu escrevo assim "p", ou assim "q"?
> (AKA don't you see? the signature is different!)

Deixe-me propor um exemplo (subestrutural) um pouquinho diferente
deste, para ver se o ponto fica mais claro.  Passo 0: Fixe o seu
cálculo de sequentes favorito para a lógica clássica (ou para a lógica
intuicionista, se preferir).  Passo 1: Adicione o conectivo nulário
\botop à linguagem.  Passo 2: jogue fora a forma irrestrita da regra
do corte, permitindo apenas o corte para o \botop, ou seja:

  de \Gamma,\botop\Rightarrow\Delta e \Gamma\Rightarrow,\botop\Delta
  podemos concluir \Gamma\Rightarrow\Delta

Do ponto de vista semântica, pode-se mostrar (seguindo a tradição que
vai de Schütte a Girard) que a lógica resultante possui uma semântica
trivalorada.  De fato, podemos neste pensar em valorações tendo como
contra-domínio o conjunto {F,N,T}, e caracterizar o novo conectivo
(que se "parece" com um átomo --- mas não é) através do "axioma":

  v(\botop) \neq N

Note que a semântica de \botop é não-determinística --- ma non troppo.

Passo 3: Adicione agora também o conectivo unário \star à linguagem,
impondo sobre sua semântica os "axiomas":

  v(A)\in\{F,T\} implica v(\star(A))=T
  v(A)\not\in\{F,T\} implica v(\star(A))=F

Exercício: caracterizar tal conectivo unário usando regras de
sequentes apropriadas.

Dada uma proposição atômica p, observe por fim que no cálculo
resultante a sentença \star(\botop) será um teorema, mas \star(p) não
será.

Abraços,
Joao Marcos

-- 
http://sequiturquodlibet.googlepages.com/

-- 
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/CAO6j_LhwFmF7hybjLTFdiATeL-8tEMdujBCFzptFh6J2vzrCdQ%40mail.gmail.com.

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

[Fernando Yamauti]

 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 

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

[Hermógenes Oliveira]

Fernando Yamauti  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.

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

[Hermógenes Oliveira]

Joao Marcos  escreveu:

> Assim que tivermos um critério de logicidade em mãos, portanto,
> poderemos discutir melhor. :-)

Eu diria que o problema não é a ausência de critérios de logicidade, mas
a abundância deles.

> Uma maneira de resumir o meu comentário seria: antes de dizer que algo
> não é "razoável", convém deixar claras as nossas expectativas e as
> regras do jogo.

Perdão, eu pensei que estivesse claro.

Se é que eu entendi bem o "conectivo" que você apresentou, minha
hesitação inicial diz respeito exatamente ao fato dele ser apenas
*parcialmente* determinado, isto é, sua semântica (valor semântico)
estaria fixada apenas com relação a uma parte das sentenças da
linguagem.  Isso parece ir de encontro a algumas propriedades que são
comumente atribuídas à logica e que, portando, deveríamos exigir de
conectivos lógicos: neutralidade e universalidade.

Esta posição, obviamente, não é sacrossanta.  Por isso mesmo, eu não
*afirmei* que o conectivo não era razoável, mas *questionei* até que
ponto ele seria razoável.  Também compartilhei a minha (pessoal)
*hesitação* em aceitar o conectivo como conectivo lógico.  Minha
esperança era que isso fosse interpretado como um *convite* a uma defesa
da logicidade do conectivo.  Por fim, concedi que o núcleo da questão
pudesse ser ideológica (ou, terminológica): alguns são mais liberais com
uso do termo "lógica", ou "negação", outros são mais conservadores.  Não
vejo nenhum problema nisso.

> (Tenho a impressão de que falhar repetidamente nesta tarefa converte
> muito do que se faz em Teoria das Demonstrações em pregação com
> caráter puramente ideológico.)

Não entendi muito bem o que você quis dizer com isso, ou sua relevância
para o tópico em questão, mas fico com a impressão de que talvez eu
tenha, inadvertidamente, tocado em alguma ferida...

Não sei muito bem o que você entende por "muito do que se faz em Teoria
das Demonstrações", mas, no que diz respeito a "deixar claras as
expectativas e regras do jogo" com relação a critérios de logicidade e
constantes lógicas, eu diria justamente o contrário[1][2].  Obviamente,
ninguém é obrigado a concordar, mas não há pobreza de argumentos.

Além disso, só para deixar registrado, eu, pessoalmente, não vejo nenhum
problema com "pregações com caráter puramente ideológico".

> [...]
>
> Moral: um conectivo não é uma proposição atômica --- nem quando ambos
> se parecem.

Você poderia elaborar mais?  Em particular, no caso de IL⁺ e hJ, dado
que você admite[3] que este é extensão conservativa daquele, qual seria
a diferença entre ⊥ e uma sentença atômica qualquer? O fato de que um
deles eu escrevo assim "⊥" e o outro eu escrevo assim "p", ou assim "q"?
(AKA don't you see? the signature is different!)


Referências:

[1]  https://plato.stanford.edu/entries/logical-constants/#InfCha

[2]  Michael Dummett.  The Logical Basis of Metaphysics. 1991.
(capítulo 9, em especial a subseção "Conservative Extensions")

[3]  João Marcos.  What is a Non-truth-functional Logic? Studia Logica
92:215-240, 2009. (página 230)

-- 
Hermógenes Oliveira

"The reasonable man adapts himself to the world; the unreasonable one
persists in trying to adapt the world to himself. Therefore all progress
depends on the unreasonable man."
George Bernard Shaw

-- 
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/87pognl0xp.fsf%40camelot.oliveira.

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

[Fernando Yamauti]

  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 é 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.
>

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



> 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).


   Sim, sim. Isso já estava claro. Para mim, o problema sempre foi o ECQ
desde a primeira mensagem.

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?
>

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?


> 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! :-)
>

Parece uma boa alternativa! Infelizmente eu não tenho conhecimento
suficiente para avaliar a validade dessa abordagem :P


> > 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.
>

   Enquanto ninguém reclamar prefiro manter minhas respostas públicas. O
juízo 'A true' = 'A é habitado' pode ser visto como uma proposição \neg ( A
\cong empty ) . Talvez seja melhor usar o \neg que eu sugeri acima, não
sei. Para mim o \neg A como A --> empty é muito estranho, dado que os
juízos '\neg A true' e 'A false' são completamente diferentes. Na minha
humilde opinião (de matemático), eles deveriam expressar a mesma coisa em
uma teoria construtivista.

   Assumindo que 'A true' também pode ser visto como proposição, que saber
que vc sabe é a mesma coisa que saber (aquela coisa da lógica epistêmica
KKB <---> KB) e que provar é a mesma coisa que saber (o que o ML havia
assumido), temos o resultado do Rodrigo, o juízo ' 'A true' true' expressa
a mesma coisa que o juízo 'A true'.

   Mas se esses juízos expressam a mesma coisa, as suas respectivas
proposições não deveriam ser equivalentes (ou melhor, deve ser requerido
que elas sejam equivalentes)? Acho que sim. Mas aí teríamos que dois tipos
completamente diferentes deveriam ser (homotópicamente) equivalentes. Mas
esse não é o caso.

   Não sei como vc havia pensado usando universos. Poderia me explicar seu
ponto de vista?



> > 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
> > 

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

[Joao Marcos]

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ância por substituição" é a propriedade que
permite substituir uniformemente certas sentenças atômicas por
fórmulas quaisquer, mantendo a validade das asserções que já eram
válidas.  Em particular, teoremas e anti-teoremas não "mudam de sinal"
quando trocamos um átomo que neles ocorre por uma fórmula arbitrária.
Um conectivo n-ário que "funcione como um bottom", qualquer que seja o
n, é sempre um conectivo.  Não se aplica substituição sobre ele, sob
pena de mudar os sinais das coisas...

Posso ter respondido (ou tentado responder) a pergunta errada, então
por favor fique à vontade para pedir esclarecimentos mais específicos!

> como eu passei uma boa parte da minha vida dizendo que
> interdefinabilidade entre conectivos e' ruim
> acho que preciso responder a:
>>Por outro lado, não vejo porque deveríamos pensar sempre na negação
> como conectivo *derivado*.  Aliás, isto parece até uma ideia bem
> ruinzinha, do ponto de vista de lógicas não-clássicas em que a
> interdefinibilidade entre conectivos clássicos usualmente se perde
> pelo caminho.
>
> sim, seria bom nao ter a negação como conectivo derivado, mas nao sei como
> escapar disso.

Humm... mudando de Dedução Natural para Cálculo de Sequentes?  Bem,
pode ser de novo que eu não tenha entendido o problema...  De todo
modo, qualquer dificuldade que desvaneça através de uma mera mudança
de formalismo não pode ser dita realmente *robusta*...

Abraços (meus mesmo),
Joao Marcos


> a consideracao maior 'e a consistencia como um todo e a relacao com logica
> classica.
> e' dessa nocao pre-formal de ecumenismo do Prawitz (no festscrift do Luiz
> Carlos)
>  que vem a constraint que negacao 'e derivada, pra mim.
> se eu soubesse (re)construir o edificio inteiro (logica classica e
> intuicionista e suas inter relacoes) sem depender da hipotese de que negacao
> 'e implicacao no absurdo, eu o faria.
> mas pra saber fazer isso, precisaria de reprovar todos os resultados que
> temos com a nocao derivada de negacao.
> isso eu nao sei fazer e nem sei se e' possivel.
>
> abs Prawitzianos,

-- 
http://sequiturquodlibet.googlepages.com/

-- 
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/CAO6j_LjpdtniaKPRPXzv9gEgQnGNmhV69g6gG6tMfegJL1P1pA%40mail.gmail.com.

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

[Valeria de Paiva]

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 uma boa parte da minha vida dizendo que
interdefinabilidade entre conectivos e' ruim
acho que preciso responder a:
>Por outro lado, não vejo porque deveríamos pensar sempre na negação
como conectivo *derivado*.  Aliás, isto parece até uma ideia bem
ruinzinha, do ponto de vista de lógicas não-clássicas em que a
interdefinibilidade entre conectivos clássicos usualmente se perde
pelo caminho.

sim, seria bom nao ter a negação como conectivo derivado, mas nao sei como
escapar disso.

a consideracao maior 'e a consistencia como um todo e a relacao com logica
classica.
e' dessa nocao pre-formal de ecumenismo do Prawitz (no festscrift do Luiz
Carlos)
 que vem a constraint que negacao 'e derivada, pra mim.
se eu soubesse (re)construir o edificio inteiro (logica classica e
intuicionista e suas inter relacoes) sem depender da hipotese de que
negacao 'e implicacao no absurdo, eu o faria.
mas pra saber fazer isso, precisaria de reprovar todos os resultados que
temos com a nocao derivada de negacao.
isso eu nao sei fazer e nem sei se e' possivel.

abs Prawitzianos,

2017-04-07 5:54 GMT-07:00 Hermógenes Oliveira :

> 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 filosófica (até onde sei, o estudo de semânticas formais
> > para a lógica intuicionista nunca foi uma das preocupações principais
> > do Martin-Löf).  De qualquer forma, não vejo porque as explicações de
> > significado não seriam “completas”, no sentido informal, para a MLETT,
> > que, repito, é a única das duas vertentes tradicionais de sua teoria
> > de tipos que interessa ao intuicionista.
>
> Você está correto em observar que as explicações semânticas de
> Martin-Löf não foram propostas como uma semântica formal e que o estudo
> de semânticas formais não tem lugar no espectro da obra dele.
>
> Porém, a questão da adequação das explicações semânticas pode ser
> levantada também no âmbito informal, como tentei indicar na minha
> mensagem original.
>
> Nas suas explicações semânticas, Martin-Löf toma as regras de introdução
> como primitivas (como aquelas que conferem significado às constantes
> lógicas) e justifica as regras de eliminação com base nelas.  Se as
> regras de eliminação também fossem consideradas primitivas, ele não
> teria porquê se dar o trabalho de justificá-las com base nas regras de
> introdução.  A questão agora surge: Será que as regras de eliminação
> justificadas por Martin-Löf são, de fato, as regras mais fortes que
> podem ser justificadas, tomando como base as regras de introdução?  Isto
> é, seria possível fornecer regras de eliminação mais fortes que também
> sejam justificadas com base nas regras de introdução?
>
> Como se trata de uma semântica (explicação, fundamentação) informal,
> esta questão não pode ser respondida, no caso de Martin-Löf, com um
> teorema.  Mas isso não significa que a questão é inócua ou
> desimportante, e, certamente, é uma questão que não pode ser afastada
> simplesmente sob o pretexto de que a semântica é informal.  Martin-Löf
> fornece uma justificação, informal, obviamente, para as suas regras de
> eliminação (suas regras de eliminação estão *corretas*).  Mas, é
> perfeitamente razoável se perguntar se haveriam outras regras de
> eliminação que pudessem ser justificadas e que resultariam numa lógica
> diferente da lógica intuicionista, que é a lógica alvo da semântica
> informal em questão.
>
> O que, com respeito a Martin-Löf, é um mero questionamento informal, se
> torna, no caso de Prawitz, uma conjectura[1], pois Prawitz, ainda que
> num estilo similar ao de Martin-Löf, fornece definições rigorosas que
> resultam, de fato, numa semântica formal.  A conjectura de Prawitz é
> justamente uma versão formal da questão que estou discutindo: Seriam as
> regras de eliminação padrões as regras mais fortes que podem ser
> validadas do ponto de vista das regras de introdução?
>
> Os resultados que mencionei anteriormente sugerem que a resposta a essa
> conjectura possa ser "não".  E, como esses resultados negativos incluem
> mesmo contraexemplos, é fácil traduzir os contraexemplos na forma de
> justificativas informais nos termos de semânticas informais como BHK e
> as explicações semânticas de Martin-Löf.  De fato, eu já forneci a você,
> em conversa privada, uma justificativa informal em termos de BHK de uma
> inferência que não é intuicionisticamente derivável.
>
> Eu entendo a 

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

[Bruno Bentzen]

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 inferir qualquer proposição A, desde que A seja 
verdadeira. Simbolicamente, podemos expressar sua regra de eliminação da 
seguinte maneira:

⊤ true   A true
 ⊤-elim
A true

No entanto, uma vez que já temos uma derivação de A, essa é claramente uma 
regra redundante. Este é o único sentido que conheço em que podemos dizer, 
dualmente, que "top não possui uma regra de eliminação". :)



Hermógenes escreveu:

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). 


Este questionamento é sem dúvidas legítimo e pode ser problemático em BHK 
dado a sua falta de rigorosidade. Contudo, só temo que seja muito injusto 
tirar daí que...

[...] Confesso que, às vezes, me pergunto se o 
> intuicionismo tradicional, como exemplificado pela tradição BHK, seria 
> mesmo uma posição filosoficamente coerente.

(Trecho de uma mensagem anterior do Hermógenes)

...a escola intuicionista ofereça uma posição filosoficamente 
insatisfatória, uma vez que BHK é uma tentativa relaxada de representar 
apenas uma pequena fatia desta corrente de pensamento. Pessoalmente, 
acredito que haja desenvolvimentos filosoficamente interessantes e 
rigorosos do intuicionismo desde a emergência da MLETT e das teorias de 
tipo computacionais mencionadas em minha mensagem anterior. O artigo 
'Constructive mathematics and computer programming' (1982) do Martin-Löf, 
que você deve conhecer, é a referência canônica no assunto.

Abraços lógicos,
Bruno

--
Bruno Bentzen
https://sites.google.com/site/bbentzena/

On Friday, April 7, 2017 at 5:58:57 PM UTC+8, Joao Marcos wrote:
>
> 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 quê, Hermógenes? 
> > 
> > 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 como ¬A≡A→⊥ *e não colocamos 
> > nada no lugar de ECQ*, então as nossas inferências dedutivas corretas 
> > são exatamente aquelas do fragmento mínimo sem negação e, do ponto de 
> > vista inferencial, não é possível distinguir o absurdo (⊥) de outra 
> > sentença qualquer: nós basicamente não teríamos a negação no âmbito 
> > das inferências lógicas. 
>
> Por um lado, vale notar que há sim uma maneira neste caso de 
> distinguir a negação, vista como um conectivo com interpretação 
> parcialmente não-determinística aplicada a uma outra sentença qualquer 
> (note-se que a negação de uma sentença falsa é perfeitamente 
> determinística, usando a definição acima; o "problema" está apenas na 
> negação de sentenças verdadeiras), de uma sentença atômica arbitrária: 
> 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. 
>
> Por outro lado, não vejo porque deveríamos pensar sempre na negação 
> como conectivo *derivado*.  Aliás, isto parece até uma ideia bem 
> ruinzinha, do ponto de vista de lógicas não-clássicas em que a 
> interdefinibilidade entre conectivos clássicos usualmente se perde 
> pelo caminho. 
>
> > Obviamente, poderiamos ainda introduzir uma 
> > noção de incompatibilidade entre sentenças e, mantendo apenas as 
> > regras de inferência do fragmento mínimo, tratar a negação no âmbito 
> > extra-lógico: a negação deixa de ser um operador lógico (se entendemos 
> > por lógica apenas aquilo que está sendo capturado pelas nossas regras 
> > de inferência). 
> > 
> > Espero que agora esteja mais claro.  Ou você estaria perguntando o 
> > porquê de eu achar ECQ um princípio suspeito? 
>
> Não.  Concordamos que ECQ é muito suspeito. :-)  Aliás, o papel do 
> símbolo ⊥ em Dedução Natural é frequentemente artificial e "suspeito". 
>
> >>> 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 

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

[Joao Marcos]

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 permanecemos com a negação definida como ¬A≡A→⊥ *e não colocamos
>>> nada no lugar de ECQ*, então as nossas inferências dedutivas corretas
>>> são exatamente aquelas do fragmento mínimo sem negação e, do ponto de
>>> vista inferencial, não é possível distinguir o absurdo (⊥) de outra
>>> sentença qualquer: nós basicamente não teríamos a negação no âmbito
>>> das inferências lógicas.
>>
>> Por um lado, vale notar que há sim uma maneira neste caso de
>> distinguir a negação, vista como um conectivo com interpretação
>> parcialmente não-determinística aplicada a uma outra sentença qualquer
>> (note-se que a negação de uma sentença falsa é perfeitamente
>> determinística, usando a definição acima; o "problema" está apenas na
>> negação de sentenças verdadeiras), de uma sentença atômica arbitrária
>
> Uma maneira de resumir o meu comentário nesse contexto seria:
>
> Até que ponto seria razoável chamar isso de *operador lógico*?
>
> Isto é, eu hesitaria em chamar o conectivo que você descreve acima de
> operador lógico (assumindo que o entendi corretamente).  No fim das
> contas, me parece, a questão é ideológica: uns vêem lógica em tudo,
> outros a procuram de dia com uma lâmpada na mão. :-)

Assim que tivermos um critério de logicidade em mãos, portanto,
poderemos discutir melhor. :-)

Uma maneira de resumir o meu comentário seria: antes de dizer que algo
não é "razoável", convém deixar claras as nossas expectativas e as
regras do jogo.  (Tenho a impressão de que falhar repetidamente nesta
tarefa converte muito do que se faz em Teoria das Demonstrações em
pregação com caráter puramente ideológico.)

No caso da negação, o mínimo que eu esperaria, do ponto de vista
abstrato, é que não valham a asserção segundo a qual "p é consequência
de não-p" nem a asserção segundo a qual "não-p é consequência de p".
Alternativamente, para lógicas tarskianas, isto consistiria em dizer
que se há de aceitar a negação de certas sentenças rejeitadas, e
rejeitar a negação de certas sentenças aceitas --- usando assim a
negação para converter "certas sentenças verdadeiras" em sentenças
falsas e vice-versa.  Tal expectativa, de fato, é um caso particular
das propriedades de uma negação "minimamente decente", que discuti na
página 204 do seguinte artigo:
http://www.sciencedirect.com/science/article/pii/S1570868304000576

>> 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.
>
> Bem, a regra de substituição uniforme não se aplica, de qualquer
> maneira, a conectivos (o quão marivolhoso seria se pudéssemos substituir
> conectivos à vontade, não é mesmo? :-D).  Mas, considerando a *sentença*
> formada usando o conectivo nulário, não consigo ver porquê a regra de
> substituição seria problemática, assumindo, é claro, que esse conectivo
> não seja governado por ECQ ou qualquer outra regra de inferência, que
> era o caso que eu tinha em mente.  Afinal, neste caso, o absurdo seria
> apenas uma sentença, embora pudéssemos conferí-la, extra-logicamente, um
> significado especial.

Se você preferir, podemos transformar o conectivo nulário em um
conectivo unário # tal que #(p) é equivalente a ⊥.  Ou um conectivo
n-ário com o mesmo efeito.  Neste(s) caso(s) você claramente
concordaria que faz menos sentido falar em aplicar substituição sobre
tal conectivo.

A propósito, eu discuto um pouco a interpretação não-determinística
conectivo ⊥ (que chamo "botop"), típica da lógica de Johánsson, na
seção final deste artigo:
https://link.springer.com/article/10.1007/s11225-009-9196-z
A discussão diz respeito à figurinha que se encontra um pouco antes,
na página 232, que herdei essencialmente de Curry 1963.

Moral: um conectivo não é uma proposição atômica --- nem quando ambos
se parecem.  Note, a propósito, que tal conectivo não teria regras de
introdução (para além das regras artificiais que o Martin-Löf
aparentemente inventaria só para manter o slogan sobre
introdução+eliminação).

Joao Marcos

-- 
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/CAO6j_LhU1-PZ0a6nrSjj1FMG%3D7o%3DT0ETw8gJo-1Y_6%3Dvd-9sNg%40mail.gmail.com.

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

[Hermógenes Oliveira]

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 como ¬A≡A→⊥ *e não colocamos
>> nada no lugar de ECQ*, então as nossas inferências dedutivas corretas
>> são exatamente aquelas do fragmento mínimo sem negação e, do ponto de
>> vista inferencial, não é possível distinguir o absurdo (⊥) de outra
>> sentença qualquer: nós basicamente não teríamos a negação no âmbito
>> das inferências lógicas.
>
> Por um lado, vale notar que há sim uma maneira neste caso de
> distinguir a negação, vista como um conectivo com interpretação
> parcialmente não-determinística aplicada a uma outra sentença qualquer
> (note-se que a negação de uma sentença falsa é perfeitamente
> determinística, usando a definição acima; o "problema" está apenas na
> negação de sentenças verdadeiras), de uma sentença atômica arbitrária

Uma maneira de resumir o meu comentário nesse contexto seria:

Até que ponto seria razoável chamar isso de *operador lógico*?

Isto é, eu hesitaria em chamar o conectivo que você descreve acima de
operador lógico (assumindo que o entendi corretamente).  No fim das
contas, me parece, a questão é ideológica: uns vêem lógica em tudo,
outros a procuram de dia com uma lâmpada na mão. :-)

> 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.

Bem, a regra de substituição uniforme não se aplica, de qualquer
maneira, a conectivos (o quão marivolhoso seria se pudéssemos substituir
conectivos à vontade, não é mesmo? :-D).  Mas, considerando a *sentença*
formada usando o conectivo nulário, não consigo ver porquê a regra de
substituição seria problemática, assumindo, é claro, que esse conectivo
não seja governado por ECQ ou qualquer outra regra de inferência, que
era o caso que eu tinha em mente.  Afinal, neste caso, o absurdo seria
apenas uma sentença, embora pudéssemos conferí-la, extra-logicamente, um
significado especial.

> Por outro lado, não vejo porque deveríamos pensar sempre na negação
> como conectivo *derivado*.  Aliás, isto parece até uma ideia bem
> ruinzinha, do ponto de vista de lógicas não-clássicas em que a
> interdefinibilidade entre conectivos clássicos usualmente se perde
> pelo caminho.

De acordo.

>> Bem, segundo Martin-Löf, há uma regra de introdução para o absurdo
>> (⊥): sob nenhuma circunstância podemos introduzir o absurdo (⊥).
>> Isto é uma regra de introdução no sentido em que diz algo sobre as
>> circunstâncias em que teríamos uma prova do absurdo (similar à
>> cláusula BHK para o absurdo).
>>
>> Daí, ele justifica ECQ como regra de eliminação usando, inclusive, um
>> exemplo não muito convincente envolvendo um chapéu. :-o
>
> 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 diria que não é apenas aparência...

-- 
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/87zifscpcm.fsf%40camelot.oliveira.

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

[Hermógenes Oliveira]

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 filosófica (até onde sei, o estudo de semânticas formais
> para a lógica intuicionista nunca foi uma das preocupações principais
> do Martin-Löf).  De qualquer forma, não vejo porque as explicações de
> significado não seriam “completas”, no sentido informal, para a MLETT,
> que, repito, é a única das duas vertentes tradicionais de sua teoria
> de tipos que interessa ao intuicionista.

Você está correto em observar que as explicações semânticas de
Martin-Löf não foram propostas como uma semântica formal e que o estudo
de semânticas formais não tem lugar no espectro da obra dele.

Porém, a questão da adequação das explicações semânticas pode ser
levantada também no âmbito informal, como tentei indicar na minha
mensagem original.

Nas suas explicações semânticas, Martin-Löf toma as regras de introdução
como primitivas (como aquelas que conferem significado às constantes
lógicas) e justifica as regras de eliminação com base nelas.  Se as
regras de eliminação também fossem consideradas primitivas, ele não
teria porquê se dar o trabalho de justificá-las com base nas regras de
introdução.  A questão agora surge: Será que as regras de eliminação
justificadas por Martin-Löf são, de fato, as regras mais fortes que
podem ser justificadas, tomando como base as regras de introdução?  Isto
é, seria possível fornecer regras de eliminação mais fortes que também
sejam justificadas com base nas regras de introdução?

Como se trata de uma semântica (explicação, fundamentação) informal,
esta questão não pode ser respondida, no caso de Martin-Löf, com um
teorema.  Mas isso não significa que a questão é inócua ou
desimportante, e, certamente, é uma questão que não pode ser afastada
simplesmente sob o pretexto de que a semântica é informal.  Martin-Löf
fornece uma justificação, informal, obviamente, para as suas regras de
eliminação (suas regras de eliminação estão *corretas*).  Mas, é
perfeitamente razoável se perguntar se haveriam outras regras de
eliminação que pudessem ser justificadas e que resultariam numa lógica
diferente da lógica intuicionista, que é a lógica alvo da semântica
informal em questão.

O que, com respeito a Martin-Löf, é um mero questionamento informal, se
torna, no caso de Prawitz, uma conjectura[1], pois Prawitz, ainda que
num estilo similar ao de Martin-Löf, fornece definições rigorosas que
resultam, de fato, numa semântica formal.  A conjectura de Prawitz é
justamente uma versão formal da questão que estou discutindo: Seriam as
regras de eliminação padrões as regras mais fortes que podem ser
validadas do ponto de vista das regras de introdução?

Os resultados que mencionei anteriormente sugerem que a resposta a essa
conjectura possa ser "não".  E, como esses resultados negativos incluem
mesmo contraexemplos, é fácil traduzir os contraexemplos na forma de
justificativas informais nos termos de semânticas informais como BHK e
as explicações semânticas de Martin-Löf.  De fato, eu já forneci a você,
em conversa privada, uma justificativa informal em termos de BHK de uma
inferência que não é intuicionisticamente derivável.

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).

Gostaria ainda de deixar claro que estas minhas observações não afetam
em nada a *utilidade* da TIT como teoria matemática e o fato de que suas
propriedades construtivas, concordo com a Valéria nesse ponto, podem ser
razões mais do que suficientes para favorecê-la em detrimento de ZF.

Referências:

[1]  Dag Prawitz. An Approach to General Proof Theory and a Conjecture
of a Kind of Completeness of Intuitionistic Logic Revisited. In:
Advances in Natural Deduction, 269-279, 2014.

-- 
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/874ly0e5sz.fsf%40camelot.oliveira.

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

[Joao Marcos]

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 quê, Hermógenes?
>
> 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 como ¬A≡A→⊥ *e não colocamos
> nada no lugar de ECQ*, então as nossas inferências dedutivas corretas
> são exatamente aquelas do fragmento mínimo sem negação e, do ponto de
> vista inferencial, não é possível distinguir o absurdo (⊥) de outra
> sentença qualquer: nós basicamente não teríamos a negação no âmbito
> das inferências lógicas.

Por um lado, vale notar que há sim uma maneira neste caso de
distinguir a negação, vista como um conectivo com interpretação
parcialmente não-determinística aplicada a uma outra sentença qualquer
(note-se que a negação de uma sentença falsa é perfeitamente
determinística, usando a definição acima; o "problema" está apenas na
negação de sentenças verdadeiras), de uma sentença atômica arbitrária:
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.

Por outro lado, não vejo porque deveríamos pensar sempre na negação
como conectivo *derivado*.  Aliás, isto parece até uma ideia bem
ruinzinha, do ponto de vista de lógicas não-clássicas em que a
interdefinibilidade entre conectivos clássicos usualmente se perde
pelo caminho.

> Obviamente, poderiamos ainda introduzir uma
> noção de incompatibilidade entre sentenças e, mantendo apenas as
> regras de inferência do fragmento mínimo, tratar a negação no âmbito
> extra-lógico: a negação deixa de ser um operador lógico (se entendemos
> por lógica apenas aquilo que está sendo capturado pelas nossas regras
> de inferência).
>
> Espero que agora esteja mais claro.  Ou você estaria perguntando o
> porquê de eu achar ECQ um princípio suspeito?

Não.  Concordamos que ECQ é muito suspeito. :-)  Aliás, o papel do
símbolo ⊥ em Dedução Natural é frequentemente artificial e "suspeito".

>>> 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.
>>
>> E o que dizer do conectivo nulário de absurdo, que não possui regra
>> de introdução?
>
> Bem, segundo Martin-Löf, há uma regra de introdução para o absurdo
> (⊥): sob nenhuma circunstância podemos introduzir o absurdo (⊥).  Isto
> é uma regra de introdução no sentido em que diz algo sobre as
> circunstâncias em que teríamos uma prova do absurdo (similar à
> cláusula BHK para o absurdo).
>
> Daí, ele justifica ECQ como regra de eliminação usando, inclusive, um
> exemplo não muito convincente envolvendo um chapéu. :-o

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.

Abraços,
Joao Marcos

-- 
http://sequiturquodlibet.googlepages.com/

-- 
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/CAO6j_LhGn2S3XU_VQfQRijLO6W2hu-tQbN33eKRmqzMEV1KKog%40mail.gmail.com.

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

[Hermógenes Oliveira]

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ó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).
>
> 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).

>  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).
>
> Mas essa parece ser a única opção do ponto de vista construtivista,
> não? De uma prova hipotética (acho que o ML usa o termo consequências
> lógica para esse operador de inferência) se constrói um mapa que
> transfere provas categóricas entre as asserções da prova
> hipotética. Não consigo ver outra opção.

Uma outra opção seria trabalhar exclusivamente com deduções (provas
hipotéticas), sem reduzí-las a provas categóricas.  É importante
observar que provas categóricas são um caso particular de deduções
(provas hipotéticas).  A circularidade pode ser evitada por meio dos
conhecidos argumentos envolvendo harmonia (normalização, canonicidade)
que já servem de base para as propostas atuais reducionistas (estilo
Martin-Löf).

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?

Normalização vale para *deduções*, não somente para "provas" fechadas!

Ademais, se temos uma fundamentação baseadas em deduções (a partir de
hipóteses) em vez de provas categóricas (fechadas), desaparece todo o
problema filosófico de se explicar a correção de certas inferências por
apelo à impossíveis provas categóricas do absurdo.

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! :-)

>  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.
>
> O problema que citei ('A true' =' 'A true' true' do ponto de vista
> epistêmico) não tem relação com 

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

[Hermógenes Oliveira]

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 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 como ¬A≡A→⊥ *e não colocamos
nada no lugar de ECQ*, então as nossas inferências dedutivas corretas
são exatamente aquelas do fragmento mínimo sem negação e, do ponto de
vista inferencial, não é possível distinguir o absurdo (⊥) de outra
sentença qualquer: nós basicamente não teríamos a negação no âmbito
das inferências lógicas.  Obviamente, poderiamos ainda introduzir uma
noção de incompatibilidade entre sentenças e, mantendo apenas as
regras de inferência do fragmento mínimo, tratar a negação no âmbito
extra-lógico: a negação deixa de ser um operador lógico (se entendemos
por lógica apenas aquilo que está sendo capturado pelas nossas regras
de inferência).

Espero que agora esteja mais claro.  Ou você estaria perguntando o
porquê de eu achar ECQ um princípio suspeito?

>> 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.
>
> E o que dizer do conectivo nulário de absurdo, que não possui regra
> de introdução?

Bem, segundo Martin-Löf, há uma regra de introdução para o absurdo
(⊥): sob nenhuma circunstância podemos introduzir o absurdo (⊥).  Isto
é uma regra de introdução no sentido em que diz algo sobre as
circunstâncias em que teríamos uma prova do absurdo (similar à
cláusula BHK para o absurdo).

Daí, ele justifica ECQ como regra de eliminação usando, inclusive, um
exemplo não muito convincente envolvendo um chapéu. :-o

Referências:

[1] Per Martin-Löf. On the Meanings of the Logical Constants and the
Justifications of the Logical Laws. Nordic Journal of Philosophical
Logic 1 (1), 11-60, 1996.
(disponível em https://github.com/michaelt/martin-lof)

-- 
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/87k26wimgm.fsf%40camelot.oliveira.

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

[Bruno Bentzen]

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/construtividade:

O intuicionismo, concebido como a escola de filosofia da matemática 
iniciada por Brouwer no começo do século XX, é fundamentado na noção de 
computação. Isso certamente é pouco claro em Brouwer, não só por suas 
inclinações ao misticismo, mas talvez principalmente pelo fato de que este 
iniciou o seu programa quase três décadas (1907, 1912) antes do 
amadurecimento matemático da noção de algorítimo fornecida pelos trabalhos 
de Turing e Church em cerca de 1936. Logo a noção de computação na qual 
Brouwer formulou o seu intuicionismo pode parecer obscura, estranha ou 
pouco familiar: uma noção primitiva de “construção mental” ou “intuição 
basal”, rotinas finitas que surgem no curso do tempo.

A matemática seria o resultado de tais construções e a lógica apenas um 
aspecto da matemática. Felizmente, parte dos escritos de Brouwer acerca de 
sua lógica foi polida e tornada mais precisa com a interpretação BHK e 
paradigma de proposição como tipos, 

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. 


mas, de todo modo, BHK (que se limita aos conectivos lógicos) é não mais 
que uma fotografia parcial do intuicionismo tradicional como todo. Acredito 
que, pela natureza do retrato, é natural que seja incompleto ou 
insatisfatório (nem mesmo todos “conectivos” são explicados, e.g. o que 
significa a igualdade?).

Já o paradigma de proposição como tipos tem provocado muita confusão e 
mal-entendidos, levando muita gente a afirmar que intuicionismo nada mais é 
que meta-matemática [1] [2]. O cerne da questão é que – como recentemente 
comentei com o Fernando off-list – há duas formas na qual podemos entender 
a correspondência entre tipos e proposições.

A primeira forma é bem óbvia: a sintática. A correspondência sintática 
entre proposição e tipos diz que os termos de uma teoria correspondem às 
derivações de uma respectiva teoria lógica. Aqui termos são meras 
caracterizações das derivações de uma teoria lógica. Isso também é 
refletido pelo fato de que o juízo de tipicidade, 'N : M', é analítico (no 
sentido de Martin-Löf [3], i.e. a checagem de tipos é decidível). Este é o 
caso da correspondência que ocorre na teoria de tipos intensional do 
Martin-Löf (MLITT) e é também – ao meu ver – a correspondência usada nos 
argumentos levantados por Rodrigo Freire acerca da circularidade da noção 
de verdade em Martin-Löf em Janeiro do ano passado.

A segunda correspondência, menos conhecida que a primeira, é a endossada 
por Brouwer e a que interessa ao intuicionista: a semântica. Provas são 
caracterizações de uma computação passo a passo que realizam a verdade de 
uma proposição. Provas são termos, mas não termos de qualquer teoria dos 
tipos definida por regras de inferências: termos de uma teoria que traz 
embutida a noção de computação. Esta é a correspondência enfatizada pelas 
explicações de significado (meaning explanations) do Martin-Löf, sobre o 
qual a sua teoria de tipos extensional (MLETT) [4] é fundamentada, e, 
portanto, é a que vale na MLETT. O juízo de tipicidade, normalmente escrito 
'N ∈ M' na literatura relevante à teoria extensional, é sintético (i.e. 
indecidível), dado que expressa não uma noção semântica: N é um programa 
que realiza o problema expresso por M. Ademais, o juízo  'N ∈ M' *deve* ser 
indecidível porque não há nenhuma maneira em geral de decidir se um 
programa, quando executado, gera um valor do tipo determinado: tal programa 
pode não ter nenhum valor. 

Pelo seu conteúdo computacional inerente, MLETT é frequentemente chamado de 
“teoria de tipos computacional” na literatura em torno do assistente de 
prova NuPRL [5], cujo próprio sistema é definido através da semântica 
fornecida pelas explicações de significado. 

De todo modo, o propósito desta mensagem certamente não é tentar convencer 
ninguém, nem retomar discussões passadas, mas apenas buscar ilustrar 
algumas das muitas razões que fazem com que outros e eu acreditem que o 
intuicionismo tradicional, concebida como uma escola em filosofia da 
matemática, apresenta uma posição filosoficamente coerente. Pagamos o preço 
da noção de computação, erguemos o edifício da matemática.

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 

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

[Fernando Yamauti]

   Oi Hermógenes,

   Obrigado pelas referências.


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).
>

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).

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).
>

   Mas essa parece ser a única opção do ponto de vista construtivista, não?
De uma prova hipotética (acho que o ML usa o termo consequências lógica
para esse operador de inferência) se constrói um mapa que transfere provas
categóricas entre as asserções da prova hipotética. Não consigo ver outra
opção.


> 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.
>

   Esse é exatamente o ponto que eu queria levantar!


> 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.
>

 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'.

 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.


> 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.
>

   Brouwer não fazia a mesma coisa? Aquela idéia de matemático ideal no
tempo me soa bem similar.

   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 

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

[Joao Marcos]

> 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?

> 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.

E o que dizer do conectivo nulário de absurdo, que não possui regra de
introdução?

Abraços, JM

-- 
http://sequiturquodlibet.googlepages.com/

-- 
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/CAO6j_Lj4N-_Lhs4y%2BcmMaLhCoMdQ7LMQ0ie3%2B%2BGFLJuOH9mTpA%40mail.gmail.com.

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

[Valeria de Paiva]

meus dois centavos nessa discussao (so' pra voces nao ficarem com a
impressao de que ninguem le...):

1.>Muitos, porém, acham o preço a se pagar muito salgado: falha da
transitividade
(monotonicidade, regra de corte).

eu acho um preco absurdo. pior do que se tem que pagar por chifre de
unicornio!

2.>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.

well, well, well... "a única vantagem" 'e vantagem a beca, pra alguns, ne',
cara-palida?

abracos constructivos e MartinLoefianos pra todos,
;)

Valeria

2017-04-06 5:59 GMT-07:00 Hermógenes Oliveira <
hermogenes.olive...@student.uni-tuebingen.de>:

> Fernando Yamauti  escreveu:
>
> > [...]
> >
> > 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?
>
> Martin-Löf possui um conceito de "prova hipotética", isto é, em vez de
> "prova" no sentido categórico, teríamos uma "prova" sob a assunção de
> hipóteses.  Nesse caso, se nós temos que "¬A true", isto é, "A→⊥
> true", e também temos "A true", então "B true" se segue por modus
> pones e ex contradictione quodlibet (ECQ).  Uma primeira questão,
> então, seria:
>
> a) Por que ECQ seria correto de um ponto de vista construtivo?
>
> Aqui, vale notar que a validade construtiva de ECQ não é uma posição
> unânime.  Nesse sentido, G. F. C. Griss[1] é um dos dissidentes mais
> importantes e interessantes, pois parece argumentar de um ponto de
> vista puramente construtivo.  Outros construtivistas apresentam
> motivações diversas para se rejeitar ECQ, em especial, motivações
> relacionadas à relevância e ao uso da implicação na linguagem
> cotidiana (por exemplo, Johansson[2] e Tennant[3]).
>
> 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).
>
> De qualquer maneira, talvez ECQ possa ser fundamentado de um ponto de
> vista construtivo.  Contudo, as fundamentações (explicações)
> oferecidas até o momento, por Martin-Löf e outros, também me parecem
> insatisfatórias.
>
> 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).
>
> Isto significa que a correção de uma prova hipotética (dedução) é
> predicada na possibilidade de se transformar provas categóricas das
> hipóteses em provas categóricas da conclusão, isto é, na construção de
> provas categóricas da conclusão com base em provas categóricas das
> hipóteses.  Portanto, em última instância, a justificativa de
> inferências como "¬A (A→⊥) true","A true" / "B true" apelam a provas
> categóricas de "¬A true" e "A true" e daí, por modus ponens, a provas
> categóricas do absurdo!  Estas provas categóricas não precisam ser
> provas reais, mas devem, pelo menos, ser concebíveis, se é que a
> explicação de Martin-Löf faz qualquer sentido.  Caberia a Martin-Löf,
> e demais construtivistas que defendem posições similares, explicar o
> que significa conceber provas categóricas do absurdo, em outras
> palavras, o que significa conceber o impossível.
>
> Alguns meses atrás, conversava com Bruno Bentzen a respeito de uma
> anedota sobre o tema.  Segundo a anedota, alguém teria perguntado a
> Martin-Löf, ou Prawitz, não me lembro qual, como seria possível
> conceber uma construção que transformasse provas do absurdo em provas
> de outra sentença, dado que não há provas do absurdo.  Ele teria
> respondido: "Como se transforma um unicórnio num cavalo?  Cortando
> fora o chifre.  Mas não há unicórnios."  A anedota é divertida, e
> ilustra como podemos tratar de construções que talvez nunca poderão
> ser efetuadas (seja porque não existem unicórnios ou porque não
> existem provas do absurdo).  Porém, a inexistência de unicórnios
> parece estar num patamar diferente (contingente) comparado com a
> inexistência de provas do absurdo.
>
> A concepção de raciocínios hipotéticos defendida por Martin-Löf, e
> compartilhada por Prawitz e muitos outros, é tributária de BHK,
> especialmente a cláusula para implicação.  Esta concepção também
> recebe o nome de "primazia do categórico sobre o 

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

[Antonio Marmo]

1. Eu trabalhei com pragmática do ponto de vista da lógica. A questão extrapola 
os limites da linguagem ao invés de encontrar soluções nela. Até porque a 
análise pragmática de fenômenos linguísticos remete a um nível de abstração 
ainda mais alto, onde a distinção entre linguagem e pensamento fica tênue 
demais, se não se perder.
Nesse sentido, por exemplo, a tradição griceana fica na interface entre 
linguística e lógica, como já se sabe. Só que o que eles levantam em seus 
inquéritos aponta de volta para as lógicas não-clássicas e aí não há um caminho 
único para continuar a abordagem e sim muitos. (Graças às tuas colocações 
acabei de resumir meu trabalho de forma melhor que antes! Vou colocar no 
Academia.edu para consulta, quando o encontrar!)

2. O que achei mais interessante nas tuas colocações foi o comentário sobre o 
princípio da trivialização não ser construtivo. Aí já estou plenamente de 
acordo. Agora, aqui vai uma observação e não uma objeção: a discussão se 
podemos dizer ou fazer coisas com o que não existe (como serrar os chifres de 
um unicórnio) tem duas posições, a saber, ou nada podemos dizer sobre/ fazer 
com o inexistente ou podemos qualquer coisa. Essa segunda posição de novo é a 
trivialização e a primeira sua rejeição, ainda que colocadas num meta-nível.



Porque o meu povo se perde por falta de conhecimento...
Oséias 4:6

> On 6 Apr 2017, at 10:12, Hermógenes Oliveira 
>  wrote:
> 
> Eu escrevi:
> 
>> [...]
>> 
>> 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. [...]
> 
> Ops. Obviamente, o correto aqui seria "que permite obter ¬A⊢A→B".  Mania
> de reler/revisar o que escreveu só depois de enviar.  
> 
> Foi mal. :-)
> 
> -- 
> 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/87a87tof1w.fsf%40camelot.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/FE71EB05-E400-4BCD-AB6D-7D425B1C3B2D%40gmail.com.

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

[Hermógenes Oliveira]

Eu escrevi:

> [...]
>
> 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. [...]

Ops. Obviamente, o correto aqui seria "que permite obter ¬A⊢A→B".  Mania
de reler/revisar o que escreveu só depois de enviar.  

Foi mal. :-)

-- 
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/87a87tof1w.fsf%40camelot.oliveira.

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

[Hermógenes Oliveira]

Fernando Yamauti  escreveu:

> [...]
>
> 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?

Martin-Löf possui um conceito de "prova hipotética", isto é, em vez de
"prova" no sentido categórico, teríamos uma "prova" sob a assunção de
hipóteses.  Nesse caso, se nós temos que "¬A true", isto é, "A→⊥
true", e também temos "A true", então "B true" se segue por modus
pones e ex contradictione quodlibet (ECQ).  Uma primeira questão,
então, seria:

a) Por que ECQ seria correto de um ponto de vista construtivo?

Aqui, vale notar que a validade construtiva de ECQ não é uma posição
unânime.  Nesse sentido, G. F. C. Griss[1] é um dos dissidentes mais
importantes e interessantes, pois parece argumentar de um ponto de
vista puramente construtivo.  Outros construtivistas apresentam
motivações diversas para se rejeitar ECQ, em especial, motivações
relacionadas à relevância e ao uso da implicação na linguagem
cotidiana (por exemplo, Johansson[2] e Tennant[3]).

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).

De qualquer maneira, talvez ECQ possa ser fundamentado de um ponto de
vista construtivo.  Contudo, as fundamentações (explicações)
oferecidas até o momento, por Martin-Löf e outros, também me parecem
insatisfatórias.

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).

Isto significa que a correção de uma prova hipotética (dedução) é
predicada na possibilidade de se transformar provas categóricas das
hipóteses em provas categóricas da conclusão, isto é, na construção de
provas categóricas da conclusão com base em provas categóricas das
hipóteses.  Portanto, em última instância, a justificativa de
inferências como "¬A (A→⊥) true","A true" / "B true" apelam a provas
categóricas de "¬A true" e "A true" e daí, por modus ponens, a provas
categóricas do absurdo!  Estas provas categóricas não precisam ser
provas reais, mas devem, pelo menos, ser concebíveis, se é que a
explicação de Martin-Löf faz qualquer sentido.  Caberia a Martin-Löf,
e demais construtivistas que defendem posições similares, explicar o
que significa conceber provas categóricas do absurdo, em outras
palavras, o que significa conceber o impossível.

Alguns meses atrás, conversava com Bruno Bentzen a respeito de uma
anedota sobre o tema.  Segundo a anedota, alguém teria perguntado a
Martin-Löf, ou Prawitz, não me lembro qual, como seria possível
conceber uma construção que transformasse provas do absurdo em provas
de outra sentença, dado que não há provas do absurdo.  Ele teria
respondido: "Como se transforma um unicórnio num cavalo?  Cortando
fora o chifre.  Mas não há unicórnios."  A anedota é divertida, e
ilustra como podemos tratar de construções que talvez nunca poderão
ser efetuadas (seja porque não existem unicórnios ou porque não
existem provas do absurdo).  Porém, a inexistência de unicórnios
parece estar num patamar diferente (contingente) comparado com a
inexistência de provas do absurdo.

A concepção de raciocínios hipotéticos defendida por Martin-Löf, e
compartilhada por Prawitz e muitos outros, é tributária de BHK,
especialmente a cláusula para implicação.  Esta concepção também
recebe o nome de "primazia do categórico sobre o hipotético" ou
"concepção das hipóteses como variáveis" (a serem saturadas por provas
categóricas)[4].  Ela parece estar por trás de alguns resultados
negativos[5][6] publicados nos últimos anos com respeito a
fundamentações apoiadas nas regras de introdução, ou nas cláusulas BHK
concebidas como regras de introdução.  Estes resultados mostram que,
sob certas condições, tais fundamentações fracassam em capturar
exatamente os raciocínios intuicionisticamente deriváveis.

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 

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

[Bruno Bentzen]

Oi Fernando,

Também há outra razão para achar as justificativas acima mencionadas 
insuficientes.

Uma vez que o caráter computacional da HoTT (na sua caracterização padrão 
descrita no livro) é desconhecido, a teoria como um todo seria destituida 
de qualquer significado ou base filosófica - pelo menos 
intuicionsiticamente. Como se sabe, o introdução de princípios como o da 
univalência e dos tipos indutivos de ordem elevada através de axiomas na 
teoria dos tipos intensional do Martin-Löf quebra todas as suas 
propriedades interessantes involvendo computação.

Muita gente está apostando nas teorias cúbicas dos tipos, já que HoTT 
possui uma interpretação construtiva na categoria de conjuntos cubicos. 
Intuicionisticamente, já há justificativas parciais. Como talvez você deva 
saber, Angiuli et al [1] recentemente tiveram sucesso em prover uma 
'meaning explanation' para uma teorias cúbicas dos tipos com instâncias da 
univalencia e tipos indutivos de ordem elevada.

  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.


Sobre este assunto, prefiro discutir off-list.

Abraços,
Bruno

[1] - Carlo Angiuli, Robert Harper, Todd Wilson. Computational 
Higher-Dimensional Type Theory 
https://www.cs.cmu.edu/~rwh/papers/chitt/popl17.pdf


--
Bruno Bentzen
https://sites.google.com/site/bbentzena/

On Wednesday, April 5, 2017 at 5:19:43 AM UTC+8, Fernando Yamauti wrote:
>
>   Oi Bruno,
>
>   Obrigado pelas referencias. Eu já conhecia todas elas menos a do Walsh 
> (que vou ler depois com mais calma, mas aparentemente o que ele faz é pegar 
> a imagem da diagonal pelo elemento final da fibra em A, mas isso leva a um 
> problema semelhante ao do artigo do Ladyman e Presnell, já que uma 
> categoria em geral tem elementos a mais; elementos locais, por exemplo, em 
> um no topos de feixes que tem seções que não são globais). Infelizmente 
> ainda acho as justificativas pré-formais dadas nesses artigos um tanto 
> insuficientes. E, além disso, tenho objeções às justificativas dadas no 
> caso extensional (as duas ultimas abaixo). 
>
>   A do Tsementzis só substitui um problema por outro, já que a 
> (meta)matemática não trata de espaços e, sim, de juízos sobre proposições. 
> No final o paper só descreve o modelo simplicial de uma maneira mais 
> intuitiva (e meio bagunçada para alguém que já sabe homotopia), mas, para 
> isso ocorrer, é necessário acreditar no modelo simplicial. 
>
>   A do Ladyman e Presnell também me parece um tanto insuficiente. Por 
> exemplo, um tipo A \times B pode ter mais termos que somente os (a, b) com 
> a : A e b: B. O que são esses termos? O que é uma prova de A \times B que 
> não pode ser definicionalmente modificada para se quebrar em provas de A e 
> B, respectivamente? Esse é o exemplo mais banal, enquanto, no artigo, é 
> usado algo mais envolvido de mesma natureza, a contratibilidade da fibra do 
> espaço dos caminhos. 
>
>   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.
>
>   Felizmente, só "trabalho" (brinco) com os modelos (infinito) categorias, 
> então mesmo se todo o construtivismo como 

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

[Fernando Yamauti]

  Oi Bruno,

  Obrigado pelas referencias. Eu já conhecia todas elas menos a do Walsh
(que vou ler depois com mais calma, mas aparentemente o que ele faz é pegar
a imagem da diagonal pelo elemento final da fibra em A, mas isso leva a um
problema semelhante ao do artigo do Ladyman e Presnell, já que uma
categoria em geral tem elementos a mais; elementos locais, por exemplo, em
um no topos de feixes que tem seções que não são globais). Infelizmente
ainda acho as justificativas pré-formais dadas nesses artigos um tanto
insuficientes. E, além disso, tenho objeções às justificativas dadas no
caso extensional (as duas ultimas abaixo).

  A do Tsementzis só substitui um problema por outro, já que a
(meta)matemática não trata de espaços e, sim, de juízos sobre proposições.
No final o paper só descreve o modelo simplicial de uma maneira mais
intuitiva (e meio bagunçada para alguém que já sabe homotopia), mas, para
isso ocorrer, é necessário acreditar no modelo simplicial.

  A do Ladyman e Presnell também me parece um tanto insuficiente. Por
exemplo, um tipo A \times B pode ter mais termos que somente os (a, b) com
a : A e b: B. O que são esses termos? O que é uma prova de A \times B que
não pode ser definicionalmente modificada para se quebrar em provas de A e
B, respectivamente? Esse é o exemplo mais banal, enquanto, no artigo, é
usado algo mais envolvido de mesma natureza, a contratibilidade da fibra do
espaço dos caminhos.

  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.

  Felizmente, só "trabalho" (brinco) com os modelos (infinito) categorias,
então mesmo se todo o construtivismo como enunciado na HoTT estiver
"errado" ainda tenho motivos para estudá-lo :)

   Abs,
   Fernando Yamauti





Em 4 de abril de 2017 10:10, Bruno Bentzen  escreveu:

> Oi Fernando,
>
> Talvez você possa se interessar também por esta animada discussão na FOM
>
> https://www.cs.nyu.edu/pipermail/fom/2016-March/019575.html
>
> que chegou a ser uma thread bem animada no mês de março do ano passado
> (inclusive este paper é mencionado).
>
> O Ladyman e o Presnell parecem ter sido os primeiros a sugerir que uma
> justificativa para as regras da identidade da HoTT deva ser apresentada de
> uma maneira 'pré-matemática'. De lá para cá tem havido outras propostas de
> justificação diferentes. Uma delas é a proposta inferencialista do Patrick
> Walsh que possui uma abordagem bastante inspirada na teoria das categorias
>
> https://www.academia.edu/22231067/Categorical_Harmony_and_Path_Induction
>
> Uma outra é a do Dimitris Tsementzis, que é uma explicação pré-formal para
> a HoTT baseada em "noções espaciais":
>
> http://philsci-archive.pitt.edu/12824/
>
> Abraços,
> Bruno
>
> --
> Bruno Bentzen
> https://sites.google.com/site/bbentzena/
>
> On Tuesday, April 4, 2017 at 12:30:25 AM UTC+8, Fernando Yamauti wrote:
>>
>> Muito obrigado!
>>
>> Em 3 de abril de 2017 13:28, Hermógenes Oliveira <
>> hermogene...@student.uni-tuebingen.de> escreveu:
>>
>>> Fernando Yamauti  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 

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

[Famadoria]

Melhor considerar exemplos específicos. 

Sent from my iPhone

> On 4 Apr 2017, at 10:10, Bruno Bentzen  wrote:
> 
> Oi Fernando,
> 
> Talvez você possa se interessar também por esta animada discussão na FOM 
> 
> https://www.cs.nyu.edu/pipermail/fom/2016-March/019575.html
> 
> que chegou a ser uma thread bem animada no mês de março do ano passado 
> (inclusive este paper é mencionado).
> 
> O Ladyman e o Presnell parecem ter sido os primeiros a sugerir que uma 
> justificativa para as regras da identidade da HoTT deva ser apresentada de 
> uma maneira 'pré-matemática'. De lá para cá tem havido outras propostas de 
> justificação diferentes. Uma delas é a proposta inferencialista do Patrick 
> Walsh que possui uma abordagem bastante inspirada na teoria das categorias
> 
> https://www.academia.edu/22231067/Categorical_Harmony_and_Path_Induction
> 
> Uma outra é a do Dimitris Tsementzis, que é uma explicação pré-formal para a 
> HoTT baseada em "noções espaciais":
> 
> http://philsci-archive.pitt.edu/12824/
> 
> Abraços,
> Bruno
> 
> --
> Bruno Bentzen
> https://sites.google.com/site/bbentzena/
> 
>> On Tuesday, April 4, 2017 at 12:30:25 AM UTC+8, Fernando Yamauti wrote:
>> Muito obrigado!
>> 
>> Em 3 de abril de 2017 13:28, Hermógenes Oliveira 
>>  escreveu:
>>> Fernando Yamauti  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.
>>> 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.
>> 
> 
> -- 
> 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+unsubscr...@dimap.ufrn.br.
> Para postar nesse grupo, envie um e-mail para logica-l@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ê 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/53FDAE62-925F-47A2-B2C6-F7F02730283C%40gmail.com.

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

[Bruno Bentzen]

Oi Fernando,

Talvez você possa se interessar também por esta animada discussão na FOM 

https://www.cs.nyu.edu/pipermail/fom/2016-March/019575.html

que chegou a ser uma thread bem animada no mês de março do ano passado 
(inclusive este paper é mencionado).

O Ladyman e o Presnell parecem ter sido os primeiros a sugerir que uma 
justificativa para as regras da identidade da HoTT deva ser apresentada de 
uma maneira 'pré-matemática'. De lá para cá tem havido outras propostas de 
justificação diferentes. Uma delas é a proposta inferencialista do Patrick 
Walsh que possui uma abordagem bastante inspirada na teoria das categorias

https://www.academia.edu/22231067/Categorical_Harmony_and_Path_Induction

Uma outra é a do Dimitris Tsementzis, que é uma explicação pré-formal para 
a HoTT baseada em "noções espaciais":

http://philsci-archive.pitt.edu/12824/

Abraços,
Bruno

--
Bruno Bentzen
https://sites.google.com/site/bbentzena/

On Tuesday, April 4, 2017 at 12:30:25 AM UTC+8, Fernando Yamauti wrote:
>
> Muito obrigado!
>
> Em 3 de abril de 2017 13:28, Hermógenes Oliveira <
> hermogene...@student.uni-tuebingen.de > escreveu:
>
>> Fernando Yamauti  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 .
>> 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
>> .
>>
>
>

-- 
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/28e4c785-a336-4b64-989f-42e3de6a9f6f%40dimap.ufrn.br.

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

[Fernando Yamauti]

Muito obrigado!

Em 3 de abril de 2017 13:28, Hermógenes Oliveira <
hermogenes.olive...@student.uni-tuebingen.de> escreveu:

> Fernando Yamauti  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+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/87wpb1tpz7.fsf%40camelot.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/CAJGvw-3gB634mxKewjO5gmpbkmy8xooig7i26cXnEpnCWRSf7w%40mail.gmail.com.

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

[Hermógenes Oliveira]

Fernando Yamauti  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+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/87wpb1tpz7.fsf%40camelot.oliveira.

[Logica-l] Philosophia Mathematica Vol 23 Issue 3

[Fernando Yamauti]

 Oi,

 Será que alguém teria acesso ao paper 

   1. 
   
   Ladyman, J., Presnell, S.: Identity in Homotopy Type Theory, Part I: 
   TheJustification of Path Induction. Philosophia Mathematica (2015) 
   
   ?
   
 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/15c58d6c-58c9-4fec-9e39-e30f4c4609ed%40dimap.ufrn.br.