Llògica intuicionista
La llògica intuicionista, o llògica constructivista, és el sistema llògic originalment desenrollat per Arend Heyting per a proveir una base formal per al proyecte intuicionista de Brouwer. El sistema emfatisa les proves, en contes de la veritat, a lo llarc de les transformacions de les proposicions.
La llògica intuicionista rebuja el principi del tercer exclòs, pero conserva el principi d'explosió. Açò es deu a una observació de Brouwer que si emfatisem les proves en contes de la veritat, llavors en els conjunts infinits el principi del tercer exclòs falla quan s'aplica a una proposició per a la qual no existix demostració, ni de la seua veritat ni de la seua falsetat.
En els conjunts finits sempre és possible verificar si una proposició és certa o falsa; en els infinits, no.