An Intuitionistic Temporal Logic for Brouwer’s Creating Subject Arguments
Josephine Sijtske van der Laan

Abstract:
We develop an intuitionistic temporal logic for Niekus’ formalization of Brouwer’s Creating Subject arguments. This formalization differs from standard ones, such as the Theory of the Creating Subject (TCS), which results in a different treatment of the sequences used in these arguments. Niekus notes that these sequences have incomplete descriptions and are therefore instances of individual choice sequences, an observation arising in connection with his proposal.
To formalize the arguments in accordance with Niekus’ approach, we introduce an intuitionistic temporal logic with temporal modalities □ and ⃝, where ⃝ admits an interpretation as a least fixed point operator. The resulting system, TICS-2, builds on earlier formalizations of Niekus’ proposal. We establish soundness and completeness of TICS-2 with respect to a class of bi-relational Kripke frames. For its □-fragment TICS-2_□ , we develop an alternative semantics based called modal cover semantics, as recently introduced by Valliappan, and obtain a constructive completeness proof via a canonical model construction. This fragment corresponds to Intuitionistic Epistemic Logic IEL, as developed by Artemov and Protopopescu; we discuss results for this logic and its connection to our system. We moreover introduce QE+-TICS-2_□ , a first-order extension of TICS-2_□ with an explicit existence predicate as in E+-logic, and establish soundness and completeness for this system.