Rules of inference with parameters for intuitionistic logic

Journal of Symbolic Logic 57 (3):912-923 (1992)
  Copy   BIBTEX


An algorithm recognizing admissibility of inference rules in generalized form (rules of inference with parameters or metavariables) in the intuitionistic calculus H and, in particular, also in the usual form without parameters, is presented. This algorithm is obtained by means of special intuitionistic Kripke models, which are constructed for a given inference rule. Thus, in particular, the direct solution by intuitionistic techniques of Friedman's problem is found. As a corollary an algorithm for the recognition of the solvability of logical equations in H and for constructing some solutions for solvable equations is obtained. A semantic criterion for admissibility in H is constructed



    Upload a copy of this work     Papers currently archived: 83,878

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library


Added to PP

220 (#68,244)

6 months
3 (#245,275)

Historical graph of downloads
How can I increase my downloads?