On Intuitionίstί c Functional Calculus
Osaka Mathematical Journal, Masao Ohnishi · 1953
1. VxF(x} -> -7-7 VxF(x}-> Vx -7-7 F(x) ;± 77 Vx 77 F(x} ;± 7 3x 7 F(x) , 2. 3xF(x} -> 3x -7-7 F(x) -> -77 3xF(x) ^± 77 3x -77 F(x) ^±7Vx7 F(x} , 3. Vx 7 F(x) ί± 77 Vx 7 F(x] ^± 7 3x 77 F(x) ^ί 7 RxF(x) , 4. 3.x 7 F(x) -> 77 3x 7 F(x} ί± 7 Vx 77 F(x] -> 7 VxF(x) . Explanations for the symbols used here: Vx and 3x are universal and existential quantifiers with respect to the individual variable x respectively. F(*} is functional variable with certain (finite) number of arguments. — > is one-way implication and ^± is (logical) equivalence of ante- and succedent formulae. (Hence these two are meta-logical symbols.) 7 is negation and 77 is double negation of the remaining sub-formula after it. 1. Iterated quantifications. Starting from the above schema by Heyting let us consider the case of iterated quantifications, where we shall be mainly concerned with the implicative relations between such formulae as follows : Vx F(x 3x F(x Vx Hy F(xy 3x Vy F(xy Vx 3y Vz F(xyz 3x Vy Hz F(xyz) and their weakened forms to which 77 's are attached. 1. 1. Formulae with one quantifier. In this case the implicative relations are : (1) Vx F(x} -> 77 Vx F(x} -> Vx 77 F(x) ^± 77 Vx 77 F(x} , (2) 3x F(x} -> 3x 77 F(x) -> 77 Hx F(x} ^ 77 3x 77 F(x) . Hereafter some conventions will be used. The attached symbol 7