A non-effective cut-elimination proof for modal mu-calculus has been given by G. J?ger, M. Kretz and T. Studer. Later an effective proof has been given for a subsystem M _1 with non-iterated fixpoints and positive endsequents. Using a new device we give an effective cut-elimination proof for M _1 without restriction to positive sequents.
展开▼
