2017년 2월 4일 (토) 16:29에 Maintenance script님의 편집

2017-02-04T16:29:03Z

새 문서

* 상위 항목: [[논리학]]
* 관련 항목: [[수학 관련 정보]], [[철학 관련 정보]], [[수리 논리학]]

[[한글]]: 양상 논리
[[한자]]: 樣相論理
[[영어]]: Modal Logic

[목차]

== 개요 ==
[[논리학#s-2.2.1|표준적인 논리학]]을 확장하여, '''가능성'''이나 '''필연성''', '''당위'''와 '''허용''' 같은 '''양상(''Modality'')'''을 표현하고자 하는 논리체계. 즉 양상 논리의 목표는 다음과 같은 명제들 간의 논리적 도출 관계를 체계화하는 것이다:

* "사람은 '''반드시''' 생물이다."
* "[[고틀로프 프레게]]는 수학자가 아니라 화가'''였을 수도 있다.'''"
* "굶는 사람이 있다면, 밥을 주는 것이 '''마땅하다'''."
* "사람은 '''필연적으로''' 죽는다. 따라서 사람은 죽는다."
* "태양계의 행성은 '''필연적으로''' 8개인 것은 아니다. 따라서 태양계의 행성이 8개가 아닌 것은 '''가능하다'''."

== 필요성 ==
양상논리는 일반적으로, 특히 현대에는 [[수리 논리학|1차 논리]]에 추가적인 공리 혹은 규칙을 추가하여 확장한 것으로 이해된다. 이때 추가되는 공리 혹은 규칙은 [[한국어]]에서 "필연적이다", "가능하다" 등에 대응하는 '''양상적 논리 연결사(modal logical connective)'''에 관한 것이다. 이때 새로운 규칙을 도입하는 까닭은 "필연적이다", "가능하다" 같은 표현이 있는 명제들의 논리적 추론을 1차 논리로는 표현할 수 없기 때문이다.

[[수리 논리학|1차 논리의 논리 연결사]](예시. 부정(￢), 조건(→))들은 '''진리함수적(truth-functional)'''이다. 즉 어떤 명제 p가 참인지 거짓인지 결정된다면, p에 논리적 연결사와 다른 명제들을 연결해서 얻은 새로운 명제가 참인지 거짓인지도 형식적으로 결정된다.
* 예시: "소크라테스는 사람이'''다'''"가 참이라고 하자. 그렇다면 "소크라테스는 사람이 '''아니다'''"는 반드시 거짓이다.

하지만 "필연적이다", "가능하다" 같은 표현에 해당하는 __양상적 논리 연결사는 진리함수적이지 않다__. 어떤 명제가 참인지 거짓인지 알 수 있다 한들, 그 명제에 양상적 논리 연결사가 붙었을 때는 새로운 명제가 참인지 거짓인지 알 수 없기 때문이다.
* 예시: "삼각형의 세 내각의 합은 180도다"와 "태양계의 행성은 8개다"는 모두 참이다. 그런데 "삼각형의 세 내각의 합은 180도인 것이 '''필연적이다'''"는 참인 반면, "태양계의 행성은 8개인 것이 '''필연적이다'''"는 거짓이다.

그러므로 "필연적이다", "가능하다", 그외에도 "-인 것이 마땅하다", "-인 것이 허용된다" 등을 비롯한 양상적 논리 연결사가 포홤된 명제들의 논리적 추론은 1차 논리의 추론규칙들에만 의지해서는 타당한 추론이 될 수 없으며, 별도의 규칙이 필요하다.

== 양상의 종류 ==
양상에는 여러 종류가 있으며, 양상 개념들도 그 양상의 종류에 따라 분류된다. 예를 들어 "필연적이다"와 "허용된다"는 둘다 양상 표현이지만, 같은 양상 종류에 속하지는 않는다. 그러므로 양상의 종류에 따라 그때 쓰이는 양상논리 체계도 구분된다. 양상 개념의 대표적인 예시들은 다음과 같다:

* '''진리(alethic) 양상 논리''': "필연적이다", "가능하다"처럼 가능성과 관련된 양상을 다루는 논리.
* '''인식(epistemic) 양상 논리''': "-를 안다"처럼 [[지식]]과 관련된 양상을 다루는 논리.
* '''당위(deontic) 양상 논리''': "마땅히 -해야한다", "-하는 것이 허용된다"처럼 [[당위]], [[도덕]] 등에 관련된 양상을 다루는 논리.
* '''시제(tense) 양상 논리''': "항상", "예전엔", "지금" 등 [[시간]], [[시제]]에 관련된 양상을 다루는 논리.

이처럼 양상의 종류는 제각기 다르지만, 형식적 측면에서 이들 양상 논리 각각은 서로 크게 다르지 않다.

== 명제 양상논리 ==
=== 문법과 기본적 뜻 풀이 ===
'''명제 양상논리(Propositional Modal Logic)''' 문법은 [[수리 논리학#s-3|표준 명제 논리]]의 문법에 두 양상 연산자 <math>\Box, \Diamond</math>에 관한 문법을 추가한 것이다. 이때 해당 연산자들의 의미를 해석하는 방식은 [[#s-3|그때 쓰이는 양상 개념]]에 따라 다르다.
||'''양상 문장들의 뜻'''
* "<math>\Box P</math>"의 의미
* '''진리 양상 논리''': "<math>P</math>가 필연적이다", "반드시 <math>P</math>다"
* 인식 논리: "<math>P</math>를 안다"[* 인식 논리에선 일반적으로 □보다는 <math>K</math>로 표시하는 경우가 더 잦다.]
* 당위 논리: "마땅히 <math>P</math>해야 한다."[* 당위 논리에선 일반적으로 □보다는 <math>O</math>로 표시하는 경우가 더 잦다.]
* "<math> \Diamond P</math>"의 의미
* '''진리 양상 논리''': "<math>P</math>가 가능하다", "<math>P</math>일 수도 있다"
* 당위 논리: "<math>P</math>하는 것이 허용된다."||
이때 <math> \Box, \Diamond </math>는 상호 정의 가능하다: "<math>\Box \phi</math>"는 "<math> \neg \Diamond \neg \phi</math>"와 동치이며, 반대로 "<math>\Diamond \phi</math>"는 "<math> \neg \Box \neg \phi</math>"와 동치이다. 즉 진리 양상 논리를 예로 들자면 __"P가 가능하다"는 "P가 아닌 것이 필연적이지 않다"와 동치이며, "P는 필연적이다"는 "P가 아닌 것이 불가능하다"와 동치__이다.

=== 증명 체계 ===
문법과 마찬가지로 양상논리의 추론 규칙 또한 [[수리 논리학#s-3.2|표준 논리의 추론 규칙]]에 새로운 추론 규칙 혹은 [[공리]]를 추가하여 확장시킨 것이다. 아래에선 편의상 [[힐베르트]] 공리계를 사용하여 추론 규칙을 설명하겠다[* [[수리 논리학#s-3.2|표준 논리의 추론 규칙]] 항목에서 사용하는 게르하르트 겐첸(Gerhard Gentzen)의 귀결 연산(sequent calculus) 방식과 다른 방식이다. 예를 들어 귀결 연산 방식에서는 공리가 등장하지 않는다. 힐베르트 공리계에 관해서는 [[https://en.wikipedia.org/wiki/Hilbert_system|해당 링크를 참조]]]

==== 추론 규칙 ====
양상논리 공리 체계에서는 다음 두 가지 추론 규칙이 쓰인다.
* '''전건 긍정(Modus Ponens)''': <math>\phi \to \psi, \phi \vdash \psi</math>
* '만약 명제 <math>\phi</math>와 명제 <math>\phi \to \psi</math>가 나오는 행이 있다면, 그 행들로부터 명제 <math>\psi</math>를 도출할 수 있다.'[* [[수리논리|표준 논리]] 및 [[삼단논법]]에서 등장하는 그거 맞다.]
* 예시. "철수가 학생이면, 철수는 사람이다", "철수는 학생이다" <math>\vdash</math> "철수는 사람이다"

* '''필연화(Necessitation)''': <math>\phi \vdash \Box \phi</math>
* '만약 명제 <math>\phi</math>가 나오는 행이 있다면, 그 행으로부터 명제 <math> \Box \phi</math>을 도출할 수 있다.'
* 단 이때 <math>\phi</math>는 그 자체가 공리이거나 공리(혹은 공리들)로부터 도출된 명제, 즉 '''정리(theorem)'''이어야 하며 공리가 아닌 임의의 전제로부터 도출된 명제여서는 안된다.
* 예시. (진리 양상 논리의 경우) "철수는 학생이거나 학생이 아니다" <math>\vdash</math> "철수는 학생이거나 학생이 아니라는 것은 필연적이다"

==== 공리체계'들' ====
앞에서 설명한 것처럼 양상논리 체계는 [[#s-3|여러 가지 양상 개념]]들을 두루 포괄한다. 따라서 어떤 양상 개념을 다루느냐에 [[공리]] 또한 달라진다. 그러므로 "양상 논리 체계"는 한 공리 체계만 가리키는게 아니라 여러 공리 체계들을 아우르는 말이다.

아래에 설명된 공리 체계들은 그중에서도 "정상(normal) 양상 논리 체계"라고 불리는 양상 논리 체계들 가운데 일부이며, [[21세기]] 현재에 주로 다뤄지는 양상 체계들이다.

===== 체계 K =====
양상 논리체계 K는 [[수리 논리학#s-3|표준 명제 논리]]의 힐베르트 공리들에 다음 공리틀이 더해진 것이다:

* '''공리틀 K''': <math>\Box(\phi \to \psi) \to (\Box \phi \to \Box \psi)</math>
* 예시: (진리 양상 논리) [[총각]]이면 [[독신]]인게 '''필연적이고''', 철수가 총각인 것이 '''필연적이라면''', 철수가 독신인 것은 '''필연적이다.'''

===== 체계 D =====
양상 논리체계 D는 [[#s-4.2.2.1|체계 K]]에 다음 공리틀이 더해진 것이다:
* '''공리틀 D''': <math>\Box \phi \to \Diamond \phi</math>
* 예시: (당위 논리) "어려운 사람을 돕는 것이 '''마땅하다면''', 어려운 사람을 도와도 '''된다.'''"

===== 체계 T =====
양상 논리체계 T는 [[#s-4.2.2.2|체계 D]]에 다음 공리틀이 더해진 것이다:
* '''공리틀 T'': <math>\Box \phi \to \phi</math>
* 예시: (진리 양상 논리) "[[물|H,,2,,O]]가 [[산소]]인 것이 '''필연적이라면''', [[물|H,,2,,O]]은 '''실제로''' [[산소]]다."

공리틀 T는 당위 논리에 포함되선 안된다고 여겨지는게 일반적이다. 공리틀 T가 당위 논리에 적용된다고 해보자. 그렇다면 경우 다음과 같은 공리가 도출된다.
* "친구들은 항상 서로 사이좋게 지내는 것이 '''마땅하다면''', 친구들은 '''실제로''' 항상 사이좋게 지낸다"
이게 참된 진술이라면 세상은 참 [[평화]]롭겠지만 안타깝게도 이는 명백히 거짓인 것 같다. 따라서 공리틀 B는 당위 논리에 적용될 수 없다고 받아들여진다.

===== 체계 B =====
양상 논리체계 B는 [[#s-4.2.2.3|체계 T]]에 다음 공리틀이 더해진 것이다:
* '''공리틀 B'': <math>\Diamond \Box \phi \to \phi</math>
* 예시: (진리 양상 논리) "[[물|H,,2,,O]]가 [[산소]]인 것이 '''필연적인게 가능하다면''', [[물|H,,2,,O]]은 '''실제로''' [[산소]]다."

===== 체계 S4 =====
양상 논리체계 S4는 [[#s-4.2.2.3|체계 T]]에 다음 공리틀이 더해진 것이다:
* '''공리틀 S4''': <math>\Box \phi \to \Box \Box \phi</math>
* 예시: (진리 양상 논리) "[[물|H,,2,,O]]가 [[산소]]인 것이 '''필연적이라면''', [[물|H,,2,,O]]은 [[산소]]라는게 '''필연적이라는 것은 필연적이다'''."

공리틀 S4는 인식 논리에선서 흔히 "KK 논제"라고 불리며, 공리틀 S4가 인식 논리에 적용되는지 여부는 [[인식론]]의 오래된 떡밥 중 하나다. 왜냐면 S4를 받아들이냐 마냐에 따라서 '[[지식]]' 개념 범위가 달라지는 것 같기 때문이다.
* 예시: "눈 앞에 먹이가 있다는 것을 '''알면''', 눈 앞에 먹이가 있다는 것을 '''안다는 것을 안다'''."

[[사람]]쯤 되는 인지 능력이 뛰어난 [[동물]]의 경우 눈 앞에 음식이 있다는 걸 알게 되면 '눈 앞에 음식이 있다!'는 것을 자기가 안다는 점도 아는 것 같다. 반면 [[청개구리]]의 경우 눈 앞에 [[파리(곤충)|파리]]가 날라다니는 것을 안다고 한들, '눈 앞에 파리가 있어!'라는 스스로의 앎에 대한 추상적인 앎을 가질만큼 뛰어난 인지 능력을 갖고 있는 것 같지는 않다. 즉 이런 청개구리 같은 사례를 [[지식]]에 포함시킬 것인지 여부가 S4 공리(혹은 KK 논제)를 두고 벌어지는 떡밥 중 하나다.

===== 체계 S5 =====
양상 논리체계 S5는 [[#s-4.2.2.3|체계 T]]에 다음 공리틀이 더해진 것이다:
* '''공리틀 S5''': <math>\Diamond \phi \to \Box \Diamond \phi</math>
* 예시: (진리 양상 논리) "[[신]]이 있는게 '''가능'''하다면, [[신]]이 있는게 '''가능하다는 것은 필연적'''이다."

공리틀 B와 S4는 S5로부터도 도출가능하다. 그리고 일반적으로 '형이상학적 필연성'에 관한 진리 양상 논리는 체계 S5와 일치한다고 여겨진다.

=== [[가능세계]] 의미론 ===
형식 논리에서 '의미론'은 각각의 명제들에 진리치들[* T, F 혹은 전산학에서 쓰이는 0, 1로 보면 된다.]이 부여되기 조건을 제시하는 이론이며, 이는 곧 수리 [[모형]]을 필요로 한다. 양상논리의 [[통사론]] 및 [[증명]]에 대한 연구가 [[20세기]] 초반에 등장한 것과 달리, 양상논리의 의미론은 [[라이프니츠]], [[루돌프 카르납]] 등의 영향을 받아 [[솔 크립키]]가 [[1950년대]]에 이른바 ''''크립키 모형'''' 혹은 ''''가능세계 의미론''''을 제시함으로써 마련되었다고 평가된다.

[[표준논리]]의 의미론과 비교했을 때 크립키 모형에서는 순서쌍 <math>\langle W, R \rangle</math>이 추가된다. "가능세계 집합" <math>W</math>는 공집합이 아닌 집합이며, "접근가능성" 관계 <math>R</math>은 <math>R \subseteq W \times W</math>로 정의된다.

특정 모형이 주어질 때, [[표준논리]]에서 임의의 명제 <math>p</math>는 그 자체로 참 혹은 거짓이다[* 함수 <math>V</math>가 명제에 진리치(참(=1), 거짓(=0))를 부여하는 [[함수]]라고 할 때, 표준 논리에서 <math>p</math>가 참이라는 것은 곧 <math>V(p)=1</math>인 것이다.]. 하지만 크립키 모형에서 명제의 참거짓 여부는 <math>W</math>의 원소인 "가능세계" <math>w</math>에 따라 상대적으로 결정되어야만 한다. 요컨대 명제 <math>p</math>는 특정한 세계 <math>w</math>에서 참이거나 거짓일 수 있을 뿐, "세계를 떠나서" 참이거나 거짓일 수는 없게 된다[* <math>V</math>가 진리치(T(=1), F(=0))를 배정 함수라고 할 때, 양상 논리에서 <math>V</math>는 논항(argument)가 2개인 [[함수]], 즉 2항 연산(2-ary operation)이다. 예를 들어 명제 <math>p</math>는 <math>V(p,w)=1</math>일 때 그리고 오직 그 경우에만 세계 <math>w</math>에서 참이다.].

위 모형을 도입함으로써 양상 문장들의 의미는 다음과 같이 정의될 수 있다:

||'''진리 양상 논리 기준 ([[#s-4.2.2.6|체계 S5]]) 의미론'''
* "<math>p</math>가 필연적으로 참이다" i.e. "<math>\Box p</math>는 참이다" iff. 모든 가능세계 <math>w \in W</math>에서 <math>p</math>가 참이다[* <math>\forall w \in W: V(p,w)=1</math>].
* "<math>p</math>가 우연적으로 참이다" i.e. "<math>\Diamond p</math>는 참이다" iff. 어떤 (하나 이상의) 가능세계 <math>w \in W</math>에서 <math>p</math>가 참이다[* <math>\exists w \in W: V(p,w)=1</math>].
* "<math>p</math>가 (현실에서) 참이다" iff. 가능세계 <math>a \in W</math>에서 <math>p</math>가 참이며, 그 세계 <math>a</math>가 바로 [[현실]]세계다.||

즉 "필연성", "가능성" 같은 개념들이 위와 같이 가능세계 집합 <math>W</math>를 통해서 설명될 수 있게 된다. 다만 [[철학]]적으로는 <math>W</math>의 원소인 '''가능세계'''의 [[형이상학]]적 지위가 매우 의심스럽다는 점에서 20세기 후반 [[솔 크립키]], [[데이빗 루이스]], [[알빈 플란팅가]] 등 여러 형이상학자들의 연구가 이어진다.[* 예를 들어 가능세계라는 것이 그저 추상적 개념이거나 언어적인 구성물에 불과한 것인지, 아니면 현실세계가 그러한 것처럼 구체적인 '''물리적 세계'''로써 존재하는 것인지 대한 논의를 다룬다.]

더불어 접근가능성 관계 <math>R</math>은 상기된 각 양상 공리 체계들의 차이를 설명하는데 쓰인다.

* [[#s-4.2.2.1|체계 K]]: 제한 없음
* [[#s-4.2.2.2|체계 D]]: <math>R</math>이 순차적이다[* <math>\forall w \exists w': Rww'</math>]
* [[#s-4.2.2.3|체계 T]]: <math>R</math>이 반사적이다[* <math>\forall w: Rww</math>]
* [[#s-4.2.2.4|체계 B]]: <math>R</math>이 반사적이며 대칭적이다[* <math>\forall w, w': Rww' \to Rw'w</math>]
* [[#s-4.2.2.5|체계 S4]]: <math>R</math>이 반사적이며 전이적이다[* <math>\forall x,y,z: (Rxy \wedge Ryz) \to Rxz </math> '전이적'이라는 표현 대신 '추이적', 혹은 '이행적'이라는 표현을 써도 된다.]
* [[#s-4.2.2.6|체계 S5]]: <math>R</math>이 [[동치관계]]다 i.e. <math>R</math>이 반사적/대칭적/전이적이다.

== 양화 양상논리과 De Dicto/Re 양상 구분[* "De Dicto 양상"은 "대언(對言) 양상"이나 "명제 양상", "De Re 양상"은 "대물(對物) 양상" 혹은 "사물 양상"으로 문헌상으론 번역되기도 하나, 둘 모두 [[2016년]] 현재까진 한국어로 명확하게 정해진 번역어는 없다.] ==
양화 논리(혹은 '술어 논리')는 명제 논리에 "모두"와 "[[존재]]"에 대응하는 논리 연산자인 "양화사"(<math>\forall, \exists</math>)를 도입하여 명제를 더욱 세밀하게 분석하는 논리 체계다. 예를 들어 한국어 문장 "학생이 있다"는 다음과 같이 분석될 수 있다:

* [[한국어]] 문장: "학생이 있다"
* [[수리 논리학#s-3|명제 논리]] 번역 예시: "<math>P</math>"
* [[수리 논리학#s-4|양화 논리]] 번역 예시: "<math>\exists x Sx</math>" ('어떤 <math>x</math>는 학생이다')

두 번째 예문은 "닫힌 식(closed formula)"이라고 불린다. 변항 <math>x</math>가 문장 앞의 양화사 <math>\exists</math>에 의해 "속박되었기(bound)" 때문이다[* 반면 열린 식(open formula)의 예시로는 "<math>Fx</math>"가 있다. 이때 변항 <math>x</math>는 어떤 양화사에 의해 속박되지 않았기 때문이다.] 이처럼 명제논리에서의 "명제"는 양화논리에서의 "닫힌 식"에 해당한다. 보다 자세한 사항은 [[수리 논리학#s-4|양화 논리]] 참조.

'''양화 양상논리(Quantificational Modal Logic)'''는 양화 논리에 양상 연산자를 추가한 것으로 정의된다. 그런데 위에서 살펴본 것처럼 명제 양상논리에서 양상 연산자 <math> \Box, \Diamond </math>는 대문자로 표기된 명제 기호 <math>P</math> 왼쪽에 붙는다. 따라서 양화 논리 관점에서 보자면 이는 곧 닫힌 식 왼쪽에 양상연산자가 붙는 것과 매한가지다.

따라서 위 문단의 예시를 따를 경우, "<math>\Box P</math>"와 "<math>\Box \exists x Sx</math>"는 그 의미가 같다. 이렇듯 __명제 혹은 닫힌 식에 양상 연산자를 붙이는 것을 두고 ''' "De Dicto 양상" '''이라고 부른다__. 그 예시는 다음과 같다.

* "필연적으로 학생은 존재한다(<math>\Box \exists x Sx</math>)"
* "모든 사람이 포유류라는 것은 필연적이다(<math>\Box \forall x (Hx \to Mx))</math>"
* "경호는 락커이지만 아이돌이었을 수도 있다(<math>Rg \wedge \Diamond Ig </math>)"

반면 많은 철학자와 논리학자들은 양화 양상 논리에서 양상 연산자가 '열린 식', 즉 '양화사에 의해 속박되지 않은 자유 변항이 있는 식' (예. "<math>Sx</math>")을 논항으로 취할 수도 있다고 생각한다. 즉 명제 양상논리로 표현불가능한 것도 양화 양상논리에서는 표현가능하다고 생각한다. 이렇듯 __열린 식에 양상 연산자를 붙이는 것을 두고 ''' "De Re 양상" '''이라고 부른다__. 그 예시는 다음과 같다:

* "모든 것은 필연적으로 물질이다(<math> \forall x \Box Mx </math>)"
* "어떤 사람은 변호사일 수는 있지만 개구리일 수는 없다(<math> \exists x (Hx \wedge \Diamond Lx \wedge \neg \Diamond Fx) </math>)".

일상 언어에서는 De Re 양상과 De Dicto 양상이 잘 구별이 되지 않는 경우가 있다. 예컨대 __문장 "일어나 있는 어떤 사람은 앉을 수 있다"는 De Dicto 양상으로 이해하면 거짓이지만, De Re 양상으로 이해하면 참이다__.

* De Dicto 양상: "어떤 사람은 일어나 있으면서 앉을 수 있다 (<math> \Diamond \exists x (Sx \wedge \neg Sx) </math>)": '''거짓'''
* De Re 양상: "일어나 있는 어떤 사람은 (원한다면) 앉을 수 있다 (<math> \exists x (Sx \wedge \Diamond \neg Sx) </math>)": '''참'''

De Re 양상과 De Dicto 양상은 이처럼 의미에 있어서 큰 차이를 낳을 뿐 아니라, [[형이상학]]적으로도 중요한 함축을 가진다. 이 때문에 De Dicto 양상이라면 몰라도 De Re 양상을 허용해야 할지 말지 여부에 관한 논쟁은 20세기 [[분석철학#s-3.2|분석 형이상학]]에서 큰 논쟁점 중 하나로 다루어졌다[* 그 대표적인 문제점이 이른바 '통세계적 동일성(trans-world identity)' 문제이다. 개략적인 소개를 위해서는 [[http://pakebi.com/philosophy/logic/pssworld.html?PHPSESSID=e7c6f6fadc86cd524d1af2c789233259| 이창후 박사의 소개문]]을 보면 좋고, 좀더 제대로 알아보기 위해선 솔 크립키의 ''Naming and Necessity''(한국 번역서명 [[http://www.aladin.co.kr/shop/wproduct.aspx?ItemId=42406331|『이름과 필연』]]) 1강의 내용이 고전적인 내용이다.]

== 양상논리에서 증명할 수 있는 것들 ==
*[[피치의 역설]]: 모든 진리를 알 수 있다면, 모든 진리는 알려져 있다.
*[[괴델의 신에 대한 존재론적 증명|신의 존재의 필연성]]: 본질적 존재는 필연성을 갖고, 신은 본질적 존재이다.

[[분류:철학]][[분류: 논리학]][[분류:수리논리학]]

양상논리 - 편집 역사

2017년 2월 4일 (토) 16:29에 Maintenance script님의 편집