andou yuuki 라는 사람의 증명입니다.
맨 마지막줄이 왜 성립하는거죠???A1 v A2, D, D 로부터 D를 얻는건 그냥 아무 추론규칙 없이 되는거 아닌가요?근데 A1 v A2 는 왜 나온거죠? (증명 Gamma를 아에 지워버릴 수 있는거 아닌가요???)
andou yuuki 라는 사람의 증명입니다.
맨 마지막줄이 왜 성립하는거죠???A1 v A2, D, D 로부터 D를 얻는건 그냥 아무 추론규칙 없이 되는거 아닌가요?근데 A1 v A2 는 왜 나온거죠? (증명 Gamma를 아에 지워버릴 수 있는거 아닌가요???)
아 저 마지막 줄도 v 제거규칙인 거 같은데, 그럼 왜 maximal fomlua가 사라진거죠? 여기서 maximal formula 는 A1 v A2 아닌가요?
아 M이구나.. 대략 해결된거 같긴한데 어렵네요
증명 Delta 1과 Delta2에서의 결론 M은 지울 필요가 없나요?
maximal formula의 정의가 단순히 도입되었다가 다시 제거되는 논리식인가요?
와.. 뭔 이상한 기호들 많이 보이는데 저게 뭣들을 말하는거죠..
선언 제거규칙의 결론의 경우 다른 제거규칙의 주전제(major premise)인 경우가 있기 때문에 선언 제거규칙의 부전제(minor premises)들을 사용해 선언 제거규칙의 결론이 다른 제거규칙의 주전제가 되지 않도록 재구성하는 절차입니다. Prawitz의 1965년작 Natural Deduction에서 소개가 되었던 테크닉이고 보통 permutation conversion이라고 불리는 방식이에요. 제시된 방식은 환원 절차(reduction procedure)를 제시한 것으로 새로운 것을 증명한다기 보다 이미 있는 증명(도출)을 다른 형식의 증명으로 바꾸는 테크닉입니다.
해당 증명에서 감마, 델타1, 델타2, 시그마1, 시그마2 도출은 이미 가지고 있는 것으로 여기는 거에요. 감마가 없어진다면 다른 종류의 증명이 되니까 환원 절차로 보기 어려울 수 있겠죠.