고전적 코어 논리의 절단

초록 이 저널의 이전 논문에서 나는 코어 논리의 건설적이고 관련된 시스템에 대한 구체적인 동기를 제공하였고, 그 주요 기능을 설명하였으며, Cut가 시스템의 규칙은 아니지만, 그럼에도 불구하고 Cut가 허용 가능하다는 것을 밝혔고, 실제로 잠재적인 인식적 이득이 있음을 증명하였다. 만약 Π가 수열 Δ : A의 증명이고 Σ가 수열 Г, A : θ의 증명이라면, ‘전체 목표 수열’ Δ, Г : θ의 어떤 후속에 대한 계산 가능한 축소 Π, Σ가 존재한다. 건설적인 경우 이 잠재적인 인식적 이득은 문제의 후속이 Δ, Г : θ의 적절한 후속이 될 가능성에 있으며, 심지어 Δ, Г : θ보다 논리적으로 더 강할 수도 있다. 이 논문에서는 Cut가 고전적 코어 논리에도 마찬가지로 허용된다는 것을 확립하며, 이는 고전적 딜레마 규칙의 적절히 관련화된 형태를 추가하여 코어 논리에서 얻어진 것이다. 고전적 경우에는 잠재적인 인식적 이득의 추가적인 특징이 있다: 증명 Π, Σ는 Π와 Σ보다 비건설성이 낮을 수 있다.