A constructivism based on classical truth (Q1117222)

The operator T is said to represent classical truth in a system S if \(\vdash_{C\Pr C}A\) iff \(\vdash_{S}TA\) where CPrC is classical predicate calculus. The properties of constructive systems which allow such operator T are studied. The exposition is limited to propositional systems with some indications about predicative extensions. Methods based on Kripke semantics are used. A maximal constructive system \(E^*\), where T represents classical truth, is described. For this system a kind of semantics based on the notion of ``valuation from'' is introduced and investigated. The work is in connection with that of \textit{R. H. Thomason} [Z. Math. Logik Grundlagen Math. 15, 247-257 (1969; Zbl 0181.009)] and \textit{D. Nelson} [J. Symb. Logic 14, 16-26 (1949; Zbl 0033.243)].