수리논리학에서 2차 논리(二次論理, 영어: second-order logic)는 임의의 다항 관계 및 다항 연산에 대한 변수 및 이에 대한 전칭·존재 기호를 사용할 수 있는 논리이다. 1차 논리에서 변수는 사용하는 모형의 원소만을 지칭하지만, 2차 논리에서는 모형 속의 임의의 부분 집합에 대하여 언급할 수 있다. 이에 따라 2차 논리는 1차 논리보다 더 다양한 개념들에 대하여 논할 수 있다. 그러나 2차 논리는 1차 논리와 달리 완전한 증명 체계를 갖지 못하며, 콤팩트성 정리나 뢰벤하임-스콜렘 정리와 같은 중요한 성질들이 성립하지 않는다.

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

2차 논리의 변수(영어: variable)들은 다음과 같은 가산 무한 개의 종류(영어: sort)에 속한다.

• 각 자연수 ${\displaystyle n\in \mathbb {N} }$에 대하여, ${\displaystyle n}$항 연산 변수 ${\displaystyle f_{0}^{n},f_{1}^{n},f_{2}^{n},\dots }$.
  • 특히, ${\displaystyle n=0}$일 때, ${\displaystyle f_{0}^{0},f_{1}^{0},\dots }$는 1차 논리의 변수에 해당한다.
  • 사실, ${\displaystyle n>0}$인 연산 변수들은 생략할 수 있다.^[1]:63 예를 들어, ${\displaystyle \forall f_{i}^{n}(\cdots )}$는 ${\displaystyle \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)}$와 같이 풀어 쓸 수 있다.
• 각 자연수 ${\displaystyle n\in \mathbb {N} }$에 대하여, ${\displaystyle n}$항 관계 변수 ${\displaystyle R_{0}^{n},R_{1}^{n},R_{2}^{n},\dots }$.
  • 특히, ${\displaystyle n=1}$일 때, ${\displaystyle R_{0}^{1},R_{1}^{1},\dots }$는 1차 논리 변수들의 집합에 해당한다.

변수 밖에도 다음과 같은 논리 기호들이 사용된다. (이들은 1차 논리와 같다.)

• 전칭 기호 ${\displaystyle \forall }$와 존재 기호 ${\displaystyle \exists }$
• 등호 ${\displaystyle =}$
• 명제 논리 기호 ${\displaystyle \land }$ (논리곱), ${\displaystyle \lor }$ (논리합), ${\displaystyle \lnot }$ (부정) 등
• 괄호 ${\displaystyle ()}$ 및 반점 ${\displaystyle ,}$ 등
• 주어진 ${\displaystyle n}$항 연산 ${\displaystyle {\mathsf {f}}}$ 및 ${\displaystyle n}$항 관계 ${\displaystyle {\mathsf {R}}}$. 예를 들어, 집합론의 언어는 하나의 2항 관계 ${\displaystyle \in }$를 갖는다. 다른 예로, 순서체의 언어는 2항 연산 ${\displaystyle +}$와 ${\displaystyle \cdot }$, 1항 연산 ${\displaystyle -}$, 0항 연산 ${\displaystyle 0}$과 ${\displaystyle 1}$, 그리고 2항 관계 ${\displaystyle \leq }$를 갖는다.

2차 논리의 항(영어: term)은 다음 문법을 따라야 한다.

• ${\displaystyle n}$항 연산 변수 ${\displaystyle f_{i}^{n}}$과 ${\displaystyle n}$개의 항 ${\displaystyle t_{1},t_{2},\dots ,t_{n}}$에 대하여, ${\displaystyle f_{i}^{n}(t_{1},t_{2},\dots ,t_{n})}$은 항이다. (편의상 ${\displaystyle n=0}$일 때 괄호 ${\displaystyle f_{i}^{0}()}$를 생략하여 ${\displaystyle f_{i}^{0}}$로 쓴다.)
• ${\displaystyle n}$항 연산 ${\displaystyle {\mathsf {f}}}$와 ${\displaystyle n}$개의 항 ${\displaystyle t_{1},t_{2},\dots ,t_{n}}$에 대하여, ${\displaystyle {\mathsf {f}}(t_{1},t_{2},\dots ,t_{n})}$은 항이다. (편의상 ${\displaystyle n=0}$일 때 괄호 ${\displaystyle {\mathsf {f}}()}$를 생략하여 ${\displaystyle {\mathsf {f}}}$로 쓴다.)

2차 논리의 논리식(영어: (well formed) formula)은 다음 문법을 따라야 한다.

• ${\displaystyle n}$항 관계 변수 ${\displaystyle R_{i}^{n}}$과 ${\displaystyle n}$개의 항 ${\displaystyle t_{1},t_{2},\dots ,t_{n}}$에 대하여, ${\displaystyle R_{i}^{n}(t_{1},t_{2},\dots ,t_{n})}$는 논리식이다.
• ${\displaystyle n}$항 관계 ${\displaystyle {\mathsf {R}}}$와 ${\displaystyle n}$개의 항 ${\displaystyle t_{1},t_{2},\dots ,t_{n}}$에 대하여, ${\displaystyle {\mathsf {R}}(t_{1},t_{2},\dots ,t_{n})}$는 논리식이다.
• 두 항 ${\displaystyle t_{1}}$, ${\displaystyle t_{2}}$에 대하여, ${\displaystyle t_{1}=t_{2}}$는 논리식이다.
• 논리식 ${\displaystyle \phi }$와 ${\displaystyle \phi }$에 등장하는 ${\displaystyle n}$항 자유 연산 변수 ${\displaystyle f_{i}^{n}}$에 대하여, ${\displaystyle \forall f_{i}^{n}\phi }$와 ${\displaystyle \exists f_{i}^{n}\phi }$는 논리식이다.
• 논리식 ${\displaystyle \phi }$와 ${\displaystyle \phi }$에 등장하는 ${\displaystyle n}$항 자유 관계 변수 ${\displaystyle R_{i}^{n}}$에 대하여, ${\displaystyle \forall R_{i}^{n}\phi }$와 ${\displaystyle \exists R_{i}^{n}\phi }$는 논리식이다.
• 두 논리식 ${\displaystyle \phi }$와 ${\displaystyle \chi }$에 대하여, ${\displaystyle \phi \land \chi }$와 ${\displaystyle \phi \lor \chi }$ 및 ${\displaystyle \phi }$에 대하여, ${\displaystyle \lnot \phi }$는 논리식이다.

여기서, 논리식 ${\displaystyle \phi }$에 등장하는 연산 변수 또는 관계 변수 ${\displaystyle x}$가 자유 변수(영어: free variable)라는 것은 ${\displaystyle \phi }$에 ${\displaystyle \forall x}$나 ${\displaystyle \exists x}$가 포함되지 않는 것을 의미한다.

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

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

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

괴델의 불완전성 정리에 따라, 2차 논리의 증명 체계는 다음 세 조건을 동시에 만족시킬 수 없다.

• (정당성 영어: soundness) 증명 체계가 증명할 수 있는 모든 명제는 2차 논리의 모든 (표준) 모형에서 참이다.
• (완전성 영어: completeness) 증명 체계는 2차 논리의 모든 (표준) 모형에서 참인 2차 논리 명제를 증명할 수 있다.
• (유효성 영어: effectiveness) 증명들의 집합은 재귀적 집합이다. 즉, 주어진 문자열이 어떤 명제의 증명인지 여부를 항상 종료하는 알고리즘으로 판별할 수 있다.

반면, 1차 논리의 경우 위 세 조건을 만족시키는 증명 체계가 존재한다 (괴델의 완전성 정리).

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

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

고틀로프 프레게는 1879년에 출판된 《개념 표기법》^[2]에서 오늘날의 2차 논리와 유사한 논리 체계를 도입하였다.^[3]:295 그러나 프레게는 1차 논리와 고차 논리를 구분하지 않았다. 이후 찰스 샌더스 퍼스가 1차 논리와 2차 논리를 구분하였으며, "2차 논리"라는 용어를 도입하였다.^[3]:296

헹킨 의미론은 리언 앨버트 헹킨(영어: Leon Albert Henkin, 1921~2006)이 1950년에 도입하였다.^[4]

2차 논리에 대하여 윌러드 밴 오먼 콰인은 (이솝 우화에 빗대어) “양의 탈을 쓴 집합론”(영어: set theory in sheep’s clothing)이라고 평하였다.^{[5]:66, Chapter 5} 즉, 2차 논리로는 집합론에 해당하는 여러 개념들(멱집합 등)을 정의할 수 있으며, 또한 적절한 증명 이론을 제시할 수 없으므로, 1차 논리와 달리 2차 ‘논리’는 사실 논리가 아니라는 것이다.

반면, 조지 불로스(영어: George Boolos)^[6]를 비롯한 다른 수리철학자들은^{[1][7][8][9][10]} 콰인의 비판에 반대하여 2차 논리를 옹호하였다.

• 1차 논리
• 고차 논리

• Rossberg, M. (2004). 〈First-order logic, second-order logic, and completeness〉 (PDF). Hendricks, Vincent; Neuhaus, Fabian; Scheffler, Uwe; Pedersen, Stig Andur; Wansing, Heinrich. 《First-order logic revisited》. Logische Philosophie (영어) 12. λογος-Verlag. 303–322쪽. ISBN 978-3-8325-0475-5. 
• Shapiro, Stewart (2001년 8월). 〈Classical logic II: higher order logic〉. Goble, Lou. 《The Blackwell Guide to Philosophical Logic》 (영어). Blackwell. 33–54쪽. doi:10.1111/b.9780631206934.2001.00005.x. ISBN 978-0-631-20693-4. 
• Lambek, Joachim; Scott, P. J. (1986). 《Introduction to higher order categorical logic》 (영어). Cambridge University Press. ISBN 978-0-521-35653-4. 
• Benzmüller, Christoph; Miller, Dale (2014). 〈Automation of higher-order logic〉 (PDF). Gabbay, Dov M.; Siekmann, Jörg H.; Woods, John. 《Handbook of the history of logic, volume 9: computational logic》 (영어). Elsevier. 215–254쪽. doi:10.1016/B978-0-444-51624-4.50005-8. ISBN 978-0-08-093067-1. 
• Moore, Gregory H. (1988). 〈The emergence of first-order logic〉 (PDF). Aspray, William; Kitcher, Philip. 《History and Philosophy of Modern Mathematics》. Minnesota Studies in the Philosophy of Science (영어) 11. University of Minnesota Press. 95–135쪽. JSTOR 10.5749/j.cttttp0k.7. 
• Eklund, Matti (1996년 12월). “On how logic became first-order” (PDF). 《Nordic Journal of Philosophical Logic》 (영어) 1 (2): 147–167. 

• Enderton, Herbert B. (2009년 3월 4일). “Second-order and higher-order logic”. 《The Stanford Encyclopedia of Philosophy》 (영어). 
• Uzquiano, Gabriel (2014년 9월 3일). “Quantifiers and quantification”. 《The Stanford Encyclopedia of Philosophy》 (영어). 
• “Second-order logic”. 《nLab》 (영어). 
• “Higher-order logic”. 《nLab》 (영어).