P 
PAx2: P P Q
P QAx3: P Q Q P
Q Q PAx4: (P Q) (Q P P Q)
Q) (Q P P Q)Observera att P, Q och R här är symboler i metaspråket.
I Hilberts bevisteori är endast härledningsregeln Modus Ponens tillåten.
I Hilberts bevisteori ingår för satslogikens del följande axiom:
P P P Q Q Q P Q) (Q P P Q)Observera att P, Q och R här är symboler i metaspråket.
I Hilberts bevisteori är endast härledningsregeln Modus Ponens tillåten.