Lógica intuicionista, ou lógica construtivista, é o sistema de lógica simbólica desenvolvido por Arend Heyting para prover uma base formal para o  intuicionismo de Brouwer. O sistema preserva, também, a justificação, e não apenas a verdade, no processo que leva de hipóteses a proposições derivadas - se as hipóteses são verdadeiras e justificáveis então a conclusão também será verdadeira e justificável. De um ponto de vista prático, há, também, uma forte motivação para usar a lógica intuicionista, já que ela possui a propriedade existencial, tornando-a adequada para outras formas de construtivismo matemático.