2차 논리 문서 원본 보기

{{위키데이터 속성 추적}}
[[파일:Kindl-Treppe Aug2021d.jpg|thumb|2차 논리의 문장 <math>\exists\phi\phi</math>가 쓰여진 [[그라피티]] ([[노이쾰른]])]]
[[수리논리학]]에서 '''2차 논리'''(二次論理, {{llang|en|second-order logic}})는 임의의 다항 관계 및 다항 연산에 대한 변수 및 이에 대한 전칭·존재 기호를 사용할 수 있는 논리이다. [[1차 논리]]에서 변수는 사용하는 [[모형 (논리학)|모형]]의 원소만을 지칭하지만, 2차 논리에서는 [[모형 (논리학)|모형]] 속의 임의의 [[부분 집합]]에 대하여 언급할 수 있다. 이에 따라 2차 논리는 [[1차 논리]]보다 더 다양한 개념들에 대하여 논할 수 있다. 그러나 2차 논리는 [[1차 논리]]와 달리 완전한 증명 체계를 갖지 못하며, [[콤팩트성 정리]]나 [[뢰벤하임-스콜렘 정리]]와 같은 중요한 성질들이 성립하지 않는다.

== 정의 ==
=== 문법 ===
2차 논리의 문법은 다음과 같은 기호들로 구성된다.

2차 논리의 '''변수'''({{llang|en|variable}})들은 다음과 같은 가산 무한 개의 '''종류'''({{llang|en|sort}})에 속한다.
* 각 자연수 <math>n\in\mathbb N</math>에 대하여, <math>n</math>항 연산 변수 <math>f_0^n,f_1^n,f_2^n,\dots</math>.
** 특히, <math>n=0</math>일 때, <math>f_0^0,f_1^0,\dots</math>는 [[1차 논리]]의 변수에 해당한다.
** 사실, <math>n>0</math>인 연산 변수들은 생략할 수 있다.<ref name="Shapiro"/>{{rp|63}} 예를 들어, <math>\forall f_i^n(\cdots)</math>는 <math>\forall R_i^{n+1}\left((\forall x_0,x_0',x_1,x_2,\dots,x_n\colon R_i^{n+1}(x_0,x_1,\dots,x_n)\land R_i^{n+1}(x_0',x_1,\dots,x_n)\implies x_0=x_0')\implies(\cdots)\right)</math>와 같이 풀어 쓸 수 있다.
* 각 자연수 <math>n\in\mathbb N</math>에 대하여, <math>n</math>항 관계 변수 <math>R_0^n,R_1^n,R_2^n,\dots</math>.
** 특히, <math>n=1</math>일 때, <math>R_0^1,R_1^1,\dots</math>는 [[1차 논리]] 변수들의 집합에 해당한다.
변수 밖에도 다음과 같은 논리 기호들이 사용된다. (이들은 [[1차 논리]]와 같다.)
* 전칭 기호 <math>\forall</math>와 존재 기호 <math>\exists</math>
* 등호 <math>=</math>
* [[명제 논리]] 기호 <math>\land</math> ([[논리곱]]), <math>\lor</math> ([[논리합]]), <math>\lnot</math> ([[부정]]) 등
* 괄호 <math>()</math> 및 반점 <math>,</math> 등
* 주어진 <math>n</math>항 연산 <math>\mathsf f</math> 및 <math>n</math>항 관계 <math>\mathsf R</math>. 예를 들어, [[집합론]]의 언어는 하나의 2항 관계 <math>\in</math>를 갖는다. 다른 예로, [[순서체]]의 언어는 2항 연산 <math>+</math>와 <math>\cdot</math>, 1항 연산 <math>-</math>, 0항 연산 <math>0</math>과 <math>1</math>, 그리고 2항 관계 <math>\le</math>를 갖는다.
2차 논리의 '''항'''({{llang|en|term}})은 다음 문법을 따라야 한다.
* <math>n</math>항 연산 변수 <math>f_i^n</math>과 <math>n</math>개의 항 <math>t_1,t_2,\dots,t_n</math>에 대하여, <math>f_i^n(t_1,t_2,\dots,t_n)</math>은 항이다. (편의상 <math>n=0</math>일 때 괄호 <math>f_i^0()</math>를 생략하여 <math>f_i^0</math>로 쓴다.)
* <math>n</math>항 연산 <math>\mathsf f</math>와 <math>n</math>개의 항 <math>t_1,t_2,\dots,t_n</math>에 대하여, <math>\mathsf f(t_1,t_2,\dots,t_n)</math>은 항이다.  (편의상 <math>n=0</math>일 때 괄호 <math>\mathsf f()</math>를 생략하여 <math>\mathsf f</math>로 쓴다.)
2차 논리의 '''[[논리식]]'''({{llang|en|(well formed) formula}})은 다음 문법을 따라야 한다.
* <math>n</math>항 관계 변수 <math>R_i^n</math>과 <math>n</math>개의 항 <math>t_1,t_2,\dots,t_n</math>에 대하여, <math>R_i^n(t_1,t_2,\dots,t_n)</math>는 논리식이다.
* <math>n</math>항 관계 <math>\mathsf R</math>와 <math>n</math>개의 항 <math>t_1,t_2,\dots,t_n</math>에 대하여, <math>\mathsf R(t_1,t_2,\dots,t_n)</math>는 논리식이다.
* 두 항 <math>t_1</math>, <math>t_2</math>에 대하여, <math>t_1=t_2</math>는 논리식이다.
* 논리식 <math>\phi</math>와 <math>\phi</math>에 등장하는 <math>n</math>항 자유 연산 변수 <math>f_i^n</math>에 대하여, <math>\forall f_i^n\phi</math>와 <math>\exists f_i^n\phi</math>는 논리식이다.
* 논리식 <math>\phi</math>와 <math>\phi</math>에 등장하는 <math>n</math>항 자유 관계 변수 <math>R_i^n</math>에 대하여, <math>\forall R_i^n\phi</math>와 <math>\exists R_i^n\phi</math>는 논리식이다.
* 두 논리식 <math>\phi</math>와 <math>\chi</math>에 대하여, <math>\phi\land\chi</math>와 <math>\phi\lor\chi</math> 및 <math>\phi</math>에 대하여, <math>\lnot\phi</math>는 논리식이다.
여기서, 논리식 <math>\phi</math>에 등장하는 연산 변수 또는 관계 변수 <math>x</math>가 '''자유 변수'''({{llang|en|free variable}})라는 것은 <math>\phi</math>에 <math>\forall x</math>나 <math>\exists x</math>가 포함되지 않는 것을 의미한다.

=== 의미론 ===
2차 논리의 의미론은 흔히 2차 논리의 [[모형 (논리학)|모형]]으로 주어진다. 이 경우, 모형 <math>\langle X,\dots\rangle</math>가 주어졌을 때, <math>n</math>항 연산 변수는 <math>X</math> 위의 모든 (외적 관점에서의) 연산 <math>X^{X^n}</math>의 값을 가질 수 있으며, <math>n</math>항 관계 변수는 <math>X</math> 위의 모든 (외적 관점에서의) 관계 <math>\mathcal P(X^n)</math>의 값을 가질 수 있다. 특히, 1항 관계 변수는 <math>X</math>의 모든 부분 집합의 값을 가질 수 있다. 반면, 1차 논리 모형에서는 ([[집합론]]의 언어를 사용할 경우, [[추이적 모형]]의 경우) 1차 논리 언어로 정의 가능한 <math>X</math>의 부분 집합만을 다룰 수 있다.

2차 논리의 경우, 위와 같은 표준적인 의미론 대신 '''헹킨 의미론'''({{llang|en|Henkin semantics}})을 사용할 수 있다. 헹킨 의미론에서는 각 변수 종류({{llang|en|sort}})가 다른 정의역({{llang|en|domain}})을 가질 수 있다. 헹킨 의미론을 사용할 경우 2차 논리는 사실상 [[1차 논리]]와 같아진다. 간혹 헹킨 의미론과 구별하기 위하여 전자를 '''표준 의미론'''({{llang|en|standard semantics}})이라고 하기도 한다.

== 성질 ==
2차 논리의 '''증명 체계'''({{llang|en|proof system}})는 (순수한 논리 기호만 포함하는, 즉 변수 및 <math>=,\forall,\exists,\lor,\land,\lnot</math>만을 포함하는) 2차 논리 명제에 대하여 증명을 제시하거나 또는 제시하지 않는 함수이다. 증명 체계가 증명을 제시하는 명제를 '''증명 가능 명제'''({{llang|en|provable proposition}})라고 한다. 여기서 "증명"이란 (주어진 알파벳에 대한) 일련의 문자열을 뜻한다.

[[괴델의 불완전성 정리]]에 따라, 2차 논리의 증명 체계는 다음 세 조건을 동시에 만족시킬 수 없다.
* (정당성 {{llang|en|soundness}}) 증명 체계가 증명할 수 있는 모든 명제는 2차 논리의 모든 (표준) [[모형 (논리학)|모형]]에서 참이다.
* (완전성 {{llang|en|completeness}}) 증명 체계는 2차 논리의 모든 (표준) [[모형 (논리학)|모형]]에서 참인 2차 논리 명제를 증명할 수 있다.
* (유효성 {{llang|en|effectiveness}}) 증명들의 집합은 [[재귀적 집합]]이다. 즉, 주어진 문자열이 어떤 명제의 증명인지 여부를 항상 종료하는 [[알고리즘]]으로 판별할 수 있다.
반면, [[1차 논리]]의 경우 위 세 조건을 만족시키는 증명 체계가 존재한다 ([[괴델의 완전성 정리]]).

2차 논리에서는 또한 [[콤팩트성 정리]]와 [[뢰벤하임-스콜렘 정리]]가 성립하지 않는다.

(위 성질들은 2차 논리의 표준 의미론에 대한 것이다. 헹킨 의미론을 사용하면 이는 1차 논리와 같은 성질들을 갖는다.)

== 역사 ==
[[고틀로프 프레게]]는 1879년에 출판된 《개념 표기법》<ref>{{서적 인용|제목=Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens|이름=Gottlob|성=Frege|저자링크=고틀로프 프레게|날짜=1879|위치=[[할레]]|출판사=Verlag von Louis Nebert|url=http://gallica.bnf.fr/ark:/12148/bpt6k65658c|언어=de}}</ref>에서 오늘날의 2차 논리와 유사한 논리 체계를 도입하였다.<ref name="Putnam"/>{{rp|295}} 그러나 프레게는 [[1차 논리]]와 고차 논리를 구분하지 않았다. 이후 [[찰스 샌더스 퍼스]]가 1차 논리와 2차 논리를 구분하였으며, "2차 논리"라는 용어를 도입하였다.<ref name="Putnam">{{저널 인용
 | doi= 10.1016/0315-0860(82)90123-9
 | 성= Putnam |이름= Hilary |저자링크=힐러리 퍼트넘
 | year=1982
 | title=Peirce the logician
 | journal=Historia Mathematica | issn=0315-0860
 | volume=9
 | pages= 290–301
 | issue= 3 | 언어=en}}</ref>{{rp|296}}

헹킨 의미론은 리언 앨버트 헹킨({{llang|en|Leon Albert Henkin}}, 1921~2006)이 1950년에 도입하였다.<ref>{{저널 인용
 | 성 = Henkin | 이름= Leon Albert
 | title = Completeness in the theory of types
 | journal = Journal of Symbolic Logic | issn = 0022-4812
 | volume = 15
 | year = 1950
 | pages = 81–91
 | issue = 2
 | doi = 10.2307/2266967
| jstor=2266967 | 언어=en}}</ref>

2차 논리에 대하여 [[윌러드 밴 오먼 콰인]]은 ([[이솝 우화]]에 빗대어) “양의 탈을 쓴 [[집합론]]”({{llang|en|set theory in sheep’s clothing}})이라고 평하였다.<ref>{{서적 인용|제목=Philosophy of logic|판=2|이름=W. V. O.|성=Quine|저자링크=윌러드 밴 오먼 콰인|url=http://www.hup.harvard.edu/catalog.php?isbn=9780674665637|날짜=1986-06|isbn=978-067466563-7|출판사=Harvard University Press|언어=en}}</ref>{{rp|66, Chapter 5}} 즉, 2차 논리로는 [[집합론]]에 해당하는 여러 개념들([[멱집합]] 등)을 정의할 수 있으며, 또한 적절한 증명 이론을 제시할 수 없으므로, [[1차 논리]]와 달리 2차 ‘논리’는 사실 논리가 아니라는 것이다.

반면, [[조지 불로스]]({{llang|en|George Boolos}})<ref>{{저널 인용|doi=10.2307/2025179|제목=On second-order logic|저널=The Journal of Philosophy|쪽=509–527|권=72|호=16|날짜=1975-09|이름=George S.|성=Boolos|언어=en}}</ref>를 비롯한 다른 수리철학자들은<ref name="Shapiro">{{서적 인용
 | 성 = Shapiro | 이름=Stewart
 | title = Foundations without foundationalism: a case for second-order logic
 | publisher = Oxford University Press
 |  날짜 = 2000
 | isbn = 978-0-19-825029-6 | doi=10.1093/0198250290.001.0001 | 총서=Oxford Logic Guides |권=17 | 언어=en}}</ref><ref>{{저널 인용
 | 성 = Shapiro | 이름=Stewart
 | 제목=Do not claim too much: second-order logic and first-order logic | doi= 10.1093/philmat/7.1.42 | 권=7 | 호=1 | 쪽= 42–64 | 저널=Philosophia Mathematica | issn= 0031-8019 | 날짜=1999-02 | 언어=en}}</ref><ref>{{저널 인용
 | 성 = Shapiro | 이름=Stewart
 | 제목=Higher-order logic or set theory: a false dilemma | doi=  10.1093/philmat/nks002 | 권=20 | 호=3 | 쪽=305–323 | 저널=Philosophia Mathematica | issn= 0031-8019 | 날짜=2012-10 | 언어=en}}</ref><ref>{{저널 인용
 | last = Väänänen
 |first = Jouko
 | url = http://www.math.helsinki.fi/logic/people/jouko.vaananen/VaaSec.pdf
 | title = Second-order logic and foundations of mathematics
 | journal = Bulletin of Symbolic Logic
 | volume = 7
 | issue = 4
 | year = 2001
 | pages = 504–520
 | doi = 10.2307/2687796
 | jstor = 2687796 | 언어=en
}}</ref><ref>{{저널 인용 | 제목=A defense of second-order logic|이름=Otávio |성=Bueno|doi=10.1007/s10516-010-9101-4|저널=Axiomathes|issn=1122-1151|날짜=2010|url=http://www.as.miami.edu/personal/obueno/Site/Online_Papers_files/SecnOrd_FINAL.pdf|언어=en}}</ref> 콰인의 비판에 반대하여 2차 논리를 옹호하였다.

== 같이 보기 ==
* [[1차 논리]]
* [[고차 논리]]
== 각주 ==
{{각주}}
* {{서적 인용
 | 성 = Rossberg | 이름 = M.
 | 장url = http://homepages.uconn.edu/~mar08022/papers/RossbergCompleteness.pdf
 | 장 = First-order logic, second-order logic, and completeness
 | 제목 = First-order logic revisited | 총서=Logische Philosophie | 권=12
 | editor1-first=Vincent | editor1-last= Hendricks |editor2-first=Fabian | editor2-last=Neuhaus | editor3-first = Uwe | editor3-last=Scheffler | editor4-first=Stig Andur | editor4-last=Pedersen | editor5-first=Heinrich | editor5-last=Wansing
 | publisher = λογος-Verlag | isbn=978-3-8325-0475-5 | 쪽=303–322
 | year = 2004 | 언어=en | url=http://www.logos-verlag.de/cgi-bin/engbuchmid?isbn=0475&lng=deu&id=
}}
* {{서적 인용|이름=Stewart|성=Shapiro|날짜=2001-08|장=Classical logic II: higher order logic|editor-first=Lou|editor-last=Goble|제목=The Blackwell Guide to Philosophical Logic|url=https://archive.org/details/blackwellguideto00gobl|출판사=Blackwell|isbn=978-0-631-20693-4|쪽=[https://archive.org/details/blackwellguideto00gobl/page/n41 33]–54|doi=10.1111/b.9780631206934.2001.00005.x|언어=en}}
* {{서적 인용|이름=Joachim|성=Lambek|성2=Scott|이름2=P. J.|날짜=1986|제목=Introduction to higher order categorical logic|출판사= Cambridge University Press|isbn=978-0-521-35653-4|url=http://www.cambridge.org/us/academic/subjects/mathematics/logic-categories-and-sets/introduction-higher-order-categorical-logic | 언어=en}}
* {{서적 인용 |last1=Benzmüller |first1=Christoph |last2=Miller |first2=Dale |editor1-last=Gabbay |editor1-first=Dov M. |editor2-last=Siekmann |editor2-first=Jörg H. |editor3-last=Woods |editor3-first=John |date=2014 |title=Handbook of the history of logic, volume 9: computational logic |장=Automation of higher-order logic |publisher=Elsevier |장url= http://www.lix.polytechnique.fr/~dale/papers/automationHOL.pdf | doi= 10.1016/B978-0-444-51624-4.50005-8 | 쪽=215–254 | isbn=978-0-08-093067-1 | 언어=en}}
* {{서적 인용|장url=http://mcps.umn.edu/philosophy/11_4Moore.pdf|장=The emergence of first-order logic|제목=History and Philosophy of Modern Mathematics|이름=Gregory H.|성=Moore|날짜=1988|쪽=95–135|editor1-first=William|editor1-last=Aspray|editor2-first=Philip|editor2-last=Kitcher|총서=Minnesota Studies in the Philosophy of Science|권=11|jstor=10.5749/j.cttttp0k.7|출판사=University of Minnesota Press|언어=en}}
* {{저널 인용|제목=On how logic became first-order|이름=Matti|성=Eklund|저널=Nordic Journal of Philosophical Logic|권=1|호=2|쪽=147–167|날짜=1996-12|url=http://www.hf.uio.no/ifikk/forskning/publikasjoner/tidsskrifter/njpl/vol1no2/howlogic.pdf|언어=en}}

== 외부 링크 ==
*{{웹 인용|성 = Enderton | 이름= Herbert B.|제목 = Second-order and higher-order logic|웹사이트= The Stanford Encyclopedia of Philosophy|url = http://plato.stanford.edu/entries/logic-higher-order/|날짜=2009-03-04 | 언어=en}}
*{{웹 인용|성 = Uzquiano | 이름= Gabriel |제목 = Quantifiers and quantification|웹사이트= The Stanford Encyclopedia of Philosophy|url = http://plato.stanford.edu/entries/quantification/|날짜=2014-09-03 | 언어=en}}
* {{nlab|id=second-order logic|title=Second-order logic}}
* {{nlab|id=higher-order logic|title=Higher-order logic}}

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