Neste trabalho, apresentamos uma lógica de primeira ordem com tipos para as categorias Psh(Q) e Sh(Q) dos prefeixes e feixes sobre quantais (right-sided e idempotentes). São estudadas as propriedades das operações lógicas entre sub-objetos em Psh(Q) com relação ao cálculo da imagem inversa por morfismos (interpretando a substituição de uma variável por um termo numa fórmula), estabelecendo condições suficientes, expressáveis na linguagem de primeira ordem, que garantem a preservação das operações. Em particular, é discutida a noção de extensão de sub-prefeixes -construídos a partir de sub-prefeixes elementares- por novos prefeixes, inerente ao processo de combinar fórmulas com variáveis de tipos diferentes. Portanto, as regras de lógica possuem cláusulas que prescrevem as condições de extensão, o que garante a corretude da lógica. São analizadas propriedades de primeira ordem das relações binárias em Psh(Q), assim algumas estruturas algébricas, tais como anéis, módulos e corpos. É provado na lógica um teorema de I. Kaplansky, que diz serem livre os módulos projetivos finitamente gerados sobre um anel local

not available