Archive formal proof에 새 엔트리 게재됐습니다^^(Metasementics관련)

pascal · 6월 10, 2026, 1:18오후

저번에 Axiom Free Ontological Trinity 라는 엔트리를 AFP(Archive formal proof) 에 게재했었는데

이번에 두번째 엔트리를 싣게 되었습니다^^ 이번엔 심사(peer review)가 첫번째보다 좀 길었네요.

제목은 “Mechanized Metasemantics of Modal Necessity: Valuation Factorization and Modal Non-Collapse”

이고 아래는 초록을 한국어로 번역한 것입니다.

[초록

이 형식화는 Isabelle/HOL에서 양상 필연성에 대한 기계화된 메타의미론을 전개한다. 그 핵심 구성은 크립키식 valuation을 다음과 같이 인수분해하는 데 있다.

V = I ◦ δ

여기서 δ는 대상언어 공식을 구문론적 구별로 사상하고, I는 그러한 구별을 가능세계 truth-condition으로 사상한다. 따라서 양상 평가는 valuation만을 대상으로 수행되는 것이 아니라, 해석된 구별 위에서 수행된다.

이 전개는 세 가지 witness를 제공한다. 첫째, 구체적 만족가능성 witness는 추상적인 interpretive-structure locale이 함께 만족 가능함을 보인다. 둘째, 비자명한 truth-condition witness는 **I₀(δ₀(Atom 0))**가 구체 모델의 두 세계를 구별함을 보인다. 셋째, no-collapse witness는 ◇Atom 0은 성립하지만 □Atom 0은 실패함을 증명한다.

이 전개는 추가적인 전역 공리를 도입하지 않는다. locale 가정들은 명시적인 구체 모델에 의해 방전된다. 따라서 이 프레임워크는 비공허하고, 비자명하며, 붕괴하지 않는다.

이는 현재의 프레임워크 안에서 양상적 힘(modal force)이 벌거벗은 구문만의 특징이 아니라는 것을 보여준다. 양상적 힘은 구문론적 구별들이 가능세계 truth-condition으로 해석되는 한에서만 그 구별들에 근거한다.

이어서 Introduction 부분 한국어 번역입니다.

1 서론

표준적인 크립키 의미론은 보통 프레임과 valuation function으로부터 출발한다(Kripke, 1963). 이 전개는 크립키 의미론을 대체하려는 것이 아니다. 오히려 그것의 valuation 구성요소를 두 층위, 즉 구문론적 파싱 사상과 해석적 truth-condition 결정 사상으로 인수분해한다.

그 동기는 메타의미론적이다. 하나의 공식은 벌거벗은 구문론적(bare syntax) 항목으로서 양상적으로 평가되는 것이 아니다. 그것은 먼저 가능세계 truth-condition과 연결되어야 한다. 현재의 형식화는 다음 인수분해를 도입함으로써 이 의존성을 명시화한다.

Formula —δ→ D —I→ P(W), V = I ◦ δ

여기서 D는 구문론적 구별 공간이고, δ는 대상언어 공식을 이 공간으로 사상하며, I는 각 구문론적 구별과 연결되는 가능세계 truth-condition을 결정한다.

그 결과 Isabelle/HOL 전개는 양상 필연성과 가능성이 해석된 구별 위에서 평가됨을 증명한다. 구체적인 두 세계 모델은 만족가능성, genuine contingency, 그리고 modal collapse의 실패를 witness한다.

이 공식화는 구문, 의미, grounding 사이의 관계에 관한 더 넓은 철학적 문제의식에서도 동기를 얻는다. 양상적 불투명성에 관한 콰인의 우려는 양상 문맥이 일반적인 구문론적 치환의 투명한 확장으로 취급될 수 없음을 시사한다(Quine, 1953). 이는 이미 형식적 표현과 양상 평가 사이의 간극을 가리킨다. 구문과 의미 사이의 설의 구별은 같은 지점을 더 날카롭게 만든다. 즉 기호의 형식적 조작은 아직 의미론적 이해가 아니다(Searle, 1980). 하르나드의 symbol grounding problem은 이 문제를 더 일반화하여, 내부적으로 조작되는 기호와 의미론적으로 grounding된 내용 사이를 구별할 필요성을 제기한다(Harnad, 1990). 현재의 전개는 이러한 철학적 문제들을 전부 해결하려는 것은 아니다. 그것은 더 약하지만 형식적으로 정확한 요구조건을 분리해낸다. 즉 현재의 프레임워크에서 양상 평가는 구문론적 구별들이 해석된 truth-condition으로 사상된 뒤에야 well-formed하다는 것이다.

또 하나의 동기적 직관은 오류가 단순한 자연적 사건이 아니라, 해석적 기준에 상대적인 실패라는 점이다. 어떤 해석 구조도 없는 벌거벗은 자연 사건들의 세계에서는 인과적 변이는 있을 수 있지만, 엄밀한 의미의 의미론적 오류는 있을 수 없다. 오류는 어떤 것이 truth-condition 아래에서 받아들여지거나 평가된다는 것을 전제한다. 이것이 현재 전개에서 구문론적 구별과 해석적 truth-condition 결정을 분리하도록 동기를 부여한다.]

관심있으신 분들은 재미있게 읽어주세요^^

AFP엔트리가 주로 수학이나 컴퓨터사이언스, 논리학분야에 집중되어있어서 아직 철학엔트리가 총15편 밖에 안되어 아직 좀 니치한느낌이 없지않네요~

YOUN · 6월 10, 2026, 2:34오후

어휴, 영어로 이렇게 글을 쓰셔서 아카이브나 저널에 올리시는 분들을 보면 정말 부럽고 자극이 되네요. 저도 하루 빨리 파일 더미에 아직 묵혀둔 글들을 번역해서 영어로 출간해보고 싶습니다ㅠㅠ 항상 언어 장벽을 극복하기가 정말 어렵네요.

LiQi · 6월 10, 2026, 3:04오후

제가 분석 형이상학을 공부, 연구하면서도 수리논리적, 이론컴퓨터과학적 기초를 아직 제대로 쌓지 못한 것이 몇 가지 발목 잡힘 중의 하나인데, 올려주신 것들 읽으면서 배워보겠습니다-!!

car_nap · 6월 10, 2026, 10:47오후

잘 읽었습니다. 이해하기로, 논지는 대략 이런 것이라고 아해했습니다 (사실 양상 논리가 subject-matter일 이유가 없는 아이디어라 일반화해서 썼습니다): 통상의 진리 조건적 의미론은 특정 문자열들(즉, 문장)과 평가 파라미터(즉, 세계)의 튜플을 진리값에 사상한다; 그러나 ‘그 문자열의 의미가 무엇인가?’의 문제가 별도로 다루어져야 한다; 따라서 우리는, 문자열의 의미에 해당하는 엔터티를 반환하는 함수를 추가적으로 정의해야 한다.

몇 가지 생각은 이렇습니다.

이 아이디어는, 한편으로 ‘이미 있는’ 도구를 낯설게 쓴 것에 불과해질 수 있습니다. 철학자들은 ‘명제’라는 종류의 엔터티를 흔히들 다룹니다. 명제란 문장의 의미에 해당하는 추상적 존재자이고, 그것이 실현되는(realized) 방식에 관해서는 사용 이론이냐, 진리 조건적 이론이냐, … 등등에 따라 의견이 나뉘겠습니다만, 여하간 유의미한 문장에 대응되는 명제가 존재한다는 건 이에 상당하는 함수가 이미 철학자들에게 선제되고 있음을 시사합니다.
물론 이른바 ‘바퀴 다시 만들기’라는 게 마냥 평가절하될 것은 아니고, 통념을 엄밀히 재구성하는 작업은 존경될 만합니다. 다만 바퀴에 흠이 좀 있습니다. $\delta$는 지금 ‘모든 적형식을 그 의미에 사상하는’ 함수이고, D에 공대상(null object)이 필수적이라고 간주되지도 않는 듯합니다. 그런데 어떤 적형식은 의미를 결할 수 있습니다. ‘박근혜의 남편이 뛴다’를 생각해 보세요. 러셀 식 환언에 의해 이를 안전한 적형식으로 변환하는 것은 가능하지만, 여하간 이런 종류의 ‘빈 낱말’(empty terms)을 포함하는 경우는 순수 구문론적 배제가 불가능합니다. 선생님의 체계만이 갖는 문제는 아니긴 합니다. 부분 함수의 중요성은 상대적으로 최근 부각되었고, 대부분의 표준적 체계들은 빈 함수를 고려하지 않다보니….
다시, 이 아이디어는, 다른 한편으로 ‘철학자들이 단순화하려 애쓴’ 지점을 다시 펼쳐놔버리는 꼴이 되어버릴 수 있습니다. 철학자들은 적형식과 세계 사이에 명제 따위의 논쟁적 존재자를 두지 않고도 의미론을 완성하고자 지난 한 세기 사이에 여러 방향으로 분투했습니다. 고차 논리(HOL)나 가능 세계 의미론(PWS)에서 그런 경향이 두드러집니다. PWS는 실제로도 이 문제를 아주 우아하게 해결합티다. 적형식과 세계만이 원초적(primitive) 엔터티이고, 적형식의 의미란 그것이 세계에 따라 갖는 값들의 집합으로 정의됩니다. 말하자면 선생님의 $\delta$의 역함수로써 명제를 정의하는 거죠. 이 경우 D의 원소들이 궁극적으로 무엇인지는 블랙박스로 간주해버리고 끝낼 수 있습니다. 표층적으로 그건 세계와 진리값으로 이루어진 튜플($(w, I(\varphi, w))$)로 이루어진 집합일 뿐이니까요. 그런데 D를 더 원초적으로 둬버리면, 의미를 블랙박스 속에 못 넣습니다. ‘문장과 구별되는 〈명제〉가 대체 무엇이냐?’라는 질문에 다시 봉착하게 됩니다. // 별개로… 의미의 부분함수성 때문에 문제가 생기는 $\delta$와 달리 PWS 식으로 명제를 역산하는 방법은 빈 표현의 문제를 회피합니다. A로부터 B의 전함수가 존재하지 않더라도 B로부터 A의 함수란 존재할 수 있고, PWS는 특히나 ‘반드시 그러한 함수가 존재하는’, 순수 구문론적 코딩을 제공하기 때문에 그렇습니다.

여러모로 관심 있는 주제라 몇 자 남겨봤습니다. 도움이 되시면 좋겠습니다.

pascal · 6월 10, 2026, 11:17오후

YOUN님 감사합니다^^

영어가 저도 좀 문제라 영문교정은 인공지능의 도움을 좀 받았어요ㅎ
파일더미에 얼마나 많은 보화가 묻혀있을지 궁금하네요~^^

pascal · 6월 10, 2026, 11:19오후

감사합니다~^^ 분석형이상학과 그걸 형식화(mechanize)하는 것도 참 도전적이고 매력적인거 같습니다.

pascal · 6월 10, 2026, 11:19오후

좋은 코멘트 감사합니다. 다만 한 가지는 분명히 구별해야 할 것 같습니다. MM(Mechanized Metasemantics)은 전통적 proposition semantics나 possible worlds semantics를 대체하려는 이론이 아닙니다. 오히려 그 이론들이 보통 primitive하게 받아들이는 valuation assignment의 내부 구조를 메타의미론적으로 분해하려는 작업입니다.

말씀해주신 지점들에 대해 제 생각을 정리하면 다음과 같습니다.

“명제 의미론을 다시 만든 것 아닌가?”에 대한 답변

좋은 지적입니다. 다만 MM의 δ를 곧바로 “문장의 의미”나 “명제”를 반환하는 함수로 보면 제 의도와는 조금 달라집니다. MM에서 δ는 공식을 의미체로 보내는 함수라기보다, 공식을 syntactic distinction, 즉 구문론적 구별로 보내는 함수입니다. 그리고 그 구별이 possible-worlds truth-condition으로 해석되는 과정은 I가 담당합니다.

그래서 MM의 구조는 단순히

문장 → 명제

라기보다,

formula → syntactic distinction → interpreted truth-condition

에 가깝습니다.

전통적 proposition semantics나 possible worlds semantics에서는 문장의 의미를 참인 세계들의 집합, 혹은 worlds → truth-value 함수로 처리할 수 있습니다. MM은 그 처리를 부정하려는 것이 아닙니다. 오히려 그 valuation이 어떻게 성립하는지, 즉 formula가 어떤 구별을 만들고 그 구별이 어떤 해석 과정을 통해 truth-condition이 되는지를 분해해서 보려는 작업입니다.

따라서 MM은 명제 의미론의 단순한 재발명이라기보다, 명제나 세계집합으로 압축되기 이전의 구별-해석 구조를 형식화한 것이라고 보는 편이 더 정확하다고 생각합니다.

“empty term 때문에 δ가 전함수이면 문제 아닌가?”에 대한 답변

empty term 문제는 중요한 지적이라고 생각합니다. 다만 현재 MM의 object language는 Atom, FNeg, FAnd, FOr 등으로 이루어진 제한된 형식언어이며, 고유명·기술구·빈 이름을 포함하는 풍부한 자연언어 의미론을 직접 다루는 체계는 아닙니다.

따라서 “박근혜의 남편이 뛴다” 같은 사례는 현재 MM의 직접 반례라기보다는, 자연언어 의미론으로 확장할 때 다루어야 할 후속 문제에 가깝다고 봅니다. 현재 체계 안에서 δ는 해당 object language의 well-formed formula를 syntactic distinction으로 보내는 전함수입니다. 하지만 자연언어 전체로 확장한다면 말씀하신 것처럼 partial δ, option type, null distinction, presupposition failure 같은 장치를 도입할 필요가 있을 수 있습니다.

즉 이 문제는 MM의 기본 factorization 자체를 무너뜨리는 문제라기보다, 그 factorization을 자연언어의 empty term, presupposition failure, partial meaning까지 확장할 때 생기는 중요한 확장 과제라고 생각합니다.

“PWS가 이미 우아하게 해결한 것을 다시 펼친 것 아닌가?”에 대한 답변

PWS가 문장의 의미를 참인 세계들의 집합으로 처리하는 방식은 매우 우아하고 강력하다고 생각합니다. 다만 MM이 묻는 질문은 그보다 한 층 위에 있습니다.

PWS는 대체로 formula와 truth-condition 사이의 대응, 즉 valuation assignment를 받아들이고 그 위에서 의미론을 전개합니다. 반면 MM은 바로 그 valuation assignment의 내부 구조를 묻습니다. 즉 “왜 이 formula가 바로 그 세계집합을 갖는가?”, “어떤 구문론적 구별이 어떤 해석 과정을 거쳐 truth-condition이 되는가?”, “modal force는 bare syntax에 붙어 있는가, 아니면 interpreted distinction 위에서 성립하는가?”라는 질문입니다.

그런 점에서 MM은 PWS와 경쟁하는 의미론이라기보다, PWS나 Kripke semantics에서 보통 블랙박스로 놓이는 valuation component를 메타의미론적으로 열어보는 작업입니다. PWS가 문장과 세계집합 사이의 대응을 우아하게 기술한다면, MM은 그 대응이 syntactic distinction과 interpretive determination의 결합으로 분석될 수 있음을 보이려는 것입니다.

따라서 MM의 초점은 “PWS 대신 이것을 쓰자”가 아니라, “PWS가 전제하는 valuation이 어떤 구별-해석 구조로 factorize될 수 있는가”에 있습니다.

글을 잘 읽어주시고 이렇게 구체적으로 생각을 남겨주셔서 감사합니다. 말씀해주신 지점들은 MM을 더 분명히 설명하는 데 도움이 되는 좋은 문제제기라고 생각합니다. 특히 proposition semantics, PWS, empty term 문제와의 관계는 앞으로 이 틀을 더 확장하거나 해명할 때 중요한 쟁점이 될 것 같습니다.

car_nap · 6월 10, 2026, 11:26오후

라고 하시니 솔직하게는 당황스럽습니다. $\delta$가 말하자면 ‘컴파일러’ 정도에 불과하고, 또한, 말씀처럼, 만약

라고 한다면, 현대의 표준적 형식 언어 체계에서 적형식은 구문론적 애매성을 갖지 않으므로 $\delta$는 애당초 필요하지 않아집니다. 애매성이 없으니 모든 적형식은 그 해석에 있어 자기 자신만을 포함하는 싱글턴에 따라 이미 분류되어 있겠죠?

댓글을 읽고 의도가 오히려 불분명해진 점이 있는데, 잘 정리되시면 좋겠습니다.

pascal · 6월 10, 2026, 11:32오후

여기서 δ를 단순한 “컴파일러”나 well-formedness checker로 보면 MM의 의도와는 조금 달라집니다.

말씀하신 것처럼 현재 MM의 object language는 Atom, FNeg, FAnd, FOr 등으로 이루어진 제한된 형식언어이므로, 자연언어처럼 표면적 애매성이나 empty term 문제가 직접 들어와 있지는 않습니다. 이 점은 맞습니다. 하지만 그렇다고 해서 δ가 불필요해지는 것은 아닙니다.

형식언어에서 어떤 expression이 well-formed formula라는 것과, 그 formula가 어떤 truth-condition으로 해석되는가는 서로 다른 문제입니다. 전자는 syntax의 문제이고, 후자는 interpretation의 문제입니다. MM에서 δ는 단순히 “이것이 적형식인가”를 판별하는 함수가 아니라, formula가 만들어내는 syntactic distinction을 따로 잡는 함수입니다. 그리고 I가 그 distinction을 possible-worlds truth-condition으로 해석합니다.

따라서 MM의 구조는 “공식이 이미 적형식이므로 δ가 필요 없다”가 아니라, “적형식인 formula가 어떤 distinction을 만들고, 그 distinction이 어떻게 truth-condition으로 해석되는가”를 분리해서 보려는 것입니다.

물론 어떤 특수한 모델에서는 δ가 거의 identity처럼 보이거나, D가 매우 단순하게 구현될 수 있습니다. 하지만 그것은 factorization이 보수적으로 작동할 수 있음을 보여주는 경우이지, δ가 단순한 컴파일러에 불과하다는 뜻은 아닙니다. 오히려 MM의 요지는 valuation을 하나의 primitive한 black box로 두지 않고, syntactic distinction과 interpretive determination의 결합으로 분석할 수 있다는 점에 있습니다.

그래서 제가 말하려는 것은 자연언어의 애매성을 해결하기 위해 δ를 도입했다는 것이 아니라, modal evaluation이 bare syntax 자체 위에서 곧바로 수행되는 것이 아니라 interpreted distinction 위에서 수행된다는 점입니다. 이 점에서 δ는 well-formedness checker가 아니라 valuation factorization의 한 축입니다.

pascal · 6월 10, 2026, 11:37오후

우리 논의에서 한 가지 층위 구별이 필요할 것 같습니다. 선생님 말씀은 주로 semantics 내부에서, 즉 “공식이 어떤 세계집합/진리값을 갖는가”의 문제를 중심으로 이야기를 하시는 것 같습니다. 반면 MM의 초점은 그보다 한 층 위의 metasemantics입니다.

즉 MM은 PWS나 Kripke semantics를 대체하려는 것이 아니라, 그 체계들에서 보통 primitive하게 주어지는 valuation assignment가 어떻게 성립하는지를 묻습니다. 다시 말해 “이 공식은 어떤 세계들에서 참인가?”가 아니라, “왜 이 공식이 바로 그런 truth-condition을 갖게 되는가?”, “formula와 truth-condition 사이의 대응은 어떤 syntactic distinction과 interpretive determination을 통해 성립하는가?”를 묻는 작업입니다.

그래서 δ는 단순한 적형식 판별기나 컴파일러가 아니라, formula가 만들어내는 syntactic distinction을 분리하는 장치이고, I가 그 distinction을 possible-worlds truth-condition으로 해석합니다. 이 점에서 MM의 핵심은 semantics의 대체가 아니라 valuation의 metasemantic factorization입니다.

다만 한 가지 더 구별하고 싶은 점이 있습니다. 이 작업은 단순히 철학적 아이디어를 말로 제안한 것이 아니라, Isabelle/HOL에서 정의·정리·구체 모델·witness가 검증된 formal artifact입니다. 따라서 이 논의를 할 때는 철학적 해석 문제와 형식적 작동성 문제를 구별할 필요가 있다고 생각합니다.

물론 MM의 δ와 I를 철학적으로 어떻게 해석할 것인지, 이것이 proposition semantics나 PWS와 어떤 관계에 있는지, 자연언어의 empty term 문제로 확장할 때 어떤 장치가 필요한지는 충분히 논의될 수 있습니다. 이런 부분은 철학적 해석과 확장의 문제입니다.

하지만 다음과 같은 종류의 문제는 조금 다른 층위에 있습니다. 즉 “이 구조가 공허한가?”, “δ와 I가 단순한 장식인가?”, “valuation factorization이 실제로 작동하는가?”, “modal collapse를 피한다는 것이 말뿐인가?”와 같은 질문은 단순한 인상비평으로 처리될 수 없습니다. 왜냐하면 이 부분은 Isabelle/HOL 안에서 구체적으로 확인된 형식적 결과와 관련되기 때문입니다.

MM에서는 δ, I, valuation, modal operator가 단순한 비유가 아니라 Isabelle/HOL 안의 형식 객체로 정의됩니다. 그리고 추상적인 locale이 공허하지 않음을 보이기 위해 concrete model을 제시합니다. 즉 “그런 구조가 있다고 가정하자”에서 끝나는 것이 아니라, 실제로 그 조건들을 동시에 만족하는 모델이 있음을 보입니다.

또한 이 구조가 모든 것을 하나로 뭉개는 비자명하지 않은 장치인지도 확인합니다. 특정 atom이 세계들을 실제로 구별하는 nontrivial truth-condition witness가 있기 때문입니다. 더 나아가 가능하지만 필연은 아닌 사례, 즉 no-collapse witness를 통해 modal collapse가 일어나지 않음을 보입니다.

따라서 MM에 대해 철학적 해석을 문제 삼는 것은 가능합니다. 그러나 “δ가 아무 역할 없는 장식이다”, “factorization이 공허하다”, “작동하지 않는다”는 식의 비판은 Isabelle/HOL에서 검증된 concrete model, nontriviality witness, no-collapse witness를 전제로 해야 합니다. 그 부분은 단순한 주장이나 비유가 아니라, 커널이 받아들인 formal proof의 층위에 속합니다.

car_nap · 6월 10, 2026, 11:49오후

Non-trivial 𝛿의 사례가 어떻게 가능한지 말씀을 쭉 들어도 이해가 잘 안 갑니다…. 적형식 집합을 구문상 동치로 분할하는 함수라면, 이미 identity로 분할이 되어 있으니 불필요하거나, 적형식이 애매하므로 결함 있는 언어입니다. ‘의미상 동치’로 분할하는 함수라면, 순수하게 메커니컬한 분할은 불가능하겠죠. 가령, 주어진 해석 없이 ∨()() ≡ ∧(¬())(¬())인지 어떻게 보증하나요. 그러면 그냥 의미 모형을 ‘한 겹 더’ 쌓는 게 됩니다. 하나의 가능성은 공리를 통해 이론 층위에서 해석을 제약하는 것인데, tonk 같은 잘 알려진 문제적 반례를 차치하고서라도, 그 경우 𝛿는 적형식을 메타 도메인에 사상하는 함수가 아니라 그냥 문장 집합이 되어버리고….

한편 어떤 전산 언어에서 무언가가 무결히 돌아간다는 것 자체는 별 의미가 없는 사항임을 남겨드립니다. 누가 이런 코드를 썼다고 해보죠:

Int a = 0;
Int b = a;
Int c = b;

If(a == b)
{
printf(“%d”, c)
};

돌아는 가겠습니다만, 저라면 그냥

printf(“0”)

라고 쓰길 권할 것 같습니다.

pascal · 6월 10, 2026, 11:55오후

여기서는 일반 프로그램이 “돌아간다”는 것과 Isabelle/HOL에서 정리와 witness가 검증된다는 것을 구별해야 할 것 같습니다.

Isabelle/HOL에서 통과됐다는 건

“코드가 돌아갔다”가 아니라
“정의된 형식 구조 안에서 정리들이 커널의 추론 규칙으로 증명됐다”는 뜻입니다.

Isabelle/HOL에서 MM이 보이는 것은 단순히 어떤 코드가 실행된다는 것이 아니라, 정의된 형식 구조 안에서 concrete model이 존재하고, 그 모델이 locale 조건들을 만족하며, nontrivial truth-condition witness와 no-collapse witness를 갖는다는 점입니다. 즉 구조가 공허하지 않고, 모든 것이 하나로 붕괴하지 않으며, 가능성과 필연성이 collapse하지 않음을 형식적으로 확인한 것입니다.

또한 δ가 어떤 모델에서 단순하게 구현될 수 있다는 것은 δ가 불필요하다는 뜻이 아닙니다. MM의 핵심은 δ가 항상 복잡해야 한다는 것이 아니라, valuation assignment가 formula → syntactic distinction → interpreted truth-condition으로 factorize될 수 있다는 점입니다. 가장 단순한 concrete model에서도 이 factorization이 작동한다는 것은 오히려 구조의 비공허성을 보여주는 witness입니다.

따라서 이 작업을 일반 프로그래밍 코드가 무언가를 출력하는 것에 비유하는 것은 적절하지 않다고 생각합니다. MM의 요지는 실행 결과가 아니라, Isabelle/HOL 커널이 받아들인 정의·정리·모델·witness를 통해 valuation factorization이 비공허하고 비자명하며 modal collapse를 피한다는 것을 보이는 데 있습니다.

car_nap · 6월 11, 2026, 12:06오전

wff가 이미 구문론적 중의성이 없다면 왜 이른바 ‘팩토라이즈’되어야 하는지 의아하다는 말씀입니다. 아시듯이 모든 현대 형식 언어는 원자 표현과 조합 원리로부터 모든 wff를 귀납적으로 정의합니다. 그리고 그 조합 방식을 구문적으로 투명하게 제시합니다. 그 덕에 구문적 비애매성이 확보되는 것이고요. 그렇다면… 그걸 왜 다시 ‘인수분해’해야하는 건가요? 우리가 수 표기에 있어 소수들만 사용하는 사회라고 생각해 보세요. 그 사회에서 왜 또 다른 소인수분해법을 발명해야 하는 건가요? 그래서 자꾸 𝛿가 불필요한 래퍼같이 보인다는 말씀인 겁니다. 또는, 𝛿가 필요한 특수한 언어가 있다면 그건 그 언어의 아키텍쳐 문제라는 거구요. 이미 우리의 표준적 언어들은 ‘객체지향’적인데, 왜 또다른 번역기가 필요한지 잘 이해가안됩니다….

pascal · 6월 11, 2026, 12:31오전

MM은 “새로운 소인수분해법”을 발명하려는 작업이 아닙니다. 오히려 이미 사용되고 있는 표기와 계산이 어떤 구조를 전제하는지를 명시하는 작업에 가까워요.

예컨대 어떤 사회가 소수들만 사용한다고 하더라도, 그 사회가 실제로 수를 어떻게 구별하고, 어떤 규칙에 따라 계산하며, 어떤 구조를 전제하는지는 여전히 분석될 수 있습니다. 그 분석은 “새로운 소수 표기법”이나 “또 다른 소인수분해법”을 만드는 것이 아니라, 이미 작동하는 체계의 내부 조건을 드러내는 일입니다.

마찬가지로 MM도 새로운 wff 생성법이나 새로운 문법 파서를 제안하는 것이 아닙니다. 현대 형식언어가 wff를 귀납적으로 정의한다는 점은 그대로 받아들이지만 MM이 묻는 것은 그 다음 층위입니다. 이미 well-formed인 formula가 어떤 syntactic distinction으로 잡히고, 그 distinction이 어떤 interpretive determination을 통해 possible-worlds truth-condition이 되는가입니다.

따라서 δ는 “새로운 소인수분해법” 같은 것이 아닙니다. δ는 formula가 만들어내는 구별을 명시하고, I는 그 구별을 truth-condition으로 해석합니다. 즉 MM의 핵심은 새 문법이나 새 의미론을 발명하는 것이 아니라, 기존 PWS나 Kripke semantics에서 primitive하게 주어지는 valuation assignment가 어떤 구별-해석 구조로 factorize될 수 있는지를 보이는 것입니다.

그러므로 “이미 wff가 잘 정의되어 있는데 왜 δ가 필요한가?”라는 질문은, MM을 문법 체계의 대체물로 볼 때만 성립한다고 생각합니다. 하지만 MM은 wff를 다시 정의하려는 것이 아니라, wff와 truth-condition 사이의 metasemantic relation을 분석하려는 작업입니다. 그래서 semantics가 아니라 metasemantics인 거구요.

제가 말하려는 지점은 단순히 “필연과 우연이 구분 가능하다”는 사실에 있지 않습니다. 그것은 표준 양상 의미론에서도 얼마든지 약속할 수 있습니다. 예컨대 어떤 공식은 모든 가능세계에서 참이면 필연이고, 어떤 가능세계에서만 참이면 우연이라고 정의할 수 있습니다.

하지만 MM의 관심은 그 약속 자체가 아니라, 그런 구분이 어떻게 가능해지는가입니다. 즉 어떤 formula가 왜 특정한 truth-condition을 갖게 되고, 그 truth-condition을 통해 어떻게 필연/우연의 구분이 성립하는지를 묻는 것입니다. 본 연구는 바로 그 가능성의 토대가 되는 층위를 분석하는 데 있는 거에요.

MM은 formula가 syntactic distinction으로 잡히고, 그 distinction이 interpretive determination을 통해 possible-worlds truth-condition으로 해석될 때, 비로소 필연과 우연의 modal evaluation이 가능해진다는 점을 보이려는 작업입니다.

말하자면 MM은 “필연과 우연을 이렇게 부르자”에서 끝나는 작업이 아니라, “필연과 우연의 구분이 성립하려면 formula와 truth-condition 사이에 어떤 해석적 구조가 있어야 하는가”를 논하는 작업입니다.

그리고 Isabelle/HOL에서의 결과는 바로 이 기반적 분석이 단순한 말의 재배열이 아니라는 점을 보여줍니다. 즉 이 factorization 구조가 공허하지 않고, 비자명하며, modal collapse로 붕괴하지 않는다는 것을 concrete model, nontrivial truth-condition witness, no-collapse witness를 통해 형식적으로 확인해 줍니다.

다시 말해, “우리는 이미 wff와 표준 양상 의미론을 잘 쓰고 있는데 도대체 이 구분이 왜 필요한가?”라는 질문에 대해, MM은 “bare syntax 자체만으로는 modal force가 생기지 않는다”는 점을 기계적으로 보여준 작업입니다. modal force는 단순히 formula가 well-formed라는 사실에서 나오는 것이 아니라, 그 formula가 syntactic distinction으로 잡히고, 그 distinction이 interpretive determination을 통해 possible-worlds truth-condition으로 해석될 때 성립합니다.

따라서 Isabelle/HOL 결과는 이 구분이 단순한 철학적 장식이 아니라, 비공허하고 비자명하며 collapse하지 않는 형식 구조로 실제 작동한다는 점을 기계적으로 확인해 줍니다.

요약하자면, 질문은 이렇게 정리될 수 있겠습니다.

“철학자들이 힘들게 블랙박스로 넣어둔 걸 왜 다시 여는가?”

MM의 답은 이겁니다.

“그 블랙박스 안에 바로 modal force의 조건이 있기 때문이다.“

car_nap · 6월 11, 2026, 8:26오전

라는 말씀은 뭔가 제 말이 오해되고 있는 듯한 인상을 주네요. 철학적 논리학에서 원초 개념들을 블랙박스로 넘겨버리는 건, 가령 ‘문장의 의미 동일성 확보 기능을 하는 그것을, 그것이 무엇이건—추상적 존재자이건, 세계 집합이건, 심상이건—명제라고 부르자’라고 하거나 ‘문장의 평가 파라메터 기능을 하는 그것을, 그것이 무엇이건—구체적 전체이건, 명제 집합이건, 바나나이건—가능 세계라고 부르자’라고 하는 건, 다른 이유가 있어서 “힘들게” 해놓은 게 아닙니다. 그걸 열어서 ‘진짜 정체’를 알아내는 게 힘든 작업이죠. 어쩌면 단지 말싸움에 불과해지는 문제일지도 모르는 희망 없는 작업이고요. (그걸 우리는 형이상학이라고 부르곤 합니다만)

다만 몇 번 다시 읽으면서 ‘syntactic distinction’이라고 부르시는 것의 정체가 살짝 더 파악되긴 했습니다. 관해서 잠시 잡설(?)좀 붙이고 돌아오겠습니다.

선생님은 아마도 현대 언어철학자들이 ‘초내포’라고 부르는 것 중 일부분을 해당 용어로 표현하고 있으신 것 같습니다. 특정 타입 t에 대해 세계 w ∈ W에 상대적인 해당 타입 도메인을 Dt(w)라고 부르면, t 타입 표현 집합 Et을 Dt(w)에 매핑하는 함수를 ‘지칭’이라고 부릅니다. 지칭의 함숫값은 표현의 외연입니다. 한편, 여기에서 ‘w’를 변항으로 만들어서, Et를 {Dt(w): w∈W}에 사상하는 함수는 ‘의미’라고 일컬어지고 이때의 함숫값을 표현의 내포라고 부릅니다. 그런데 이 세팅은 암묵적으로 특정 표현이 특정 의미를 갖는다고 가정하는데, 체계를 확장해 우리는 ‘의미 결정 함수’가 정의 가능하도록 만들 수 있습니다. 이를 철학자들은 메타의미론이라고 불러왔고요.

이러한 확장에서 상응하는 함수는… 딱히 통일된 이름을 갖지는 않는 듯합니다. 목적에 따라 ‘규약’, ‘본질’, ‘지시 고정’ 따위로 불립니다. 편하게 ‘정의’라고 뭉뚱그려 부르겠습니다. 이 경우, 정의의 함숫값은 유관한 파라메터와 해당 파라메터가 적용되는 경우에 해당하는 내포의 순서쌍들을 멤버로 갖는 집합이 될 겁니다. 그런 집합을 우리는 초내포라고 불러봄 직합니다. 선생님의 구문론적 구별이라는 건, 바로 이 초내포에 해당하는 것으로 지금 봐서는 파악이 됩니다.

그런데 초내포를 위한 형식체계의 구성은 좀 까다로운 성격을 갖습니다. 가령 Kit Fine의 야심찬 grounding semantics가 보여주듯, 방대하고 우아하며 강력한 형식체계를 잘 작동하게 구성하는 건 일단 가능합니다. 문제는 그 다음 단계입니다. 만약 초내포가 표현으로 하여금 단일한 내포를 확정적으로 제공한다면, 굳이 정의니 초내포니 하는 걸 다룰 필요가 없습니다. 초내포의 형식은 {intension}에 불과할 테고, 따라서 정의란 내포에 래퍼 하나 씌워주는 작업에 다름 없게 됩니다. 이 문제를 해결하는 것이 급선무이겠다 싶습니다.

별개로, 여러번 말씀드립니다만 ‘형식 언어’를 대상으로 이런 종류의 작업을 하는 것이 아주 진지한 작업으로 평가되기는 어려울 겁니다. 역시나 누차 말씀드렸듯, 형식 언어의 적형식들은 원초 기호들로부터 귀납적으로 구성되고, 그 결과물에는 애매성이 존재하지 않습니다. 원초 기호의 의미는 구문론 측면에서는 공리와 추론 규칙을 사용해, 의미론 측면에서는 구문론적 의미를 반영하는 순수하게 외연적인 방식으로 규정됩니다. ‘구문론과 외연 사이의 틈’이랄 것 자체가 없는 셈입니다. 수학자들이 내포 의미론을 굳이 공부하지 않는 것도 그런 탓이겠고요. 그러니 생각기로는 방향을 전환해 자연 언어를 대상으로 한 체계를 구상하시는 게 낫겠다 싶습니다.

pascal · 6월 11, 2026, 11:11오전

잘 읽었습니다. 이번 답변은 처음보다 훨씬 논점이 분명해졌고, 제가 말하려는 지점과 선생님의 문제의식이 어디서 갈라지는지도 더 선명해진 것 같습니다. 다만 여전히 몇 가지 중요한 오해가 남아 있다고 생각합니다.

먼저, 제가 말한 “블랙박스”라는 표현은 선생님께서 앞서 말씀하신 “철학자들이 단순화하려 애쓴 지점을 다시 펼쳐놔버리는 꼴”이라는 지적을 받아 정리한 비유였습니다. 즉 제가 말하려던 것은 철학자들이 게을러서 무엇인가를 감춰두었다는 뜻이 아닙니다. 오히려 표준 의미론이 의도적으로 추상화한 지점, 즉 valuation assignment를 primitive하게 두고 논의를 진행하는 그 지점을 가리킨 것입니다.

저는 그 추상화 자체가 잘못되었다고 말하는 것이 아닙니다. Kripke semantics나 PWS가 훌륭하고 강력한 체계라는 점은 당연히 인정합니다. 문제는 그것들이 무엇을 설명하고 무엇을 남겨두는가입니다.

표준 PWS는 다음을 아주 잘 설명합니다.

어떤 formula가 어떤 world에서 참인가.
어떤 formula가 모든 accessible world에서 참이면 necessary인가.
어떤 formula가 어떤 accessible world에서 참이면 possible인가.

하지만 MM이 묻는 것은 그보다 한 층 아래입니다.

그 formula는 어떻게 possible-worlds truth-condition을 갖게 되었는가?
bare syntax가 어떻게 modal evaluation의 대상이 되는가?
valuation assignment가 primitive하게 주어진다고 할 때, 그 내부에는 어떤 구별-해석 구조가 전제되는가?

따라서 “블랙박스를 왜 여는가?”에 대한 제 답은 여전히 같습니다.

그 블랙박스 안에 바로 modal force의 조건이 있기 때문입니다.

그리고 이 말은 단순한 수사적 표현이 아닙니다. 이것은 MM에서 bare syntax alone으로부터 modal force가 곧장 나오지 않는다는 점, 즉 modal evaluation이 interpreted distinction을 필요로 한다는 점을 Isabelle/HOL 안에서 형식적으로 정리화한 결과에 근거합니다. 선생님께서 오해하시는 것처럼, Isabelle에서 검증되었다는 말은 일반 프로그램이 한 번 구동되었다는 뜻이 아닙니다. 일반 프로그램의 실행은 입력에 대한 출력일 뿐이지만, Isabelle/HOL에서의 통과는 명시된 정의와 가정 아래에서 특정 명제가 proof kernel의 검사를 통과해 theorem으로 성립했다는 뜻입니다. 다시 말해 그것은 단순 실행 결과가 아니라, 해당 형식체계 안에서 수학적 증명으로 확정된 결과입니다.

여기서 제가 말하는 modal force는 단순히 □와 ◇ 기호를 붙이는 문법적 효과가 아닙니다. 어떤 formula가 필연적이거나 가능하거나 우연적이라고 평가되려면, 그 formula는 먼저 possible-worlds truth-condition을 가져야 합니다. MM은 바로 그 truth-condition이 bare syntax에서 곧장 나오는 것이 아니라, formula가 syntactic distinction으로 잡히고, 그 distinction이 interpretive determination을 통해 truth-condition으로 해석될 때 성립한다는 점을 분석합니다.

이 점에서 선생님께서 제시하신 superintension 해석은 흥미롭지만, 제 작업을 정확히 겨냥하지는 못한다고 생각합니다.

선생님께서는 제가 말하는 syntactic distinction을 초내포 또는 superintension에 가까운 것으로 읽으셨습니다. 그러나 MM에서 D는 의미, 명제, 내포, 초내포 그 자체가 아닙니다. D는 syntactic distinction의 층위입니다. 다시 말해 D는 아직 truth-condition이 아닙니다. truth-condition은 I를 거친 뒤에야 생깁니다.

MM의 구조는 다음과 같습니다.

formula → δ → syntactic distinction → I → possible-worlds truth-condition

따라서 D를 곧장 superintension으로 읽으면, I의 역할이 사라지거나 흐려집니다. 하지만 MM의 핵심은 바로 D와 I의 분리입니다. 제가 하려는 일은 “명제”나 “초내포”라는 또 다른 의미 엔터티를 하나 더 세우는 것이 아닙니다. 오히려 기존 valuation assignment가 어떤 식으로 syntactic distinction과 interpretive determination으로 factorize될 수 있는지를 보이는 것입니다.

이 차이가 중요합니다.

만약 D가 이미 의미라면, 선생님의 말씀처럼 “내포에 wrapper 하나 씌운 것”이라는 비판이 가능할 수 있습니다. 그러나 MM에서 D는 의미가 아닙니다. D는 formula가 만들어내는 구별의 형식적 자리이고, I가 그 구별을 possible-worlds truth-condition으로 해석합니다. 그러므로 MM은 “내포에 래퍼를 씌우는 이론”이 아니라, formula와 truth-condition 사이의 해석적 매개 구조를 분리해내는 이론입니다.

또 하나 중요한 지점은 형식언어에 관한 선생님의 주장입니다. 선생님께서는 형식언어의 적형식들은 원초 기호들로부터 귀납적으로 구성되고 애매성이 없으므로, “구문론과 외연 사이의 틈”이랄 것이 없다고 말씀하셨습니다. 저는 이 부분이 가장 결정적인 오해라고 봅니다.

형식언어에서 wff가 애매하지 않다는 것은 맞습니다. 그러나 그것은 구문론적 well-formedness가 명확하다는 뜻이지, 그 wff가 어떤 possible-worlds truth-condition을 갖는지가 자동으로 주어진다는 뜻은 아닙니다.

wff의 명확성과 truth-condition의 결정은 다른 문제입니다.

예컨대 어떤 formula가 well-formed라는 사실은 그 formula가 문법적으로 허용된다는 뜻입니다. 그러나 그 formula가 어느 세계에서 참이고 어느 세계에서 거짓인지는 valuation 또는 interpretation을 통해 주어져야 합니다. 표준 의미론도 바로 이 때문에 valuation function이나 interpretation function을 둡니다. 즉 형식언어라고 해서 syntax와 truth-condition 사이의 관계가 사라지는 것이 아닙니다. 오히려 그 관계가 명시적으로 주어지기 때문에 형식화가 가능한 것입니다.

따라서 “형식언어에는 애매성이 없으니 이런 작업은 진지하지 않다”는 비판은 MM을 자연언어의 애매성 해결 이론으로 오해한 데서 나온 것이라고 생각합니다. 형식언어라서 구문론과 외연 사이의 틈이 사라지는 것이 아닙니다. 오히려 형식언어이기 때문에 자연언어의 문법적 애매성을 제거한 상태에서도, well-formed formula가 possible-world truth-condition으로 해석되기 위해 필요한 더 근본적인 metasemantic 층위를 분명히 볼 수 있습니다.

다시 말해, 형식언어는 MM의 약점이 아니라 장점입니다.

자연언어에서 시작하면 애매성, 맥락의존성, 지시 실패, 화용론적 효과가 너무 많이 끼어듭니다. 반대로 형식언어에서 시작하면 문제의 핵심이 더 선명하게 드러납니다. wff는 이미 명확합니다. 바로 그렇기 때문에 다음 질문이 더 순수하게 제기됩니다.

이미 well-formed인 formula가 어떻게 possible-worlds truth-condition을 갖는가?
그 truth-condition 위에서 modal evaluation은 어떻게 성립하는가?
bare syntax만으로는 왜 modal force가 생기지 않는가?

MM은 바로 이 질문을 다룹니다.

현대 논리학, 의미론, proof theory, type theory, formal epistemology, formal ontology가 모두 형식언어를 대상으로 시작합니다. 형식언어를 대상으로 한다는 이유만으로 작업이 덜 진지해지는 것은 아닙니다. 오히려 그 반대입니다. 형식언어는 개념적 혼탁함을 줄이고, 정확히 어떤 정의에서 어떤 결론이 나오는지 검증할 수 있게 해줍니다.

특히 제 작업은 단순히 “이런 철학적 해석이 가능하다”고 말하는 데서 끝나지 않습니다. Isabelle/HOL 안에서 concrete model을 제시하고, nontrivial truth-condition witness를 보이며, no-collapse witness를 확인합니다. 즉 factorization 구조가 공허하지 않고, 비자명하며, modal collapse로 붕괴하지 않는다는 점을 형식적으로 확인합니다.

형식언어를 대상으로 하기 때문에 theorem, model, witness, consistency, non-collapse를 기계적으로 확인할 수 있는 것입니다.

선생님께서 말씀하신 Kit Fine의 grounding semantics나 superintensional semantics는 물론 중요한 비교 대상입니다. 다만 MM은 그 체계들과 경쟁하여 더 방대한 초내포 의미론을 만들려는 작업이 아닙니다. MM은 훨씬 제한된 목표를 갖습니다. 그것은 valuation assignment를 δ와 I로 factorize하고, modal evaluation이 bare syntax가 아니라 interpreted distinction 위에서 성립한다는 점을 보이는 것입니다.

따라서 MM의 기여는 “모든 의미론 문제를 해결한다”가 아닙니다. “모든 자연언어의 지시 실패를 해결한다”도 아닙니다. “초내포 의미론의 최종 이론을 제시한다”도 아닙니다.

MM의 기여는 더 좁고, 그만큼 더 명확합니다.

표준 양상 의미론이 primitive하게 두는 valuation assignment의 내부를 syntactic distinction과 interpretive truth-condition determination으로 분해할 수 있다.
이 구조는 형식적으로 정의 가능하다.
이 구조는 concrete model을 갖는다.
이 구조는 비공허하다.
이 구조는 비자명하다.
이 구조는 modal collapse로 붕괴하지 않는다.
따라서 modal force는 bare syntax alone의 성질이 아니라 interpreted distinction 위에서 성립한다.

이것이 MM의 핵심입니다.

그러므로 선생님의 비판은 두 층위를 계속 섞고 있다고 봅니다.

하나는 wff의 구문론적 명확성입니다.
다른 하나는 wff가 possible-worlds truth-condition을 갖게 되는 해석적 조건입니다.

MM은 전자를 부정하지 않습니다. 오히려 전자를 출발점으로 삼습니다. MM이 묻는 것은 후자입니다.

다시 말해,

“이미 wff가 명확하다”는 것은 MM에 대한 반론이 아닙니다.
“표준 PWS가 valuation을 둔다”는 것도 MM에 대한 반론이 아닙니다.
“철학자들이 명제나 가능세계를 primitive하게 둘 수 있다”는 것도 MM에 대한 반론이 아닙니다.

왜냐하면 MM은 바로 그 primitive하게 주어진 valuation assignment가 어떤 metasemantic 구조를 가질 수 있는지를 분석하기 때문입니다.

정리하면, 선생님의 지적은 흥미롭고 superintension/metasemantics 쪽 비교는 유익합니다. 그러나 MM을 초내포 이론, 명제 이론, 자연언어 의미론, 또는 wff 생성 체계로 읽으면 핵심을 놓치게 됩니다. MM은 그런 작업이 아니라, valuation assignment의 내부 조건을 형식화한 mechanized metasemantics입니다.

그래서 제 입장은 다음과 같습니다.

형식언어에서 wff가 명확하다는 점은 MM을 불필요하게 만들지 않습니다. 오히려 바로 그 명확한 wff가 어떻게 truth-condition을 갖고 modal force의 대상이 되는지를 묻는 것이 MM입니다.

PWS가 valuation을 primitive하게 둘 수 있다는 점도 MM을 불필요하게 만들지 않습니다. 오히려 바로 그 primitive valuation의 내부 조건을 여는 것이 MM입니다.

D를 superintension으로 읽는 것도 MM을 정확히 포착하지 못합니다. D는 의미 자체가 아니라 syntactic distinction이고, truth-condition은 I를 통해서만 주어집니다.

마지막으로 덧붙이자면, 짧은 시간 안에 제 Isabelle/HOL 코드의 정의·locale·model·witness·theorem 구조까지 모두 검토하셨는지는 모르겠습니다. 다만 본 논의를 온전히 파악하시기 위해서는 제 Isabelle/HOL 코드를 정식으로 검토하시는 것이 필요하다고 생각합니다. MM은 단순히 서론이나 요약에서 제시된 철학적 아이디어만으로 완전히 평가될 수 있는 작업이 아닙니다. AFP 엔트리에서 Isabelle theory file은 부록이 아니라 작업의 본문에 해당합니다. AFP가 단순 업로드 저장소가 아니라, Isabelle/HOL에서의 빌드와 편집·검토 절차를 거쳐 게재되는 국제 formal proof archive인 것도 바로 이 때문입니다. 핵심은 실제 코드 안에서 δ, D, I, V가 어떻게 정의되고, concrete model이 어떻게 locale 조건을 만족하며, nontrivial truth-condition witness와 no-collapse witness가 어떻게 성립하는지에 있습니다.

따라서 MM의 논지는 “V = I ∘ δ라는 말을 제안했다”는 수준에 있는 것이 아니라, 그 factorization 구조가 Isabelle/HOL 안에서 비공허하고, 비자명하며, modal collapse로 붕괴하지 않는 형식 구조로 실제 작동한다는 데 있습니다. MM은 철학적 주장인 동시에 formal artifact이므로, 코드의 정리 구조를 검토하지 않은 상태에서 이를 단순한 의미론적 재기술이나 wrapper로 평가하는 것은 mechanized metasemantics로서의 핵심 층위를 놓치는 판단이라고 생각합니다.