1차 논리

"오늘의AI위키"는 AI 기술로 일관성 있고 체계적인 최신 지식을 제공하는 혁신 플랫폼입니다.
"오늘의AI위키"의 AI를 통해 더욱 풍부하고 폭넓은 지식 경험을 누리세요.

1. 개요

1차 논리는 논리식, 추론 규칙, 의미론으로 구성되며, 형식적인 언어를 사용하여 수학적 추론을 형식화하는 데 사용되는 형식 논리 체계이다. 1차 논리는 변수, 논리 기호, 연산 기호, 관계 기호 등으로 구성된 문법을 가지며, 힐베르트 체계, 자연 연역, 시퀀트 계산 등 다양한 공리화 방식을 통해 증명 이론을 전개한다. 의미론은 모형을 통해 정의되며, 콤팩트성 정리, 뢰벤하임-스콜렘 정리와 같은 성질을 갖는다. 1차 논리는 명제 논리와 비교하여 술어 기호와 양화사를 사용하여 더욱 풍부한 표현력을 제공하며, 자동 정리 증명 및 형식적 검증 등 다양한 분야에 응용된다.

더 읽어볼만한 페이지

술어 논리 - 양화
양화는 논리학과 수학에서 명제의 범위를 지정하는 개념으로, '모든', '어떤'과 같은 의미를 나타내며, 전칭 양화자 '∀'와 존재 양화자 '∃' 등의 기호로 표현된다.
술어 논리 - 존재 양화사
존재 양화사는 형식 논리에서 특정 조건을 만족하는 대상이 존재함을 나타내는 방법으로, 수리 논리학에서는 기호 " $\exists$ "를 사용하여 변수가 특정 집합에 속하면서 주어진 조건을 만족하는 원소가 적어도 하나 존재함을 나타내며, 존재 일반화, 존재 제거 등의 추론 규칙과 관련이 있고, 담화 영역에 따라 진술의 참과 거짓이 달라질 수 있으며, 존재 양화된 명제 함수의 부정은 해당 명제 함수의 부정의 전칭 양화와 논리적으로 동치이다.

1차 논리
지도
기본 정보
유형	논리 체계
분야	수리논리학, 철학, 컴퓨터 과학
하위 유형	이차 논리, 고차 논리
동의어	1차 술어 논리, 일계 술어 논리, 일차 논리
역사
창시자	고틀로프 프레게
특징
양화	전칭 기호 (∀) 및 존재 기호 (∃) 사용
변수	개체 변수 (명제 변수 제외)
표현력	명제 논리보다 높은 표현력
대상	명제들의 주어와 술어 간 관계를 다룸
대상영역	공집합이 아닌 대상영역에서 양화 가능
술어	대상 영역 원소들에 대한 술어 사용
의미론
해석	대상영역과 술어 해석 필요
진리값	주어진 해석에 따라 문장의 참/거짓 결정
문법
논리 기호	논리곱(∧), 논리합(∨), 부정(¬), 함축(→), 동치(↔), 전칭 기호(∀), 존재 기호(∃)
비논리 기호	술어 기호, 상수 기호, 함수 기호
수식	항(term), 원자식(atomic formula), 복합식(compound formula)
형식 체계
공리	논리적 공리 및 비논리적 공리
추론 규칙	모두스 포넨스, 일반화
응용
분야	수학, 컴퓨터 과학, 철학, 언어학
응용 예시	정리 증명, 프로그래밍 언어 의미론, 데이터베이스
한계
표현력 제한	자기 참조 및 무한 집합 표현의 한계
불완전성	괴델의 불완전성 정리의 적용
관련 개념
관련 논리	명제 논리, 이차 논리, 고차 논리
관련 이론	모델 이론, 증명 이론

2. 정의

1차 논리는 크게 세 가지 요소로 이루어진다.

'''논리식'''(well-formed formula|논리식^영어): 특정 규칙(문법)에 따라 기호들을 조합하여 만들어지는 의미 있는 표현이다. 1차 논리의 문법은 어떤 문자열이 올바른 논리식인지를 재귀적으로 정의한다. 논리식은 항(객체를 나타냄)과 술어(속성이나 관계를 나타냄)를 포함할 수 있다.
'''추론''': 이미 알려진 논리식(전제)들로부터 새로운 논리식(결론)을 이끌어내는 규칙이다. 힐베르트 체계나 자연 연역 등 다양한 방식으로 추론 규칙을 명시할 수 있다. 이를 통해 논리적으로 타당한 주장을 증명할 수 있다.
'''의미론''': 1차 논리 언어의 표현들에 의미를 부여하는 방식이다. 주로 모형(구조)을 통해 정의되며, 각 논리식이 어떤 조건에서 참 또는 거짓이 되는지를 결정한다. 모형은 논의 영역(다루는 대상들의 집합)과 기호들의 해석으로 구성된다.

명제 논리가 단순한 명제 자체를 다루는 반면, 1차 논리는 명제 내부 구조를 분석하여 술어와 양화사를 도입한다. 예를 들어 "소크라테스는 철학자이다"와 "플라톤은 철학자이다"라는 두 문장은 명제 논리에서는 단순히 별개의 명제 ''p''와 ''q''로 취급될 수 있다.^[6] 하지만 1차 논리에서는 "철학자이다"라는 술어(

\text{isPhil}

)가 특정 개체(소크라테스, 플라톤)에 적용된 형태, 즉

\text{isPhil}(\text{소크라테스})

와

\text{isPhil}(\text{플라톤})

으로 분석한다. 이처럼 개체와 술어를 다룰 수 있어 1차 논리는 명제 논리보다 더 풍부한 표현력을 가진다.^[7]

술어는 하나 이상의 항을 받아 참 또는 거짓을 판별한다. 예를 들어 "''x''는 철학자이다" (

\text{isPhil}(x)

)라는 표현의 진리값은 변수 ''x''에 어떤 개체가 대입되는지와 "철학자이다"라는 술어가 어떻게 해석되는지에 따라 달라진다.^[18]

양화사는 변수가 포함된 논리식의 범위를 지정한다. 보편 양화사

\forall

("모든")는 해당 논리식이 논의 영역의 모든 개체에 대해 성립함을 나타내고, 존재 양화사

\exists

("어떤" 또는 "존재한다")는 해당 논리식을 만족하는 개체가 논의 영역에 적어도 하나 존재함을 나타낸다. 예를 들어 "모든 ''x''에 대해, ''x''가 철학자이면 ''x''는 학자이다" (

\forall x (\text{isPhil}(x) \rightarrow \text{isScholar}(x))

)와 같이 표현할 수 있다.

결국 1차 논리는 구문론과 의미론이라는 두 가지 핵심 부분으로 나뉜다. 구문론은 어떤 기호열이 올바른 표현(항 또는 논리식)인지를 규정하고, 의미론은 이러한 표현들이 무엇을 의미하고 언제 참이 되는지를 결정한다.

2. 1. 문법

1차 논리의 언어는 형식 언어이며, 그 문법은 어떤 기호열이 올바른 표현인지 엄격하게 규정한다. 이 언어는 크게 기호, 항, 논리식이라는 세 가지 요소로 구성된다.

1차 논리 언어를 구성하는 기본적인 문자들을 기호라고 한다. 이는 컴퓨터 언어의 알파벳과 유사하다. 기호는 크게 논리 기호와 비논리 기호로 나뉜다.

논리 기호: 어떤 해석에서도 의미가 변하지 않는 기호들이다.^[8]
변수: $x, y, z, x_0, x_1, \dots$ 와 같이 개체를 나타내기 위해 사용되는 기호들이다. 보통 가산 무한 개의 변수가 있다고 가정한다.
논리 연결사: 명제 논리에서처럼 명제들을 연결하는 기호이다. 기본적으로 함의 ( $\rightarrow$ 또는 $\implies$ )와 부정 ( $\lnot$ 또는 $\neg$ )을 사용하며, 이를 통해 논리곱 ( $\land$ 또는 $\wedge$ ), 논리합 ( $\lor$ 또는 $\vee$ ), 쌍조건문 ( $\leftrightarrow$ 또는 $\Leftrightarrow$ ) 등을 정의할 수 있다.
양화사: 변수의 범위를 지정하는 기호이다. 전칭 기호 ( $\forall$ , "모든")와 존재 기호 ( $\exists$ , "어떤" 또는 "존재한다")가 있다. 둘 중 하나만 기본 기호로 사용하고 다른 하나를 정의하여 사용할 수도 있다. ( $\forall x\phi\iff \lnot\exists x\lnot\phi$ , $\exists x\phi\iff \lnot\forall x\lnot\phi$ )
등호: $=$ 기호는 두 항이 같은 대상을 나타냄을 의미한다. 논리 기호로 간주되기도 하고, 비논리 기호인 2항 관계 기호로 취급되기도 한다.
괄호 및 구두점: $(, ), [, ], {, }$ 등은 논리식의 구조를 명확히 하기 위해 사용된다.

비논리 기호: 사용되는 분야나 특정 이론(해석)에 따라 의미가 달라지는 기호들이다. 이들의 모음을 해당 언어의 시그니처라고 한다.^[13]
관계 기호 (또는 술어 기호): $P, Q, R, \dots$ 과 같이 개체들 사이의 관계나 속성을 나타낸다. 각 관계 기호는 정해진 개수의 항을 인수로 받는데, 이를 항수(arity|항수^영어)라고 한다.^[39] 예를 들어, $P(x)$ 는 1항 관계(술어), $Q(x, y)$ 는 2항 관계를 나타낸다. 0항 관계 기호는 명제 변수와 동일하게 취급될 수 있다.
함수 기호: $f, g, h, \dots$ 와 같이 개체들을 입력받아 다른 개체를 출력하는 함수를 나타낸다. 함수 기호도 각각 항수를 가진다. 예를 들어, $f(x)$ 는 1항 함수, $g(x, y)$ 는 2항 함수를 나타낸다.
상수 기호: $a, b, c, 0, \dots$ 와 같이 특정한 개체를 나타내는 기호이다. 상수 기호는 항수가 0인 함수 기호로 간주될 수 있다.

항(term|항^영어)은 논의 영역 내의 특정 개체를 지칭하는 표현이다. 항은 다음과 같은 규칙에 따라 귀납적으로 정의된다.^[16]

1. 모든 변수는 항이다.

2. 모든 상수 기호는 항이다. (0항 함수 기호로 간주)

3. 만약

f

가

n

항 함수 기호이고,

t_1, t_2, \dots, t_n

이 각각 항이라면,

f(t_1, t_2, \dots, t_n)

도 항이다.^[40]

예를 들어, 산술의 언어에서

0

(상수),

x

(변수),

S(x)

(1항 함수

S

적용),

+(x, S(0))

(2항 함수

+

적용) 등은 모두 항이다. 중위 표기법을 사용하면

x + S(0)

와 같이 쓸 수 있다.
논리식(well-formed formula|논리식^영어, 줄여서 WFF)은 참 또는 거짓으로 평가될 수 있는 문장이나 명제를 나타내는 표현이다. 논리식은 다음과 같은 규칙에 따라 귀납적으로 정의된다.^[17]

1. 원자 논리식(atomic formula|원자 논리식^영어): 가장 기본적인 형태의 논리식이다.

만약 $P$ 가 $n$ 항 관계 기호이고 $t_1, \dots, t_n$ 이 항이라면, $P(t_1, \dots, t_n)$ 은 원자 논리식이다.
만약 $t_1, t_2$ 가 항이라면, $t_1 = t_2$ 는 원자 논리식이다. (등호를 언어에 포함하는 경우)

2. 만약

\phi

가 논리식이라면,

\lnot \phi

(또는

\neg \phi

)도 논리식이다.

3. 만약

\phi

와

\psi

가 논리식이라면,

(\phi \land \psi)

,

(\phi \lor \psi)

,

(\phi \implies \psi)

,

(\phi \Leftrightarrow \psi)

등도 논리식이다. (괄호는 구문 트리의 유일성을 보장하기 위해 사용될 수 있다.)

4. 만약

\phi

가 논리식이고

x

가 변수라면,

\forall x \phi

와

\exists x \phi

도 논리식이다.

규칙 1-4를 유한 번 적용하여 만들어지는 표현만이 논리식이다. 예를 들어,

\forall x (P(x) \implies Q(f(x), c))

는 논리식이지만,

\forall x P(

와 같은 것은 규칙에 맞지 않아 논리식이 아니다.

논리식에 나타나는 변수는 자유 변수(free variable|자유 변수^영어)이거나 종속 변수(bound variable|종속 변수^영어)일 수 있다.^[18] 직관적으로, 변수가 양화사(

\forall

또는

\exists

)에 의해 범위가 지정되지 않으면 자유 변수이고, 양화사의 범위 안에 있으면 종속 변수이다. 각 논리식

\phi

에 대해, "

\phi

에서의 자유 변수 전체의 집합"

fr(\phi)

는 다음과 같이 재귀적으로 정의된다:

1.

\phi

가 원자 논리식이라면,

fr(\phi)

는 기호열

\phi

에 나타나는 모든 변수로 이루어진 집합이다.

2.

fr(\lnot\phi)= fr(\phi)

3.

fr(\phi\land\psi) = fr(\phi\lor\psi) = fr(\phi\Rightarrow\psi) = fr(\phi\Leftrightarrow\psi) = fr(\phi) \cup fr(\psi)

4.

fr(\forall x\phi) = fr(\exists x\phi) = fr(\phi) - \{ x \}

예를 들어, 논리식

P(x) \land \forall x Q(x, y)

에서,

$P(x)$ 에 나타나는 $x$ 는 자유 변수이다. ( $fr(P(x)) = \{x\}$ )
$\forall x Q(x, y)$ 에서 $x$ 는 양화사 $\forall x$ 에 의해 종속 변수이다. ( $fr(Q(x,y)) = \{x, y\}$ 이므로 $fr(\forall x Q(x, y)) = \{x, y\} - \{x\} = \{y\}$ )
$y$ 는 양화사의 영향을 받지 않으므로 $Q(x, y)$ 에서 자유 변수이고, 따라서 전체 논리식 $P(x) \land \forall x Q(x, y)$ 에서의 자유 변수 집합은 $fr(P(x)) \cup fr(\forall x Q(x, y)) = \{x\} \cup \{y\} = \{x, y\}$ 이다.

하나의 변수가 한 논리식 안에서 자유 변수로도, 종속 변수로도 나타날 수 있다. 예를 들어

P(x) \implies \forall x Q(x)

에서 첫 번째

x

는 자유 변수이고, 두 번째

x

는 종속 변수이다. (

fr(P(x) \implies \forall x Q(x)) = fr(P(x)) \cup fr(\forall x Q(x)) = \{x\} \cup (fr(Q(x)) - \{x\}) = \{x\} \cup (\{x\} - \{x\}) = \{x\} \cup \emptyset = \{x\}

)

자유 변수를 전혀 포함하지 않는 논리식, 즉

fr(\phi)=\varnothing

인 논리식

\phi

를 문장(sentence|문장^영어) 또는 닫힌 논리식(closed formula|닫힌 논리식^영어)이라고 한다. 문장은 특정 해석이 주어졌을 때 명확한 진릿값(참 또는 거짓)을 가진다. 예를 들어

\forall x \exists y (x = y)

는 문장이지만,

x = y

는

fr(x=y) = \{x, y\} \neq \emptyset

이므로 문장이 아니다.

2. 2. 공리와 추론 규칙

1차 논리의 증명 이론은 다양한 방식으로 공리화할 수 있다. 예를 들어 다비트 힐베르트의 힐베르트 체계( Hilbert system^영어)나, 게르하르트 겐첸의 시퀀트 계산( sequent calculus^영어)이나 자연 연역( natural deduction^영어) 등을 사용할 수 있다. 이 외에도 해석표 방법( Method of analytic tableaux^영어)이나 결정( Resolution^영어)과 같은 연역 체계가 존재한다. 이러한 체계들은 모두 연역이 유한한 구문적 객체라는 공통점을 가지며, 건전성(soundness)과 완전성(completeness)을 갖추고 있다. 즉, 증명 가능한 모든 식은 논리적으로 타당하며, 논리적으로 타당한 모든 식은 증명 가능하다.

추론 규칙은 특정 속성을 가진 공식(가정)으로부터 다른 공식(결론)을 도출할 수 있게 하는 규칙이다. 가정을 만족시키는 모든 해석이 결론도 만족시킬 때 그 규칙은 건전하다고 한다. 예를 들어, ''대입 규칙''은 항

t

와 변수

x

를 포함할 수 있는 공식

\phi

에 대해,

\phi

에서

x

의 모든 자유 발생을

t

로 대체한 결과인

\phi[t/x]

를 추론할 수 있게 한다. 단, 이 과정에서

t

의 자유 변수가 결합 변수가 되지 않도록 주의해야 한다.

=== 힐베르트 체계 ===

1차 논리를 힐베르트 체계를 사용하여 공리화하는 예를 살펴보자. 편의상 다음과 같은 기호만을 사용한다고 가정한다.

명제 논리에서는 함의 $\implies$ 와 부정 $\lnot$ 만을 사용한다. (논리합이나 논리곱 등 다른 기호는 이 둘로 표현 가능하다.)
술어 논리에서는 전칭 기호 $\forall$ 만을 사용한다. (존재 기호 $\exists$ 는 $\forall$ 만으로 표현 가능하다.)

이 체계는 다음과 같은 추론 규칙과 공리 기본꼴( axiom schema^영어)들을 사용한다. 여기서

\phi

,

\chi

,

\psi

는 임의의 논리식,

t

,

u

는 임의의 항,

x

는 임의의 변수를 뜻한다.

==== 추론 규칙 ====

'''전건 긍정의 형식''' (모두스 포넨스, Modus Ponens, MP):

\begin{matrix}\phi\implies\chi\\\phi\\\hline\chi\end{matrix}

'''일반화''' (Generalization, GEN):

\begin{matrix}\phi\\\hline\forall x\phi\end{matrix}

(단, 일반화 규칙에서

x

는

\phi

의 자유 변수여야 한다.)

==== 공리 기본꼴 ====

'''명제 논리 공리 기본꼴''':
* ㈂ $\phi \implies \left( \chi \implies \phi \right)$
* ㈃ $\left( \phi \implies \left( \chi \implies \psi \right) \right) \implies \left( \left( \phi \implies \chi \right) \implies \left( \phi \implies \psi \right) \right)$
* ㈄ $\left ( \lnot \phi \implies \lnot \chi \right) \implies \left( \chi\implies \phi \right)$
'''술어 논리 추가 공리 기본꼴''':
* ㈅ $\forall x\phi\implies\phi[t/x]$ (단, $\phi$ 에서 $t$ 가 $x$ 에 치환 가능해야 한다. 즉, $t$ 의 자유 변수가 치환 과정에서 $\phi$ 내의 양화사에 의해 속박되지 않아야 한다.)
* ㈆ $\forall x\left(\phi\implies\chi\right) \implies \left( \forall x\phi \implies \forall x\chi\right)$
'''등호에 관한 공리''' (언어에 등호 기호 $=$ 가 포함될 경우):
* ㈇ $x = x$ (반사성)
* ㈈ $\left(t=u\right) \implies \left( \phi[t/x] \implies \phi[u/x] \right)$ (라이프니츠의 법칙, 치환 속성. 단, $x$ 는 $\phi$ 의 자유 변수여야 한다.)^[26]

여기서

\phi[t/x]

는 논리식

\phi

에 등장하는 모든 자유 변수

x

를 항

t

로 대체하여 얻는 논리식을 뜻한다. 예를 들어, 체의 언어에서

\text{“}\lnot(x=2)\land\left(\forall xx=y)\right)\lor x=3\text{”}

라는 논리식에

[(1+1)/x]

치환을 적용하면

\text{“}\lnot\left((1+1)=2\right)\land\left(\forall xx=y)\right)\lor 1+1=3\text{”}

이 된다. 이때, 논리식 내부의 ‘

\forall xx=y

’ 부분에서

x

가 치환되지 않는 이유는 이 부분에서

x

가 종속 변수이기 때문이다.

등호에 관한 공리 ㈇과 ㈈로부터 대칭성(

x = y \implies y = x

)^[27]과 추이성(

(x = y \land y = z) \implies x = z

)^[28]과 같은 다른 등호의 속성들을 증명할 수 있다.

=== 기타 연역 체계 ===

힐베르트 체계 외에도 다른 연역 체계들이 있다.

'''자연 연역''': 힐베르트 체계와 유사하게 추론이 공식의 유한한 목록이지만, 논리적 공리 대신 추론 규칙을 더 많이 사용하여 증명에서 공식의 논리 연결사를 조작한다.
'''시퀀트 계산''':^[25] 자연 연역의 성질을 연구하기 위해 개발되었으며, 단일 공식 대신 $A_1, \ldots, A_n \vdash B_1, \ldots, B_k$ 형태의 시퀀트(sequent)를 사용한다. 이는 $(A_1 \land \cdots\land A_n)$ 가 $(B_1\lor\cdots\lor B_k)$ 를 함축한다는 의미를 나타낸다.
'''해석표 방법''':
명제 논리식 (a ∨ ¬b) ∧ b) → a에 대한 테이블로 증명
유도가 공식 목록이 아닌 트리 형태를 가진다. 공식 A를 증명하기 위해 A의 부정 $\lnot A$ 가 충족 불가능함을 보이려고 시도한다. 트리는 루트에 $\lnot A$ 를 두고 공식의 구조에 따라 분기한다.
'''결정''': 단일 추론 규칙인 해결 규칙과 일치를 사용하여, 공식의 부정이 불만족스러움을 보여 공식을 증명한다. 주로 자동 정리 증명에 사용되며, 적용 전에 공식을 스콜렘화하여 절(clause) 형태로 변환해야 한다.

형식적 증명은 논리식의 집합

\Sigma

에 속하는 논리식과 논리 공리로부터 추론 규칙을 유한 번 적용하여 특정 논리식

\phi

를 얻는 과정이다.

\Sigma

로부터

\phi

의 증명이 존재할 때,

\phi

는

\Sigma

로부터 '''증명 가능'''하다고 하며

\Sigma\vdash\phi

로 표기한다.

2. 3. 의미론

1차 논리 언어의 '''의미론'''이란 그 언어의 문장들에 대하여 참인지 여부를 일관적으로 부여하는 구조이다. 이는 보통 모형으로 주어진다. 1차 논리의 의미론은 형식 언어의 해석에 대한 연구인 형식 의미론의 일부이다.

=== 모형 ===

1차 논리의 의미론은 보통 모형 (model) 또는 구조 (structure)로 주어진다. 주어진 연산 집합

I

와 관계 집합

J

을 갖는 1차 논리 언어

\mathcal L_{I,J}

가 주어졌다고 하자. 그렇다면, 이 언어의 '''모형'''

M

은 다음 요소로 구성된다.

'''논의 영역''' (domain of discourse 또는 universe) $D$ : 어떤 종류의 "객체"들의 공집합이 아닌 집합이다. $|M|$ 으로 표기하기도 한다.
'''해석 함수''' (interpretation function) $I$ (또는 $F$ ): 언어의 비논리적 기호(술어 기호, 함수 기호, 상수 기호) 각각에 의미를 부여한다.
''n''항 술어 기호 $P$ 의 해석 $I(P)$ (또는 $P^M$ ): $D$ 의 원소들로 이루어진 ''n''-튜플들의 집합( $D^n$ 의 부분집합)으로, 이 술어가 참이 되는 튜플들의 모임이다. 또는 $D^n$ 에서 $\{\mathrm{참, 거짓}\}$ 으로 가는 부울 값 함수로 볼 수도 있다.
''n''항 함수 기호 $f$ 의 해석 $I(f)$ (또는 $f^M$ ): $D^n$ 에서 $D$ 로 가는 함수이다.
상수 기호 $c$ 의 해석 $I(c)$ (또는 $c^M$ ): $D$ 의 특정 원소이다. (0항 함수로 볼 수도 있다.)

예를 들어, 논의 영역

D

가 정수의 집합일 때, 2항 함수 기호 '+'는 덧셈 함수로, 상수 기호 '0'은 정수 0으로, 2항 술어 기호 '<'는 "보다 작음" 관계로 해석될 수 있다.

=== 참값의 할당 ===

모형

M

과 각 변수에 논의 영역의 원소를 대응시키는 변수 할당 (variable assignment)

s

(또는

\mu

)가 주어지면, 1차 논리의 각 항(term)과 논리식(formula)의 참 또는 거짓 여부를 결정할 수 있다.

먼저, 각 항

t

는 변수 할당

s

하에서 논의 영역

D

의 특정 원소

t^M(s)

로 평가된다.

변수 $x$ 의 값은 $s(x)$ 이다.
상수 $c$ 의 값은 $c^M$ 이다.
항 $t_1, \dots, t_n$ 의 값이 각각 $d_1, \dots, d_n$ 일 때, 함수 적용 $f(t_1, \dots, t_n)$ 의 값은 $f^M(d_1, \dots, d_n)$ 이다.

다음으로, 모형

M

과 변수 할당

s

하에서 논리식

\phi

가 참인지 여부, 즉 "

M

이

s

하에서

\phi

를 만족한다"(

M \models \phi [s]

또는

M(\phi, s)=1

로 표기)는 재귀적으로 정의된다. 이는 타르스키의 진리 정의 또는 T-스키마라고도 불린다.

'''원자 논리식''':
$t_1 = t_2$ 는 $t_1$ 과 $t_2$ 가 $s$ 하에서 같은 값으로 평가될 때 참이다.
$P(t_1, \dots, t_n)$ 은 각 $t_i$ 의 값 $v_i = t_i^M(s)$ 에 대해 튜플 $\langle v_1, \dots, v_n \rangle$ 이 술어 $P$ 의 해석 $P^M$ 에 속할 때 참이다.
'''논리 연결사''': $\neg \phi$ , $\phi \land \psi$ , $\phi \lor \psi$ , $\phi \rightarrow \psi$ , $\phi \leftrightarrow \psi$ 등의 진리값은 명제 논리에서와 같이 각 부분 논리식의 진리값과 연결사의 진리표에 따라 결정된다.
'''양화사''':
'''존재적 양화''': $\exists x \phi(x)$ 는 논의 영역 $D$ 에 속하는 어떤 원소 $m$ 에 대해, 변수 $x$ 에 $m$ 을 할당하고 나머지 변수는 $s$ 와 동일하게 할당한 새로운 할당 $s[x|m]$ 하에서 $\phi(x)$ 가 참일 때, 그리고 오직 그럴 때만 참이다. 즉, $\phi(x)$ 를 만족하는 $x$ 가 영역 안에 존재할 때 참이다.
'''보편적 양화''': $\forall x \phi(x)$ 는 논의 영역 $D$ 의 모든 원소 $m$ 에 대해, 할당 $s[x|m]$ 하에서 $\phi(x)$ 가 참일 때, 그리고 오직 그럴 때만 참이다. 즉, 영역 안의 모든 $x$ 가 $\phi(x)$ 를 만족할 때 참이다.

만약 논리식

\phi

가 자유 변수를 갖지 않는 문장(sentence)이라면, 그 참값은 변수 할당

s

에 의존하지 않는다. 이 경우, 문장

\phi

가 모형

M

에서 참이면 "

M

이

\phi

를 만족한다" 또는 "

M

이

\phi

의 모형이다"라고 말하며,

M \models \phi

로 표기한다.^[20] 어떤 모형에서 참인 문장을 '만족가능한'(satisfiable) 문장이라고 한다.

=== 논리적 타당성과 귀결 ===

'''논리적 타당성''' (Logical validity): 어떤 논리식 $\phi$ 가 모든 가능한 모형 $M$ 과 모든 변수 할당 $s$ 에 대해 참일 때 ( $M \models \phi [s]$ ), $\phi$ 는 논리적으로 타당하다고(logically valid) 한다.^[22] 이는 명제 논리의 토톨로지에 해당한다. 타당한 문장은 $\vDash \phi$ 로 표기한다.
'''논리적 귀결''' (Logical consequence): 문장들의 집합 $\Sigma$ 와 문장 $\phi$ 에 대해, $\Sigma$ 에 속하는 모든 문장을 만족하는 임의의 모형 $M$ 이 항상 $\phi$ 도 만족할 때, $\phi$ 는 $\Sigma$ 의 논리적 귀결이라고 하며, $\Sigma \vDash \phi$ 로 표기한다. 이는 $\Sigma$ 가 $\phi$ 를 논리적으로 함축(imply)함을 의미한다.
'''논리적 동치''' (Logical equivalence): 두 논리식 $\phi$ 와 $\psi$ 가 모든 모형과 할당에 대해 동일한 진리값을 가질 때, 즉 $\{\phi\} \vDash \psi$ 이고 $\{\psi\} \vDash \phi$ 일 때, 서로 논리적으로 동치라고 한다. 이는 $\phi \leftrightarrow \psi$ 가 논리적으로 타당한 것과 같다.

=== 주요 성질 ===

1차 논리의 의미론은 다음과 같은 중요한 성질들을 만족한다.

'''콤팩트성 정리''' (Compactness theorem): 1차 논리 문장들의 집합 $\Sigma$ 가 모형을 가질 필요충분조건은 $\Sigma$ 의 모든 유한 부분집합이 모형을 가지는 것이다.^[29] 이는 어떤 문장이 무한한 공리 집합의 논리적 귀결이라면, 실제로는 그 공리들 중 유한 개의 논리적 귀결임을 의미한다. 이 정리는 모형 이론에서 모형을 구성하는 기본적인 도구로 사용된다. 예를 들어, 임의로 큰 유한 모형을 갖는 이론은 반드시 무한 모형도 가져야 함을 보이는데 사용될 수 있다.
'''뢰벤하임-스콜렘 정리''' (Löwenheim–Skolem theorem): 셀 수 있는(countable) 언어로 된 1차 논리 이론이 무한 모형을 가진다면, 그 이론은 모든 무한한 기수 크기의 모형을 가진다. 이는 1차 논리로는 무한 구조의 크기를 정확히 특정할 수 없음을 의미한다. 예를 들어, 실수 집합만을 유일한 모형으로 갖는 1차 이론은 존재할 수 없다. 실수 모형이 있다면, 셀 수 있는 모형이나 더 큰 기수의 모형도 존재해야 하기 때문이다. 집합론에 적용될 경우 스콜렘의 역설과 같은 흥미로운 결과를 낳는다.

이러한 정리들은 1차 논리의 표현력과 한계를 보여주는 중요한 결과들이다.

3. 성질

1차 논리는 여러 중요한 메타논리적 성질을 가진다. 이는 특정 이론이 아닌 1차 논리 자체의 일반적인 속성으로, 1차 이론의 모형을 구성하는 기본적인 도구를 제공한다.

명제의 집합 Σ가 주어졌을 때, Σ로부터 명제 φ를 증명할 수 있다는 것( $\Sigma\vdash\varphi$ )과, Σ를 만족하는 모든 모형이 φ도 만족한다는 것( $\Sigma \vDash \varphi$ , 즉 φ가 Σ의 논리적 귀결이라는 것)은 다음과 같은 관계를 가진다.

'''건전성''': 증명 가능한 모든 명제는 논리적 귀결이다. 즉, $\Sigma\vdash\varphi \Longrightarrow \Sigma \vDash \varphi$ 이다.
'''완전성''': 모든 논리적 귀결은 증명 가능하다. 즉, $\Sigma\vDash\varphi \Longrightarrow \Sigma \vdash \varphi$ 이다.

쿠르트 괴델이 1929년에 증명한 괴델의 완전성 정리에 따르면, 고전적인 1차 술어 논리는 건전성과 완전성을 모두 만족한다. 이는 1차 논리에 대해 건전하고, 완전하며, 효과적인 연역 체계가 존재함을 의미하며, 따라서 1차 논리적 귀결 관계는 유한한 증명 가능성으로 포착될 수 있다. 이는 1차 논리적 귀결이 반결정가능하다는 것을 의미한다. 즉, 어떤 명제가 논리적 귀결일 경우 이를 확인할 수 있는 절차는 존재하지만, 논리적 귀결이 아닐 경우 이를 확인하고 멈추는 절차는 없을 수 있다.

주요 메타논리적 정리는 다음과 같다.

'''콤팩트성 정리''': 명제들의 집합이 모형을 가질 필요충분조건은 그 집합의 모든 유한 부분집합이 모형을 가지는 것이다.^[29] 이는 어떤 공식이 무한한 공리 집합의 논리적 귀결이라면, 그 공식은 그 공리들 중 유한한 개수의 논리적 귀결이라는 것을 의미한다. 이 정리는 모형 이론에서 모형을 구성하는 기본적인 방법을 제공하며, 어떤 구조들의 집합이 기본 클래스인지에 제한을 가한다. 예를 들어, 컴팩트성 정리에 따르면 임의로 큰 유한 모형을 갖는 모든 이론은 무한 모형을 가지므로, 모든 유한 그래프들의 클래스는 기본 클래스가 될 수 없다.

'''뢰벤하임-스콜렘 정리''': 무한 모형을 가지는 (가산 언어의) 1차 이론은 임의의 무한 기수 크기의 모형을 가진다. 특히 하향 정리에 따르면, 무한 모형을 가지는 이론은 가산 무한 모형도 가진다. 이는 1차 논리로는 무한 구조의 크기를 정확히 고정할 수 없음을 의미한다. 예를 들어, 실수 전체 집합을 유일한 모형으로 가지는 1차 이론은 존재할 수 없다. 모든 무한 모형을 가지는 이론은 비표준 모델이라고 불리는 다른 크기의 모형들도 가진다.

'''결정 불가능성''': 1차 논리는 (언어에 2항 이상의 관계 기호가 있다면) 결정 불가능하다. 즉, 임의의 공식이 논리적으로 타당한지(모든 모형에서 참인지) 여부를 항상 결정할 수 있는 알고리즘은 존재하지 않는다. 이는 1936년 앨런 튜링과 1937년 알론조 처치가 독립적으로 증명하여, 다비드 힐베르트가 제기한 엔트샤이둥스프로블렘에 대한 부정적인 답을 제시했다. 이 결과는 1차 논리의 결정 문제와 정지 문제의 해결 불가능성 사이의 연관성을 보여준다.
* 그럼에도 불구하고, 1차 논리의 타당성은 준결정 가능하다. 즉, 주어진 공식이 타당할 경우 이를 확인하고 멈추는 알고리즘은 존재한다 (타당하지 않을 경우 멈추지 않을 수 있다).
* 반면, 명제 논리나 일항 술어 기호만 사용하는 일항 술어 논리와 같은 더 약한 논리 시스템이나, 1차 논리의 특정 부분집합(예: 보호된 조각, 이변수 논리, 베르나이스-셰엔핀켈 클래스, 기술 논리)은 결정 가능하다.

'''린드스트룀 정리'''(Lindström’s theorem^영어): 페르 린드스트롬(Per Lindström)은 1차 논리가 (가산) 콤팩트성 정리와 하향 뢰벤하임-스콜렘 정리를 만족시키는 가장 강력한 논리 체계임을 증명했다.^[42] 즉, 1차 논리보다 강력하면서 이 두 성질을 모두 만족하는 논리 시스템은 존재하지 않는다.

4. 예

1차 논리는 다양한 수학적 구조를 형식적으로 기술하는 데 사용될 수 있다. 몇 가지 예를 들면 다음과 같다.

집합론: 체르멜로-프렝켈 집합론은 오직 하나의 2항 관계 기호 $\in$ (원소 관계)만을 사용하여 대부분의 집합론적 명제를 표현할 수 있다.
체: 체의 구조는 덧셈( $+$ ), 곱셈( $\cdot$ ), 덧셈 역원( $-$ ) 연산과 상수 $0, 1$ 을 포함하는 1차 논리 언어로 정의된다. 예를 들어, $a+b$ 는 함수 표기 $\mathsf f_+(a,b)$ 에 해당한다.
순서체: 순서체는 체의 언어에 2항 관계 기호 $\le$ (작거나 같음)를 추가하여 정의된다. $a \le b$ 는 관계 표기 $\mathsf R_\le(a,b)$ 에 해당한다.
범주: 범주는 사상들의 합성을 나타내는 3항 관계 $\mathsf C(x,y,z)$ (즉, $x \circ y = z$ )와 사상의 정의역 및 공역을 나타내는 1항 연산 $\operatorname{dom}(-)$ , $\operatorname{codom}(-)$ 을 사용하여 1차 논리로 형식화될 수 있다. 이 이론의 모형은 작은 범주와 같다.
순서 있는 아벨 군: 이 구조는 상수 기호 0, 일항 함수 기호 −, 이항 함수 기호 +, 그리고 이항 관계 기호 ≤를 사용하는 언어로 표현된다.
예를 들어, $x + y$ 와 $x + y - z$ 는 이 언어에서의 항(term)이다.
$x + y = 0$ 와 $x + y - z \le x + y$ 는 원자 공식(atomic formula)이다.
$\forall x \forall y ( x + y \leq z) \to \forall x \forall y (x+y = 0)$ 와 같은 표현은 공식(formula)이며, 변수 $z$ 를 자유 변수로 갖는다.
아벨 군의 공리, 예를 들어 교환 법칙 $(\forall x)(\forall y)[x+ y = y + x]$ 도 이 언어로 표현된 문장(sentence)이다.

일반적으로, 특정 기호 집합(서명)에 대한 1차 이론은 그 기호들로 구성된 문장들의 집합인 공리들로 정의된다. 이러한 공리들로부터 이론 내에서 참인 다른 문장들을 논리적으로 유도할 수 있다. 주어진 이론의 모든 공리를 만족시키는 수학적 구조를 그 이론의 모델이라고 한다. 예를 들어, 페아노 산술의 모델 중 하나는 우리가 일상적으로 사용하는 자연수 체계이다. 하지만 뢰벤하임-스콜렘 정리에 따르면, 대부분의 1차 이론은 의도된 모델 외에도 여러 다른 비표준 모델을 가질 수 있다. 모델 이론은 이러한 모델들의 성질을 연구하는 분야이다.

이론의 중요한 성질로는 일관성 (모순을 증명할 수 없음)과 완전성 (모든 문장이나 그 부정을 증명할 수 있음)이 있다. 그러나 괴델의 불완전성 정리는 자연수 이론을 포함할 만큼 충분히 강력한 1차 이론은 동시에 일관적이면서 완전할 수는 없다는 것을 보여준다.

4. 1. 집합론

체르멜로-프렝켈 집합론의 언어는 하나의 2항 관계

\in

만을 포함하며, 아무런 연산을 갖지 않는다. 집합론에서 사용되는 대부분의 명제들은 이 언어로 나타낼 수 있다.

4. 2. 체와 순서체

체의 1차 논리 언어는 다음과 같이 정의된다.

기호 집합 $I=\{+,\cdot,-,0,1\}$
연산 기호의 항수: $m_+=m_\cdot=2$ (이항 연산), $m_-=1$ (일항 연산), $m_0=m_1=0$ (상수, 즉 0항 연산)
관계 기호 집합: $J=\varnothing$ (관계 기호 없음)

이 언어는 두 개의 이항 연산 기호(

+

,

\cdot

), 하나의 일항 연산 기호(

-

), 그리고 두 개의 상수 기호(

0

,

1

)를 포함한다. 등호 외의 다른 관계 기호는 사용하지 않는다. 일반적으로 함수 표기법

\mathsf f_+(a,b)

대신 중위 표기법

a+b

를 사용한다.

순서체의 1차 논리 언어는 체의 언어에 순서 관계를 추가하여 정의된다.

기호 집합 $I=\{+,\cdot,-,0,1\}$ (체와 동일)
연산 기호의 항수: $m_+=m_\cdot=2$ , $m_-=1$ , $m_0=m_1=0$ (체와 동일)
관계 기호 집합: $J=\{\le\}$
관계 기호의 항수: $n_\le=2$ (이항 관계)

순서체의 언어는 체의 연산 및 상수 기호와 더불어, 하나의 이항 관계 기호

\le

를 포함한다. 보통 관계 표기법

\mathsf R_\le(a,b)

대신 중위 표기법

a\le b

를 사용한다.

1차 논리에서 항의 집합은 다음 규칙에 따라 귀납적으로 정의된다.^[16]

변수: 모든 변수 기호는 항이다.
함수: 만약 ''f''가 ''n''항 함수 기호이고, ''t''₁, ..., ''t''_''n''이 항이라면, ''f''(''t''₁,...,''t''_''n'')은 항이다. 특히, 개별 상수를 나타내는 기호는 0항 함수 기호이므로 그 자체로 항이다.

위의 두 규칙을 유한 번 적용하여 만들 수 있는 표현식만이 항으로 인정된다. 예를 들어, 술어(관계) 기호를 포함하는 표현식은 항이 아니다.

수학에서 순서 있는 아벨 군의 언어를 예로 들어보자. 이 언어는 상수 기호 0, 일항 함수 기호 −, 이항 함수 기호 +, 그리고 이항 관계 기호 ≤를 가진다. 이 언어에서:

$x$ , $y$ , $z$ 가 변수일 때, $+(x, y)$ 와 $+(x, +(y, -(z)))$ 는 항이다. 이들은 보통 각각 $x + y$ 와 $x + y - z$ 로 표기한다.
$+(x, y) = 0$ 과 $\le(+(x, +(y, -(z))), +(x, y))$ 는 원자 공식(atomic formula)이다. 이들은 보통 각각 $x + y = 0$ 과 $x + y - z \le x + y$ 로 표기한다.
$(\forall x \forall y \, [\mathop{\leq}(\mathop{+}(x, y), z) \to \forall x\, \forall y\, \mathop{+}(x, y) = 0)]$ 는 공식(formula)이며, 보통 $\forall x \forall y ( x + y \leq z) \to \forall x \forall y (x+y = 0)$ 로 표기한다. 이 공식은 변수 $z$ 를 자유 변수로 가진다.

순서 있는 아벨 군의 공리들은 이 언어로 된 문장(자유 변수가 없는 공식)들의 집합으로 표현될 수 있다. 예를 들어, 군 연산이 교환 법칙을 만족한다는 공리는

(\forall x)(\forall y)[x+ y = y + x]

와 같이 표현된다.

4. 3. 범주

범주를 1차 논리 언어로 표현할 수 있다. 이 언어는 하나의 3항 관계와 두 개의 1항 연산으로 구성된다.

3항 관계: $\mathsf C(-,-,-)$
$\mathsf C(x,y,z)$ 는 사상 $x$ 와 $y$ 의 합성이 $z$ 임을 의미한다 ( $x\circ y=z$ ).
1항 연산:
$\operatorname{dom}(-)$ : 사상의 정의역을 나타낸다.
$\operatorname{codom}(-)$ : 사상의 공역을 나타낸다.

이 언어에서 변수들은 사상을 나타내며, 대상은 항등 사상으로 표현된다. 편의상, 특정 사상이 항등 사상(즉, 대상)임을 나타내는 술어

\mathsf{Obj}(x)

를 다음과 같이 정의할 수 있다.

:

\mathsf{Obj}(x)\iff \operatorname{dom}(x)=\operatorname{codom}(x)=x

이를 바탕으로, 범주의 1차 논리 이론은 다음 공리들로 구성된다.

$\operatorname{dom}(x)=x\iff\operatorname{codom}(x)=x$
의미: 어떤 사상이 자신의 정의역과 같다면, 그 사상은 자신의 공역과도 같으며, 그 역도 성립한다. 즉, 항등 사상의 두 가지 정의 방식이 동치임을 나타낸다.
$\mathsf{Obj}(\operatorname{dom}x)$
의미: 모든 사상의 정의역은 대상(항등 사상)이다.
$\mathsf{Obj}(\operatorname{codom}x)$
의미: 모든 사상의 공역은 대상(항등 사상)이다.
$\mathsf C(x,y,z)\implies\operatorname{dom} x=\operatorname{codom}y$
의미: 사상 $x$ 와 $y$ 를 합성할 수 있다면( $\mathsf C(x,y,z)$ ), $x$ 의 정의역은 $y$ 의 공역과 같아야 한다. 이는 사상 합성 가능성의 필요 조건이다.
$\mathsf C(x,y,z)\implies\operatorname{dom} y=\operatorname{dom} z$
의미: 합성 사상 $z$ ( $x \circ y$ )의 정의역은 $y$ 의 정의역과 같다.
$\mathsf C(x,y,z)\implies\operatorname{codom}x=\operatorname{codom}z$
의미: 합성 사상 $z$ ( $x \circ y$ )의 공역은 $x$ 의 공역과 같다.
$\mathsf C(x,y,a)\land\mathsf C(a,z,c)\land\mathsf C(y,z,b)\land\mathsf C(x,b,d)\implies c=d$
의미: 사상 합성은 결합 법칙을 만족한다. 즉, $(x \circ y) \circ z = x \circ (y \circ z)$ 이다. ( $a = x \circ y$ , $c = a \circ z$ , $b = y \circ z$ , $d = x \circ b$ )
$\mathsf{Obj}(x)\land\mathsf C(x,y,z)\implies y=z$
의미: 대상(항등 사상) $x$ 를 오른쪽에 합성하면 원래 사상 $y$ 가 된다 ( $x \circ y = y$ ).
$\mathsf{Obj}(y)\land\mathsf C(x,y,z)\implies x=z$
의미: 대상(항등 사상) $y$ 를 왼쪽에 합성하면 원래 사상 $x$ 가 된다 ( $x \circ y = x$ ).

이 공리 체계의 모형은 수학에서의 '''작은 범주''' 개념과 정확히 일치한다.

5. 역사

고틀로프 프레게가 1879년에 출판한 《개념 표기법》^[43]에서 사용한 논리는 현대적인 용어로는 2차 논리에 해당한다.^[45]^[46] 이후 1885년에 찰스 샌더스 퍼스는 처음으로 1차 논리와 2차 논리를 구분하였다.^[44]^[45]^[46] 퍼스는 1차 논리를 "1차 내포 논리"(first-intensional logic^eng)로, 2차 논리를 "2차 내포 논리"(second-intensional logic^eng)라고 명명했다.^[46]

에른스트 체르멜로는 처음에 2차 논리를 사용하여 집합론을 개발했다. 그러나 토랄프 스콜렘은 1922년에 체르멜로의 집합론을 1차 논리를 사용하여 재정의하였다.^[47]^[46]^[48]^[49] 스콜렘의 이러한 작업은 오늘날 널리 사용되는 체르멜로-프렝켈 집합론의 중요한 기반이 되었다.

제2차 세계 대전 이후, 1차 논리는 2차 논리나 유형 이론 등 다른 논리 체계들을 대신하여 수학의 통상적인 기반으로 자리 잡게 되었다.^[49]

6. 1차 술어 논리와 다른 논리와의 비교

일차 논리는 여러 다른 논리 체계와 비교될 수 있으며, 다양한 방식으로 확장되거나 변형될 수 있다. 이러한 확장된 논리들은 대부분 1차 논리의 기본적인 논리 연산자와 양화자를 포함하며 그 의미도 공유하지만, 추가적인 표현 능력을 갖는 경우가 많다. 예를 들어, 고차 논리는 술어나 관계 자체를 양화할 수 있게 하고, 무한 논리는 무한히 긴 문장을 다루며, 모달 논리는 가능성이나 필연성과 같은 양상을 표현한다.

1차 논리의 중요한 특징 중 하나는 특정 메타논리적 속성들을 만족한다는 점이다. 린드스트룀의 정리는 1차 논리가 뢰벤하임-스콜렘 하강 정리와 컴팩트성 정리를 모두 만족하는 논리 체계 중 하나이며, 이 두 정리를 모두 만족하는 더 강력한 논리 확장은 존재하지 않음을 보여준다. 즉, 1차 논리를 확장하여 이 두 정리를 동시에 만족시키는 논리는 없다. 이 정리를 정확히 이해하기 위해서는 논리가 만족해야 하는 여러 조건들을 고려해야 하지만, 핵심은 1차 논리가 표현력과 다루기 좋은 이론적 성질 사이에서 중요한 균형을 이룬다는 점이다.

또한, 1차 논리는 다른 수학적 구조와도 연결된다. 타르스키와 Givant는 순서쌍 구성을 갖는 1차 논리가 특정 형태의 관계 대수와 정확히 등가임을 증명했다. 이는 1차 논리의 구조와 표현력이 대수적 관점에서도 이해될 수 있음을 보여준다.

6. 1. 명제 논리와의 차이점

명제 논리는 문장을 구성하는 가장 기본적인 단위인 원자 명제를 하나의 '''명제 기호'''(예: ''p'', ''q'')로 나타낸다. 예를 들어 "소크라테스는 철학자이다"와 "플라톤은 철학자이다"라는 두 문장이 있다면, 명제 논리에서는 이들을 각각 별개의 기호 ''p''와 ''q''로 취급하며, 문장 내부의 구조("...는 철학자이다")는 분석하지 않는다.^[6]

반면, 1차 논리(또는 1차 술어 논리)는 문장의 내부 구조를 분석한다. 가장 기본적인 명제를 '''원자 술어식'''으로 나타내는데, 이는 개체의 속성이나 개체 간의 관계를 나타내는 '''술어 기호'''(

P

)와 개체를 지칭하는 '''항'''(

t_1,\,\cdots,\,t_n

)으로 구성된

P(t_1,\,\cdots,\,t_n)

형태의 표현이다. 앞선 예시에서 "철학자이다"라는 속성을

\text{isPhil}

이라는 술어 기호로, "소크라테스"와 "플라톤"을 각각 상수 기호

a

,

b

(또는 그냥 이름 그대로 사용)라는 항으로 나타내면, 두 문장은

\text{isPhil}(a)

와

\text{isPhil}(b)

처럼 표현된다. 이를 통해 "어떤 대상

x

는 철학자이다"라는 공통된 형태

\text{isPhil}(x)

를 파악할 수 있다.^[7] "''x''는 철학자이다"와 같은 식의 참/거짓 여부는 변수 ''x''가 어떤 개체를 나타내는지, 그리고 "철학자이다"라는 술어가 어떻게 해석되는지에 따라 달라진다.^[18]

명제 논리에는 없는 1차 논리의 또 다른 중요한 특징은 '''양화'''(quantification) 개념이다. 명제 논리만으로는 다음과 같은 추론의 타당성을 형식적으로 다루기 어렵다.

: 모든 사람은 죽는다.

: 소크라테스는 사람이다.

: 그러므로 소크라테스는 죽는다.

1차 논리는 "모든 …에 대해" 또는 "어떤 …에 대해"와 같은 표현을 다루기 위해 '''전칭 양화 기호'''(

\forall

, "모든")와 '''존재 양화 기호'''(

\exists

, "어떤 ...가 존재한다")를 도입한다. 이를 이용하면 "모든

x

에 대해

\phi

이다"는

\forall x\phi

로, "어떤

x

에 대해

\phi

이다"는

\exists x\phi

로 표현할 수 있다.

위의 추론 예시는 1차 논리에서 다음과 같이 형식화될 수 있다. (여기서

P(x)

는 "

x

는 사람이다",

Q(x)

는 "

x

는 죽는다",

a

는 "소크라테스"를 나타낸다고 하자.)

:

\forall x[P(x)\Rightarrow Q(x)]

(모든 x에 대해, x가 사람이면 x는 죽는다)

:

P(a)

(소크라테스는 사람이다)

:

Q(a)

(소크라테스는 죽는다)

이 형식화에서 결론

Q(a)

는 두 전제

\forall x[P(x)\Rightarrow Q(x)]

와

P(a)

의 '''논리적 귀결'''(logical consequence)이 된다. 즉, 전제들을 참으로 만드는 모든 해석(구조) 하에서는 결론도 반드시 참이 된다는 것을 보여줌으로써 추론의 타당성을 입증할 수 있다. 여기서 해석이란, 변수가 움직일 수 있는 대상들의 집합인 '''영역'''(universe, domain)을 설정하고, 각 술어 기호, 함수 기호, 상수 기호에 구체적인 의미(대상, 관계, 함수 등)를 부여하는 것을 말한다.

6. 2. 2차 술어 논리 및 고차 술어 논리

일차 논리는 개체(사물이나 대상)에 대해서만 양화(얼마나 많은지에 대한 표현)를 허용하지만, 술어(성질이나 관계)에 대해서는 양화를 허용하지 않는다. 예를 들어, "철학을 하는 어떤 사람(

a

)이 존재한다"는

\exists a ( \text{Phil}(a))

와 같이 표현할 수 있어 올바른 1차 논리 공식이지만, "어떤 성질(

\text{Phil}

)이 있어서, 그 성질을

a

가 만족한다"는

\exists \text{Phil} ( \text{Phil}(a))

와 같이 표현하는 것은 대부분의 1차 논리 형식화에서는 허용되지 않는다.

이차 논리는 이러한 1차 논리를 확장하여, 술어나 함수 자체에 대해서도 양화하는 것을 허용한다. 즉,

\exists \text{Phil} ( \text{Phil}(a))

와 같은 표현이 가능해진다. 더 나아가 고차 논리는 이차 논리보다 더 높은 타입에 대한 양화를 허용한다. 여기서 더 높은 타입이란 관계들 사이의 관계, 관계에서 또 다른 관계들의 관계로 가는 함수 등 더 복잡한 개념들을 포함한다. 따라서 '일차', '이차', '고차'라는 이름은 양화될 수 있는 대상의 타입을 구분하는 것이다.

1차 논리는 일반적으로 단 하나의 의미론만 연구되는 반면, 이차 논리에는 여러 가지 가능한 의미론이 존재한다. 이 중에서 이차 및 고차 논리에 가장 널리 사용되는 것은 완전 의미론이다.

이차 및 고차 논리는 추가적인 양화 기능과 완전 의미론 덕분에 1차 논리보다 더 강력한 표현 능력을 가진다. 예를 들어, 완전 의미론을 사용하는 이차 논리에서는 자연수나 실수의 집합을 유일하게 특징짓는 공리계를 만들 수 있다. 하지만 이러한 표현력 증가는 몇 가지 이론적 한계를 동반한다. 이차 및 고차 논리의 (의미론적) 논리적 귀결 관계는 알고리즘으로 참거짓을 판별하는 것이 불가능하다는 의미에서 반결정 불가능(undecidable)하다. 또한, 완전 의미론 하에서는 건전하면서도 완전한, 즉 모든 참인 문장을 증명할 수 있는 효과적인 연역 체계가 존재하지 않는다.

표현력이 높아진 대신, 이차 및 고차 논리는 1차 논리가 가진 몇 가지 중요한 이론적 성질들을 잃어버린다. 대표적으로 뢰벤하임-스콜렘 정리와 컴팩트성 정리는 완전 의미론을 사용하는 고차 논리에서는 더 이상 성립하지 않는다.

6. 3. 기타 논리

1차 논리에는 여러 변형이 존재한다. 일부는 의미론에 영향을 주지 않고 표기법만 변경하는 사소한 변형이지만, 다른 것들은 추가적인 양화사나 새로운 논리 기호를 통해 의미론을 확장하여 표현력을 크게 변화시킨다.

'''무한 논리''': 무한히 긴 문장을 허용하는 논리이다. 예를 들어, 무한히 많은 공식의 합이나 곱, 또는 무한히 많은 변수에 대한 양화를 허용할 수 있다. 이러한 무한 논리는 위상수학과 모델 이론 등 수학 분야에서 사용된다. 무한 공식은 유한한 문자열로 표현할 수 없으므로, 보통 트리 형태로 표현하고 구문 분석한다. 가장 일반적으로 연구되는 무한 논리는 ''L''_αβ로 표기하며, 여기서 α와 β는 기수 또는 ∞이다. 일반적인 1차 논리는 ''L''_ωω에 해당한다.
''L''_∞ω: 임의 개수의 합이나 곱을 허용하고, 변수 공급이 무제한이다.
''L''_κω: κ보다 작은 구성 요소를 갖는 합이나 곱을 허용한다. 예를 들어 ''L''_ω₁ω는 가산적인 합과 곱을 허용한다. 공식의 자유 변수 집합은 κ보다 작은 기수를 가질 수 있지만, 유한한 수의 변수만 양화사 범위 내에 있을 수 있다.^[34]
''L''_κ∞: 단일 전칭 양화사 또는 존재 양화사가 임의로 많은 변수를 동시에 묶을 수 있다.
''L''_κλ: λ보다 적은 변수에 대한 동시 양화와 κ보다 작은 크기의 합과 곱을 허용한다.

'''직관주의 논리''': 고전 논리와 달리 직관주의적 추론을 사용한다. 예를 들어, 이중 부정 제거 법칙(¬¬φ ⇔ φ)이 성립하지 않으며, ¬∀x.φ가 ∃x.¬φ를 함의하지 않을 수 있다.

'''모달 논리''': 가능성(possible, ◇)과 필연성(necessary, □)을 다루기 위한 모달 연산자를 추가한 논리이다. 표준 1차 논리가 단일 세계를 가정하는 것과 달리, 모달 논리는 여러 '가능세계'를 가정하고 각 세계마다 다른 진리값을 가질 수 있도록 한다. 각 가능한 세계는 자체적인 논의 영역(domain)을 가질 수 있으며, 술어의 외연(extension)은 각 세계에 따라 달라진다. 이를 통해 "φ는 필연적이다"(모든 가능세계에서 참) 또는 "φ는 가능하다"(어떤 가능세계에서 참)와 같은 명제를 형식화할 수 있다. 예를 들어, '알렉스는 철학자이지만(현실 세계), 수학자였을 수도 있고(다른 가능세계 1), 아예 존재하지 않았을 수도 있다(다른 가능세계 2)'와 같은 상황을 모델링할 수 있다.

'''1차 퍼지 논리''': 고전 명제 논리 대신 퍼지 논리를 기반으로 하는 1차 논리 확장이다.

'''부동점 논리''': 양의 연산자의 최소 부동점에 대한 폐쇄(closure)를 추가하여 1차 논리를 확장한다.^[35]

'''타입화된 1차 술어 논리''': 변수나 항에 '타입(type)' 또는 '종(sort)'을 도입하여, 변수가 가질 수 있는 값의 종류를 제한하는 논리이다. 타입 수가 유한하면 일반 1차 논리와 큰 차이가 없으며, 유한한 개수의 단항 술어와 몇몇 공리를 추가하여 타입을 기술할 수 있다.

'''고차 논리''': 1차 논리가 개별 대상에 대한 양화만 허용하는 것과 달리, 술어(속성)나 관계 자체에 대한 양화를 허용한다.
'''약 2차 술어 논리''': 유한한 개수의 부분집합에 대한 양화를 허용한다.
'''단항 2차 술어 논리''': 부분집합, 즉 단항 술어에 대한 양화만 허용한다.
'''2차 술어 논리''': 부분집합 및 관계, 즉 모든 술어에 대한 양화를 허용한다.
'''고차 술어 논리''': 술어를 인수로 받는 술어 등 더 일반화된 대상에 대한 양화를 허용한다.

'''새로운 양화자를 더한 1차 술어 논리''': 표준적인 전칭 양화사(∀, 모든)와 존재 양화사(∃, 어떤) 외에 "대부분의", "많은" 등과 같은 의미를 갖는 새로운 양화자(예: Qx)를 추가한다.

이러한 논리의 대부분은 1차 논리의 확장으로 볼 수 있으며, 1차 논리의 논리 연산자와 양화자를 포함하고 그 의미도 같다. 그러나 린드스트룀의 정리에 따르면, 1차 논리를 확장하면서 동시에 뢰벤하임-스콜렘 하강 정리와 콤팩트성 정리를 모두 만족하는 논리는 존재하지 않는다.

한편, 1차 논리는 순서쌍 구성을 갖는 관계 대수와 등가임이 타르스키와 Givant에 의해 증명되었다.

7. 1차 술어 논리의 표현력

1차 술어 논리는 수학의 거의 모든 영역을 형식화하기에 충분한 표현력을 가지고 있다. 실제로, 현대의 표준적인 집합론 공리계인 ZFC는 1차 술어 논리를 이용하여 형식화되어 있으며, 수학의 대부분은 그렇게 형식화된 ZFC 안에서 수행할 수 있다. 즉, 수학의 명제는 1차 술어 논리의 논리식으로 기술할 수 있으며, 그렇게 논리식으로 기술된 수학의 정리는 ZFC의 공리로부터 '''형식적 증명'''(formal proof)이 존재한다. 이것이 1차 술어 논리가 중요시되는 이유 중 하나이다. 이 외에도 페아노 산술처럼 단독으로 형식화하는 이론도 있다.

8. 1차 술어 논리의 한계

1차 논리는 수학의 많은 부분을 형식화하고 컴퓨터 과학 등 다양한 분야에서 유용하게 사용되지만, 몇 가지 중요한 한계를 가지고 있다.

'''결정 불가능성'''

1차 논리는 결정 불가능(undecidable)하다. 즉, 어떤 임의의 1차 논리 문장이 주어졌을 때, 그 문장이 논리적으로 타당한지 (모든 해석에서 참인지) 아닌지를 항상 판별할 수 있는 일반적인 알고리즘이 존재하지 않는다.^[29] 이는 앨런 튜링과 알론조 처치가 1936년에 튜링 기계의 정지 문제와의 관련성을 통해 각각 독립적으로 증명한 중요한 결과이다. 구체적으로 말하면, 타당한 1차 논리 문장들의 괴델 수 집합은 귀납 함수가 아니다.

하지만 1차 논리의 타당성 문제는 '''준결정 가능'''(semi-decidable)하다. 즉, 어떤 문장이 타당하다면 유한한 시간 안에 그렇다는 것을 확인할 수 있는 알고리즘(증명 절차)은 존재한다. 그러나 문장이 타당하지 않은 경우에는 알고리즘이 영원히 끝나지 않을 수도 있다. 타당한 문장들의 괴델 수 집합은 귀납 가산 집합이다.

이러한 결정 불가능성 때문에, 실제 응용에서는 모든 변수를 2개로 제한하거나 특정 종류의 한정사(예: 계수 한정사 $\exists^{\ge n}$ , $\exists^{\le n}$ )만 사용하는 등, 결정 가능한 1차 논리의 단편(fragment)들을 연구하기도 한다.^[30] 예를 들어, 모든 술어 기호가 1개의 대상만을 받는 1변수 술어(monadic predicate)로만 이루어진 1차 논리는 결정 가능하다.

'''무한 구조의 표현 한계: 뢰벤하임-스콜렘 정리와 범주성'''

뢰벤하임-스콜렘 정리는 1차 논리가 무한한 대상들의 구조를 다룰 때 갖는 근본적인 한계를 보여준다. 이 정리에 따르면, 만약 어떤 1차 이론(공리들의 집합)이 무한 모형(model, 이론을 만족시키는 구조)을 하나라도 가진다면, 그 이론은 크기가 다른 임의의 무한 모형도 반드시 가진다.

이는 1차 논리로는 특정 무한 구조, 예를 들어 자연수의 집합( $\mathbb{N}$ )이나 실수의 집합( $\mathbb{R}$ )을 유일한 모형으로 갖도록 정확히 특정할 수 없음을 의미한다. 예를 들어, 자연수에 대한 페아노 공리계(1차 논리 버전)는 우리가 생각하는 표준적인 자연수 구조 외에도 다른 비표준 모형들을 허용한다. 마찬가지로, 실수의 완비성을 표현하는 공리는 1차 논리로 표현할 수 없기 때문에, 실수를 유일한 모형으로 갖는 1차 이론은 존재하지 않는다. 어떤 이론이 실수를 모형으로 가진다면, 그 이론은 실수와는 다른 비표준 모형도 반드시 가지게 된다.

이처럼 1차 논리 이론은 무한 모형에 대해 범주적(categorical)이 될 수 없다. 즉, 그 이론을 만족하는 모든 무한 모형들이 서로 동형(isomorphic, 구조적으로 동일함)이 되도록 만들 수 없다. 스콜렘의 역설은 이 정리를 집합론의 공리계(예: ZFC)에 적용했을 때 나타나는 역설적인 상황을 가리킨다.

무한 논리나 고계 논리와 같은 더 강력한 논리 체계에서는 자연수나 실수에 대한 범주적 공리화가 가능하지만, 이러한 표현력 증가는 대가를 수반한다. 린드스트룀 정리에 따르면, 1차 논리보다 강력하면서 동시에 컴팩트성 정리와 하향 뢰벤하임-스콜렘 정리(모든 무한 모형은 더 작은 크기의 무한 모형을 가짐)를 모두 만족하는 논리 체계는 존재할 수 없다.

'''컴팩트성 정리와 표현력의 한계'''

컴팩트성 정리는 1차 논리의 중요한 성질 중 하나로, 어떤 논리식들의 (무한할 수 있는) 집합이 모형을 가질 필요충분조건은 그 집합의 모든 유한한 부분집합이 모형을 가지는 것이라고 말한다.^[29] 이 정리는 모델 이론에서 모형을 구성하는 강력한 도구이지만, 동시에 1차 논리의 표현력에 제약을 가하기도 한다.

예를 들어, 컴팩트성 정리를 이용하면 "유한하다"는 성질을 1차 논리로 표현할 수 없음을 보일 수 있다. 만약 어떤 이론이 임의로 큰 유한 모형들을 가진다면, 컴팩트성 정리에 의해 그 이론은 반드시 무한 모형도 가져야 한다. 따라서 모든 유한 그래프들의 집합과 같이, 정확히 유한한 구조들만으로 이루어진 클래스는 1차 논리로 정의될 수 없다(기본 클래스가 아니다).

또한, 그래프 이론에서의 연결성(connectedness)과 같은 중요한 개념도 1차 논리로는 완전히 표현할 수 없다. 즉, 그래프의 두 노드 ''x''와 ''y'' 사이에 경로가 존재한다는 것을 나타내는 단일 1차 논리 공식 $\phi(x, y)$ 는 존재하지 않는다. 연결성은 2계 논리와 같은 더 강력한 논리에서는 표현 가능하지만, 1차 논리의 표현력을 넘어선다.

'''자연어 표현의 한계'''

1차 논리는 "모든 사람은 죽는다" ( $\forall x (\text{사람}(x) \rightarrow \text{죽는다}(x))$ ) 와 같이 자연어의 많은 단순한 문장 구조를 형식화하는 데 유용하며, 인공지능의 지식 표현 분야 등에서 기초적인 언어로 활용된다. 그러나 더 복잡하고 미묘한 자연어의 특징들을 포착하는 데에는 명확한 한계가 있다. 자연어를 제대로 분석하기 위해서는 1차 논리보다 훨씬 풍부한 구조를 가진 논리 체계가 필요하다.

다음은 1차 논리로 표현하기 어려운 자연어 구조의 몇 가지 예시이다.

유형	예시	설명
속성에 대한 양화	존이 자기 만족스러우면, 그에게는 피터와 공통점이 적어도 하나 있다.	"공통점이 적어도 하나 있다"는 것은 존과 피터가 공유하는 속성이 존재한다는 의미( $Zj \rightarrow \exists X(Xj \land Xp)$ )이다. 이는 속성(술어) 자체에 대한 양화를 필요로 하는데, 표준 1차 논리는 대상에 대해서만 양화할 수 있고 속성에 대해서는 양화할 수 없다.
속성에 대한 양화	산타클로스는 사디스트의 모든 속성을 가지고 있다.	이는 사디스트가 가진 모든 속성을 산타클로스도 가진다는 의미( $\forall X((\forall x(\text{사디스트}(x) \rightarrow Xx)) \rightarrow Xs)$ )로, 역시 속성에 대한 양화가 필요하다.
술어 부사	존은 빨리 걷고 있다.	빨리는 동사 걷다를 수식하는 부사이다. 이를 단순히 존은 걷는다와 존은 빠르다의 논리곱( $Wj \land Qj$ )으로 분석하는 것은 부사의 의미를 제대로 포착하지 못한다. 부사는 사건이나 행위의 방식을 나타내며, 이는 사건 의미론(event semantics) 등 더 복잡한 분석틀을 요구할 수 있다.
관계 형용사	점보는 작은 코끼리이다.	작은은 절대적인 크기를 나타내는 것이 아니라, 코끼리라는 범주 내에서의 상대적인 크기를 나타내는 관계 형용사이다. 이를 단순히 점보는 작다와 점보는 코끼리이다의 논리곱( $Sj \land Ej$ )으로 분석하면 의미가 왜곡될 수 있다.
술어 부사 수식어	존은 매우 빨리 걷고 있다.	—
관계 형용사 수식어	점보는 엄청나게 작다.	"엄청나게"와 같은 표현은 "작은"과 같은 관계 형용사에 적용될 때 "엄청나게 작은"과 같은 새로운 복합 관계 형용사를 만든다.
전치사	메리는 존 옆에 앉아 있다.	"옆에"라는 전치사는 "존"에 적용될 때 "존 옆에"라는 술어 부사를 만든다.

9. 1차 술어 논리의 응용

1차 논리는 컴퓨터 과학의 여러 분야에서 중요한 이론적 기반이자 실용적인 도구로 활용된다. 대표적인 응용 분야로는 자동 정리 증명과 형식적 검증이 있다.

자동 정리 증명: 컴퓨터 프로그램을 이용하여 수학적 정리의 증명을 자동으로 생성하거나 검증하는 연구 분야이다. 1차 논리는 정리와 증명을 형식적으로 표현하는 데 사용된다.
형식적 검증: 소프트웨어나 하드웨어 시스템이 주어진 형식 명세를 정확히 만족하는지 수학적으로 검증하는 기술이다. 1차 논리는 시스템의 속성이나 동작을 명확하게 기술하고 추론하는 데 활용된다.

이 외에도 1차 논리는 데이터베이스 이론, 인공지능, 계산 언어학 등 다양한 분야에서 기초적인 형식 언어 및 추론 시스템으로 응용되고 있다.

9. 1. 자동 정리 증명

자동 정리 증명은 컴퓨터 프로그램을 사용하여 수학적 정리의 유도(공식적인 증명)를 찾고 검색하는 분야이다.^[36] 유도를 찾는 과정은 탐색 공간이 매우 클 수 있기 때문에 어려운 작업이다. 이론적으로는 모든 가능한 유도를 탐색할 수 있지만, 수학에서 다루는 많은 시스템에서는 계산적으로 불가능하다. 따라서 단순히 모든 경우를 탐색하는 대신, 더 짧은 시간 안에 유도를 찾기 위해 복잡한 휴리스틱 함수들이 개발되었다.^[37]

이와 관련된 분야로 증명 검증이 있는데, 이는 사람이 만든 증명이 정확한지 확인하기 위해 컴퓨터 프로그램을 사용하는 것이다. 복잡한 자동 정리 증명기와 달리, 증명 검증 시스템은 상대적으로 크기가 작아서 사람이 직접 확인하거나 자동 소프트웨어 검증을 통해 정확성을 검증할 수 있다. 이러한 검증 과정은 증명 검증기가 "정확하다"고 판정한 모든 유도가 실제로 정확하다는 신뢰를 주기 위해 필요하다.

증명 검증 시스템에는 여러 종류가 있다. Metamath와 같은 시스템은 완전한 유도 과정을 입력으로 요구한다. 반면 Mizar나 Isabelle과 같은 시스템은 잘 구조화된 증명 개요(매우 길고 상세할 수 있음)를 입력받아, 간단한 증명 탐색이나 알려진 의사 결정 절차를 적용하여 누락된 부분을 채운다. 이후 결과 유도는 작은 핵심 "커널"을 통해 검증된다. 이러한 시스템들은 주로 수학자들이 상호작용하며 사용하도록 설계되었으며, 이를 증명 보조기라고 부른다. 또한, 이 시스템들은 1차 논리보다 더 강력한 형식 논리(예: 타입 이론)를 사용하기도 한다. 중요한 결과에 대한 1차 논리 증명은 사람이 직접 작성하기에는 매우 길기 때문에,^[38] 결과는 종종 여러 개의 보조 정리로 나누어 공식화되고, 각 보조 정리는 별도로 증명된다.

자동 정리 증명기는 컴퓨터 과학 분야에서 형식적 검증을 구현하는 데에도 활용된다. 이 경우, 정리 증명기는 형식 명세에 따라 프로그램이나 프로세서와 같은 하드웨어의 정확성을 검증하는 데 사용된다. 이러한 분석 작업은 시간과 비용이 많이 들기 때문에, 주로 오작동 시 심각한 인명 또는 재정적 손실을 초래할 수 있는 중요한 프로젝트에 적용된다.

모델 검증 문제에서는, 주어진 유한 구조가 1차 논리 공식을 만족하는지 판별하는 효율적인 알고리즘들이 알려져 있으며, 관련 계산 복잡도 경계도 연구되고 있다.

9. 2. 형식적 검증

자동 정리 증명기는 컴퓨터 과학에서 형식적 검증을 구현하는 데에도 사용된다. 형식적 검증은 형식 명세에 따라 프로그램 및 프로세서와 같은 하드웨어의 정확성을 검증하는 과정이다. 이러한 분석은 시간이 많이 걸리고 비용이 많이 들기 때문에, 일반적으로 오작동이 심각한 인적 또는 재정적 결과를 초래할 수 있는 프로젝트에 주로 사용된다.

모델 검증 문제의 경우, 효율적인 알고리즘을 통해 입력 유한 구조가 1차 논리 공식을 만족하는지 여부를 결정할 수 있으며, 이에 대한 계산 복잡도 경계도 알려져 있다.

참조

_[1] 웹사이트 First Order Logic http://people.sju.ed[...]
_[2] 서적 A New Introduction to Modal Logic https://books.google[...] Routledge
_[3] 서적 Undecidable Theories North-Holland
_[4] 서적 Introduction to Mathematical Logic https://books.google[...] Van Nostrand Reinhold
_[5] 간행물 Semantics for Existential Graphs
_[6] 웹사이트 Adventures in Foundations of Mathematics 1: Logical Reasoning https://bpb-us-w2.wp[...] 2023-07-28
_[7] 서적 Real-World Reasoning: Toward Scalable, Uncertain Spatiotemporal, Contextual and Causal Inference https://books.google[...] Atlantis Press
_[8] 서적 Representations of Commonsense Knowledge Morgan Kauffmann
_[9] 웹사이트 Predicate Logic https://brilliant.or[...] 2020-08-20
_[10] 웹사이트 Introduction to Symbolic Logic: Lecture 2 http://cstl-cla.semo[...] 2021-01-04
_[11] 서적 Introduction to Mathematical Logic Springer
_[12] 일반
_[13] 일반
_[14] 서적 Mathematische Logik mit Informatik-Anwendungen https://books.google[...] Springer
_[15] 서적 First-order Logic https://books.google[...] Dover Publications
_[16] 서적 Proof Theory
_[17] 일반
_[18] 서적 Mathematical Logic Harvard University Press
_[19] 일반
_[20] 일반
_[21] 서적 Set theory: An introduction to large cardinals
_[22] 서적 Mathematical Logic and Formalized Theories: A Survey of Basic Concepts and Results https://books.google[...] North-Holland Publishing Company
_[23] 서적 Relational Methods in Computer Science https://books.google[...] Springer
_[24] 서적 Mathematical Reviews American Mathematical Society
_[25] 웹사이트 PVS Prover Guide 7.1 http://pvs.csl.sri.c[...] 2020-08
_[26] 서적 First-Order Logic and Automated Theorem Proving https://books.google[...] Springer
_[27] 일반
_[28] 일반
_[29] 서적 An Introduction to Mathematical Logic https://books.google[...] Dover
_[30] 웹사이트 Description Logic: A Formal Foundation for Languages and Tools http://www.cs.ox.ac.[...]
_[31] 일반
_[32] 백과사전 Quantifiers and Quantification 2018-10-17
_[33] 서적 A Mathematical Introduction to Logic https://books.google[...] Academic Press
_[34] 일반
_[35] 서적 Computer Science Logic: 6th Workshop, CSL'92, San Miniato, Italy, September 28 - October 2, 1992. Selected Papers Springer-Verlag
_[36] 서적 First-Order Logic and Automated Theorem Proving https://books.google[...] Springer Science & Business Media 2012-12-06
_[37] 웹사이트 15-815 Automated Theorem Proving https://www.cs.cmu.e[...] 2024-01-10
_[38] 논문 The formalized proof of the prime number theorem. 2007
_[39] 일반텍스트 アリティの定義
_[40] 일반텍스트 수식 표기법에 대한 설명
_[41] 서적 The Blackwell Guide to Philosophical Logic Blackwell 2001-08
_[42] 저널 On extensions of elementary logic 1969-04
_[43] 서적 Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens http://gallica.bnf.f[...] Verlag von Louis Nebert 1879
_[44] 저널 On the algebra of logic: a contribution to the philosophy of notation 1885-01
_[45] 저널 Peirce the logician 1982
_[46] 서적 History and philosophy of modern mathematics http://mcps.umn.edu/[...] University of Minnesota Press 1988
_[47] 서적 Matematikerkongressen i Helsingfors den 4–7 Juli 1922, Den femte skandinaviska matematikerkongressen, Redogörelse Akademiska Bokhandeln 1923
_[48] 저널 On how logic became first-order http://www.hf.uio.no[...] 1996-12
_[49] 저널 The road to modern logic — an interpretation http://personal.us.e[...] 2016-07-29

본 사이트는 AI가 위키백과와 뉴스 기사,정부 간행물,학술 논문등을 바탕으로 정보를 가공하여 제공하는 백과사전형 서비스입니다.
모든 문서는 AI에 의해 자동 생성되며, CC BY-SA 4.0 라이선스에 따라 이용할 수 있습니다.
하지만, 위키백과나 뉴스 기사 자체에 오류, 부정확한 정보, 또는 가짜 뉴스가 포함될 수 있으며, AI는 이러한 내용을 완벽하게 걸러내지 못할 수 있습니다.
따라서 제공되는 정보에 일부 오류나 편향이 있을 수 있으므로, 중요한 정보는 반드시 다른 출처를 통해 교차 검증하시기 바랍니다.

문의하기 : help@durumis.com