É conhecido, de longa data, que a Lógica Proposicional Intuicionista (LPI) é decidível. O cálculo de sequentes LJT* para LPI, definido por Roy Dyckhoff, não requer contracção de fórmulas e possui a propriedade da terminação (qualquer desenvolvimento de uma derivação parcial é finito), constituindo por isso uma base adequada para o desenho de métodos de decisão para LPI.

O sistema CRIP, definido por Roy Dyckhoff e Luís Pinto, formaliza a não derivabilidade de sequentes em LJT* (um sequente ou é derivável em LJT* ou é derivável em CRIP) e, à semelhança de LJT*, tem a propriedade da terminação. À estrutura de uma derivação em CRIP é possível associar contra-modelos: Roy Dyckhoff e Luís Pinto mostraram como o fazer com base em estruturas de Kripke. Usando ideias similares, Sara Negri e Jan von Plato mostram como construir álgebras de Heyting para testemunhar a não validade intuicionista.

O seminário será dividido em duas sessões. A primeira sessão ocupar-se-á da revisão de noções sobre cálculo de sequentes. Em particular, será revista a forma de obter contra-modelos para a Lógica Proposicional Clássica a partir da não derivabilidade de sequentes e será apresentado o formalismo de Roy Dyckhoff LJT*. Na primeira sessão, serão ainda revistas as noções de validade intuicionista baseadas em estruturas de Kripke e em álgebras de Heyting.

A segunda sessão será centrada no formalismo para a não derivabilidade intuicionista CRIP e nos métodos que lhe estão associados para a construção de contra-modelos, baseados quer em estruturas de Kripke quer em álgebras de Heyting. Adicionalmente, serão ilustradas nesta sessão algumas das dificuldades que se levantam na transposição destas ideias para o fragmento proposicional da Lógica Intuicionista Dual (uma lógica que estende LPI com uma operação dual à implicação e que admite caracterizações semânticas baseadas em estruturas de Kripke e em álgebras de Heyting-Brouwer).