{'fraction_non_alphanumeric': 0.033854166666666664, 'fraction_numerical': 0.020833333333333332, 'mean_word_length': 5.252032520325203, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
A Canonical Model for Presheaf Semantics

Presheaf models [Osius, 1975, Fourman and Scott, 1979, Moerdijk and Mac Lane, 1992] are a simple generalization of Kripke models and provide one of the most natural semantics for intuitionistic predicate logic. Al-though a completeness result for this semantics is known, this is usually obtained either non-constructively, by deﬁning a canonical Kripke model, or indirectly, e.g. via categorical equivalences with Ω − models as in [Troel-stra and Van Dalen, 1988]. This paper describes an elementary canonical model construction by means of which completeness is established in a perspicuous, direct and constructive way. Presheaf semantics. We start by recalling the deﬁnition of presheaf semantics for intuitionistic logic.