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

The present work is dealing with model theory in sheaves of L-structures over a complete Heyting algebra 'omega'. Modifying the notion of the symbols of constantes in a first order language, allowing a parcial existence, we will generalize the method of diagrams and elementary diagrams originated by A. Robinson in the context o L-structures in the category 'pSh(omega)'. Further-more, we will improve Fraïssé's theorem, apearing in [6], for L-structures in the category 'Sh(OMEGA)'. In all details we will demonstrate the completeness theorem for sheaves of L-structures, for a intutionistic, consistent theory we will prove - using the Lindenbaum algebra - that we can construct a sheaf of L-structures over a complete Heyting algebra. We will demonstrate for a language L# - a usual first order language without the universal quantifier - the model existence theorem for sheaves over topological spaces. For this, we will introduce the spectral space of prime extensions. Using this model existence theorem and Baire's theorem, we will genweralize the ommiting types theorem for the intuitionistic logic