Esta apresentação introduz dois desenvolvimentos recentes na semântica bilateral da teoria da prova. Em primeiro lugar, apresentamos uma extensão da semântica de extensão de base (B-eS) para o contexto bilateral, resultando numa semântica sólida e completa para N2Int*, uma versão modificada do sistema de dedução natural de Wansing para a lógica bi-intuicionista bilateral 2Int. Esta extensão é conseguida permitindo que as bases atómicas contenham regras tanto de prova como de refutação, captando a ideia bilateralista de que a asserção e a negação são atos independentes. De seguida, exploramos o conceito de incompatibilidade entre provas e refutações, particularmente relevante no raciocínio matemático. Ao enriquecer o N2Int* com regras de interação adequadas, derivamos a BPR, um sistema que possui normalização, a propriedade de subfórmula e consistência. Uma semântica B-eS bilateral refinada, definida sobre bases restritas, captura esta incompatibilidade ao nível semântico. Por fim, demonstramos que a BPR está intimamente relacionada com o conceito de falsidade construtiva de Nelson, interiorizando a falsidade através da noção de refutação.
Apresentação por: Maria Osório Costa (Universidade de Lisboa, CEMS.UL and University College London)