Abstract:
The author's method [1] of establishing deducibility is intuitionistie propositional calculus (JPC) is clarified in this note. A tested formula is first transformed into a conjunction of $\pi$-chains [1]. Then each $\pi$-chain is rewritten as a matrix. After that some occurences of atomic formulas are marked by “+” or “-” according to so called “rule of marks”. A notion of completed matrix is introduced. The main result is the following theorem:
The deducibility of a $\pi$-chain in JPC is equivalent to the possibility to construct a completed matrix for that $\pi$-chain.