분지 유형 이론
정의 > 논리식

분지 유형 이론의 유사 논리식(類似論理式, 영어: pseudoformula)은 다음과 같다.
n 항 관계 R 및 변수 또는 개체 p_{1},\dots ,p_{n} 에 대하여, R(p_{1},\dots ,p_{n}) 은 유사 논리식이다.
n=0일 경우 유사 논리식  R()은 0항 관계  R와 구분되어야 한다. 분지 유형 이론에서  n항 관계는 유사 논리식이 아니다.
변수 x 및 유한 개의 변수 또는 개체 또는 유사 논리식 p_{1},\dots ,p_{n} 에 대하여, x(p_{1},\dots ,p_{n}) 는 유사 논리식이다.
n=0일 경우 유사 논리식  x()은 변수  x와 구분되어야 한다. 분지 유형 이론에서 변수나 개체는 유사 논리식이 아니다.
유사 논리식  \phi ,\psi 에 대하여,  \phi \lor \psi 와  \lnot \phi 는 유사 논리식이다.
유사 논리식  \phi  및 그 자유 변수  x\in \operatorname {FVar} (\phi ) 및 분지 유형  \tau ^{d}에 대하여,  \forall x{:}\tau ^{d}\phi 는 유사 논리식이다.
유사 논리식의 집합을  {\mathcal {P}}라고 하자. 또한 각 유사 논리식  \phi 에 대하여,  \operatorname {Var} (\phi )가  \phi  속에 등장하는 모든 변수의 집합이라고 하고,
가  \phi 의 모든 자유 변수라고 하자.
문맥  \Gamma 에서 개체 또는 유사 논리식  \phi 가 분지 유형  \tau ^{d}를 갖는다는 것은  \Gamma \vdash \phi {:}\tau ^{d}로 표기하며, 다음과 같이 재귀적으로 정의된다. (여기서  \vdash \phi {:}\tau ^{d}는  \varnothing \vdash \phi {:}\tau ^{d}를 뜻한다.)
개체  a에 대하여,  \vdash a{:}\iota ^{0}이다.
n항 관계  R 및 개체  a_{1},\dots ,a_{n}에 대하여,  \vdash R(a_{1},\dots ,a_{n}){:}()^{1}이다.
(논리 연산) 문맥  \Gamma ,\Delta  및 유사 논리식  \phi ,\psi  및 분지 유형  (\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{m}})^{d},({\tau _{1}'}^{d_{1}'},\dots ,{\tau _{n}'}^{d_{n}'})^{d'}에 대하여, 만약  \Gamma \vdash \phi {:}(\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{m}})^{d}이며,  \Delta \vdash \psi {:}({\tau _{1}'}^{d_{1}'},\dots ,{\tau _{n}'}^{d_{n}'})^{d'}이며,  \max \operatorname {dom} (\Gamma )<\min \operatorname {dom} (\Delta )라면, \Gamma \cup \Delta \vdash \phi \lor \psi {:}(\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{m}},{\tau _{1}'}^{d_{1}'},\dots ,{\tau _{n}'}^{d_{n}'})^{\max\{d,d'\}} \Gamma \vdash \lnot \phi {:}(\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{m}})^{d}이다.
(한정) 문맥  \Gamma  및 유사 논리식  \phi  및  i\in \{1,\dots ,|{\operatorname {FVar} (\phi )}|\} 및 분지 유형  (\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{n}})^{d}에 대하여, 만약  \Gamma \cup \{x_{i}^{\phi }{:}\tau _{i}^{d_{i}}\}\vdash \phi {:}(\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{n}})^{d}라면, \Gamma \vdash \forall x_{i}^{\phi }{:}\tau _{i}^{d_{i}}\phi {:}(\tau _{1}^{d_{1}},\dots ,\tau _{i-1}^{d_{i-1}},\tau _{i+1}^{d_{i+1}},\dots ,\tau _{n}^{d_{n}})^{d}이다.
(매개 변수에 대한 추상화) 문맥  \Gamma  및 유사 논리식  \phi  및 그 개체이거나 유사 논리식인 매개 변수  \psi \in \operatorname {Par} (\phi )\cap ({\mathcal {A}}\cup {\mathcal {P}}) 및 분지 유형  (\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{n}})^{d},\tau _{n+1}^{d_{n+1}} 및 변수  y>\max \operatorname {dom} (\Gamma )에 대하여, 만약  \Gamma \vdash \phi {:}(\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{n}})^{d}이며  \Gamma \vdash \psi {:}\tau _{n+1}^{d_{n+1}}이라면, \{x{:}\tau ^{d}\in \Gamma \cup \{y{:}\tau _{n+1}^{d_{n+1}}\}|x\in \operatorname {Var} ((\phi )_{\Gamma ,\psi ,y})\}\vdash (\phi )_{\Gamma ,\psi ,y}{:}(\tau _{1}^{d_{1}},\dots ,\tau _{n+1}^{d_{n+1}})^{\max\{d,d_{n+1}+1\}}이다. 여기서  (\phi )_{\Gamma ,\psi ,y}는  \phi 에 등장하는  \psi 와 αΓ-동치인 각 매개 변수  \psi '를  y로 대체하여 얻는 유사 논리식이다. (《수학 원리》에서 이는  (\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{n}})^{d}가 술어적 분지 유형인 경우로 제한된다.)
(논리식에 대한 추상화) 문맥  \Gamma  및 유사 논리식  \phi  및 분지 유형  (\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{n}})^{d} 및 변수  y>\max \operatorname {dom} (\Gamma )에 대하여, 만약  \Gamma \vdash \phi {:}(\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{n}})^{d}이라면, \{x{:}\tau ^{d}\in \Gamma \cup \{y{:}(\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{n}})^{d}\}|x\in \operatorname {FVar} (\phi )\cup \{y\}\}\vdash y(x_{1}^{\phi },\dots ,x_{n}^{\phi }){:}(\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{n}},(\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{n}})^{d})^{d+1}이다. (이 경우 반드시  {|{\operatorname {FVar} (\phi )}|}=n임을 보일 수 있다.) (《수학 원리》에서 이는  (\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{n}})^{d}가 술어적 분지 유형인 경우로 제한된다.)
(치환) 문맥  \Gamma  및 자유 변수를 갖는 유사 논리식  \phi  및 개체 또는 유사 논리식  \psi  및 분지 유형  (\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{n}})^{d}에 대하여, 만약  \Gamma \cup \{x_{1}^{\phi }{:}\tau _{1}^{d_{1}}\}\vdash \phi {:}(\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{n}})^{d}이며,  \Gamma \vdash \psi {:}\tau _{1}^{d_{1}}라면, \{x{:}\tau ^{d}\in \Gamma \cup \{x_{1}^{\phi }{:}\tau _{1}^{d_{1}}\}|x\in \operatorname {Var} (\phi [\psi /x_{1}^{\phi }])\}\vdash \phi [\psi /x_{1}^{\phi }]{:}(\tau _{2}^{d_{2}},\dots ,\tau _{n}^{d_{n}})^{\max(\{d_{2},\dots ,d_{n}\}\cup \{e|\phi [\psi /x_{1}^{\phi }]=\cdots \forall x{:}\tau ^{e}\cdots \})+1}이다. (이 경우  \phi [\psi /x_{1}^{\phi }]는 반드시 정의됨을 보일 수 있다.)
(약화) 문맥  \Gamma ,\Delta  및 유사 논리식  \phi  및 분지 유형  \tau ^{d}에 대하여, 만약  \Gamma \vdash \phi {:}\tau ^{d}이며,  \Gamma \subseteq \Delta 라면,  \Delta \vdash \phi {:}\tau ^{d}이다.
(순열) 문맥  \Gamma  및 유사 논리식  \phi  및  i\in \{1,\dots ,|{\operatorname {FVar} (\phi )}|\} 및 분지 유형  (\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{n}})^{d} 및 변수  y>\max \operatorname {dom} (\Gamma )에 대하여, 만약  \Gamma \cup \{x_{i}^{\phi }{:}\tau _{i}^{d_{i}}\}\vdash \phi {:}(\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{n}})^{d}라면, \{x{:}\tau ^{d}\in \Gamma \cup \{x_{i}^{\phi }{:}\tau _{i}^{d_{i}},y{:}\tau _{i}^{d_{i}}\}|x\in \operatorname {Var} (\phi [y/x_{i}^{\phi }])\}\vdash \phi [y/x_{i}^{\phi }]{:}(\tau _{1}^{d_{1}},\dots ,\tau _{i-1}^{d_{i-1}},\tau _{i+1}^{d_{i+1}},\dots ,\tau _{n}^{d_{n}},\tau _{i}^{d_{i}})^{d}이다.
주어진 문맥 속에서, 유사 논리식의 분지 유형은 존재하지 않을 수 있으나, 만약 존재한다면 이는 유일하다. 주어진 유사 논리식은 서로 다른 문맥 속에서 서로 다른 분지 유형을 가질 수 있다. 유사 논리식  \phi 에 대하여,  \Gamma \vdash \phi {:}\tau ^{d}인 문맥  \Gamma 과  \tau ^{d}가 존재한다면,  \phi 를 논리식(論理式, 영어: formula)이라고 한다.