# Does second-order Heyting arithmetic have the disjunction and existence properties?

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)$$?

• 1 and 2 are equivalent for any decent arithmetical theory by a result of Friedman. Jan 11, 2022 at 19:45