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.