Consider full second-order Heyting arithmetic, axiomatized in two-sorted first-order intuitionistic logic (with “number” and “class” variables) by the usual Peano axioms (with induction being stated quantified over classes) and a class-forming notation which, for every formula $\varphi(n)$ with a free number variable $n$, allows forming the class term $\{n : \varphi(n)\}$ satisfying the comprehension axiom $k \in \{n : \varphi(n)\} \Longleftrightarrow \varphi(k)$. (I hope this is reasonably standard. If there is something obviously wrong with this theory as stated, my intent is to define second-order arithmetic with an explicit notation for comprehension.)


**Questions:**


1. Does this satisfy the disjunctive property? I.e., if it proves $P\lor Q$, does it prove $P$ or prove $Q$?
2. Does this satisfy the numeric existence property? I.e., if it proves $\exists n. P(n)$, does it prove $P(\overline{n})$ for some explicit natural number $n$?
3. Does this satisfy the class existence property? I.e., if it proves $\exists Z. P(Z)$, does it prove $P(\{n : \varphi(n)\})$ for some formula $\varphi(n)$?



Does second-order Heyting arithmetic have the disjunction and existence properties?
Yes to all. For example see Chapter IX, Section 2 of Beeson, Foundations of Constructive Mathematics.


