2.4.8: Proof-Theoretic Notions
- Page ID
- 121688
\( \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \)
\( \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} \)
\( \newcommand{\id}{\mathrm{id}}\) \( \newcommand{\Span}{\mathrm{span}}\)
( \newcommand{\kernel}{\mathrm{null}\,}\) \( \newcommand{\range}{\mathrm{range}\,}\)
\( \newcommand{\RealPart}{\mathrm{Re}}\) \( \newcommand{\ImaginaryPart}{\mathrm{Im}}\)
\( \newcommand{\Argument}{\mathrm{Arg}}\) \( \newcommand{\norm}[1]{\| #1 \|}\)
\( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\)
\( \newcommand{\Span}{\mathrm{span}}\)
\( \newcommand{\id}{\mathrm{id}}\)
\( \newcommand{\Span}{\mathrm{span}}\)
\( \newcommand{\kernel}{\mathrm{null}\,}\)
\( \newcommand{\range}{\mathrm{range}\,}\)
\( \newcommand{\RealPart}{\mathrm{Re}}\)
\( \newcommand{\ImaginaryPart}{\mathrm{Im}}\)
\( \newcommand{\Argument}{\mathrm{Arg}}\)
\( \newcommand{\norm}[1]{\| #1 \|}\)
\( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\)
\( \newcommand{\Span}{\mathrm{span}}\) \( \newcommand{\AA}{\unicode[.8,0]{x212B}}\)
\( \newcommand{\vectorA}[1]{\vec{#1}} % arrow\)
\( \newcommand{\vectorAt}[1]{\vec{\text{#1}}} % arrow\)
\( \newcommand{\vectorB}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \)
\( \newcommand{\vectorC}[1]{\textbf{#1}} \)
\( \newcommand{\vectorD}[1]{\overrightarrow{#1}} \)
\( \newcommand{\vectorDt}[1]{\overrightarrow{\text{#1}}} \)
\( \newcommand{\vectE}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash{\mathbf {#1}}}} \)
\( \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \)
\( \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} \)
\(\def\Atom#1#2{ { \mathord{#1}(#2) } }\)
\(\def\Bin{ {\mathbb{B}} }\)
\(\def\cardeq#1#2{ { #1 \approx #2 } }\)
\(\def\cardle#1#2{ { #1 \preceq #2 } }\)
\(\def\cardless#1#2{ { #1 \prec #2 } }\)
\(\def\cardneq#1#2{ { #1 \not\approx #2 } }\)
\(\def\comp#1#2{ { #2 \circ #1 } }\)
\(\def\concat{ { \;\frown\; } }\)
\(\def\Cut{ { \text{Cut} } }\)
\(\def\Discharge#1#2{ { [#1]^#2 } }\)
\(\def\DischargeRule#1#2{ { \RightLabel{#1}\LeftLabel{\scriptsize{#2} } } }\)
\(\def\dom#1{ {\operatorname{dom}(#1)} }\)
\(\def\Domain#1{ {\left| \Struct{#1} \right|} }\)
\(\def\Elim#1{ { {#1}\mathrm{Elim} } }\)
\(\newcommand{\Entails}{\vDash}\)
\(\newcommand{\EntailsN}{\nvDash}\)
\(\def\eq[#1][#2]{ { #1 = #2 } }\)
\(\def\eqN[#1][#2]{ { #1 \neq #2 } }\)
\(\def\equivclass#1#2{ { #1/_{#2} } }\)
\(\def\equivrep#1#2{ { [#1]_{#2} } }\)
\(\def\Exchange{ { \text{X} } }\)
\(\def\False{ { \mathbb{F} } }\)
\(\def\FalseCl{ { \lfalse_C } }\)
\(\def\FalseInt{ { \lfalse_I } }\)
\(\def\fCenter{ { \,\Sequent\, } }\)
\(\def\fdefined{ { \;\downarrow } }\)
\(\def\fn#1{ { \operatorname{#1} } }\)
\(\def\Frm[#1]{ {\operatorname{Frm}(\Lang #1)} }\)
\(\def\fundefined{ { \;\uparrow } }\)
\(\def\funimage#1#2{ { #1[#2] } }\)
\(\def\funrestrictionto#1#2{ { #1 \restriction_{#2} } }\)
\(\newcommand{\ident}{\equiv}\)
\(\newcommand{\indcase}[2]{#1 \ident #2\text{:}}\)
\(\newcommand{\indcaseA}[2]{#1 \text{ is atomic:}}\)
\(\def\indfrm{ { A } }\)
\(\def\indfrmp{ { A } }\)
\(\def\joinrel{\mathrel{\mkern-3mu}}\)
\(\def\lambd[#1][#2]{\lambda #1 . #2}\)
\(\def\Lang#1{ { \mathcal{#1} } }\)
\(\def\LeftR#1{ { {#1}\mathrm{L} } }\)
\(\def\len#1{ {\operatorname{len}(#1)} }\)
\(\def\lexists#1#2{ { \exists #1\, #2 } }\)
\(\def\lfalse{ {\bot} }\)
\(\def\lforall#1#2{ { \forall#1\, #2 } }\)
\(\newcommand{\lif}{\rightarrow}\)
\(\newcommand{\liff}{\leftrightarrow}\)
\(\def\Log#1{ { \mathbf{#1} } }\)
\(\def\ltrue{ {\top} }\)
\(\def\Id#1{ {\operatorname{Id}_#1} }\)
\(\def\Int{ {\mathbb{Z}} }\)
\(\def\Intro#1{ { {#1}\mathrm{Intro} } }\)
\(\def\mModel#1{ { \mathfrak{#1} } }\)
\(\newcommand{\mSat}[3][{}]{\mModel{#2}{#1}\Vdash{#3}}\)
\(\newcommand{\mSatN}[3][{}]{\mModel{#2}{#1}\nVdash{#3}}\)
\(\def\Nat{ {\mathbb{N}} }\)
\(\def\nicefrac#1#2{ {{}^#1/_#2} }\)
\(\def\num#1{ { \overline{#1} } }\)
\(\newcommand{\Obj}[1]{\mathsf{#1}}\)
\(\def\Rat{ {\mathbb{Q}} }\)
\(\def\Real{ {\mathbb{R}} }\)
\(\def\RightR#1{ { {#1}\mathrm{R} } }\)
\(\def\Part#1#2{ { \Atom{\Obj P}{#1, #2} } }\)
\(\def\pto{ { \hspace{0.1 cm}\to\hspace{-0.44 cm}\vcenter{\tiny{\hbox{|}}}\hspace{0.35 cm} } }\)
\(\def\PosInt{ {\mathbb{Z}^+} }\)
\(\def\Pow#1{ {\wp(#1)} }\)
\(\newcommand{\Proves}{\vdash}\)
\(\newcommand{\ProvesN}{\nvdash}\)
\(\def\Relbar{\mathrel{=}}\)
\(\newcommand{\Sat}[3][{}]{\Struct{#2}{#1}\vDash{#3}}\)
\(\newcommand{\SatN}[3][{}]{\Struct{#2}{#1}\nvDash{#3}}\)
\(\newcommand{\Sequent}{\Rightarrow}\)
\(\def\Setabs#1#2{ { \{#1:#2\} } }\)
\(\newcommand{\sFmla}[2]{#1\,#2}\)
\(\def\Struct#1{ {#1} }\)
\(\def\subst#1#2{ { #1/#2 } }\)
\(\def\Subst#1#2#3{ { #1[\subst{#2}{#3}] } }\)
\(\def\TMblank{ { 0 } }\)
\(\newcommand{\TMendtape}{\triangleright}\)
\(\def\TMleft{ { L } }\)
\(\def\TMright{ { R } }\)
\(\def\TMstay{ { N } }\)
\(\def\TMstroke{ { 1 } }\)
\(\def\TMtrans#1#2#3{ { #1,#2,#3 } }\)
\(\def\Trm[#1]{ {\operatorname{Trm}(\Lang #1)} }\)
\(\def\True{ { \mathbb{T} } }\)
\(\newcommand{\TRule}[2]{#2#1}\)
\(\def\tuple#1{ {\langle #1 \rangle} }\)
\(\newcommand{\Value}[3][\,]{\mathrm{Val}_{#1}^{#3}(#2)}\)
\(\def\Var{ { \mathrm{Var} } }\)
\(\newcommand{\varAssign}[3]{#1 \sim_{#3} #2}\)
\(\def\Weakening{ { \text{W} } }\)
Just as we’ve defined a number of important semantic notions (validity, entailment, satisfiability), we now define corresponding proof-theoretic notions. These are not defined by appeal to satisfaction of sentences in structures, but by appeal to the derivability or non-derivability of certain sequents. It was an important discovery that these notions coincide. That they do is the content of the soundness and completeness theorem.
A sentence \(A\) is a theorem if there is a derivation in \(\Log{LK}\) of the sequent \(\quad \Sequent A\). We write \(\Proves A\) if \(A\) is a theorem and \(\ProvesN A\) if it is not.
A sentence \(A\) is derivable from a set of sentences \(\Gamma\), \(\Gamma \Proves A\), iff there is a finite subset \(\Gamma_0 \subseteq \Gamma\) and a sequence \(\Gamma_0'\) of the sentences in \(\Gamma_0\) such that \(\Log{LK}\) derives \(\Gamma_0' \Sequent A\). If \(A\) is not derivable from \(\Gamma\) we write \(\Gamma \ProvesN A\).
Because of the contraction, weakening, and exchange rules, the order and number of sentences in \(\Gamma_0'\) does not matter: if a sequent \(\Gamma_0' \Sequent A\) is derivable, then so is \(\Gamma_0'' \Sequent A\) for any \(\Gamma_0''\) that contains the same sentences as \(\Gamma_0'\). For instance, if \(\Gamma_0 = \{B, C\}\) then both \(\Gamma_0' = \tuple{B, B, C}\) and \(\Gamma_0'' = \tuple{C, C, B}\) are sequences containing just the sentences in \(\Gamma_0\). If a sequent containing one is derivable, so is the other, e.g.:
From now on we’ll say that if \(\Gamma_0\) is a finite set of sentences then \(\Gamma_0 \Sequent A\) is any sequent where the antecedent is a sequence of sentences in \(\Gamma_0\) and tacitly include contractions, exchanges, and weakenings if necessary.
A set of sentences \(\Gamma\) is inconsistent iff there is a finite subset \(\Gamma_0 \subseteq \Gamma\) such that \(\Log{LK}\) derives \(\Gamma_0 \Sequent \quad\). If \(\Gamma\) is not inconsistent, i.e., if for every finite \(\Gamma_0 \subseteq \Gamma\), \(\Log{LK}\) does not derive \(\Gamma_0 \Sequent \quad\), we say it is consistent.
If \(A \in \Gamma\), then \(\Gamma \Proves A\).
Proof. The initial sequent \(A \Sequent A\) is derivable, and \(\{A\} \subseteq \Gamma\). ◻
If \(\Gamma \subseteq \Delta\) and \(\Gamma \Proves A\), then \(\Delta \Proves A\).
Proof. Suppose \(\Gamma \Proves A\), i.e., there is a finite \(\Gamma_0 \subseteq \Gamma\) such that \(\Gamma_0 \Sequent A\) is derivable. Since \(\Gamma \subseteq \Delta\), then \(\Gamma_0\) is also a finite subset of \(\Delta\). The derivation of \(\Gamma_0 \Sequent A\) thus also shows \(\Delta \Proves A\). ◻
If \(\Gamma \Proves A\) and \(\{A\} \cup \Delta \Proves B\), then \(\Gamma \cup \Delta \Proves B\).
Proof. If \(\Gamma \Proves A\), there is a finite \(\Gamma_0 \subseteq \Gamma\) and a derivation \(\pi_0\) of \(\Gamma_0 \Sequent A\). If \(\{A\} \cup \Delta \Proves B\), then for some finite subset \(\Delta_0 \subseteq \Delta\), there is a derivation \(\pi_1\) of \(A, \Delta_0 \Sequent B\). Consider the following derivation:
Since \(\Gamma_0 \cup \Delta_0 \subseteq \Gamma \cup \Delta\), this shows \(\Gamma \cup \Delta \Proves B\). ◻
Note that this means that in particular if \(\Gamma \Proves A\) and \(A \Proves B\), then \(\Gamma \Proves B\). It follows also that if \(A_1, \dots, A_n \Proves B\) and \(\Gamma \Proves A_i\) for each \(i\), then \(\Gamma \Proves B\).
\(\Gamma\) is inconsistent iff \(\Gamma \Proves {A}\) for every sentence \(A\).
Proof. Exercise. ◻
Prove Proposition \(\PageIndex{4}\).
- If \(\Gamma \Proves A\) then there is a finite subset \(\Gamma_0 \subseteq \Gamma\) such that \(\Gamma_0 \Proves A\).
- If every finite subset of \(\Gamma\) is consistent, then \(\Gamma\) is consistent.
Proof.
- If \(\Gamma \Proves A\), then there is a finite subset \(\Gamma_0 \subseteq \Gamma\) such that the sequent \(\Gamma_0 \Sequent A\) has a derivation. Consequently, \(\Gamma_0 \Proves A\).
- If \(\Gamma\) is inconsistent, there is a finite subset \(\Gamma_0 \subseteq \Gamma\) such that \(\Log{LK}\) derives \(\Gamma_0 \Sequent \quad\). But then \(\Gamma_0\) is a finite subset of \(\Gamma\) that is inconsistent.
◻