A CERTAIN CLASSIFICATION OF THE HEYTING-BROUWER INTERMEDIATE PROPOSITIONAL LOGICS
Bożena Szostek · Demonstratio Mathematica · 1983
We shall deal with the Heyting-Brouwer pro positional calculus (briefly %_]})» defined in [6j.Th6 language of Ifj.g is an extension of the language of intuitionistic propositional calculus, obtained by adding an unary propositional connective r and a binary propositional connective -Ji_ .For the technical reasons we assume that the constants 1, 0 are the symbols of this language.The class of all formulas P of Ljj_ b is defined in the usual way.Propositional variables will be denoted by p, q, r,... with indices if necessary and formulas by «, $ , p f ... with indices if necessary.The axioms of Ljj_ b are the following formulas: p =*» (p v q), q =>(pv q ), (p=s*r) => ((q =s.r) =s» ((pvq) =>r)), (pAq) =*» p, (p/\q) =s»q, (r=s»p) => i(r ==s>q ) ==> (r (p/vq))), ( P '•=> (q =s> 'c)) ==s> (( p a q ) =s»r), (( p/\ q ) =s>r) ==> (p (q =i»r)) , (p =s>q) => frq ==^.-|p),P =i>(q V (p -q)), (P -=-q ) -»r(p =*.q) f 945 -