#Kleene's #recursive realizability proofs of intuitionistic arithmetic: recursive function f( proof of a formula expressing that recursive function "realizes", i.e. correctly instantiates the disjunctions) + existential quantifiers of the initial formula st formula gets true