알고리듬으로 풀어내는 철학적 논증
귀류법을 코드로 구현해 봅시다.
컴퓨터를 가지고 논리식을 분석하고 테스트해 볼 수 있을까요? 쉽게 말해 프로그래밍 언어로 논리식을 형식화시켜서 테스트를 해 볼 수 있을까에 대한 것입니다. 당연하지만 가능합니다. 현대 컴퓨터 구조의 탄생 자체가 이것과 관련이 있습니다.
지난번 글에서 귀류법에 대해서 알아보았는데요. 이번 글에서는 귀류법을 코드로 구현해 본 뒤 논리식을 평가해서 귀류법의 논리적 정당성을 평가해 보겠습니다. 이것은 일종의 간단한 코딩을 통한 귀류법에 대한 메타논리 테스트라고 볼 수 있습니다.
귀류법은 울프럼 언어를 통해서 코드로 구현하겠습니다. 울프럼 언어가 생소하신 분들을 위해 잠시 소개해 드리겠습니다.
울프럼 언어 공식 로고 (출처: 위키피디아)울프럼 언어는 대표적인 폴리매스 천재인(물리학, 수학, 컴퓨터 과학) 스티븐 울프럼 박사가 개발한 고수준 프로그래밍 언어입니다.
이 언어는 수학, 과학, 공학, 데이터 분석 등 다양한 분야에서 사용됩니다. 이 언어의 가장 큰 특징 중 하나는 심볼릭 연산에서의 탁월한 능력입니다.
즉, 복잡한 수식을 기호 그대로 다룰 수 있어, 대수학적 조작, 미적분, 방정식 풀이 등을 정확하고 효율적으로 수행합니다. 이는 수치적 근사가 아닌 정확한 해를 구할 수 있게 해 줍니다.
심볼릭 연산에 강하기 때문에 울프럼 언어는 논리식을 작성하기에 최적화된 언어라고 볼 수 있습니다. 자 이제 아래의 과정을 거쳐서 귀류법을 울프럼 언어로 작성 한 뒤 논리적 정당성을 평가해 볼 것입니다. 울프럼 언어는 매스매티카에서 작성되었습니다.
1. 귀류법을 형식 논리로 표현하기.
여기서 형식 논리로 사용할 체계는 술어 논리식으로 선택했습니다. 울프럼 언어는 술어 논리 표현을 아주 잘 지원합니다.
https://gist.github.com/otter275/12291da0ad98e51c0089d673ed6becb1
위의 코드를 실행 하면 아래의 결과를 얻습니다.
코드 설명: ForAll, Implies 함수로 논리식을 실제로 손으로 작성하는 기분으로 직관적으로 작성할 수 있습니다. 기술적인 사항으로 HoldForm 함수를 사용해서 원래의 술어 논리식을 보존하도록 처리했습니다. 이렇게 하지 않으면 울프럼 언어에서 술어 논리식을 simplify 한 형태로 보여 주기 때문에 가독성이 떨어집니다.
2. 귀류법에 대한 정방향, 역방향에 대한 술어 논리식 평가.
https://gist.github.com/otter275/46dfdf00cf164eae35d4e11f9a9806c1
위의 코드를 실행 하면 아래의 결과를 얻습니다.
코드 설명: FullSimplify 함수로 귀류법에 대한 정방향, 역방향에 대한 술어 논리식의 진리값이 모두 True로 반환되었습니다. 이것은 귀류법에 대한 정방향, 역방향에 대한 논리 표현이 동치관계임을 의미합니다. 기술적인 사항으로 술어논리식을 담은 변수들이 HoldForm 처리가 되어 있으므로 연산을 수행하기 전에 ReleaseHold를 해 주어야 합니다.
3. 귀류법에 대한 정방향, 역방향에 대한 술어 논리식의 동등성 평가
https://gist.github.com/otter275/54be8f72c0c424aed2640bc057477ffc
위의 코드를 실행 하면 아래의 결과를 얻습니다.
코드 설명: 귀류법에 대한 정방향, 역방향이 동치관계임은 위에서 이미 확인했으나 울프럼 언어의 Equivalent 함수를 통해서 언어 레벨에서의 동등성을 다시 한번 평가해 볼 수 있습니다. 동등성 평가 결과는. True입니다. 이것은 귀류법이 논리적으로 완전하고 강건한 추론 규칙임을 의미합니다.
귀류법을 울프럼 언어로 구현하고 메타논리 진술(여기서는 술어논리) 테스트를 해 봄으로 몇 가지 사실을 확인할 수 있습니다.
형식화의 힘과 한계: 울프럼 언어를 통해 귀류법의 논리적 구조를 명확히 표현할 수 있었지만, 동시에 이러한 형식화가 귀류법의 모든 측면을 완벽히 포착하지는 못한다는 점도 드러났습니다.
메타논리적 고찰의 중요성: 귀류법을 술어 논리로 표현한 논리식과 그 역의 동등성을 검증함으로써, 우리는 이 추론 규칙의 논리적 완전성을 확인할 수 있었습니다. 이는 단순한 구현을 넘어서는 메타논리적 통찰을 제공합니다.
컴퓨터 지원 논리 분석의 가능성: 울프럼 언어의 강력한 심볼릭 연산 능력을 통해, 복잡한 논리적 개념을 효율적으로 분석하고 검증할 수 있음을 확인했습니다.
형식 논리와 실제 적용 사이의 간극: 귀류법의 술어 논리적 표현이 실제 수학적 증명에서의 귀류법 사용과는 차이가 있다는 점을 인식함으로써, 형식 체계의 한계와 수학적 추론의 풍부함을 동시에 이해할 수 있었습니다.
철학적 함의: 이러한 분석은 논리학, 수학 철학, 그리고 인공지능의 기반이 되는 형식 체계의 본질과 한계에 대한 더 깊은 철학적 고찰로 이어질 수 있습니다.
위에서 형식화의 힘과 한계 부분에 대해서 조금 더 부연 설명을 하면 위의 코드 테스트는 단순하게 귀류법을 술어논리식으로 형식화한 것에 불과합니다. 귀류법의 모든 측면을 완벽히 포착하려면 a. 귀류법의 증명 과정에 대한 단계별 형식화 b. 추론 규칙 집합 정의 c. 메타논리적 프레임워크(공리계) d. 증명 보조 시스템 구현 e. 타입 이론 활용 등의 많은 추가 작업이 필요합니다. 이것들에 대한 논의는 추가 글을 통해서 이어가 보도록 하겠습니다.
