Modal set theory

요약문
1

요즘 개인적으로 공부하는 수리철학의 영역입니다.
오슬로 대학의 Davide Sutto가 쓴 "on modal set theory. three routes to the iterative conception(2022)"이란 문헌인데, 집합론에 대한 문제의식을 전체적으로 조망하고, 그러한 문제의식이 어떻게 zf집합론을 양상 집합론으로 변환하는지를 철학적으로 개괄하면서도, 형식적으로도 체계화 하고 있는 문헌입니다.

처음에 이 주제를 접하게 된 건 괴델 신 존재론적 증명을 살펴보다 우연히 발견한 건데, 괴델은 이 논의의 방향과는 정반대로 양상언어를 통해 구성한 존재론적 증명의 대상이 ultra-filter이라는 수학 개념으로 간주될 수 있다고 한 바가 있습니다. 양상체계를 집합론으로의 변환을 간접적으로나마 시도한 것인데,

어쨋든 이걸 알아보다 양상 집합론이란 키워드를 검색해 우연히 본건데, 관심의 동기는 집합론을 양상 언어로 변환하여 그 공리를 유지한 채 온전히 변환 가능하다는 논의로만 러프하게 접해서, 수학적 공리에 양상 언어에 대한 의미론을 부여하면, 집합론의 공리나 정리를 양상 언어를 사용하는 논증에 적용할 수 있지 않을까? 그렇다면 집합론에 어떠한 양상성을 가진 체계가 가능하며, 이것이 좀 더 일상언어에 가까운 논증을 표현하는 도구로 쓸 수 있는가 하는 궁금증이 그 동기가 되었습니다. 물론 이 책에서 이 분야의 선구자 격인 린네보는 양상 집합론의 도메인에는 수학적 대상만이 가능하다고 보는 것 같다는 입장이 짤막하게 나와서 아쉽긴 했지만요.

어쨋든 혼자서 공부하고 있는 입장이라, 그리고 생소한 분야라 공부가 더디긴한데, 관심있는 사람이 더 있으면 좋지 않을까 싶어 조금씩 직역문에 가까운 요약 정리문을 가끔씩 적으려 하는데, 혹시 같이 공부하실 분 계시다면, 언제든 쪽지로 연락 주시면 감사하겠습니다.(혼자 공부하니 너무 외롭습니다ㅋㅋ)

양상 집합론은 집합론에서 러셀과 서수에 관한 Burali-Forti 역설, 즉 전체 집합이라는 proper class의 존재로부터 야기된 논의이다.

해당 역설들은 집합론을 구성하는 적합한 체계에 대한 고민보다 더 초등적인 질문인 집합이 될 수 있는 것은 무엇인가에 대한 질문을 발생시키는데, 이에 대한 논의들은 칸토어, Boolos Parsons, Hao Wang등의 학자들에게서 볼 수 있다.

그들은 이러한 질문에 대한 접근법으로 다소 묘사적인narrative 접근법을 채택하는데, 이는 어떻게 집합 형성 과정이 진행되는가에 관해 우리의 직관을 잘 설명한다.

집합의 형성에 대한 네러티브한 서술이 어떻게 집합론의 공리를 잘 설명하면서도, 집합을 형성하는 것에 대한 우리의 직관을 해치지 않을 수 있는가에 대한 논의는 집합의 반복적 구상iterative conception of set으로 대표적으로 알려져 있다.

네러티브한 이론들 중에서 반복적 구상은 가장 유명한 것이며, 이것은 러셀의 역설에 대한 제르멜로의 응답인 랭크, 즉 유형론이 그 논의의 선조격이 된다. 그리고 이후 불로스로 이어진다.

불로스의 논의는 집합에 대한 반복적 구상을 포착하는 가장 훌륭한 방식으로 여전히 인정되며, 최근에는 오스틴 린네보가 plural logic과 양상 논리의 조합으로 이 구상을 형식화 하고, 이는 양상 집합론의 중요한 이정표가 된다.

린네보의 관점은 칸토어가 집합이 될 수 있는 존재와 없는 존재를 일관적 다수consistent multiplicity와 비일관적 다수로 구분하는 작업에 기반한다. 린네보는 집합에 대한 축적적 계층에 내재적으로 잠재적인 특성을 귀속하는 것으로 보인다.

이 문헌의 목표는 양상 집합론에 대한 현대적 논재의 상태를 다루는 것. 정확히 는 반복적 개념에 암묵적으로 내재된 양상적 특징을 일관적으로 추출해, 집합들의 '잠재적' 축적적 계층을 기반하는 새로운 구상을 진행하는 것이며, 여기에 세가지 선택지가 있다 : 린네보의 unimodal 접근법, Studd의 bimodal 접근법, Tim Button의 환원주의적 접근.
결과적으로 두 가지 질문들에 의해 인도된다 : "양상적 접근은 단지 비-양상적 이론의 표기적인 접근에 불과한가?", "만일 아니라면, 구분되는 특징은 무엇이며 무엇을 선택해야 하나?"

린네보와 Studd는 퍼트넘이 양상과 비-양상 사이 동치로 봤던 논제를 일축하기 위해 유발된 것이다. 더구나 앞선 두번째 질문에 관해 린네보의 접근은 Studd보다 더 본질적으로 이상적인 무게를 가지고, 양상 집합론의 내재적인 다원적 본성을 포함한다는 점에서 더 특권적이다. 그러나 린네보는 bimodal접근에서 나타나는 필연성과 단점들로부터 자유롭지 않다. 그리고 이러한 업무를 달성하는 최선의 선택지는 Button에 의해 개괄되는 양상-집합론을 배제하길 원하는 잠재주의적 설명에 의해 개별화 된다. 본 문헌은 다음에 따른다

ch.0. 현대적인 양상적 접근의 전제가 되는 학제들에 대한 역사를 수집
ch.0.1 : 초기 관점

  • 칸토어의 일관적 다수와 비일관적 다수의 정의를 통한 집합 형성의 과정에 대한 그의 관점
  • 초기 제르멜로의 공리적 집합론과 그가 제시한 축적적 계층에 대한 모델
    ch0.2. 반복적 구상에 대한 출발점
  • 불로스의 형식화의 원형과 개념의 철학적 논의
  • Parsons의 집합과 양상성에 대한 연구, 이것에서 나타나는 잠재적인 조직화
  • 더밋의 무한정한 확장성indefinite extensibility에 대한 해석
  • Yablo의 소박한 comprehension principle에 대한 이해

ch.1. 린네보에 대한 작업을 제시

  • 어떻게 복수적, 양상적 도구를 사용해 반복적 구상을 조직하는가에 대한 비형식적인 설명을 제공한다
  • 형식화에 대한 조직화 : 양상적 접근을 통해 ZF집합론을 제시하기 위해 공리와 더 근본적인 정리들을 제시
  • 린네보의 이론에 대한 효용에 대한 분석

ch.2. Studd의 bimodal 접근에 대한 포괄적인 해명을 제공

  • 형식적인 관점으로부터 이론의 핵심을 제시
  • 철학적인 접근에 대한 집중, 이는 초기 형식화 이후에 발생한 주요한 변화들을 지적할 것
  • 비용 효율적인 분석을 통해 이러한 접근의 장단을 조명

ch.3. Tim Button의 환원주의적 이론

  • level theroy의 핵심을 제시, 이것은 그의 비-양상적 제안이며, 어떻게 이것이 블로스와 Scott이 제시한 원래의 접근들로부터 발전되는지를 보임이면서 제시할 것
  • Button 그 자신이 제시한 양상적 접근을 제시, 이는 퍼트넘의 동치 논증을 통해 상대화 하는 것에 이용된다
  • 비용효율적인 분석

ch.4. 세가지 개괄된 제안들의 양립가능성에 대한 고찰

  • 양상적, 비-양상적 집합론에 대한 궁극적인 비-환원성에 대한 접근. 이는 각 입장들의 차이점을 수집하는 것을 기반으로 한다. 이는 세가지 설명들이 공유하는 결과에 의한 형식적 단계에서 예화될 수도 있다
  • Studd의 비판. 즉 이념적인 비용과 절대적인 일반성에 대한 비판으로부터 린네보를 옹호하는 식으로 변호를 할 것이다.
5개의 좋아요
2

전 고등학교 시절부터 수리철학에 관심은 있었는데 수학을 잘 하지는 못합니다. 근데 최근에 무한소 증명과 관련해서 abraham robinson에 대해 위키에서 어제 잠깐 알아봤는데, 말씀하신 ultra-filter가 hyper-real number system과 연관된 그 ultra-filter일까요?

3

synthese 같은 저널에도 보면 수리 논리학 기호로 범벅이 된 논문이 너무 많더군요. 이런데 받아들여지려면 아무래도 수리 논리학에 해박해야 한 것 같습니다. 한 콜로라도 대학교 교수 홈피에 들어가면 다음과 같은 말이 있습니다.
7. Be technical, rigorous, and confusing

Referees look for reasons to reject a paper, not reasons to accept. And because they are confused, their reasons for rejection are often of the form, “I think this paper is wrong because X.” To avoid rejection, you want to write something where it is hard for the referee to say it is wrong. If it features technical arguments, especially mathematical or formal logical manipulations, it should be impossible for the referee to claim you are wrong in those parts (assuming the technical arguments are in fact technically correct).

I have, however, relied on mathematical and formal logical arguments. The first paper I got into Phil Review featured a fair amount of formal logical manipulations. The paper I got into J Phil featured a bunch of probability theory, including proofs of two probabilistic theorems in the appendices. I think the technical nature of these papers helped make it possible to get them into top journals.

Publishing in Philosophy

4

저도 수학은 잘몰라서 초-실수 체계라는건 첨들어보지만, 집합론에서 쓰이는 filter의 개념이 따로 있습니다. 집합간 위계나 순서에 대한 연구에 주로 다뤄지는 것 같던데,

괴델이 신 존재증명에서 속성을 다루기 위해 속성에 대한 술어인 positive개념을 상정한 것이 filter의 작동방식이나 양상이 유사해 보여서 그리 주장한 것 같아요.

5

린 커뮤니티에서 카일 밀러(Kyle Miller) 박사 후 연구원님이 쓴 댓글이 떠오르네요. 아래의 코드에서, P는 긍정적 속성의 집합이자, '긍정적 속성임'이라는 메타속성입니다. 그리고 G는 신적 존재의 집합이자, '신적임'이라는 속성입니다. 이분이 형식화하신, 괴델의 신 존재 증명은 양상 논리를 바탕으로 하지 않았어요.

Kyle Miller said:

@Matt Diamond That's fun. I've switched it over to the language of sets. There, it's sort of like that P has most of the axioms of an ultrafilter. axiom_2 is "upwards closed", axiom_3 is "nonempty", and axiom_1 is the ultrafilter property. What's missing is that pairwise intersections of positive properties are still positive. Even without it, the point is that the ultrafilter property implies that the empty set can't be in it, since it contradicts upwards closure applied to nonemptiness. Hence the G set is nonempty.

import Mathlib

opaque individual : Type

abbrev property : Type := Set individual
abbrev metaproperty : Type := Set property

-- Positive
opaque P : metaproperty
-- God-like
opaque G : property

-- Either a property or its negation is positive, and not both
axiom axiom_1 : ∀ (ϕ : property), P ϕᶜ ↔ ¬P ϕ

-- A property entailed by a positive property is positive
axiom axiom_2 : ∀ ϕ ψ, ϕ ⊆ ψ → P ϕ → P ψ

-- being God-like is a Positive property
axiom axiom_3 : P G

theorem univ_positive : P Set.univ :=
  axiom_2 G _ (Set.subset_univ _) axiom_3

theorem empty_property_not_positive : ¬P ∅ := by
  rw [← axiom_1, Set.compl_empty]
  exact univ_positive

theorem all_positive_properties_exemplified {ϕ : property} (hϕ : P ϕ) : ϕ.Nonempty := by
  by_contra! h
  cases h
  exact empty_property_not_positive hϕ

theorem god_exists : G.Nonempty := all_positive_properties_exemplified axiom_3
6

신적임에 대한 속성을 단순히 빨강임 속성과 같이 간주하는 것처럼 보이는데, 괴델의 논증은 '필연적으로 존재함NE' 속성과 본질 속성Ess를 정의하고 이 두 속성으로 '신적임' 속성을 정의하고 있습니다. 물론 이후, 괴델 논의 자체가 양상-붕괴라는 '참이면, 필연참'을 발생시키게 되는데, 양상-붕괴 현상이 발생하는게 또 코드로 짜여지면 합당한 논증인지는 궁금해지네요.

양상 논리를 바탕으로 하지 않은게 프로그레밍의 한계 때문인가요, 아니면 양상논리를 배제한 형식화가 목적이라 그런건가요?

7

린 증명 보조기로도 문제없이 양상 논리를 형식화할 수 있으므로, 양상 논리를 바탕으로 해서 괴델의 신 존재 증명을 형식화할지 말지는 그저 개인의 선호에 달려 있습니다. 아래의 저장소에 린 4로 형식화한 양상 논리가 있네요.

고차 양상 논리를 바탕으로 괴델의 신 존재 증명을 코크와 이저벨 증명 보조기로 형식화한 연구물도 있습니다.