형식언어의 연산(?)이 순수하게 구문론적일 수있다(?)라는 개념이 이해가 안가요 (그니까 그냥 턴스틸의 의미가 이해가 안가요)


그러니까 의미론적인 작업이라는 귀결(이중 턴스틸)은 대체로 이해가 가는 거같거든요? 

어떤 문장집합이 특정 해석 아래에서 참이 될 때, 같은 해석아래에서 참이되는 임의의 문장집합 밖의 문장을 논리적 귀결이라고 할 수 있는 거죠? 

그리고 서로가 서로의 논리적 귀결이면 논리적 동치가 되는거고요, 논리적 동치가 되면 쌍조건문(if and only if)의 양변에 각 문장을 집어넣으면 참이 나오는 거고요


반면 구문론적 증명 혹은 derivation이란 건 해석이 없이도 할 수 있다고 하는데 


막상 그래놓고 증명에 필요한 추론규칙이라는 것들을 보면 논리 연산자로 구성되어있잖아요? 

근데 결국 논리 연산자라는 것은 진리치를 받아서 진리치를 리턴하는 함수인것이고

이 진리치라는 것은 결국 해석을 통해서 결정되는거잖아요? 모든 해석아래 항상 참이되거나 거짓이 되는 문장이 더러 있지만, 어쨌든 원칙적으로는 해석을 다르게 하면 진리값이 달라질 수 있는 것이고요


결국 추론규칙이라는 게 성립한다는 것도 이런 추론 규칙을 정의하는데 사용한 문장에 하나하나 해석을 넣어보고 경험적으로 알아낸 거 아닌가요?

그렇게 해서 모든 해석 아래에서 턴스틸 왼쪽에 있는 문장들의 진리값이랑 오른쪽에 있는 문장의 진리값이 일치하는 걸 보고 

아 "이 녀석들은 논리적 귀결 관계에 놓여있구나" 하고 이렇게 알아낸 거 아닌가요?


그럼 이렇게 알아낸 추론규칙들이란 건 뭐가 해석이랑 무관한 '구문론적 작업'인건가요?

해석과 논리적 귀결 개념만 있으면 됐지 무슨 증명이니 추론이니 그런게 따로 필요한거죠? 
설혹 그런 구문론적 작업이란 것이 있다고 해도 그것은 그냥 해석을 부여했을 때 진리치가 일치하는지 아닌지 잘 살펴봤다가 
그 진리치가 항상 일치하는 경우를 따로 추려두고 정리해둬서 근의 공식외워서 인수분해 하듯이 그렇게 기계적으로 써먹는 것이고 
이런 것은 어쨌든 기본적으로는 논리적 귀결개념으로 환원될 수 있는 거 아닌가요?

 



+ 논리학 초보니까 좀 용어가 부정확해도 이해해주세요오