[Logica-l] Logica Universalis Webinar - April 14 - UNILOG’2022: 7th World Congress and School on Universal Logic April 1-11, 2022 by Jean-Yves Beziau

[jean-yves beziau]

*Join the Logica Universalis Webinar!*

The *L*ogica *U*niversalis *W*ebinar is a World Seminar Series connected to
the journal *Logica Universalis *,
the book series *Studies in Universal Logic
* and the *Universal Logic Project*
. It is an open platform for all scholars
interested in the many aspects of logic.

The LUW series started with two "extraordinary" sessions:

   - Introduction to the Universal Logic Project
   , Dec 16, 2020
   - *Welcome Celebration for the World Logic Day
   *, Jan 14, 2021

We are now launching a series of regular sessions for the year 2021. See
the full program here
. The sessions
take place on Wednesdays at 4pm CET (click here
to
convert to your timezone). They are held via Zoom and are free to
attend. Please register in advance.
*Registration is now open!*


The next session will be held on Wednesday, April 14 at 4pm CET with the
talk



UNILOG’2022: 7th World Congress and School on Universal Logic April 1-11,
2022


Jean-Yves Beziau 

Editor-in-Chief of Logica Universalis



Video recordings of the seminars are uploaded on the YouTube channel *Universal
Logic Project *.



-- 

*Antje Herbst*

Associate Editor Mathematics

Journals



*Springer* *Nature*

Tiergartenstraße 17, 69121 Heidelberg, Germany

T   +49 62214878984

*antje.her...@springernature.com *

www.springernature.com

--

Springer Nature is a leading research, educational and professional
publisher, providing quality content to our communities through a range of
innovative platforms, products and services. Every day, around the globe,
our imprints, books, journals and resources reach millions of people –
helping researchers, students, teachers & professionals to discover, learn
and achieve.

--

Branch of Springer-Verlag GmbH, Heidelberger Platz 3, 14197 Berlin, Germany

Registered Office: Berlin / Amtsgericht Berlin-Charlottenburg, HRB 91881 B

Directors: Martin Mos, Dr. Ulrich Vest, Dr. Niels Peter Thomas

-- 
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 ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAF2zFLBez1k5JBGP9JF%3DNOaCoEdMJg6u10QUtbeL-Ag9TiLvXg%40mail.gmail.com.

Re: [Logica-l] Re: A persistência da burrice

[Walter Carnielli]

Me permito discordar cavalheirescamente de vocês : o cara é pomposo,
falador, cheiao de oratória e beletrismo como muitos dos nossos colegas da
Filosofia .

Mas ele levanta um ponto que eu acho que é legal : a chamada burrice tem
uma lógica,  tem um modus operandi ,tem um estatuto metafísico de
esistência propria, não é só um hiato de inteligência.

Mais ou menos assim: não adianta jogar uma panela de água fervente no
iceberg- ao invés de derreter um pouco  o gelo , o gelo acaba congelando a
água fervente. A burrice contagia.

Eu estou querendo ler (aliás comprando) por causa dos aforismos dos quais
gosto bastante, mas  esse ponto existencial também me parece interessante

Enfim, não quero dizer "não li e  não
gostei" :-)
Abraços

Em seg, 12 de abr de 2021 17:00, Flaulles Bergamaschi <
flaulles.bo...@uesb.edu.br> escreveu:

> Também acho a mesma coisa.
>
>
> On 12 de abr de 2021, at 3:20 PM, Julio Stern  wrote:
>
>
>
>
> Caros Redistas:
> Acabo de ver o video do
> > Marco Casanova
> > A Persistencia da Burrice.
>
> Confesso que Nao Gostei, nem um pouco.
> O autor, muito inflamado e cheio de si, trompeteia o tempo todo que qum
> dele discorda eh Burro.
> No debate, todos de comum se espantam e Concordam com o fato de que gente
> Inteligente, como Medicos e Engenheiros, podem ser tao Burros (sic)
> Muitos tambores, muitas trombetas, e Pouca Filosofia (no meu humilde
> entender).
>
> Em contraste, acabo de assistir o video da:
>
> >  Romy Jaster
> >  Bullshit and the Norms of Assertion
> >  Virtual International Consortium for Truth Research ("VICTR")
>
> Ai Sim, perspectivas que de um ponto de vista politico e social tem varias
> similaridades,
> sao apresentadas com metodo e rigor filosofico (eu diria Inteligente, so
> para cutucar :-)
>
> A proposito, recomendo fortemente as palestras do projeto VICTR a todos os
> interessados
> em temas ligados a Verdade (suas formas de ser e de se apresentar, e suas
> deturpacoes)
>
> Abraco (virtual) e Tudo de bom,
> ---Julio Stern
>
> --
> *From:* Cassiano Terra Rodrigues 
> *Sent:* Monday, April 12, 2021 1:27 PM
> *To:* LOGICA-L 
> *Subject:* [Logica-l] Re: A persistência da burrice
>
> Camaradas, bons dias.
> Paz, saúde e alegria, espero q esta os encontre bem.
> O negacionismo não é um fenômeno novo, como sabemos, tampouco a "ascensão"
> do irracionalismo, q de ascensão não tem nada, dada a sua permanência
> histórica milenar.
> Mas ao ver o video enviado pelo Eduardo, eu me lembrei de um livro da
> Irina Metzler,
> <>
> Facilmente encontrável na biblioteca putiniana.
> Na Idade Média, em algumas situações, animais chegaram a ser julgados pela
> lei, ao passo q "idiotas", "néscios", "estúpidos", crianças e outros seres
> ilógicos ou irracionais não eram considerados imputáveis. O contraste
> histórico com os nossos critérios positivistas de racionalidade ("verdade
> dos fatos", "validade lógica" etc.) é interessantíssimo e nos faz pensar se
> somos o q gostamos de pensar q somos.
> Um abraço e boa semana,
> cass.
>
> On Saturday, April 10, 2021 at 8:25:42 PM UTC-3 eduardoochs wrote:
>
> Acabou de acontecer uma live/entrevista com o Marco Casanova,
> sobre o livro dele "A persistência da burrice":
>
> https://www.youtube.com/watch?v=8pFTG_tvP5Y
>
> Eu tou assistindo a gravação empolgadíssimo.
> Acho que ela complementa bem os vídeos sobre falácias.
>
> [[]] =) =) =),
> Eduardo
>
> --
> Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos
> Grupos do Google.
> Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie
> um e-mail para logica-l+unsubscr...@dimap.ufrn.br.
> Para ver essa discussão na Web, acesse
> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/f66b803a-0cbd-491f-8ae5-72d3434d062en%40dimap.ufrn.br
> 
> .
>
> --
> Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos
> Grupos do Google.
> Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie
> um e-mail para logica-l+unsubscr...@dimap.ufrn.br.
> Para ver essa discussão na Web, acesse
> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CPYP284MB143135E1FBEF6168A6E7A586B6709%40CPYP284MB1431.BRAP284.PROD.OUTLOOK.COM
> 
> .
>
>
> --
> Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos
> Grupos do Google.
> Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie
> um e-mail para logica-l+unsubscr...@dimap.ufrn.br.
> Para ver essa discussão na Web, acesse
> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/879BFAFB-CC51-4F88-BD1A-EB41E52D24FD%40uesb.edu.br
> 

[Logica-l] Fwd: Eduardo Barrio, "Anti-Exceptionalism, Truth, and the BA-Plan" @ VICTR | 10:00am EDT / 14:00 UTC, April 26

[Joao Marcos]

-- Forwarded message -

The Virtual International Consortium for Truth Research (VICTR) will
have a talk by Eduardo Barrio (University of Buenos Aires), on
“Anti-exceptionalism, Truth, and the BA-Plan” on April 26, 10:00am EDT
/ 14:00 UTC.

Abstract: Anti-exceptionalism about logic states that logical theories
have no special epistemological status. Such theories are continuous
with scientific theories. Contemporary anti-exceptionalists include
data about semantic paradoxes as a part of the logical evidence.
Exploring the Buenos Aires Plan, the recent development of the
metainferential hierarchy of ST-logics shows that there are multiple
options to deal with such paradoxes. There is a whole ST-based
hierarchy, of which LP and ST themselves are only the first steps. The
logics in this hierarchy are also options to analyze the inferential
patterns allowed in a language that contains its own truth predicate.
This talk explores these responses analyzing some reasons to go beyond
the first steps. I will show that LP, ST, and the logics of the
ST-hierarchy offer different diagnoses for the same evidence: the
inferences and metainferences the agents endorse in the presence of
the truth-predicate. But even if the data are not enough to adopt one
of these logics, there are other elements to evaluate the revision of
classical logic. How close should we be to classical logic? Which
logic should be used during the revision? Should a logic be closed
under its own rules? How could a logic obey the validities it
contains? And mainly, which is the best explanation for the logical
principles to deal with semantic paradoxes? I will argue that, if the
answers to these questions are provided from an anti-exceptionalist
perspective, ST-metainferential logics in general are the best
available options.

You can register for this event at this link:
https://us02web.zoom.us/meeting/register/tZIocu-prj4iGdY0NwHUWjPYWLvywnGfLeku

Following this link will generate a unique zoom link to you, that you
can then use to access any of the Centrally Organized talks coming up
at VICTR through May.

The Virtual International Consortium for Truth Research (VICTR) is
sponsored by the Future of Truth project at the University of
Connecticut Humanities Institute, the University of Waikato, and the
University of Alabama.

For more information, check out our website:
https://tinyurl.com/VICTR, twitter @VICTR_Group, and YouTube Channel
https://www.youtube.com/channel/UCkPMDbdEnm14MK4tvcGfItw.

You can find an up-to-date calendar of VICTR happenings at this link:
https://calendar.google.com/calendar/embed?src=h9gf3505q784cati3dkip27b60%40group.calendar.google.com=America%2FNew_York

To Join VICTR’s mailing list, email cwr...@ua.edu, or victrgr...@gmail.com.

Best,

The VICTR organizing team

-- 
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 ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_Ljes6_HgG%2BmFM5teDQZ3CRKKURhdrBmMiHf5sZPhVzTpQ%40mail.gmail.com.

Re: [Logica-l] Vácuo

[Joao Marcos]

Obrigado pela mensagem, Hermógenes!

> Relendo as mensagens anteriores, parece que há algumas camadas envolvidas no
> desafio proposto. A mais rasa delas, aquela que está formulada de maneira mais
> explícita, pede um desenvolvimento formal no qual A e B não fossem
> equivalentes. A alegação aqui, me parece, era que as objeções ao condicional
> clássico estavam apoiadas apenas em análises informais e apelos ao "bom
> senso", seja lá o que isso signifique.

Confesso que sequer cheguei a entender exatamente porque a questão
original da "vacuidade" se transformou de repente em uma discussão
sobre o condicional...  Embora eu tenha feito isso, seguindo a
proposta do próprio Daniel, eu não me sinto de modo algum _compelido_
a traduzir a sentença "Todo A é B" como uma sentença contendo uma
implicação particular (e Aristóteles também nunca cogitou fazer tal
tradução)...  Trata-se de uma sentença com um *quantificador
relativizado*, na realidade.  Por que não estamos discutindo a
"quantificação relevante", ao invés?

> Esta me parece uma boa réplica, pois há tradicionalmente escolhas difíceis
> relacionadas à formulação de sistemas relevantes. Talvez seja este o ponto que
> JM estava no fundo tentando salientar. Aqui há diversas abordagens. Anderson &
> Belnap escolheram abrir mão do chamado silogismo disjuntivo. Tennant chama a
> atenção como o sujeito que escolheu abrir mão da regra do corte (e manter o
> silogismo disjuntivo).

Eu conheci o Neil Tennant na África do Sul, há 22 anos, e estudei um
pouco de Core Logic na biblioteca da UNICAMP, em momentos de ócio.  Eu
gosto muito, hoje em dia, da ideia de jogar fora o corte para obter
uma lógica que se livra da formulação metalógica do princípio do
terceiro excluído.  Mas realmente não me apetece ler um paper inteiro
do Neil para tentar adivinhar que razão poderia ter tido o colega que
afirmou, sem apresentar uma justificativa formal, que certas duas
sentenças seriam folk-inequivalentes... :-(  O ônus da prova, neste
caso, não é meu!

> Enfim, me parece muito mais proveitoso aos meus alunos de filosofia o 
> aprendizado
> de aspectos informais da argumentação, tais como explorados no projeto Lógica
> Viva, por exemplo. Acho que vale a pena refletir para que ensinamos lógica de
> primeira ordem, completude, correção, e o restante da parafernália para alunos
> de graduação em filosofia. Não sei a quantas andam os cursos de graduação por
> aí, mas aqui na UFPB, Lógica I e II (isto é, lógica de predicados e seus
> metateoremas) são obrigatórias na filosofia, o que me parece completamente
> insano.

Quando estudei pela primeira vez Lógica na graduação em Filosofia, na
UFMG, há quase três décadas, eu sequer ouvi falar que existiam tais
coisas (correção, completude, ou mesmo "lógica de primeira ordem").
Foi um desfavor que me fizeram, não me ensinar _nada_ de "lógica de
verdade" (a propósito, também não me ensinaram nada sobre
*argumentação*, como qualquer um pode inferir aqui nesta lista, a
partir de cada mensagem que eu envio :).  Parece-me, neste sentido,
que o curso da UFPB está de parabéns!

(Isto _não_ é dizer que os estudantes de Filosofia ---e de outras
áreas--- não deveriam ser também convidados à *reflexão*, e fartamente
equipados com ferramentas para contribuir de maneira produtiva à
construção de *argumentações relevantes*!)

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 ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LhufxguVsZYGNiFBsDeEUAeZH9gVn7Z5qSG718gQRFvwA%40mail.gmail.com.

Re: [Logica-l] Re: A persistência da burrice

[Julio Stern]

Caros Redistas:
Acabo de ver o video do
> Marco Casanova
> A Persistencia da Burrice.

Confesso que Nao Gostei, nem um pouco.
O autor, muito inflamado e cheio de si, trompeteia o tempo todo que qum dele 
discorda eh Burro.
No debate, todos de comum se espantam e Concordam com o fato de que gente 
Inteligente, como Medicos e Engenheiros, podem ser tao Burros (sic)
Muitos tambores, muitas trombetas, e Pouca Filosofia (no meu humilde entender).

Em contraste, acabo de assistir o video da:

>  Romy Jaster
>  Bullshit and the Norms of Assertion
>  Virtual International Consortium for Truth Research ("VICTR")

Ai Sim, perspectivas que de um ponto de vista politico e social tem varias 
similaridades,
sao apresentadas com metodo e rigor filosofico (eu diria Inteligente, so para 
cutucar :-)

A proposito, recomendo fortemente as palestras do projeto VICTR a todos os 
interessados
em temas ligados a Verdade (suas formas de ser e de se apresentar, e suas 
deturpacoes)

Abraco (virtual) e Tudo de bom,
---Julio Stern


From: Cassiano Terra Rodrigues 
Sent: Monday, April 12, 2021 1:27 PM
To: LOGICA-L 
Subject: [Logica-l] Re: A persistência da burrice

Camaradas, bons dias.
Paz, saúde e alegria, espero q esta os encontre bem.
O negacionismo não é um fenômeno novo, como sabemos, tampouco a "ascensão" do 
irracionalismo, q de ascensão não tem nada, dada a sua permanência histórica 
milenar.
Mas ao ver o video enviado pelo Eduardo, eu me lembrei de um livro da Irina 
Metzler,
<>
Facilmente encontrável na biblioteca putiniana.
Na Idade Média, em algumas situações, animais chegaram a ser julgados pela lei, 
ao passo q "idiotas", "néscios", "estúpidos", crianças e outros seres ilógicos 
ou irracionais não eram considerados imputáveis. O contraste histórico com os 
nossos critérios positivistas de racionalidade ("verdade dos fatos", "validade 
lógica" etc.) é interessantíssimo e nos faz pensar se somos o q gostamos de 
pensar q somos.
Um abraço e boa semana,
cass.

On Saturday, April 10, 2021 at 8:25:42 PM UTC-3 eduardoochs wrote:
Acabou de acontecer uma live/entrevista com o Marco Casanova,
sobre o livro dele "A persistência da burrice":

https://www.youtube.com/watch?v=8pFTG_tvP5Y

Eu tou assistindo a gravação empolgadíssimo.
Acho que ela complementa bem os vídeos sobre falácias.

[[]] =) =) =),
Eduardo

--
Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos Grupos 
do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um 
e-mail para 
logica-l+unsubscr...@dimap.ufrn.br.
Para ver essa discussão na Web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/f66b803a-0cbd-491f-8ae5-72d3434d062en%40dimap.ufrn.br.

-- 
Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos 
Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um 
e-mail para logica-l+unsubscr...@dimap.ufrn.br.
Para ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CPYP284MB143135E1FBEF6168A6E7A586B6709%40CPYP284MB1431.BRAP284.PROD.OUTLOOK.COM.

Re: [Logica-l] Vácuo

[Joao Marcos]

> > Os lemas que eu invoquei eram intuicionisticamente válidos, certo?
>
> OK. O bom senso dos lógicos clássicos e intuicionistas, então. Ambos endossam
> lógicas não relevantes. E os lógicos relevantes? Não são lógicos? São
> anátemas? Blásfemos?

Suponho que não --- mas podem até ser. :-)

Vale recordar, não obstante, que o Daniel sequer se declarou
relevantista, então tudo que estou fazendo é tatear por uma solução
para o problema que ele levantou (para mim), ao alegar que o Teorema
que eu formulei não seria válido em uma semântica folk (não
detalhada).

> > > Porém, ainda que o fosse, não me parece correto impor um artefato da
> > > tradição matemática, especialmente como conteúdo obrigatório em cursos de
> > > filosofia, nos quais, inclusive, é comumente apresentado como regra do
> > > raciocinar correto, dentre outras baboseiras.
> >
> > Ainda gostaria de ver uma interpretação formal (de qualquer tipo) que
> > justificasse a alegada inequivalência entre (A) e (B).
>
> Assumindo que se trata de um desejo sincero da sua parte, trata-se de uma
> simples aplicação da lógica intuicionista *relevante*, cujos detalhes formais
> estão disponíveis no artigo que mencionei antes. Na verdade, a apresentação
> aqui está mais robusta, ainda que o título não seja tão chamativo quanto:
>
> https://sci-hub.se/10.1017/s1755020311000360

Hummm, você poderia talvez explicar _aqui_ esta "aplicação simples",
ao invés de me mandar ler (mais) um artigo?!

Recordo que eu levantei um desafio bastante simples: mostrar a
_inequivalência_ entre (A) e (B) no contexto de uma aritmética
_qualquer_ que valide (C).  Aparentemente, este é, aliás, um
raciocínio usado pelas pessoas de bom senso.  Seria possível
detalhá-lo aqui mesmo, na lista de Lógica, para a ilustração geral das
pessoas que não necessariamente partilham das mesmas faculdades de
julgamento?  (Se não for _possível_, tudo bem: o artigo ganhará seu
lugar embaixo da minha pilha de estudos...)

A questão levantada parece *relevante*, de todo modo, para a
formalização da argumentação construída em linguagem natural --- o que
_para mim_ pareceu justificar plenamente o desafio, neste fórum.

[]s, Joao Marcos

-- 
Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos 
Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um 
e-mail para logica-l+unsubscr...@dimap.ufrn.br.
Para ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LjOc%3DYh%2BWzctYiJ5q6OHe4bOO%3DWWQB%3DVd9QtfCF-Df6_Q%40mail.gmail.com.

[Logica-l] 7th International Workshop on Proof eXchange for Theorem Proving (PxTP) - Second CFP

[Giselle Reis]

Call for Papers, PxTP 2021

   The Seventh International Workshop on
 Proof eXchange for Theorem Proving (PxTP)

   https://pxtp.gitlab.io/2021

   21 July 2021, online

 associated with the CADE-28 conference


## Background

  The PxTP workshop brings together researchers working on various
  aspects of communication, integration, and cooperation between
  reasoning systems and formalisms.

  The progress in computer-aided reasoning, both automatic and
  interactive, during the past decades, has made it possible to build
  deduction tools that are increasingly more applicable to a wider range
  of problems and are able to tackle larger problems progressively
  faster. In recent years, cooperation of such tools in larger
  verification environments has demonstrated the potential to reduce the
  amount of manual intervention. Examples include the Sledgehammer tool
  providing an interface between Isabelle and (untrusted) automated
  provers, and collaboration of the HOL Light and Isabelle systems in
  the formal proof of the Kepler conjecture.

  Cooperation between reasoning systems relies on availability of
  theoretical formalisms and practical tools for exchanging problems,
  proofs, and models. The PxTP workshop strives to encourage such
  cooperation by inviting contributions on suitable integration,
  translation, and communication methods, standards, protocols, and
  programming interfaces. The workshop welcomes developers of automated
  and interactive theorem proving tools, developers of combined systems,
  developers and users of translation tools and interfaces, and
  producers of standards and protocols. We are interested both in
  success stories and descriptions of current bottlenecks and proposals
  for improvement.

## Topics

  Topics of interest for this workshop include all aspects of
  cooperation between reasoning tools, whether automatic or interactive.
  More specifically, some suggested topics are:

  * applications that integrate reasoning tools (ideally with
certification of the result);
  * interoperability of reasoning systems;
  * translations between logics, proof systems, models;
  * distribution of proof obligations among heterogeneous reasoning
tools;
  * algorithms and tools for checking and importing (replaying,
reconstructing) proofs;
  * proposed formats for expressing problems and solutions for different
classes of logic solvers (SAT, SMT, QBF, first-order logic,
higher-order logic, typed logic, rewriting, etc.);
  * meta-languages, logical frameworks, communication methods,
standards, protocols, and APIs related to problems, proofs, and
models;
  * comparison, refactoring, transformation, migration, compression and
optimization of proofs;
  * data structures and algorithms for improved proof production in
solvers (e.g., efficient proof representations);
  * (universal) libraries, corpora and benchmarks of proofs and
theories;
  * alignment of diverse logics, concepts and theories across systems
and libraries;
  * engineering aspects of proofs (e.g., granularity, flexiformality,
persistence over time);
  * proof certificates;
  * proof checking;
  * mining of (mathematical) information from proofs (e.g., quantifier
instantiations, unsat cores, interpolants, ...);
  * reverse engineering and understanding of formal proofs;
  * universality of proofs (i.e. interoperability of proofs between
different proof calculi);
  * origins and kinds of proofs (e.g., (in)formal, automatically
generated, interactive, ...)
  * Hilbert's 24th Problem (i.e. what makes a proof better than
another?);
  * social aspects (e.g., community-wide initiatives related to proofs,
cooperation between communities, the future of (formal) proofs);
  * applications relying on importing proofs from automatic theorem
provers, such as certified static analysis, proof-carrying code, or
certified compilation;
  * application-oriented proof theory;
  * practical experiences, case studies, feasibility studies.

## Submissions

  Researchers interested in participating are invited to submit either an
  extended abstract (up to 8 pages) or a regular paper (up to 15 pages).
  Submissions will be refereed by the program committee, which will select a
  balanced program of high-quality contributions. Short submissions that could
  stimulate fruitful discussion at the workshop are particularly welcome. We
  expect that one author of every accepted paper will present their work at the
  workshop.

  Submitted papers should describe previously unpublished work, and must
  be prepared using the LaTeX EPTCS class (http://style.eptcs.org).
  Papers will be submitted via EasyChair, at the PxTP'2021 workshop page
  (https://easychair.org/conferences/?conf=pxtp-7).
  Accepted regular papers will appear in an EPTCS volume.

## Important Dates

  * Abstract submission: April 21, 2021
  * Paper submission: April 28, 

Re: [Logica-l] Vácuo

[Hermógenes Oliveira]

Em segunda-feira, 12 de abril de 2021, às 11:53:36 -03, Joao Marcos escreveu:
> > 
> > Quais lógicos são esses, cujo bom senso está sendo invocado aqui? Lógicos
> > clássicos, eu suponho?
> 
> Os lemas que eu invoquei eram intuicionisticamente válidos, certo?

OK. O bom senso dos lógicos clássicos e intuicionistas, então. Ambos endossam 
lógicas não relevantes. E os lógicos relevantes? Não são lógicos? São 
anátemas? Blásfemos?
 
> > Porém, ainda que o fosse, não me parece correto impor um artefato da
> > tradição matemática, especialmente como conteúdo obrigatório em cursos de
> > filosofia, nos quais, inclusive, é comumente apresentado como regra do
> > raciocinar correto, dentre outras baboseiras.
> 
> Ainda gostaria de ver uma interpretação formal (de qualquer tipo) que
> justificasse a alegada inequivalência entre (A) e (B).

Assumindo que se trata de um desejo sincero da sua parte, trata-se de uma 
simples aplicação da lógica intuicionista *relevante*, cujos detalhes formais 
estão disponíveis no artigo que mencionei antes. Na verdade, a apresentação 
aqui está mais robusta, ainda que o título não seja tão chamativo quanto:

https://sci-hub.se/10.1017/s1755020311000360

Divirta-se!

--
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 ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/2426189.3kHWx39YlV%40avalon.

Re: [Logica-l] Vácuo

[Joao Marcos]

> > Meu raciocínio:
> > Se houvesse uma "Aritmética Relevante", estendendo [A4], que tivesse
> > algo relevante (perdão) a dizer sobre [A1], sem ao mesmo tempo se
> > comprometer com [A2] (como Daniel parece desejar), talvez ela
> > consistisse em uma resolução satisfatória para o mistério de [A3]?
>
> Core Logic?
> https://sci-hub.se/10.1007/bf00763511

Só posso devolver a pergunta, já que a minha familiaridade com o
trabalho do Tennant é pequena...

> > Claro, esta seria a solução _mais simples_.  Outra explanação para o
> > funcionamento da semântica "folk", que vai contra o bom senso _dos
> > lógicos_, também poderia ser satisfatória.  Uma Aritmética sempre será
> > necessária, de uma maneira ou de outra, para dar conta de [A1].
>
> Quais lógicos são esses, cujo bom senso está sendo invocado aqui? Lógicos
> clássicos, eu suponho?

Os lemas que eu invoquei eram intuicionisticamente válidos, certo?

> Porém, ainda que o fosse, não me parece correto impor um artefato da tradição
> matemática, especialmente como conteúdo obrigatório em cursos de filosofia, 
> nos
> quais, inclusive, é comumente apresentado como regra do raciocinar correto,
> dentre outras baboseiras.

Ainda gostaria de ver uma interpretação formal (de qualquer tipo) que
justificasse a alegada inequivalência entre (A) e (B).

[]s, 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 ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_Lg-hZ%3Dzf8eiVh34VJvFe93rM8ebekhwkKwezhcKEaaMeg%40mail.gmail.com.

Re: [Logica-l] Vácuo

[Hermógenes Oliveira]

No domingo, 11 de abril de 2021, às 17:45:16 -03, Joao Marcos escreveu:
>  [...]
> 
> Meu raciocínio:
> Se houvesse uma "Aritmética Relevante", estendendo [A4], que tivesse
> algo relevante (perdão) a dizer sobre [A1], sem ao mesmo tempo se
> comprometer com [A2] (como Daniel parece desejar), talvez ela
> consistisse em uma resolução satisfatória para o mistério de [A3]?

Core Logic?

https://sci-hub.se/10.1007/bf00763511

> Claro, esta seria a solução _mais simples_.  Outra explanação para o
> funcionamento da semântica "folk", que vai contra o bom senso _dos
> lógicos_, também poderia ser satisfatória.  Uma Aritmética sempre será
> necessária, de uma maneira ou de outra, para dar conta de [A1].

Quais lógicos são esses, cujo bom senso está sendo invocado aqui? Lógicos 
clássicos, eu suponho?

Não me parece que a relevância seja um problema para a aritmética em si. Ao 
menos, não me recordo de inferências patentemente irrelevantes em teoria dos 
números, com a qual tenho certa familiaridade, mas, reconhecidamente, não sou
um especialista. Ficaria agradavelmente surpreso se alguém fornecesse um 
exemplo.

A irrelevância do condicional clássico oferece alguns ganhos técnicos no 
âmbito dos programas de fundamentação que pairavam por volta do início do 
século XX, mas não parece ser um elemento essencial da argumentação matemática 
informal.

Porém, ainda que o fosse, não me parece correto impor um artefato da tradição 
matemática, especialmente como conteúdo obrigatório em cursos de filosofia, nos 
quais, inclusive, é comumente apresentado como regra do raciocinar correto, 
dentre outras baboseiras.

--
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 ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/3581293.RALIiNX56z%40avalon.

Re: [Logica-l] A persistência da burrice

[Adolfo Neto]

É o Casanova que escreveu este livro?
https://produto.mercadolivre.com.br/MLB-707994181-programaco-em-logica-e-a-linguagem-prolog-casanova-giorno-_JM

Em sáb., 10 de abr. de 2021 às 20:25, Eduardo Ochs 
escreveu:

> Acabou de acontecer uma live/entrevista com o Marco Casanova,
> sobre o livro dele "A persistência da burrice":
>
>   https://www.youtube.com/watch?v=8pFTG_tvP5Y
>
> Eu tou assistindo a gravação empolgadíssimo.
> Acho que ela complementa bem os vídeos sobre falácias.
>
>   [[]] =) =) =),
> Eduardo
>
> --
> 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 ver esta discussão na web, acesse
> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CADs%2B%2B6iGRVxN67%2BdHBvdjM7JCh%3DRT-VoA8xSHS4_qzfBoa2Yzg%40mail.gmail.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 ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAP52AGes%3Djpmz-AGHimQ6E1doi5f00qYLrWqG%3Da7vOdzJ_KJiQ%40mail.gmail.com.

Re: [Logica-l] Vácuo

[Joao Marcos]

> Eu me lembro de ter assistido uma palestra do Bob Meyer em Londres na década 
> de 90 sobre a demonstração do teorema de Goedel numa meta-matemática 
> relevante.  Não me lembro se a aritmética era relevante... o que eu mais me 
> lembro é que ele já não tinha um pedaço do cérebro e sua fala estava alterada.

Ah, nessa época ele já havia inclusive demonstrado que a existência de
Deus é equivalente ao Axioma da Escolha. ;-b
https://www.jstor.org/stable/2215186

(Historinha: Eu não sei se isto tinha a ver com o pedaço grande que
lhe faltava à cabeça, mas o Bob tinha uns hábitos de trabalho bastante
curiosos, acordando seus co-autores no meio da noite para discutir
como resolver todos os problemas lógicos do universo.)

[]s, JM

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

-- 
Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos 
Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um 
e-mail para logica-l+unsubscr...@dimap.ufrn.br.
Para ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LgpYAU8oBKiiapngg3Fhk5rkEZpD2_QGfsFa3%2BnxW%2B%3DwA%40mail.gmail.com.

[Logica-l] Re: A persistência da burrice

[Cassiano Terra Rodrigues]

Camaradas, bons dias. 
Paz, saúde e alegria, espero q esta os encontre bem. 
O negacionismo não é um fenômeno novo, como sabemos, tampouco a "ascensão" 
do irracionalismo, q de ascensão não tem nada, dada a sua permanência 
histórica milenar. 
Mas ao ver o video enviado pelo Eduardo, eu me lembrei de um livro da Irina 
Metzler, 
<> 
Facilmente encontrável na biblioteca putiniana. 
Na Idade Média, em algumas situações, animais chegaram a ser julgados pela 
lei, ao passo q "idiotas", "néscios", "estúpidos", crianças e outros seres 
ilógicos ou irracionais não eram considerados imputáveis. O contraste 
histórico com os nossos critérios positivistas de racionalidade ("verdade 
dos fatos", "validade lógica" etc.) é interessantíssimo e nos faz pensar se 
somos o q gostamos de pensar q somos.
Um abraço e boa semana,
cass.  

On Saturday, April 10, 2021 at 8:25:42 PM UTC-3 eduardoochs wrote:

> Acabou de acontecer uma live/entrevista com o Marco Casanova,
> sobre o livro dele "A persistência da burrice":
>
> https://www.youtube.com/watch?v=8pFTG_tvP5Y
>
> Eu tou assistindo a gravação empolgadíssimo.
> Acho que ela complementa bem os vídeos sobre falácias.
>
> [[]] =) =) =),
> Eduardo
>

-- 
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 ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/f66b803a-0cbd-491f-8ae5-72d3434d062en%40dimap.ufrn.br.

Re: [Logica-l] Logica viva: Computadores podem pensar?, por Walter Carnielli

[Thiago Galbiatti Vespa]

Um podcast interessante que há um certo relacionamento como assunto:

https://podcast.numec.prp.usp.br/c%C3%A9rebro-e-computador/

Thiago Galbiatti Vespa


Em sáb., 3 de abr. de 2021 às 19:58, Marcos Silva 
escreveu:

> Caros,
>
> novo video do coletivo Lógica Viva.
>
> Afinal, computadores podem de fato pensar?
>
> https://youtu.be/R2QL4YLNIRI
> https://www.instagram.com/p/CNOIfFFJPHS/
>
> 
>
> Nesta contribuição, Walter Carnielli explica o conceito de Inteligência
> Artificial através do famoso Teste de Turing. Carnielli compara este teste
> ao Argumento do Quarto Chinês apresentado por John Searle em 1980 para
> argumentar que a implementação de um programa de computador não é, por si
> só, suficiente para a instanciação de estados mentais genuínos por parte
> dos sistemas de IA.  Video feito em parceria com o projeto IDEIA +.
> https://mov8.com.br/ideia_mais/
>
> Por favor, divulguem para os seus alunos e alunas!
>
> Abraços,
> Marcos
>
> --
> Marcos Silva (UFPE/CNPq)
> Philosophy Department
> Federal University of Pernambuco, Brazil
> Editor-in-chief Revista Perspectiva Filosófica
> 
> https://sites.google.com/view/marcossilvaphilosophy
> "amar e mudar as coisas me interessa mais"
>
> --
> Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos
> Grupos do Google.
> Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie
> um e-mail para logica-l+unsubscr...@dimap.ufrn.br.
> Para ver essa discussão na Web, acesse
> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAGZ3pzKjbsLmZhjkpi%2BG%2Bd5BKh4N1kvKkGXAX%2Bo0F%3DjX8oSxqA%40mail.gmail.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 ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAMhDzhVf7jDKPmT%3DDqWcFA3HtDKOytrDSMW5fogxYzFmKO5gng%40mail.gmail.com.

Re: [Logica-l] Vácuo

[Marcelo Finger]

João Marcos.

Eu me lembro de ter assistido uma palestra do Bob Meyer em Londres na
década de 90 sobre a demonstração do teorema de Goedel numa meta-matemática
relevante.  Não me lembro se a aritmética era relevante... o que eu mais me
lembro é que ele já não tinha um pedaço do cérebro e sua fala estava
alterada.

[]s




Em dom., 11 de abr. de 2021 às 16:57, Joao Marcos 
escreveu:

> Pareceria interessante, em particular, checar se uma Aritmética
> Relevante (se existir tal coisa!) conseguiria explicar a semântica
> "folk" ---aquela das pessoas de bom senso--- que Daniel usou para
> alegar a não-equivalência entre as sentenças (A) e (B), da minha
> mensagem anterior.
>
> JM
>
>
> On Sun, Apr 11, 2021 at 11:51 AM Andrea Loparic 
> wrote:
> >
> > Essa discussão me lembra uma outra
> > intimamente relacionada, que foi a
> > que se deu no Círculo de Viena e sua
> > escola na primeira metade do
> > século passado, sobre a implicação
> > material e as contrafactuais.
> > Pois as universais da forma
> > "Para todo x , se x tem mais de 200 anos
> > então P(x)", onde P(x) é uma condição
> > qualquer, são ditas verdadeiras porque não
> > há instância verdadeira da implicação
> > se fulano tem mais de 200 anos então  P(fulano)
> > onde fulano é um parâmetro com o qual se pode
> > percorrer o domínio.
> > E isso não acontece porque a falsidade do
> > antecedente da condicional é condição suficiente da
> > verdade da condicional na definição clássica da
> > implicação material. Dessas discussões - que
> > apontavam para as dificuldades de traduzir o
> > "se... então..." pela implicação material fora dos
> > domínios dos objetos formais, como os da
> > aritmética - estão dentre as motivações principais
> > do surgimento das lógicas relevantes e das lógicas
> > modais.
> > Convém dar uma boa espiada nas que estavam sendo
> > discussões quentes da filosofia da linguagem  há
> > quase um século.
> > Questões reais retornam sempre quando o ofício
> > é o de pensar...
> > Beijo da titia velhinha,
> > Andrea
>
> --
> 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 ver esta discussão na web, acesse
> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LhZ4kSbT_STUJtRtozhysW2kTjHJa_KMjOVoA2GTU%2Bbqw%40mail.gmail.com
> .
>


-- 
 Marcelo Finger
 Departament of Computer Science, IME
 University of Sao Paulo
 http://www.ime.usp.br/~mfinger
 ORCID: https://orcid.org/-0002-1391-1175
 ResearcherID: A-4670-2009

-- 
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 ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAGG7Aw3imqao0538P1ASPoJ7aVPWRf24iko_z2V6X6hN0uhiBQ%40mail.gmail.com.