Philosophia Mathematica Vol 23 Issue 3

[Fernando Yamauti]

     Oi,

     Será que alguém teria acesso ao paper 

16. Ladyman, J., Presnell, S.: Identity in Homotopy Type Theory, Part I: TheJustification of Path Induction. Philosophia Mathematica (2015)   ?

     Abs,

     Fernando Yamauti

[Hermógenes Oliveira]

Fernando Yamauti <fgya...@gmail.com> escreveu:

> Oi,
>
> Será que alguém teria acesso ao paper
>

> 1 Ladyman, J., Presnell, S.: Identity in Homotopy Type Theory, Part I:
> The Justification of Path Induction. Philosophia Mathematica (2015) ?

Coincidência. Eu li esse artigo recentemente. A versão que eu li está
disponível em

http://philsci-archive.pitt.edu/11079/1/Identity_in_HTT_public.pdf

Sem contar o selinho da Oxford University Press, não sei se há muitas
diferenças entre a versão acima e a versão oficial.

Além das páginas tradicionais,

https://homotopytypetheory.org/links/
https://ncatlab.org/nlab/show/homotopy+type+theory#References

mais referências interessantes para quem estiver estudando Teoria
Homotópica dos Tipos podem ser encontradas no repositório do grupo de
estudos que estamos organizando aqui em Tübingen:

https://github.com/BinderDavid/HoTT-StudyGroup

--
Hermógenes Oliveira

[Fernando Yamauti]

Muito obrigado!

--
Hermógenes Oliveira

--
Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscribe@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logi...@dimap.ufrn.br.
Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/87wpb1tpz7.fsf%40camelot.oliveira.

[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 <fgya...@gmail.com> escreveu:

> Oi,
>
> Será que alguém teria acesso ao paper
>
> 1 Ladyman, J., Presnell, S.: Identity in Homotopy Type Theory, Part I:
> The Justification of Path Induction. Philosophia Mathematica (2015) ?

Coincidência.  Eu li esse artigo recentemente.  A versão que eu li está
disponível em

http://philsci-archive.pitt.edu/11079/1/Identity_in_HTT_public.pdf

Sem contar o selinho da Oxford University Press, não sei se há muitas
diferenças entre a versão acima e a versão oficial.

Além das páginas tradicionais,

https://homotopytypetheory.org/links/
https://ncatlab.org/nlab/show/homotopy+type+theory#References

mais referências interessantes para quem estiver estudando Teoria
Homotópica dos Tipos podem ser encontradas no repositório do grupo de
estudos que estamos organizando aqui em Tübingen:

https://github.com/BinderDavid/HoTT-StudyGroup

--
Hermógenes Oliveira

--
Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google.

Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+u...@dimap.ufrn.br.

[Famadoria]

Melhor considerar exemplos específicos. 

Sent from my iPhone

--
Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos Grupos do Google.

Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+u...@dimap.ufrn.br.

Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
Acesse esse grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/28e4c785-a336-4b64-989f-42e3de6a9f6f%40dimap.ufrn.br.

[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

   

   

      

--
Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscribe@dimap.ufrn.br.

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

Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+u...@dimap.ufrn.br.

[Hermógenes Oliveira]

Fernando Yamauti <fgya...@gmail.com> 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 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.

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.

> [...]

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

Na minha opinião, o potencial explanatório e de fundamentação da
Teoria Intuicionista de Tipos (TIT) se estraçalha a partir do momento
que se introduz universos. A partir daí, me parece, a TIT assume um
caráter fortemente ad hoc e muitas da intuições iniciais vão para o
espaço. Neste ponto, a única vantagem de TIT em comparação à ZF (sua
concorrente igualmente ad hoc), principalmente se você é um computeiro
ou matemático preocupado com computabilidade, é o fato de TIT ser
construtiva. Por outro lado, os argumentos de que ZF seria
filosoficamente mais robusta e conceitualmente mais coerente (ver, por
exemplo, Harvey Friedman na FOM) não me convencem. Acontece que, dado
que ZF é a doutrina ortodoxa, estamos acostumados a fazer vista grossa
para as aberrações em ZF e maldizer excessivamente qualquer
idiossincrasia de propostas alternativas, como TIT.

De qualquer maneira, mesmo num contexto muito elementar, abordar o
intuicionismo, ou construtivismo, de um ponto de vista epistemológico,
tal como Martin-Löf faz, me parece um equívoco. Concordo ainda que a
discussão epistemológica de Martin-Löf em conexão com a fundamentação
da sua Teoria de Tipos é muito confusa, para se dizer o mínimo.

A epistemologia, contudo, não é a única rota para o intuicionismo, e
sequer me parece a melhor. No âmbito puramente lógico, uma rota mais
interessante rumo ao intuicionismo passa pela filosofia da linguagem,
em particular, por um certo pragmatismo linguístico. Neste sentido,
princípios lógicos estariam apoiados em práticas linguísticas regradas
(ver trabalho recente do Marcos Silva). Esse tipo de inferencialismo
lógico ainda é muito incipiente, é verdade, mas me parece muito
promissor.

Saudações,

Referências:

[1] Arend Heyting. G. F. C. Griss and his negationsless
intuitionistic mathematics. Synthese 9 (1):91-96, 1955.
(ver referências nesse artigo para os escritos de Griss)

[2] Ingebrigt Johansson. Der Minimalkalkül, ein reduzierter
intuitionistischer Formalismus. Compositio Mathematica 4, 119-136,
1937.

[3] Neil Tennant. The Taming of the True. Clarendon Press, 1997.
(ver também artigos no RSL sobre "Core Logic")

[4] Peter Schroeder-Heister. The Categorical and the Hypothetical: A
critique of some fundamental assumptions of standard
semantics. Synthese 187 (3), 925-942, 2012.

[5] Wagner de Campos Sanz, Thomas Piecha and Peter
Schroeder-Heister. Constructive Semantics, Admissibility of Rules and
the Validity of Peirce's Law. Logic Journal of the IGPL 22 (2),
297-308, 2014.

[6] Thomas Piecha, Wagner de Campos Sanz and Peter
Schroeder-Heister. Failure of Completeness in Proof-Theoretic
Semantics. Journal of Philosophical Logic 44 (3), 321-335, 2015.

[7] Per Martin-L\"of. On the Meanings of the Logical Constants and the
Justifications of the Logical Laws. Nordic Journal of Philosophical
Logic 1 (1), 11-60, 1996.

--
Hermógenes Oliveira

[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

[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

--
Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+u...@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logi...@dimap.ufrn.br.
Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.

Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/87a87tof1w.fsf%40camelot.oliveira.

[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 

--
Hermógenes Oliveira

--
Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google.

Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscribe@dimap.ufrn.br.

Para postar neste grupo, envie um e-mail para logi...@dimap.ufrn.br.
Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.

Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/87shllitep.fsf%40camelot.oliveira.

--

Valeria de Paiva
http://vcvpaiva.github.io/
http://research.nuance.com/author/valeria-de-paiva/
http://www.cs.bham.ac.uk/~vdp/

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

[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

  

[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 argumento em seu favor.  

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.

Abraços lógicos,

Bruno

[1] – Bob Harper. Constructive mathematics is not meta-mathematics. https://existentialtype.wordpress.com/2013/07/10/constructive-mathematics-is-not-meta-mathematics/

[2] – Bob Harper. Extensionality, Intensionality, and Brouwer’s Dictum. https://existentialtype.wordpress.com/2012/08/11/extensionality-intensionality-and-brouwers-dictum/

[3] – Per Martin-Löf. Analytic and Synthetic Judgements in Type Theory. 1994

[4] – Per Martin-Löf. Constructive mathematics and computer programming. 1982

[5] – PRL Group. Implementing Mathematics with The Nuprl Proof Development System. 1985.

--

Bruno Bentzen

https://sites.google.com/site/bbentzena/

[Hermógenes Oliveira]

Joao Marcos <boto...@gmail.com> 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

[Hermógenes Oliveira]

Fernando Yamauti <fgya...@gmail.com> 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 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.

É possível ainda que eu não tenha compreendido muito bem o seu
comentário.

> Também acho que a definição de universo univalente é bem intuitiva e
> consistente com a pratica matemática. O universo é só um objeto a mais
> na teoria que mostra a compatibilidade da identidade com a
> equivalência homotópica. Eles fazem o mesmo papel dos V_{\kappa}. E
> como a TIT deve ser semântica e sintática ao mesmo tempo, acho natural
> colocar um universo (ou melhor, uma estratificação em universos) na
> teoria. Gostaria, portanto, de entender o que gera essa tal destruição
> do potencial explanatório da TIT.

O principal problema com os universos é que eles borram a distinção
entre os juízos "A é um tipo" e "x tem o tipo A" (i.e. A é habitado).
Na presença de universos, o juízo "B é um tipo" se reduz a um juízo da
forma "x tem o tipo A" ou "x é um termo do tipo A", onde A é um
universo. Tecnicamente, isso pode até ser muito conveniente, mas,
filosoficamente, é desastroso.

Sem me alongar muito, creio que a gravidade do problema pode ser
depreendida de uma leitura atenta e refletiva do artigo de fundamentação
do Martin-Löf[1]. Ali, ele discorre sobre a importância em se
distinguir entre os juízos "A prop" ("A é um tipo", pois ali o único
tipo tratado é o tipo das proposições) e "A true" ("x tem o tipo A", "o
tipo proposicional A é habitado", "x é uma prova de A"). Esta distinção
me parece importantíssima para o funcionamento da teoria como
fundamentação filosófica. Quando se introduz universos, toda as
intuições e coerência filosófica que estavam apoiadas nesta distinção
vão para o espaço.

Qual seria o valor como fundamentação filosófica de uma teoria
construtiva se, todas as vezes que efetuo uma construção com base nos
princípios básicos da teoria, tenho que verificar, *caso a caso*, se as
construções são bem tipadas sob pena de inconsistência?

A justificativa para a adição de universos é basicamente ad hoc: por que
eles são necessários para se fazer matemática para além da
aritméticazinha de primeira ordem. Nesse sentido, TIT+universos não me
parece menos ad hoc do que ZF. Eu, particularmente, tenho a impressão
de que a introdução irrestrita de universos é a maneira dos
construtivistas de jogar a toalha, após o que Martin-Löf chamou de
"segundo fracasso do programa de Hilbert"[2].

Agora, pode ser que universos sejam intuitivos e essenciais de um ponto
de vista homotópico, mas, até o momento, a aspiração da Teoria
Homotópica dos Tipos (THT) como fundamentação alternativa para a
matemática está apoiada na Teoria Intuicionista de Tipos adjacente, uma
vez que, até o momento, como você mesmo observou, as tentativas de
oferecer explicações e justificativas para os elementos básicos da
teoria por vias diretamente homotópicas, contornando a teoria de tipos,
são insatisfatórias.

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

Brouwer não fazia a mesma coisa. Fazia muito pior!

De qualquer maneira, não considero Brouwer, Heyting, Martin-Löf, ou
qualquer outro, como donos do intuicionismo. Creio que há razões para
ser um intuicionista ou construtivista que independe da exegese desses
autores.


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)

[2] Per Martin-Löf. The Hilbert-Brouwer Controversy Resolved? In: One
Hundred Years of Intuitionism (1907-2007), 243-256, 2008.

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

[Hermógenes Oliveira]

Bruno Bentzen <b.be...@hotmail.com> 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

[Hermógenes Oliveira]

Joao Marcos <boto...@gmail.com> 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

[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

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

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

--
Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+u...@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logi...@dimap.ufrn.br.
Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.

Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/874ly0e5sz.fsf%40camelot.oliveira.

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

[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
> colocar um universo (ou melhor, uma estratificação em universos) na
> teoria. Gostaria, portanto, de entender o que gera essa tal destruição
> do potencial explanatório da TIT.

O principal problema com os universos é que eles borram a distinção
entre os juízos "A é um tipo" e "x tem o tipo A" (i.e. A é habitado).
Na presença de universos, o juízo "B é um tipo" se reduz a um juízo da
forma "x tem o tipo A" ou "x é um termo do tipo A", onde A é um
universo.  Tecnicamente, isso pode até ser muito conveniente, mas,
filosoficamente, é desastroso.

Sem me alongar muito, creio que a gravidade do problema pode ser
depreendida de uma leitura atenta e refletiva do artigo de fundamentação
do Martin-Löf[1].  Ali, ele discorre sobre a importância em se
distinguir entre os juízos "A prop" ("A é um tipo", pois ali o único
tipo tratado é o tipo das proposições) e "A true" ("x tem o tipo A", "o
tipo proposicional A é habitado", "x é uma prova de A").  Esta distinção
me parece importantíssima para o funcionamento da teoria como
fundamentação filosófica.  Quando se introduz universos, toda as
intuições e coerência filosófica que estavam apoiadas nesta distinção
vão para o espaço.

    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?

   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.

 

Brouwer não fazia a mesma coisa.  Fazia muito pior!

   Que bom que concordamos nisso! :)

   Abs,

   Fernando Yamauti

[Hermógenes Oliveira]

Joao Marcos <boto...@gmail.com> 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

[Hermógenes Oliveira]

Fernando Yamauti <fgya...@gmail.com> escreveu:

> Não. A minha sugestão é diferente. \neg A deve ser definido como A
> \cong empty := \sum_{f: A --> empty} isequ (f) . Já iseq (f) é um
> pouco mais complicado de escrever via email, portanto vou pedir que
> olhe a pagina 78 do HoTT book

Isso não faz muito sentido para mim. Em primeiro lugar, o termo sendo
definido, ¬A, não aparece na definição (estou usando "0" para o seu
"empty"): A≅0 := ∑(f: A→0) isequiv(f). A não ser que você já esteja
tomando A→0 como definição de ¬A, mas aí a coisa fica ainda mais
confusa. Em segundo lugar, não me parece muito conveniente, para se
dizer o mínimo, uma abordagem que defina a negação em termos de tipos
mais complexos como a soma ∑ (também conhecido como quantificador
existencial) e tipos de igualdades (uma vez que isequiv(f) é definido de
acordo com os tipos idA e idB para f: A→B).

> Mas isso é considerado quando se usa tipos dependentes. De uma prova
> hipotética \Gamma \vdash A e outra \Delta \vdash \Gamma se
> concatenarmos tudo temos \Delta \vdash \Gamma \vdash A, ou seja, outra
> prova hipotética, não?

Sim. Mas esse não era o ponto.

> [...]

>
> A introdução de 'A prop' como proposição até onde eu entenda serve
> para evitar em falar de um domínio (onde as expressões variam)
> contendo objetos de caráter semânticos e não puramente formais. Em
> contrapartida em Analytic and Synthetic Judgements in Type Theory, ML,
> inspirado por Church, introduz um tipo 'prop' (que é igual a 'set') e
> usa 'A : prop' ao invés de 'A prop' . Além disso, ele introduz um tipo
> 'type' e termos 'i (A) : prop' para cada tipo A.
>
> Portanto, de acordo com a sua afirmação, ML não estaria sendo
> consistente?

Não, não foi isso que eu quis dizer (eu acho). Você está trazendo mais
e mais elementos para a discussão, e eu não estou conseguindo ver a
relação deles com os meus comentários iniciais (isto não significa que
não haja relação, somente que *eu* não estou conseguindo vê-la). Isso
não é ruim, *em si*, mas eu já estou ficando meio velho e não tenho mais
fôlego intelectual para discussões assim. Você poderia, por gentileza,
tentar se focar naquilo que eu escrevi e responder ponto-a-ponto para
que eu possa identificar exatamente aquilo que não ficou claro.

> Desculpe-me, mas ainda estou falhando em entender o que vai para o
> espaço. Creio eu que você esteja pensando em um problema diferente do
> que eu mencionei acima : criar uma estratégia para A variar em
> expressões completas ao invés de proposições, que tem um caráter
> semântico.

Espero que você tenha compreendido, pelo menos, que, com a introdução
*irrestrita* de universos (i.e. com a introdução completa da hierarquia
infinita de universos), nós perdemos a distinção entre os juízos "A é um
tipo" e "x tem o tipo A" (i.e. "x é um termo do tipo A" ou "A é
habitado"). Você poderia dizer: "Tá bem. E daí?" Bem, para
compreender o tamanho da perda, é preciso apreciar o valor da distinção.
Para isso, eu sugeri uma leitura atenta e *reflexiva* dos escritos mais
*filosóficos* do Martin-Löf, com uma mente voltada para fundamentação.
Não fornecerei uma explicação detalhada disso aqui na lista para não
encher ainda mais o saco do pessoal que, a este ponto, já deve estar
lotado de doutrina martin-löfiana. :-)

--
Hermógenes Oliveira

[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 uma mente voltada para fundamentação.
Não fornecerei uma explicação detalhada disso aqui na lista para não
encher ainda mais o saco do pessoal que, a este ponto, já deve estar
lotado de doutrina martin-löfiana. :-)

      Infelizmente, eu não consigo compreender a sua objeção enquanto eu não entender a que parte você está se referindo (assim como mencionei acima).

    Abs,

    Fernando Yamauti

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

[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