para os teóricos das demonstrações avaliarem

[Joao Marcos]

On the Canonicity of Linear Logic Connectives
https://prooftheory.blog/2026/06/03/on-the-canonicity-of-linear-logic-connectives/

A conclusão é de que "[...] only the additive connective[s] should
really be considered canonical".

Any comments?
JM

[Elaine Pimentel]

Caro João,

Obrigada pela mensagem. O BlogPost é interessante e a conclusão (como o texto do blog) concerne ILL apenas.

Mais interessante, a meu ver, foi a palestra do Rodolfo Ertola-Biraben no SLALM semana passada (https://slalm21.uniandes.edu.co/en/), onde ele apresentou o resultado do artigo (em conjunto com Branden Fitelson) https://www.jstor.org/stable/27424523 que mostra que a implicação na lógica intuicionista *não é canônica* (eles usam o termo "unívoca") se consideramos o sistema axiomático usual. 

Me parece mais razoável definir "canonicidade" em relação a um sistema específico (tipo sequentes, sistemas diádicos, dedução natural, bunches, Hilbert, etc), como de fato fazem Rodolfo e Branden.

Abraços,

Elaine.

--
LOGICA-L
Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica <logi...@dimap.ufrn.br>
---
Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+u...@dimap.ufrn.br.
Para ver esta conversa, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LgxA02vCkEaMCzn%3DMN5f-z8BjRbsdtYU2hH1ARDQxs4Dw%40mail.gmail.com.

--

Elaine. 

-----------------------------------

Elaine Pimentel

Schools Outreach Lead

Professor of Logic and Computation

Deputy Director of the Computer Science and Philosophy programme

Programming Principles, Logic, and Verification 

Department of Computer Science, Office: Room 3.11, 66-72 Gower Street

University College London

URL: https://sites.google.com/site/elainepimentel/

UCL Computer Science is an Athena Swan Gold award winner for gender equality

UCL is ranked among the top ten in the QS World University Rankings 2024 and is winner of The Times and Sunday Times University of the Year 2024

-----------------------------------

[Joao Marcos]

> Mais interessante, a meu ver, foi a palestra do Rodolfo Ertola-Biraben no SLALM semana passada (https://slalm21.uniandes.edu.co/en/), onde ele apresentou o resultado do artigo (em conjunto com Branden Fitelson) https://www.jstor.org/stable/27424523 que mostra que a implicação na lógica intuicionista *não é canônica* (eles usam o termo "unívoca") se consideramos o sistema axiomático usual.
>
> Me parece mais razoável definir "canonicidade" em relação a um sistema específico (tipo sequentes, sistemas diádicos, dedução natural, bunches, Hilbert, etc)

De acordo! Mas creio que isso também mostra mais uma razão pela qual
o problema geral de "colapso" de conectivos (isto é, a questão ligada
a determinar quando dois conectivos presentes numa mesma lógica devem
ser considerados, em última análise, um único conectivo) é geralmente
*mal definido*. Por exemplo, o alegado colapso da implicação
intuicionista com a implicação clássica, que ocorre quando
consideramos que estes conectivos são introduzidos via cálculos de
sequentes ou sistemas de dedução natural, NÃO ocorre quando estes
conectivos são introduzidos via sistemas axiomáticos hilbertianos.
Portanto, mais uma vez estamos falando de uma propriedade *não
intrínseca à lógica*, mas de fato bastante dependente da forma de
apresentação dedutiva de uma dada lógica, e dependente portanto dos
recursos expressivos da formalização escolhida. O alegado "colapso",
portanto, diz mais sobre o uso de cálculo de sequentes ou de dedução
natural do que propriamente sobre a combinação de lógicas... Para uma
conclusão mais positiva e menos drástica, podemos dizer talvez que o
conceito de "colapso" é relativo a um critério de individuação de
conectivos, e diferentes formalismos dedutivos podem incorporar
critérios diferentes. Você concorda?

> como de fato fazem Rodolfo e Branden.

Sim, mas parece neste caso fundamental apontar que se um sistema
axiomático hilbertiano possui dois conectivos que respeitam as mesmas
regras mas não "colapsam" um no outro (ou seja, eles não são
*sinônimos*), isto ocorre porque a lógica *não é congruencial* (isto
é, não respeita a meta-propriedade de intersubstitutividade de
equivalentes). No artigo de Biraben e Branden eles acrescentam uma
nota sobre sinonímia, mas infelizmente não discutem a
[não-]congruencialidade das variantes do sistema LHJ ali
consideradas...

O Humberstone tem um artigo muito substancial chamado "Identical
Twins, Deduction Theorems, and Pattern Functions", de 2006, no qual
ele exibe um sistema contendo duas implicações que se comportam em
separado exatamente como a implicação de BCSK (que é, de certo modo,
uma "implicação clássica"), mas que não "colapsam" uma sobre a outra.
[Nota: Humberstone toma a terminologia "identical twins" de um artigo
de 1953 do Lukasiewicz.] No interessante artigo de "Logical
discrimination", de 2005, Humberstone discute o fenômeno mais amplo
das *distinções conceituais* expressáveis por uma determinada lógica,
de acordo com a sua força dedutiva e consequente "poder
discriminatório" (e de acordo também com esta lógica ser apresentada
no framework Fmla, Set-Fmla, ou Set-Set, os quais possuem diferentes
capacidades de "discriminação") e a sua conexão com a
congruencialidade (que é, esta sim, uma propriedade intrínseca de uma
determinada lógica, não dependendo portanto em absoluto de qual
formalismo dedutivo foi escolhido para apresentar esta lógica).

Abraços,
Joao Marcos

--
https://sites.google.com/site/sequiturquodlibet/

[Elaine Pimentel]

Interessante.

Mas, voltando ao tema da canonicidade, penso que conectivos não canônicos em um determinado sistema dedutivo podem abrir uma avenida para explorar propriedades das derivações que permanecem invisíveis em sistemas axiomáticos. Na verdade, a resposta do Dale Miller ao blog post que iniciou esta troca de mensagens ilustra bem esse ponto.

Por exemplo, se queremos provar que o 12º número de Fibonacci é 144, podemos adotar uma estratégia inteligente e reutilizar resultados já obtidos (por exemplo, que o 3º número de Fibonacci é 2) para calcular os números seguintes. Ou podemos, sempre que necessário, recalcular o 3º número de Fibonacci desde o início, o que leva a uma explosão exponencial no tamanho da derivação. Essa distinção pode ser capturada por meio de uma não canonicidade de predicados atômicos.

Ótimo poder contar com essa diversidade de temas e interesses dentro da lógica. :)

Abraços,

[Thiago Gomes]

Car@s,

Complementando a discussão, recentemente o P. Milne publicou um artigo sobre o assunto. https://link.springer.com/article/10.1007/s11225-025-10211-y

Milne argumenta que, na abordagem de Belnap, a garantia da unicidade da negação intuicionista depende fundamentalmente da "open-endness" na caracterização dedutiva. Ele também problematiza se essa mesma abordagem poderia ser aceita sob uma perspectiva inferencialista dummettiana, uma vez que a exigência de manifestabilidade do significado pelas práticas dedutivas parece incompatível com a exigência belnapiana. Assim, o artigo sugere que, na raiz do problema, reside um debate mais profundo sobre a própria natureza da teoria do significado.

Atenciosamente,
Thiago.

[Joao Marcos]

> Complementando a discussão, recentemente o P. Milne publicou um artigo sobre o assunto.
> https://link.springer.com/article/10.1007/s11225-025-10211-y

Obrigado pela referência, Thiago! Mais uma vez, uma parte essencial
da discussão parece ser empurrada inteirinha para uma nota de pé de
página, não é? (nota 19)

Um dos lógicos que mais profundamente estudou questões de "unicidade
de conectivos" é seguramente o Humberstone, citado apenas muito
brevemente nesta nota. Copio aqui um trecho curto do segundo
parágrafo do verbete SEP dele sobre "Sentence Connectives in Formal
Logic":

"[...] whether a given connective is uniquely characterized—in the
sense of being governed by rules which when reduplicated to govern a
new connective render compounds formed from the same component
sentences using the original and the new connective completely
interchangeable—is relative not just to a logic but to a particular
proof system (set of rules systematizing the logic)"

Você diria que algo controverso foi dito neste trecho?

> Milne argumenta que, na abordagem de Belnap, a garantia da unicidade da negação intuicionista depende fundamentalmente da "open-endness" na caracterização dedutiva.

... caracterização esta que deve ocorrer, forçosamente, via dedução
natural? (em caso afirmativo, por quê?!)

Sobre "open-endedness", segundo entendi, esta consiste na ideia de que
uma regra de inferência não governa apenas uma linguagem fixada de
antemão, mas também quaisquer extensões futuras dessa linguagem. Em
sistemas axiomáticos usuais isto está automaticamente garantido. Nos
sistemas de dedução natural, com regras esquemáticas sem um co-domínio
de instanciação escolhido de antemão ---como os que eu ensino para os
meus alunos--- também está garantido... Não é este o standard, em
geral? (Quer dizer, o argumento central do artigo em questão
certamente pareceria mais relevante/urgente/informativo se os
praticantes de dedução natural em geral _não_ assumissem
"open-endedness" ao explicitarem as regras de introdução e de
eliminação com as quais trabalharão, não é?)

Abraços, Joao Marcos

--
https://sites.google.com/site/sequiturquodlibet/

[Thiago Gomes]

Bom dia,

Sobre o trecho do Humberstone: 

Concordo plenamente que a unicidade é relativa ao sistema de prova. Mas gostaria de sugerir que essa relatividade não é um indicativo de que a noção seja mal definida ou secundária. Antes ela aponta para a insuficiência de um certo critério de identidade entre lógicas. No apêndice 1.2 do grandioso The Connectives, Humberstone aponta quatro níveis em que uma lógica pode ser individuada. Em uma passagem ele diz: 

"The example of independence indicates that there are some questions about systems of logic which can only sensibly be raised if system of logic is understood as meaning collection of rules. There are numerous other such examples, including the question of whether (e.g.) intuitionistic logic uniquely characterizes the connective ¬." 

> caracterização esta que deve ocorrer, forçosamente, via dedução
natural? (em caso afirmativo, por quê?!)

Acredito que a escolha por dedução natural(o mesmo vale pra sequentes) se dá pelo modo como este sistema torna explicito(noção, talvez, não muito lógica kk) o papel inferencial de cada conectivo isoladamente.

>  o argumento central do artigo em questão certamente pareceria mais relevante/urgente/informativo se os praticantes de dedução natural em geral _não_ assumissem "open-endedness" ao explicitarem as regras de introdução e de eliminação com as quais trabalharão, não é?  

Acho filosoficamente informativo afirmar que a noção de "open-endness"(e, portanto, a unicidade) seja incompatível com a abordagem inferencialista dummetiana, mas não sei ao certo se esta é uma propriedade mais forte que a instanciação de regras esquemáticas. (De todo modo, Milne parece pensar que sim.).

Abraços
Thiago

[Joao Marcos]

> > caracterização esta que deve ocorrer, forçosamente, via dedução
> natural? (em caso afirmativo, por quê?!)
>
> Acredito que a escolha por dedução natural(o mesmo vale pra sequentes) se dá pelo modo como este sistema torna explicito(noção, talvez, não muito lógica kk) o papel inferencial de cada conectivo isoladamente.

Mas a desvantagem de escolher cálculos de sequentes (ou, como caso
particular, dedução natural) parece muito grande se ao juntarmos
regras de diferentes conectivos os sistemas resultantes têm o
potencial de gerar interações indesejadas... De que forma estamos
"isolando o papel inferencial de cada conectivo" se: (1) ao juntarmos
as regras da conjunção com as regras da disjunção (clássica ou
intuicionista, dá no mesmo), elas dão origem magicamente a esquemas
relativos à distributividade, ou à absorção? (2) ao juntarmos as
regras da negação clássica às regras da implicação intuicionista, o
resultado é que a implicação se torna clássica? (3) ao juntarmos duas
implicações diferentes, digamos clássica e intuicionista, estas acabam
colapsando uma na outra?

Se o critério de escolha de formalismo dedutivo se baseia no desejo de
analisar "o papel inferencial de cada conectivo isoladamente", então a
questão parece ter mais a ver com a *analiticidade* do sistema do que
com a escolha de formalismo dedutivo... Note que o problema de
não-analiticidade dos sistemas hilbertianos no framework Set-Fmla não
se aplica ao framework Set-Set. Neste último framework, em muitos
casos, é perfeitamente possível analisar as regras de cada conectivo
_realmente_ em separado dos demais. Um inferencialista não deveria se
interessar por isso?
Referências:
- parte II do livro "Multiple-conclusion Logic", de Shoesmith & Smiley, 1978
- artigos de Caleiro & Marcelino nos anais do 26th WoLLIC (2019), e na
Synthese (2021).

> > o argumento central do artigo em questão certamente pareceria mais relevante/urgente/informativo se os praticantes de dedução natural em geral _não_ assumissem "open-endedness" ao explicitarem as regras de introdução e de eliminação com as quais trabalharão, não é?
>
> Acho filosoficamente informativo afirmar que a noção de "open-endness"(e, portanto, a unicidade) seja incompatível com a abordagem inferencialista dummetiana, mas não sei ao certo se esta é uma propriedade mais forte que a instanciação de regras esquemáticas. (De todo modo, Milne parece pensar que sim.).

Entendi. Mas observe que eu NÃO disse que "open-endedness" é
diretamente garantida pela esquematicidade das regras (reitero: "[...]

com regras esquemáticas sem um co-domínio de instanciação escolhido de

antemão").

Há duas formas mais ou menos _standard_ de garantir tal propriedade, contudo:

(1) Usando variáveis especiais que garantam que as regras não sejam
formuladas de modo a estarem ligadas a uma linguagem específica, e
estejam portanto prontas para se aplicarem antes e depois de eventuais
extensões linguísticas.
(Referência: artigo "Fibring of logics as a categorial
construction", no JLC de 1999)

(2) Usando explicitamente uma regra de substituição que se aplique
sempre sobre toda a linguagem que temos à disposição, antes e depois
de uma eventual extensão linguística.
(Referência: praticamente qualquer apresentação axiomática
encontrada na literatura)

Acho interessante, na realidade, apontar a importância da
"open-endedness", principalmente tendo em vista o fato de que grande
parte dos sistemas não-hilbertianos que encontramos na literatura
parece descuidar disso, e acabam não garantindo tal propriedade --- o
que é grave... Mas a minha questão é: há uma variedade de sistemas na
literatura de Teoria das Demonstrações que tenham sido formulados _de
propósito_ de modo a NÃO serem "open-endedness"? (ou será que há
sistemas que simplesmente foram formulados ---reitero, de maneira
descuidada--- de modo a não terem tal propriedade, e que com isto
resultam não serem capazes de acomodar extensões linguísticas, e não
se prestarem assim, por exemplo, a aplicações relevantes ao problema
de *combinar lógicas* via fibrilação?)

[]s, Joao Marcos

--
https://sites.google.com/site/sequiturquodlibet/

[Thiago Gomes]

Não conhecia essa forma de produzir sistemas axiomáticos analíticos. Sem dúvida é algo a ser olhado. Obrigado pelas referências.

(Um outro motivo que justifica a preferência por sistemas ND ou sequentes é a forma como raciocínios hipotéticos são introduzidos, mas isso já é outra questão)

Sobre a questão de sistemas propositalmente "não open-ended", tenho uma dúvida. Suponha que eu tenho duas lógicas que, isoladamente, são fechadas por substituições. Por alguma razão ao combina-las, eu deliberadamente _não_ fecho a combinação por substituição, com o objetivo de impedir que as fórmulas se misturem descontroladamente. Nesse caso, eu ainda posso dizer que o sistema combinado é "open-ended"? Ou essa propriedade se perde necessariamente?

Abraços,

Thiago

[Joao Marcos]

Viva, Thiago:

> (Um outro motivo que justifica a preferência por sistemas ND ou sequentes é a forma como raciocínios hipotéticos são introduzidos, mas isso já é outra questão)

Uma questão sem dúvida interessantíssima! A habilidade de fazer
*raciocínio hipotético* é sem dúvida uma das primeiras coisas que
devemos ensinar aos nossos alunos, em qualquer nível de ensino. A
outra habilidade lógica a ensinar, igualmente importante, é a de
apresentar evidências argumentativas na forma de *justificativas* para
o raciocínio --- e isto é parte integrante dos sistemas dedutivos em
geral, e da dedução natural em particular.

> Sobre a questão de sistemas propositalmente "não open-ended", tenho uma dúvida. Suponha que eu tenho duas lógicas que, isoladamente, são fechadas por substituições. Por alguma razão ao combina-las, eu deliberadamente _não_ fecho a combinação por substituição, com o objetivo de impedir que as fórmulas se misturem descontroladamente.

Hummm, o que seria uma "mistura descontrolada de fórmulas"? Do ponto
de vista de uma fórmula da lógica 1 uma subfórmula que vem da lógica 2
(e vice-versa), funciona como uma caixinha impenetrável... Se não
fecharmos por substituição, por outro lado, será que podemos dizer que
houve mesmo a _combinação_ dos dois sistemas?

> Nesse caso, eu ainda posso dizer que o sistema combinado é "open-ended"? Ou essa propriedade se perde necessariamente?

Com efeito, em tal caso (hipotético!) a propriedade pode facilmente se
perder. É justamente por isso que, ao combinar lógicas ou ao
simplesmente expandir [*] a linguagem de uma determinada lógica, _em
geral_, o "padrão" é que as substituições passam a se aplicar sobre
toda a nova linguagem. O curioso é que pouca gente parece se lembrar
de explicitar isso, ao apresentar seus sistemas dedutivos favoritos.

João Marcos


[*] A terminologia vem da álgebra, onde é usual falar na *expansão*
[conservativa, neste caso] de um grupo abeliano, digamos, para um anel
(ou, mais frequentemente, na direção contrária, falar no grupo
abeliano associado ao anel como o seu *reduto*); as novas operações
"multiplicativas" acrescentadas pelo anel interagem naturalmente com
as operações "aditivas" que já estavam presentes no grupo, e as
equações que valiam para o grupo passam a valer também na linguagem
expandida do anel. Igualmente, na combinação de lógicas, o interesse
reside na produção de expansões conservativas (com um _mínimo_ de
interação).


--
https://sites.google.com/site/sequiturquodlibet/