Creative subject, Beth models and neighbourhood functions (Q1908820)

The activity of the ``creative subject'' (or the idealized mathematician) was treated explicitly in various of Brouwer's works since 1948. In order to develop a semantical analysis of Brouwer's basic idea, the author considers some extensions of Heyting first-order logic with the ``creative subject axioms'' based on the first-order language enriched with the new logical operator \(\square\) making it possible to express the central notion \(\square_n A\), meaning that ``the creative subject has evidence for \(A\) at stage \(n\)''. A Beth type semantics for the considered systems is proposed, followed by the corresponding completeness results; and some statements concerning the conservativity of certain systems with respect to Heyting first-order logic are proved.