Re: [Logica-l] um probleminha com logica intuicionista...

[Fernando Yamauti]

 Oi Valéria,

 Obrigado pelas referências. O Chico respondeu sim. Pelas suas referencias
ficou mais claro: são só (bi)hiperdoutrinas de categorias bicartesianas
fechadas e cocartesianamente cofechadas (nome muito grande!). Nem sabia que
isso tinha utilidade. O caso monoidal parece ser mais interessante, mas
mesmo o caso (co)cartesiano parece que não implica ser uma algebra Booleana
nessas referencias. Portanto algum axioma da diferença simétrica que o
Chico usa não deve valer nessas categorias.

 Abs.

Em 25 de outubro de 2017 20:51, Valeria de Paiva 
escreveu:

> oi Fernando,
> provavelmente o Chico ja respondeu, mas se nao, de uma olhada em
> https://arxiv.org/abs/1708.05896
> A Cointuitionistic Adjoint Logic
>
> ou Crolard's papers:
>
>
>-
>
>“A formulae-as-types interpretation of Subtractive Logic
>”. T. Crolard. 
> *Journal
>of Logic and Computation. Special issue on Intuitionistic Modal Logic and
>Application.* Volume 14, Issue 4, August 2004. pp 529-570.
>
>*Abstract.* We present a formulae-as-types interpretation of
>Subtractive Logic (*i.e.* bi-intuitionistic logic). This presentation
>is two-fold: we first define a very natural restriction of the λμ-calculus
>which is closed under reduction and whose type system is a constructive
>restriction of the Classical Natural Deduction. Then we extend this
>deduction system conservatively to Subtractive Logic. From a computational
>standpoint, the resulting calculus provides a type system for first-class
>coroutines (a restricted form of first-class continuations).
>-
>
>“Subtractive logic
>”. T. Crolard. 
> *Theoretical
>Computer Science* 254:1–2(2001):151-185.*Abstract.* This paper is the
>first part of a work whose purpose is to investigate duality in some
>related frameworks (cartesian closed categories, lambda-calculi,
>intuitionistic and classical logics) from syntactic, semantical and
>computational viewpoints. We start with category theory and we show that
>any bicartesian closed category with coexponents is degenerated (i.e. there
>is at most one arrow between two objects). The remainder of the paper is
>devoted to logical issues. We examine the propositional calculus underlying
>the type system of bicartesian closed categories with coexponents and we
>show that this calculus corresponds to subtractive logic: a conservative
>extension of intuitionistic logic with a new connector (subtraction) dual
>to implication. Eventually, we consider first order subtractive logic and
>we present an embedding of classical logic into subtractive logic.
>
> abs
> Valeria
>
> 2017-10-25 3:21 GMT-07:00 Fernando Yamauti :
>
>>  Oi Chico,
>>
>>  Só uma pergunta idiota. Que adjunção entre a diferença simétrica e a
>> disjunção (que voce havia citado) é essa? Suponho que deva ser algo que
>> vale em qualquer topos Booleano, mas mesmo em Set algo do tipo  (-) \vee A
>> -| (-)  \Delta A  (ou o contrario), onde ambos endofuntores são entre o
>> reticulado dos subobjetos,  não parece ser verdade. Portanto acho que voce
>> esta pensando em algo menos obvio que isso, mas não consegui descobrir o
>> que é...
>>
>>  Abs.
>>
>>
>> Em 24 de outubro de 2017 04:08, Francisco Miraglia 
>> escreveu:
>>
>>> Cara Valéria,
>>>
>>> Observações que talvez possam ser úteis:
>>>
>>> 1) O esquema (A --> B) --> (Ng A --> Ng B) é válido no Intucionismo,
>>> (versão Heyting); as álgebras de Heyting fornecem uma semântica completa
>>> para a versão do Intuicionismo do Arend;
>>>
>>> 2) Adicionar o esquema recíproco à axiomatização de Heyting da Lógica
>>> Intucionista imediatamente fornece a Lógica Clássica; é semelhante ao
>>> que acontece com a equivalência no sistema Intuicionista: se for
>>> distributiva, a Lógica é clássica.
>>>
>>> 3) Estou insistindo em incluir o nome do Arend pois afinal nem sempre
>>> nos lembramos que o Brower tinha a firme opinião que a sua visão da
>>> Lógica era impossível (por definição, já que envolvia a "prática
>>> quotidiana dos matemáticos") de ser axiomatizada.
>>>
>>> 4) Interessante observar que posições filosóficas não se materializam
>>> na "prática quotidiana dos matemáticos": um dos resultados mais conhecidos
>>> de Brower (toda função contínua do disco de dimensão n em sí mesmo possui
>>> ponto fixo) é estabelecido pelo próprio por contradição!
>>> O primeiro passo da contradição já é de ordem grande: não há retração
>>> contínua do disco em sua borda (em qualquer dimensão n maior ou igual a
>>> 1), o que exige métodos homológicos ou homotópicos); exibir o ponto fixo:
>>> "para com isso"
>>>
>>> 5) Quanto à nomenclatura, tanto Heyting, quanto Kleene (e Vesley)  dão o
>>> nome de contraposição ao esquema em (1), sempre chamando a atenção de que ,
>>> no 

Re: [Logica-l] um probleminha com logica intuicionista...

[Valeria de Paiva]

oi Bruno,
desculpe a demora. (quarta-feira 'e um dia complicado por aqui, sua
mensagem foi overlooked...)

mas sim, achei muito BOM ver o seu Cubo e os lambda-termos pra essas 40
derivacoes:

>Uma lista razoável com provas de mais de 40 proposições válidas
intuicionisticamente (incluindo grande parte dos teoremas listados na
entrada citada da Wikipedia) pode ser achada nesta mini biblioteca
 do Cubo. A sintaxe
do sistema é brevemente explicada aqui
. Quaisquer
comentários são bem-vindos. :)

acho que seria legal se a gente unisse os esforcos pra fazer todos os
lambda-termos pros teoremas intuicionistas do Kleene em (S. C. Kleene.
Introduction to metamathematics, volume 1 of Bibliotheca mathematica.
NorthHolland Publishing Co., 1952.).

Eu e a Sara Kalvala usamos esses teoremas intuicionistas faceizinhos do
Kleeene em
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.97.3475=rep1=pdf
pra comecar a pensar numa testsuite de teoremas de Logica Linear.

o que 'e mais interessante aqui 'e pensar nas varias maneiras de adicionar
!'s que fazem os teoremas de IL verdadeiros em LL, isso foi a tese do
Harold Schellinx (
The noble art of linear decorating ) que 'e super interessante!!
abs
Valeria

2017-10-25 15:51 GMT-07:00 Valeria de Paiva :

> oi Fernando,
> provavelmente o Chico ja respondeu, mas se nao, de uma olhada em
> https://arxiv.org/abs/1708.05896
> A Cointuitionistic Adjoint Logic
>
> ou Crolard's papers:
>
>
>-
>
>“A formulae-as-types interpretation of Subtractive Logic
>”. T. Crolard. 
> *Journal
>of Logic and Computation. Special issue on Intuitionistic Modal Logic and
>Application.* Volume 14, Issue 4, August 2004. pp 529-570.
>
>*Abstract.* We present a formulae-as-types interpretation of
>Subtractive Logic (*i.e.* bi-intuitionistic logic). This presentation
>is two-fold: we first define a very natural restriction of the λμ-calculus
>which is closed under reduction and whose type system is a constructive
>restriction of the Classical Natural Deduction. Then we extend this
>deduction system conservatively to Subtractive Logic. From a computational
>standpoint, the resulting calculus provides a type system for first-class
>coroutines (a restricted form of first-class continuations).
>-
>
>“Subtractive logic
>”. T. Crolard. 
> *Theoretical
>Computer Science* 254:1–2(2001):151-185.*Abstract.* This paper is the
>first part of a work whose purpose is to investigate duality in some
>related frameworks (cartesian closed categories, lambda-calculi,
>intuitionistic and classical logics) from syntactic, semantical and
>computational viewpoints. We start with category theory and we show that
>any bicartesian closed category with coexponents is degenerated (i.e. there
>is at most one arrow between two objects). The remainder of the paper is
>devoted to logical issues. We examine the propositional calculus underlying
>the type system of bicartesian closed categories with coexponents and we
>show that this calculus corresponds to subtractive logic: a conservative
>extension of intuitionistic logic with a new connector (subtraction) dual
>to implication. Eventually, we consider first order subtractive logic and
>we present an embedding of classical logic into subtractive logic.
>
> abs
> Valeria
>
> 2017-10-25 3:21 GMT-07:00 Fernando Yamauti :
>
>>  Oi Chico,
>>
>>  Só uma pergunta idiota. Que adjunção entre a diferença simétrica e a
>> disjunção (que voce havia citado) é essa? Suponho que deva ser algo que
>> vale em qualquer topos Booleano, mas mesmo em Set algo do tipo  (-) \vee A
>> -| (-)  \Delta A  (ou o contrario), onde ambos endofuntores são entre o
>> reticulado dos subobjetos,  não parece ser verdade. Portanto acho que voce
>> esta pensando em algo menos obvio que isso, mas não consegui descobrir o
>> que é...
>>
>>  Abs.
>>
>>
>> Em 24 de outubro de 2017 04:08, Francisco Miraglia 
>> escreveu:
>>
>>> Cara Valéria,
>>>
>>> Observações que talvez possam ser úteis:
>>>
>>> 1) O esquema (A --> B) --> (Ng A --> Ng B) é válido no Intucionismo,
>>> (versão Heyting); as álgebras de Heyting fornecem uma semântica completa
>>> para a versão do Intuicionismo do Arend;
>>>
>>> 2) Adicionar o esquema recíproco à axiomatização de Heyting da Lógica
>>> Intucionista imediatamente fornece a Lógica Clássica; é semelhante ao
>>> que acontece com a equivalência no sistema Intuicionista: se for
>>> distributiva, a Lógica é clássica.
>>>
>>> 3) Estou insistindo em incluir o nome do Arend pois afinal nem sempre
>>> nos lembramos que o Brower tinha a firme opinião que a sua visão da
>>> Lógica era impossível (por 

Re: [Logica-l] um probleminha com logica intuicionista...

[Valeria de Paiva]

oi Fernando,
provavelmente o Chico ja respondeu, mas se nao, de uma olhada em
https://arxiv.org/abs/1708.05896
A Cointuitionistic Adjoint Logic

ou Crolard's papers:


   -

   “A formulae-as-types interpretation of Subtractive Logic
   ”. T.
Crolard. *Journal
   of Logic and Computation. Special issue on Intuitionistic Modal Logic and
   Application.* Volume 14, Issue 4, August 2004. pp 529-570.

   *Abstract.* We present a formulae-as-types interpretation of Subtractive
   Logic (*i.e.* bi-intuitionistic logic). This presentation is two-fold:
   we first define a very natural restriction of the λμ-calculus which is
   closed under reduction and whose type system is a constructive restriction
   of the Classical Natural Deduction. Then we extend this deduction system
   conservatively to Subtractive Logic. From a computational standpoint, the
   resulting calculus provides a type system for first-class coroutines (a
   restricted form of first-class continuations).
   -

   “Subtractive logic
   ”. T.
Crolard. *Theoretical
   Computer Science* 254:1–2(2001):151-185.*Abstract.* This paper is the
   first part of a work whose purpose is to investigate duality in some
   related frameworks (cartesian closed categories, lambda-calculi,
   intuitionistic and classical logics) from syntactic, semantical and
   computational viewpoints. We start with category theory and we show that
   any bicartesian closed category with coexponents is degenerated (i.e. there
   is at most one arrow between two objects). The remainder of the paper is
   devoted to logical issues. We examine the propositional calculus underlying
   the type system of bicartesian closed categories with coexponents and we
   show that this calculus corresponds to subtractive logic: a conservative
   extension of intuitionistic logic with a new connector (subtraction) dual
   to implication. Eventually, we consider first order subtractive logic and
   we present an embedding of classical logic into subtractive logic.

abs
Valeria

2017-10-25 3:21 GMT-07:00 Fernando Yamauti :

>  Oi Chico,
>
>  Só uma pergunta idiota. Que adjunção entre a diferença simétrica e a
> disjunção (que voce havia citado) é essa? Suponho que deva ser algo que
> vale em qualquer topos Booleano, mas mesmo em Set algo do tipo  (-) \vee A
> -| (-)  \Delta A  (ou o contrario), onde ambos endofuntores são entre o
> reticulado dos subobjetos,  não parece ser verdade. Portanto acho que voce
> esta pensando em algo menos obvio que isso, mas não consegui descobrir o
> que é...
>
>  Abs.
>
>
> Em 24 de outubro de 2017 04:08, Francisco Miraglia 
> escreveu:
>
>> Cara Valéria,
>>
>> Observações que talvez possam ser úteis:
>>
>> 1) O esquema (A --> B) --> (Ng A --> Ng B) é válido no Intucionismo,
>> (versão Heyting); as álgebras de Heyting fornecem uma semântica completa
>> para a versão do Intuicionismo do Arend;
>>
>> 2) Adicionar o esquema recíproco à axiomatização de Heyting da Lógica
>> Intucionista imediatamente fornece a Lógica Clássica; é semelhante ao que
>> acontece com a equivalência no sistema Intuicionista: se for distributiva,
>> a Lógica é clássica.
>>
>> 3) Estou insistindo em incluir o nome do Arend pois afinal nem sempre nos
>> lembramos que o Brower tinha a firme opinião que a sua visão da
>> Lógica era impossível (por definição, já que envolvia a "prática
>> quotidiana dos matemáticos") de ser axiomatizada.
>>
>> 4) Interessante observar que posições filosóficas não se materializam  na
>> "prática quotidiana dos matemáticos": um dos resultados mais conhecidos de
>> Brower (toda função contínua do disco de dimensão n em sí mesmo possui
>> ponto fixo) é estabelecido pelo próprio por contradição!
>> O primeiro passo da contradição já é de ordem grande: não há retração
>> contínua do disco em sua borda (em qualquer dimensão n maior ou igual a
>> 1), o que exige métodos homológicos ou homotópicos); exibir o ponto fixo:
>> "para com isso"
>>
>> 5) Quanto à nomenclatura, tanto Heyting, quanto Kleene (e Vesley)  dão o
>> nome de contraposição ao esquema em (1), sempre chamando a atenção de que ,
>> no Intuicionismo segundo Arend, difere da regra de contraposição clássica,
>> que, em geral, é  enunciada como o esquema "contrapositivo", mencionado em
>> (2).
>>
>> (6) Não me lembro de ler acerca dessas coisas no livro do Dummet (mas
>> também não foi lá que aprendi a lidar com o intuicionismo do Arend), porém
>> sabes como é: a memória não é mais o que era, sendo substituída pela
>> "prática quotidiana" de utilizar metateoria intuicionista para fazer
>> Matemática. Exemplo: anéis de Gelfand (aqueles comutativos com unidade tais
>> que que por cima de todo ideal há apenas um maximal) são,
>> intuicionisticamente, fielmente quadráticos (possuem uma teoria de formas
>> quadráticas "bem comportada" e satisfazem a conjectura 

Re: [Logica-l] um probleminha com logica intuicionista...

[Fernando Yamauti]

 Oi Chico,

 Só uma pergunta idiota. Que adjunção entre a diferença simétrica e a
disjunção (que voce havia citado) é essa? Suponho que deva ser algo que
vale em qualquer topos Booleano, mas mesmo em Set algo do tipo  (-) \vee A
-| (-)  \Delta A  (ou o contrario), onde ambos endofuntores são entre o
reticulado dos subobjetos,  não parece ser verdade. Portanto acho que voce
esta pensando em algo menos obvio que isso, mas não consegui descobrir o
que é...

 Abs.


Em 24 de outubro de 2017 04:08, Francisco Miraglia 
escreveu:

> Cara Valéria,
>
> Observações que talvez possam ser úteis:
>
> 1) O esquema (A --> B) --> (Ng A --> Ng B) é válido no Intucionismo,
> (versão Heyting); as álgebras de Heyting fornecem uma semântica completa
> para a versão do Intuicionismo do Arend;
>
> 2) Adicionar o esquema recíproco à axiomatização de Heyting da Lógica
> Intucionista imediatamente fornece a Lógica Clássica; é semelhante ao que
> acontece com a equivalência no sistema Intuicionista: se for distributiva,
> a Lógica é clássica.
>
> 3) Estou insistindo em incluir o nome do Arend pois afinal nem sempre nos
> lembramos que o Brower tinha a firme opinião que a sua visão da
> Lógica era impossível (por definição, já que envolvia a "prática
> quotidiana dos matemáticos") de ser axiomatizada.
>
> 4) Interessante observar que posições filosóficas não se materializam  na
> "prática quotidiana dos matemáticos": um dos resultados mais conhecidos de
> Brower (toda função contínua do disco de dimensão n em sí mesmo possui
> ponto fixo) é estabelecido pelo próprio por contradição!
> O primeiro passo da contradição já é de ordem grande: não há retração
> contínua do disco em sua borda (em qualquer dimensão n maior ou igual a
> 1), o que exige métodos homológicos ou homotópicos); exibir o ponto fixo:
> "para com isso"
>
> 5) Quanto à nomenclatura, tanto Heyting, quanto Kleene (e Vesley)  dão o
> nome de contraposição ao esquema em (1), sempre chamando a atenção de que ,
> no Intuicionismo segundo Arend, difere da regra de contraposição clássica,
> que, em geral, é  enunciada como o esquema "contrapositivo", mencionado em
> (2).
>
> (6) Não me lembro de ler acerca dessas coisas no livro do Dummet (mas
> também não foi lá que aprendi a lidar com o intuicionismo do Arend), porém
> sabes como é: a memória não é mais o que era, sendo substituída pela
> "prática quotidiana" de utilizar metateoria intuicionista para fazer
> Matemática. Exemplo: anéis de Gelfand (aqueles comutativos com unidade tais
> que que por cima de todo ideal há apenas um maximal) são,
> intuicionisticamente, fielmente quadráticos (possuem uma teoria de formas
> quadráticas "bem comportada" e satisfazem a conjectura de Milnor). Isto já
> é meio complicado; o caso clássico (que penso também ser verdadeiro) parece
> ser ainda mais complicado. Interessante que os meus colegas de formas
> quadráticas e K-teoria não dão a menor importância para a informação
> intuicionista...
>
> (7) A relação intucionista da disjunção com a implicação resume-se ao
> óbvio; qualquer outra relação é FALSA (experimente nos abertos da reta
> real). Ou seja, na minha opinião, "barking up the wrong tree".
>
> Como voce sabe muito bem, o modo mais adequado de tratar estes conceitos é
> via adjunções: a implicação é  adjunta da conjunção, enquanto que a
> disjunção é, classicamente, adjunta da diferença simétrica (o complementar
> clássico da equivalência); porém esta última adjunção está longe de ser
> intuicionisticamente válida. Aliás, se um reticulado distribitivo possui
> uma operação parecida com a diferença simétrica, tem que ser uma álgebra de
> Boole. Aqui começam a aparecer diferenças conceituais importantes e a
> necessidade de empregar
> outras noções, mais gerais (e.g., functores adjuntos), para construir
> Lógicas. Já escrevi demais
>
>
> Um grande abraço,
>
> Chico Miraglia
>
>
>
>
>
>
>> On Oct 23, 2017 9:00 PM, "Valeria de Paiva" 
>> wrote:
>>
>> prezados colegas,
>>>
>>> estou com um probleminha na wikipedia e em vez de gastar o tempo que
>>> precisaria pra achar minha copia do Dummett em casa, resolvi apelar pros
>>> amigos.
>>>
>>> Acho que  tem um "erro" em https://en.wikipedia.org/
>>> wiki/Intuitionistic_logic
>>> onde  na secao 9 alguem diz que:
>>>
>>> Relation to classical logic[edit
>>> >> logic=edit=9>
>>> ]
>>>
>>> The system of classical logic is obtained by adding any one of the
>>> following axioms:
>>>
>>>- {\displaystyle \phi \lor \lnot \phi }[image: \phi \lor \lnot \phi]
>>> (Law
>>>of the excluded middle. May also be formulated as {\displaystyle (\phi
>>>\to \chi )\to ((\lnot \phi \to \chi )\to \chi )}[image: (\phi \to \chi
>>>) \to ((\lnot \phi \to \chi ) \to \chi )].)
>>>- {\displaystyle \lnot \lnot \phi \to \phi }[image: \lnot \lnot \phi
>>>\to \phi] (Double negation elimination)
>>>- {\displaystyle ((\phi \to \chi 

[Logica-l] Kosta Dosen and substructural logic

[jean-yves beziau]

Kosta Dosen foi invited speaker do primeiro UNILOG em Montreux em 2005,
http://www.uni-log.org/enter-montreux.html
onde ele apresentou a palestra
"Coherence in General Proof Theory", o artigo relacionado foi publicado no
volume
Perespectives on Universal Logic,
https://www.amazon.com/Perspectives-Universal-Logic-
Jean-Yves-B%C3%A9ziau/dp/8876990771
o PSH convidou ele para o workshop ma teoria da rpova que ele esta
organizando no UNILOG'2018
http://www.uni-log.org/wk6-proof-theory.html
mas devido a doencia, ele não pude aceitar

Kosta editou junto com o PSH o livro
Substructural Logics
https://www.amazon.com/Substructural-Logics-Studies-Logic-Computation/dp/
0198537778
publicado pela OUP em 1994
o primeiro livro no assunto, resultado do evento que eles organizaram em
Tübingen em outubro de 1990, onde eles lançaram esta expressão.
Este livro é uma coletana com artigos do Dunn, Gabbay, Ono, Sambin, etc
Em 2002 Francesco Paoli publicou uma monografia sobre o assunto:
Substructural Logics: A Primer
https://www.amazon.com/Substructural-Logics-Primer-
Trends-Logic/dp/1402006055
O Francesco apresentou também um tutorial sobre o assunto no UNILOG'2015

Tem varios  ambiguidades em torno na expressão "Substructural logic".
A originem desta expressão é ligada as chamadas regras esturturais dos
sistemas de sequentes:
A ideia é que uma lógica substructural é uma lógica gerada par um sistema
de sequent na qual não vale essas regras.
Enfraqueciemento, Contracao, permutacao são consideradas com regras
estuturais.
A noção de regra estutural é concebida por oposição a noção de regras
lógica que definam os operatores lógicos (connectivos, modalidades,
quantificadores, ...)

Uma  questão é de saber se a regra de corte é ou não um regra estrutural.
Segundo o Girard não é o caso, ele bota ela numa terceira categoria, junto
com o axioma de identitade.
A lógica linear do Girard (que participou do evento em Tübingen) é
construinda a partir de um sistema de sequente com modificacaoes das regras
de enfraquecimento e contacao ou que permite em particular definir novos
connectivos: dois tipos de conjuncões, etc

Outra pergunta interessante é a seguinte:
sera que a logica intuicionista é uma logica substructural?
Do ponto de visto de sequentes, poderiamos dizer que sim, porque as regras
para conectivos nao sao alteradas, so a estutura do sequentes - so uma
formula na direita.

No artigo "Sequents and bivaluations" ( Logique et Analyse, 44 (2001),
pp.373-394)
tem uma figura chamada "The Architecture of Sequents Systems"
http://www.jyb-logic.org/archi-seq.jpg
onde eu faz a distincao entre principio estuturais e regras estruturais.

Escrevi recetemmente um artigo onde apresento um sistema de sequentes com
restricao a uma formula tanto na equerda que na direita, mostrando que com
isso não temos mais a distibutividade:
“Monosequent proof systems”
http://www.jyb-logic.org/papirs/mono.pdf

Essa restricao estrutural na logica intuicionista modifica as propriedades
dos connectivos (negacao, implicacao).
Todavia a logica intuicionista obedece aos tres axiomas de Tarski,
“Les axiomes de Tarski”, in R.Pouivet and M.Rebuschi (eds), La philosophie
en Pologne 1918-1939, Vrin, Paris, 2006, pp.135-149.
http://www.jyb-logic.org/Les%20axiomes%20de%20Tarski.pdf
que podem ser de uma certa forma considerada com "estruturais".
Alias uma logica non-monotona,  é geralemente definida com non-monotona
porque ela nao obedece ao segundo axioma de Tarski, não porque ela definida
a partir de um sistema de sequente sem regra de enfraqueciemento.

A definicao do conceito de logica substructural  é confrontada a esta
confusão entre regras estruturais de um sistema de sequentes e axiomas para
um relacao de consequence, duas tradições diferentes.

E na tradição polonesa, um termo estrutural é também usado, com sentido
totalemente diferente!
Uma relacao de consequencia é considerada com estrutural se ela obedece um
axioma (não no sentido da teoria da prova) que caracteriza a substituicao
Essa abordagem foi promovido por Los  e Suszko no famoso artigo deles de
1958 que foi repoduzido na antologia de logica universal com apresentacao
do Jan Zygmunt
https://www.amazon.com/Universal-Logic-Anthology-
Gabbay-Studies/dp/3034601441
Um logica não esturural deste ponto de vista seria um logica onde nao vale
a substituico (que nao deve ser confundida com o replacement).
Os polones consider que um logica sempre dever ser estrutural neste
sentido. Não é nrcesseramente obvio.
Destouches e Février aprensentaram um logica para dar conta do principio de
indeterminacao do Heisenberg que quebra a substituicao.

Pretendo detalhar esses pontos num artigo chamado
"What is a substructural logic?"
que ja estou preparando a um certo tempo
Comentarios são bemvindos

JYB

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