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.)


  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
    $\begingroup$ 1 and 2 are equivalent for any decent arithmetical theory by a result of Friedman. $\endgroup$ Jan 11, 2022 at 19:45

1 Answer 1


Yes to all. For example see Chapter IX, Section 2 of Beeson, Foundations of Constructive Mathematics.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.