La logique mathématique a développé une branche qui est consacrée à l'étude des démonstrations et des systèmes déductifs et s'appelle pour cela la théorie de la démonstration.
Il est parfois possible de démontrer qu'une certaine assertion ne peut pas être démontrée dans un certain système axiomatique dont on aurait pourtant attendu qu'il puisse formaliser « toutes » les mathématiques ; ainsi l'axiome du choix ne peut pas être démontré dans la théorie des ensembles de Zermelo-Fraenkel, non plus que sa négation. De façon analogue, ni l'hypothèse du continu ni sa négation ne sont démontrables dans la théorie de Zermelo-Fraenkel avec axiome du choix. On dit que ces assertions sont indépendantes de ce système d'axiomes : il est par exemple possible d'ajouter aussi bien l'axiome du choix que sa négation à la théorie des ensembles, la théorie restera cohérente (en supposant que la théorie des ensembles le soit). En fait, comme l'énonce le théorème d'incomplétude de Gödel, dans toute théorie axiomatique « raisonnable » qui contient les nombres naturels, il existe des propositions qui ne peuvent pas être démontrées alors qu'elles sont en fait « vraies » ; plus précisément toutes les instances de la proposition par chacun des entiers naturels sont démontrables.
L'informatique a construit des outils d'aide à la démonstration qui sont de deux ordres: