Completeness of global intuitionistic set theory

Gentzen's sequential system LJ of intuitionistic logic has two symbols of implication. One is the logical symbol → and the other is the metalogical symbol ⇒ in sequents Considering the logical system LJ as a mathematical object, we understand that the logical symbols ∧, ∨, →, ¬, ∀, ∃ are operators on formulas, and ⇒ is a relation. That is, φ ⇒ Ψ is a metalogical sentence which is true or false, on the understanding that our metalogic is a classical logic. In other words, we discuss the logical system LJ in the classical set theory ZFC, in which φ ⇒ Ψ is a sentence. The aim of this paper is to formulate an intuitionistic set theory together with its metatheory. In Takeuti and Titani 6, we formulated an intuitionistic set theory together with its metatheory based on intuitionistic logic. In this paper we postulate that the metatheory is based on classical logic. Let Ω be a cHa. Ω can be a truth value set of a model of LJ. Then the logical symbols ∧, ∨, →, ¬, ∀ x , ∃ x are interpreted as operators on Ω, and the sentence φ ⇒ Ψ is interpreted as 1 (true) or 0 (false). This means that the metalogical symbol ⇒ also can be expressed as a logical operators such that φ ⇒ Ψ is interpreted as 1 or 0.