{'fraction_non_alphanumeric': 0.011948529411764705, 'fraction_numerical': 0.0, 'mean_word_length': 5.0472222222222225, '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}}
Formally defined operations in Kripke models

The introduction of Kripke models in intuitionistic logic has originated a growing interest in this field. There is no doubt that the relation between these models and forcing has played a role in this development. As a consequence the traditional interpretation of intuitionistic logic, namely the notion of constructiveness considered by Brower, Heyting and others, appears to have lost some of its former preponderance. Recently several logicians have been interested in defining arbitrary operations in the models, to some extent independently of the operations which are proper of intuitionistic logic. In this paper some results in this direction are presented. We consider only the propositional calculus. We study operations which are formally defined in the following sense. Each operation is introduced first as a formal connective together with some provability rules. Then we use the same rules to give the interpretation of the connective in the model. This is possible because we use Gentzen type rules for which the subformula property holds. We give some formal conditions for the rules that are both necessary and sufficient for the system to be adequate and complete. The most interesting property of these operations is that whenever two of them agree in one of the Kripke models then they agree in all models, hence they are actually the same operation. The usual connectives of intuitionistic logic are formally defined in our sense, hence our results apply to them. Not only that, it is easy to show that every formally defined connective can be also defined explicitly by some formula containing only the usual connectives. On the other hand we show that there are operations defined explicitly by formulas containing only the usual connective which are not formally defined in our sense. Such operations agree with some formally defined operation in at least one model—the classical model—but for every formally defined operation there is a model in which they are different. This result generalizes the well known result that there are classical tautologies which are not provable in intuitionistic logic.