Complexité d'une proposition

Salut

Dans le calcul propositionnel, la démonstration d'une propositions est une suite de propositions du type
A1 A2 ... Ai P1 P2 ... Pn
où Pn est ce qu'on souhaite démontrer, A1 ... Ai sont des axiomes du calcul propositionnel, et où chaque Pj se déduit des propositions précédentes par coupure.

En est-il de même dans d'autres théories ? Par exemple dans ZF peut on mettre n'importe quelle démonstration sous cette forme ?
Le cas échéant peut on définir un genre de complexité d'une proposition qui correspondrait à la longueur de la plus petite démonstration de cette proposition ?

Merci, ciao