O método das constantes na teoria dos modelos em feixes sobre uma álgebra de Heyting - Brunner, Andreas Bernhard Michael (2000)
O trabalho presente trata de teoria dos modelos em feixes de L-estruturas sobre uma álgebra de Heyting completa 'omega'. Modificando a noção dos símbolos de constantes de uma linguagem de primeira ordem, admitindo uma existência parcial, generalizamos o método dos diagramas e diagramas elementares devido a A. Robinson para L-estruturas na categoria 'pSh(omega)'. Além disso, melhoramos o teorema de Fraïssé aparecendo em [6] para L-estruturas na categoria 1Sh(omega)'. Demonstramos o teorema da completude em todos os detalhes para feixes de L-estruturas, mostramos que para toda teoria intuicionista consistente podemos construir - usando a álgebra de Lindenbaum - um feixe de L-estruturas sobre uma álgebra de Heyting completa. Também demonstramos para a linguagem L# - uma linguagem usual de primeira ordem sem o quantificador universal - o teorema de existência de modelos para feixes sobre espaços topológicos. Para isso, introduzimos o espaço espectral das extensões primas. Finalmente, generalizamos o teorema de omissão de tipos para lógica intuicionista, usando o teorema de existência de modelos e o teorema de Baire