Intuitionistic Predicate Calculus with ^|^epsilon;-Symbol
Kokio Shirai · Annals of the Japan Association for Philosophy of Science · 1971
The two explicitly shown formulas A in the upper sequents are called the cut formulas of the cut. 2.22.Logical rules of inference: Intuitionistic Predicate Calculus with ?-Symbol 553) restrict the use of the following rules of inference within the case where t is a free variable: