The Decidability of Dependency in Intuitionistic Propositional Logi
de Jongh, Dick ; Chagrova, L. A.
J. Symbolic Logic, Tome 60 (1995) no. 1, p. 498-504 / Harvested from Project Euclid
A definition is given for formulae $A_1,\ldots,A_n$ in some theory $T$ which is formalized in a propositional calculus $S$ to be (in)dependent with respect to $S$. It is shown that, for intuitionistic propositional logic $\mathbf{IPC}$, dependency (with respect to $\mathbf{IPC}$ itself) is decidable. This is an almost immediate consequence of Pitts' uniform interpolation theorem for $\mathbf{IPC}$. A reasonably simple infinite sequence of $\mathbf{IPC}$-formulae $F_n(p, q)$ is given such that $\mathbf{IPC}$-formulae $A$ and $B$ are dependent if and only if at least on the $F_n(A, B)$ is provable.
Publié le : 1995-06-14
Classification: 
@article{1183744749,
     author = {de Jongh, Dick and Chagrova, L. A.},
     title = {The Decidability of Dependency in Intuitionistic Propositional Logi},
     journal = {J. Symbolic Logic},
     volume = {60},
     number = {1},
     year = {1995},
     pages = { 498-504},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183744749}
}
de Jongh, Dick; Chagrova, L. A. The Decidability of Dependency in Intuitionistic Propositional Logi. J. Symbolic Logic, Tome 60 (1995) no. 1, pp.  498-504. http://gdmltest.u-ga.fr/item/1183744749/