olemus
matemaatilise loogika haru, milles tõesed laused
konstrueeritakse aksioomidest, tuletusreeglitega

Wikipedia:
a major branch of mathematical logic and theoretical computer science within which proofs are treated as formal mathematical objects

näide
lausearvutuses saab tõesed laused tuletada aksioomidest,
kus A, B ja C on suvalised laused (mitte tingimata lihtlaused):
A → (B → A)
(A → (B → C)) → ((A → B) → (A → C))
(¬A → ¬B) → ((¬A → B) → A)
ja tuletusreeglist modus ponens:
kui A ja A → B on tõesed, siis B on tõene

ülevaateid
https://plato.stanford.edu/entries/proof-theory-development/

https://en.wikipedia.org/wiki/Proof_theory

https://en.wikipedia.org/wiki/Category:Proof_theory

https://encyclopediaofmath.org/wiki/Proof_theory

https://www.lix.polytechnique.fr/~lutz/papers/ESSLLI10notes.pdf

https://math.ucsd.edu/~sbuss/ResearchWeb/handbookI/ChapterI.pdf

http://home.uchicago.edu/~wwtx/Proof.pdf

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.137.1959&rep=rep1&type=pdf