4
$\begingroup$

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

Improve this question
$\endgroup$
1
  • 1
    $\begingroup$ 1 and 2 are equivalent for any decent arithmetical theory by a result of Friedman. $\endgroup$
    – Emil Jeřábek
    Commented Jan 11, 2022 at 19:45

1 Answer 1

Reset to default
6
$\begingroup$

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

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .