Rules of Inference with Parameters for Intuitionistic Logic
Rybakov, Vladimir V.
J. Symbolic Logic, Tome 57 (1992) no. 1, p. 912-923 / Harvested from Project Euclid
An algorithm recognizing admissibility of inference rules in generalized form (rules of inference with parameters or metavariables) in the intuitionistic calculus $\mathbf{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 $\mathbf{H}$ and for constructing some solutions for solvable equations is obtained. A semantic criterion for admissibility in $\mathbf{H}$ is constructed.
Publié le : 1992-09-14
Classification: 
@article{1183744048,
     author = {Rybakov, Vladimir V.},
     title = {Rules of Inference with Parameters for Intuitionistic Logic},
     journal = {J. Symbolic Logic},
     volume = {57},
     number = {1},
     year = {1992},
     pages = { 912-923},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183744048}
}
Rybakov, Vladimir V. Rules of Inference with Parameters for Intuitionistic Logic. J. Symbolic Logic, Tome 57 (1992) no. 1, pp.  912-923. http://gdmltest.u-ga.fr/item/1183744048/