We perform a proof-theoretical investigation of two modal predicate logics: global intuitionistic logic
GI and global intuitionistic fuzzy logic
GIF. These logics were introduced by Takeuti and Titani to formulate an intuitionistic set theory and an intuitionistic fuzzy set theory together with their metatheories. Here we define analytic Gentzen style calculi for
GI and
GIF. Among other things, these calculi allows one to prove Herbrand
s theorem for suitable fragments of
GI and
GIF.
Key words or phrases: Modal predicate logics - Globalization - Hypersequent calculi - Cut-elimination
Work Supported by C. Bühler-Habilitations-Stipendium H191-N04, from the Austrian Science Fund (FWF).