SOS Projection

               GP/PARI CALCULATOR Version 2.14.0 (development git-b0a4238356)
                amd64 running linux (x86-64/GMP-6.2.1 kernel) 64-bit version
           compiled: Feb 21 2021, gcc version 9.3.0 (Ubuntu 9.3.0-17ubuntu1~20.04)
                                  threading engine: single
                       (readline v8.0 enabled, extended help enabled)

                           Copyright (C) 2000-2021 The PARI Group

PARI/GP is free software, covered by the GNU General Public License, and comes WITHOUT ANY 
WARRANTY WHATSOEVER.

Type ? for help, \q to quit.
Type ?17 for how to get moral (and possibly technical) support.

parisizemax = 10000003072, primelimit = 500000
? tst11Sv2s01([all],[a,b,c,x],id,"a*x^2+b*x+c<=0",2);Ans();pp
[x,1]
[c,2]
[b,1]
[a,1]
var.:a b c x   *** connecting adjacent 6/135 cells.
1[a < [a,1],true,c <= [4*c*a-b^2,1],true]
2[a = [a,1],b = [b,1],c <= [c,1],true]
time = 16 ms.
%1 = [[a],[b],[4*c*a-b^2,c],[a*x^2+b*x+c]] /* Lazard's projection */
? tst11Sv2s01([all],[a,b,c,x],id,"a*x^2+b*x+c<=0",2*7);Ans();pp
 *** using the sum of squares projection.
[x,1]
[c,2]
[b,1]
[a,1]
var.:a b c x   *** connecting adjacent 2/41 cells.
1[a < [a,1],true,c <= [-4*c*a+b^2,1],true]
2[a = [a,1],b = [b,1],c <= [c,1],true]
time = 6 ms.
%2 = [[a],[a^2+b^2],[-4*c*a+b^2,a^2+(b^2+c^2)],[a*x^2+b*x+c]] /* Sum Of Squares projection */
? tst11Sv2s01([ex,ex,ex,ex],[e,v,a,b,c,d],(f1,f2,f3)->f1*f2*f3,"v==(a-1)*(c-1)+b*d,a^2+e*b^2==1,c^2+e*d^2==1",2);Ans();pp
[d,2]
[c,4]
[b,5]
[a,8]
[v,11]
[e,11]
var.:e v a b c d   *** connecting adjacent 524/191440 cells.
1[e <= [e,1],true,true,true,true,true]
2[[e,1] < e <= [2*e-1,1],[(e^2+e)*v+1,1] <= v <= [(e^2-e)*v+1,1],true,true,true,true]
3[[2*e-1,1] < e,[(e^2+e)*v+1,1] <= v <= [v-4,1],true,true,true,true]
time = 1min, 55,679 ms.
%3 = [[3*e+1,3*e-1,7*e^4+10*e^2-1,2*e+1,2*e-1,8*e^2-1,3*e^2-1,2*e^2-1,e+1,e-1,e],[(4*e^4-4*e^2+1)*v^2+(8*e^2-4)*v+8,(e^2+e)*v+1,(e^2-e)*v+1,e^2*v^2-2*e^2*v-1,(e^4-2*e^2+1)*v^2+(4*e^2-4)*v+8,(e^2+1)*v-4,(e^2-1)*v+4,v-4,(e^2-1)*v+2,v-2,v],[2*a^2+(2*v-4)*a+(v^2-2*v+2),a^2+2*e^2*v*a+(e^2*v^2-2*e^2*v-1),(e^2+1)*a^2+(2*e^2*v-2*e^2)*a+(e^2*v^2-2*e^2*v+(e^2-1)),(e^2-1)*a+(-e^2-1),2*a+(v-2),a+1,a+(v-1),a-1],[-2*e*v*a+(b^2+(-e*v^2+2*e*v)),-e*a^2+(-2*e*v+2*e)*a+(b^2+(-e*v^2+2*e*v-e)),e*a^2-2*e*a+(b^2+e),a^2+(e*b^2-1),b],[c+1,c-1,(e*c^2-2*e*c+e)*a^2+(-2*e*c^2+(-2*e*v+4*e)*c+(2*e*v-2*e))*a+((c^2-1)*b^2+(e*c^2+(2*e*v-2*e)*c+(e*v^2-2*e*v+e))),(c-1)*a+(-c+(-v+1))],[c^2+(e*d^2-1),(c-1)*a+(d*b+(-c+(-v+1)))]]  /* Lazard's projection */
? tst11Sv2s01([ex,ex,ex,ex],[e,v,a,b,c,d],(f1,f2,f3)->f1*f2*f3,"v==(a-1)*(c-1)+b*d,a^2+e*b^2==1,c^2+e*d^2==1",2*7);Ans();pp
 *** using the sum of squares projection.
[d,2]
[c,4]
[b,5]
[a,8]
[v,11]
[e,11]
var.:e v a b c d   *** connecting adjacent 524/143294 cells.
1[e <= [e,1],true,true,true,true,true]
2[[e,1] < e <= [2*e-1,1],[(e^2+e)*v+1,1] <= v <= [(e^2-e)*v+1,1],true,true,true,true]
3[[2*e-1,1] < e,[(e^2+e)*v+1,1] <= v <= [v-4,1],true,true,true,true]
time = 1min, 32,646 ms.
%4 = [[3*e+1,3*e-1,7*e^4+10*e^2-1,2*e+1,2*e-1,8*e^2-1,3*e^2-1,2*e^2-1,e+1,e-1,e],[(4*e^4-4*e^2+1)*v^2+(8*e^2-4)*v+8,(e^2+e)*v+1,(e^2-e)*v+1,(e^4-2*e^2+1)*v^2+(4*e^2-4)*v+8,e^2*v^2-2*e^2*v-1,(e^2-1)*v+4,(e^2+1)*v-4,v-4,(e^2-1)*v+2,v-2,v],[(e^2+4)*a^4+((2*e^2+8)*v+(-4*e^2-16))*a^3+((e^2+8)*v^2+(-6*e^2-24)*v+(6*e^2+24))*a^2+(4*v^3+(-2*e^2-16)*v^2+(6*e^2+24)*v+(-4*e^2-16))*a+(v^4-4*v^3+(e^2+8)*v^2+(-2*e^2-8)*v+(e^2+4)),(e^2-1)*a+(-e^2-1),a^2+2*e^2*v*a+(e^2*v^2-2*e^2*v-1),(e^4+3*e^2+1)*a^4+((4*e^4+6*e^2)*v+(-4*e^4-8*e^2))*a^3+((6*e^4+3*e^2)*v^2+(-12*e^4-10*e^2)*v+(6*e^4+6*e^2-2))*a^2+(4*e^4*v^3+(-12*e^4-2*e^2)*v^2+(12*e^4+2*e^2)*v-4*e^4)*a+(e^4*v^4-4*e^4*v^3+(6*e^4-e^2)*v^2+(-4*e^4+2*e^2)*v+(e^4-e^2+1)),2*a+(v-2),a+1,a-1,a+(v-1)],[e*a^2-2*e*a+(b^2+e),2*e*v*a+(-b^2+(e*v^2-2*e*v)),(e^2*b^2+e^4)*a^6+(-6*e^2*b^2-6*e^4)*a^5+((e^2+2*e)*b^4+(e^4+2*e^3+15*e^2+1)*b^2+(15*e^4+2*e^2))*a^4+((-4*e^2-8*e)*b^4+(2*v+(-4*e^4-8*e^3-20*e^2-4))*b^2+(6*e^2*v+(-20*e^4-8*e^2)))*a^3+((2*e+1)*b^6+(2*e^3+7*e^2+12*e+1)*b^4+(v^2-6*v+(6*e^4+12*e^3+16*e^2-2*e+6))*b^2+(7*e^2*v^2-18*e^2*v+(15*e^4+12*e^2)))*a^2+((-4*e-2)*b^6+(2*v+(-4*e^3-6*e^2-8*e-2))*b^4+(-2*v^2+(2*e^2-4*e+6)*v+(-4*e^4-8*e^3-8*e^2+4*e-4))*b^2+(4*e^2*v^3-14*e^2*v^2+18*e^2*v+(-6*e^4-8*e^2)))*a+(b^8+(e^2+2*e+1)*b^6+(v^2-2*v+(2*e^3+2*e^2+2*e+2))*b^4+((e^2-2*e+1)*v^2+(-2*e^2+4*e-2)*v+(e^4+2*e^3+2*e^2-2*e+1))*b^2+(e^2*v^4-4*e^2*v^3+7*e^2*v^2-6*e^2*v+(e^4+2*e^2))),a^2+(e*b^2-1),b],[c+1,c-1,(e*c^2-2*e*c+e)*a^2+(-2*e*c^2+(-2*e*v+4*e)*c+(2*e*v-2*e))*a+((c^2-1)*b^2+(e*c^2+(2*e*v-2*e)*c+(e*v^2-2*e*v+e))),(c^2-2*c+1)*a^2+(-2*c^2+(-2*v+4)*c+(2*v-2))*a+(b^2+(c^2+(2*v-2)*c+(v^2-2*v+1)))],[c^2+(e*d^2-1),(c-1)*a+(d*b+(-c+(-v+1)))]]  /* Sum Of Squares projection */

京都大学理学部特色入試［３］（２）

もう一問，解いてみました．

　設問の各条件は $f$ を $-f$ に変えても等価なので，${\rm lc}(f)>0$ としてよく，${f}({x})\to+\infty\ ({x\to+\infty})$，$f$ は連続なので $\exists x\in\mathbb{R} \left({{f}({x})\in\mathbb{Z}}\right)$ であり，設問の仮定により $\exists x\in\mathbb{R} \left({{g}({x})\in\mathbb{Z}}\right)$ となるから，${\rm deg}(g)>0$ として矛盾を導く．このとき，同様に ${\rm lc}(g)>0$ としてよく

【方法０】　${\rm deg}(f)>{\rm deg}(g)$ ならば，区間 $({a,\ +\infty})$ において $f,\ g,\ f-g$ が狭義増加で，$f(c)=f(b)+1,\ g(b),\ g(c)\in \mathbb{Z},\ a<$ $b<$ $c$ となる $a,\ b,\ c$ があり
$$f(b)-g(b)\,{<}\,f(c)-g(c)$$ したがって $$1\le g(c)-g(b)\,{<}\, f(c)-f(b)=1$$ なので矛盾．

あるいは

　$f,\ g$ が狭義増加となる区間 $I=({a_0,\ +\infty})$ があり，$({{f}({a_i})\in\mathbb{Z}})_{i=1}^{\infty}$ が公差 $1$ の等差数列で，$a_i\to+\infty\ ({i\to\infty})$ となる狭義増加な $({a_i\in I})_{i=1}^{\infty}$ がある．よって

【方法１】　$({{g}({a_i})\in\mathbb{Z}})_{i=1}^{\infty}$ の階差はつねに $1$ 以上だから，$i=1,2,\ldots$ のとき
$${f}({a_i})-{f}({a_1})=i-1\le{g}({a_i})-{g}({a_1})$$
つまり
$${f}({a_i})-{g}({a_i})\le {f}({a_1})-{g}({a_1})$$
となるが，${\rm deg}\,f>{\rm deg}\,g$ ならば ${f}({a_i})-{g}({a_i})\to+\infty\ ({i\to\infty})$ なので矛盾．

【方法２】　$n>d={\rm deg}(g)$ として，$1\le x<$ $y$ のとき
$$
{g}({x})=\sum_{j=0}^{d}{ A_j x^j },\quad
{f}({x})=\sum_{j=0}^{n}{ B_j x^j },\quad
{G}({x,\ y})=\frac{{g}({x})-{g}({y})}{x^n-y^n},\quad
{F}({x,\ y})=\frac{{f}({x})-{f}({y})}{x^n-y^n}-B_n
$$
とおくと，(1) により
$$|{{G}({x,\ y})}|\le\sum_{j=0}^{d}{ |{A_j}|\cdot \left|{\frac{x^j-y^j}{x^n-y^n}} \right| }{<}\frac{1}{x} \sum_{j=0}^{d}{ |{A_j}| },\quad |{{F}({x,\ y})}|\le\sum_{j=0}^{n-1}{ |{B_j}|\cdot \left|{\frac{x^j-y^j}{x^n-y^n}}\right| }{<}\frac{1}{x} \sum_{j=0}^{n-1}{ |{B_j}| }$$
なので，$i\to\infty$ のとき，${G}({a_i,\ a_{i+1}}),\ {F}({a_i,\ a_{i+1}})\to0$，したがって
\begin{equation*}
1\le\left|{{g}({a_i})-{g}({a_{i+1}})}\right|
=\left|{\frac{{g}({a_i})-{g}({a_{i+1}})}{{f}({a_i})-{f}({a_{i+1}})}}\right|
=\left|{\frac{ {G}({a_i,\ a_{i+1}}) }{ {F}({a_i,\ a_{i+1}})+B_n }}\right|
\to\left|{\frac{0}{B_n}}\right|=0
\end{equation*}
となり矛盾．

京都大学理学部特色入試［４］

ちょっとした経緯があり，解いてみました．

　$O$ を原点とする $xyz$ 空間内の任意の点 $X=(x,\ y,\ z)$ に対して，$X'=(0,\ y,\ z)$ とし，$X$ と $x$ 軸との距離を ${d}({X})$ で表すと，${d}({X})=\sqrt{y^2+z^2}=\left|\overrightarrow{OX'}\right|$ だから，$4$ 点 $V_i\ (i=1,2,3,4)$ と和が $1$ である非負の $4$ 数 $t_i\ (i=1,2,3,4)$ に対して，$T_1=\sum_{i=1}^{4}{ t_i V_i }$ とおくと

$${d}({T_1})=\left|\sum_{i=1}^{4}{ t_i \overrightarrow{O{V_i}'} }\right| \le \sum_{i=1}^{4}{ t_i \left|{\overrightarrow{O{V_i}'}}\right| }
=\sum_{i=1}^{4}{ t_i {d}({V_i}) }\le\max\{{d}({V_i}):i=1,2,3,4\}$$

さらに，$x$ 軸上の $2$ 点 $T_2,\ T_3$ に対して，$3$ 角形 $XT_2T_3$ の面積を ${m}({X})$ で表すと，${m}({X})=\left|{\overrightarrow{T_2T_3}}\right|\times{d}({X})/2$ だから

$${m}({T_1})\le\max\{{m}({V_i}):i=1,2,3,4\}$$

したがって，設問の $\mathrm{P,\ Q,\ R}$ を逐次 $T_1$ とし，この不等式の右辺を与える $4$ 面体 $\mathrm{ABCD}$ の頂点に移せば，面積が減少しない $3$ 角形の列が得られ，$4$ 面体 $\mathrm{ABCD}$ の面に至る．

√素数が有理数でないこと（その３）

同じ内容をどこかに書いた気もするのですが，等号の話が出た流れで．かなり以前の「√素数が有理数でないこと」http://ehito.hatenablog.com/entry/20130419/1366333894 の続編です．

定数記号ｃ，２項関数記号ｆ，ｇをもつ言語に，前回のように等号の公理を導入して，理論

｛∀ｘ（ｆｃｘ＝ｘ），∀ｘ（ｇｘｘ＝ｘ），∀ｘ∀ｙ∀ｚ（ｇ（ｆｘｙ）ｚ＝ｃ ｇｘｚ＝ｃ∧ｇｙｚ＝ｃ）｝

をＴとおくと，domain が自然数全体，ｃ，ｆ，ｇの解釈がそれぞれ１，乗算，最大公約数を与える関数である任意の構造Ｍは，Ｔのモデルですが，論理式

∀ｐ（ｐ≠ｃ∧∀ｘ∀ｙ（ｆｘｙ＝ｐ→ｘ＝ｃ∨ｙ＝ｃ）→ ￢（∃ｘ∃ｙ（ｇｘｙ＝ｃ∧ｆｘｘ＝ｆ（ｆｙｙ）ｐ）））

は，Ｔから証明可能なので，（健全性により）Ｍにおいて valid です．

# (UNDISCH_ALL o SPEC_ALL) (METIS [] 
`!f g:a->a->a. (!x. f c x = x) ==> (!x. g x x = x) 
==> (!x y z. g (f x y) z = z <=> g x z = c /\ g y z = c) 
==> (!p. ~(p = c) /\ (!x y. f x y = p ==> x = c \/ y = c) ==> ~(?x y. g x y = c /\ f x x = f (f y y) p))`
);;
val it : thm = !x y z. g (f x y) z = z <=> g x z = c /\ g y z = c,
  !x. f c x = x, !x. g x x = x
  |- !p. ~(p = c) /\ (!x y. f x y = p ==> x = c \/ y = c)
         ==> ~(?x y. g x y = c /\ f x x = f (f y y) p)

数理論理４：等号

今回は
・等号の公理
と
・理論と構造の濃度との関係
について述べます．

以下，２項述語記号＝を等号と呼び，これを元にもつ言語を固定，ｔ１，ｔ２がその項ならば
　＝（ｔ１，ｔ２）をｔ１＝ｔ２
　￢（＝（ｔ１，ｔ２））をｔ１≠ｔ２
とそれぞれ略記します．

まず，等号の公理を導入します．

（定義４－１）適当な変数記号ｘによって
　　∀ｘ（ｘ＝ｘ）
或いは，ｔ，ｔ’がＡのｘに代入可能である（つまり，新たな束縛が生じない）適当な項ｔ，ｔ’，変数記号ｘ，論理式Ａによって
　　ｔ＝ｔ’→（→）の全称閉包
と表せる論理式を等号の公理と呼びます．

ここで，， はＡ内のｘの全ての自由出現をぞれぞれｔ，ｔ’に置き換えたものです．

また，次のような流儀もあります．

（定義４－２）適当な変数記号ｘ，ｙ，ｚによって
　　∀ｘ（ｘ＝ｘ）
　　∀ｘ∀ｙ（ｘ＝ｙ→ｙ＝ｘ）
　　∀ｘ∀ｙ∀ｚ（ｘ＝ｙ→（ｙ＝ｚ→ｘ＝ｚ））
或いは，適当なｎ（＞０）項関数記号ｆ，適当な項ｔ１，...，ｔｎ，ｔ１’，...，ｔｎ’によって
　　ｔ１＝ｔ１’∧...∧ｔｎ＝ｔｎ’→ｆ（ｔ１，...，ｔｎ）＝ｆ（ｔ１’，...，ｔｎ’）の全称閉包
或いは，適当なｎ（＞０）項述語記号ｐ，適当な項ｔ１，...，ｔｎ，ｔ１’，...，ｔｎ’によって
　　ｔ１＝ｔ１’∧...∧ｔｎ＝ｔｎ’→（ｐ（ｔ１，...，ｔｎ）→ｐ（ｔ１’，...，ｔｎ’））の全称閉包
と表せる論理式を等号の公理と呼びます．

このとき

・　（定義４－２）の各公理は（定義４－１）の公理全体の集合から証明可能
・　（定義４－１）の各公理は（定義４－２）の公理全体の集合から証明可能

であり，（定義２－１）に

　とくに
　Ｉ（＝）はＤ上の相等関係，つまり，任意の（ａ，ｂ）∈Ｄ＾２に対して，ａ＝ｂ（この＝はＤ上の等号）ならば１，そうでないならば０となる写像

を追加すると

・　（定義４－１），（定義４－２）の各公理は valid

です．

以下，（定義２－１）に上記を，（定義３－１）に

Ｋが（定義４－１）の等号の公理ならば
０．｛｝｛Ｋ｝

をそれぞれ追加し，理論と構造の濃度との関係を見て行きます．

まず
　　∀ｘ∀ｙ（ｘ＝ｙ） ⇔ ∃ｘ∀ｙ（ｘ＝ｙ）
であり，２つの理論｛∀ｘ∀ｙ（ｘ＝ｙ）｝，｛∃ｘ∀ｙ（ｘ＝ｙ）｝はどちらも濃度が１の任意の構造のみをモデルにもちます（domain が空である構造を許す流儀では，∀から始まる任意の論理式はその構造において valid なので，前者は濃度が２より小の任意の構造のみをモデルにもちます）．

同様に，２つの理論
　　｛∃ｘ１∃ｘ２（ｘ１≠ｘ２）∧∀ｘ１∀ｘ２∀ｘ３（ｘ１＝ｘ２∨ｘ１＝ｘ３∨ｘ２＝ｘ３））｝
　　｛∃ｘ１∃ｘ２（ｘ１≠ｘ２∧∀ｙ（ｘ１＝ｙ∨ｘ２＝ｙ））｝
はどちらも濃度が２の任意の構造のみをモデルにもちます．

そして，２以上の任意の整数ｎに対して，φｎを
　　∀ｘ１...∀ｘｎ（１≦ｉ＜ｊ≦ｎを満たす各整数の対（ｉ，ｊ）に対するｘｉ＝ｘｊを∨で結んだもの）
とおくと，それぞれ
　　｛φｎ｝は濃度がｎより小
　　｛￢φｎ｝ は濃度がｎ以上
　　｛￢φｎ，φ(ｎ＋１)｝ は濃度がｎ
の任意の構造のみをモデルにもちます．

このように任意の正の整数ｎに対して，理論Ｔｎが存在して
　　任意の構造Ｓに対して，Ｓの濃度がｎとＳ|=Ｔｎとは等価
ですが
　　任意の構造Ｓに対して，Ｓの濃度が有限とＳ|=Ｔとは等価
となる理論Ｔは存在しません（そのようなＴがあるとＴ’＝Ｔ∪｛￢φｊ：ｊ≧２｝の任意の有限部分集合がモデルをもつのでコンパクト性定理（ https://en.wikipedia.org/wiki/Compactness_theorem ）によりＴ’もモデルをもちますが、その濃度は有限かつ無限となり不合理です）．

これと双対的に，無限濃度については，上記のφにより
　　任意の構造Ｓに対して，Ｓの濃度が無限とＳ|=｛￢φｊ：ｊ≧２｝とは等価
ですが，任意の無限濃度ｍに対して，濃度ｍの任意の構造のみをモデルにもつ理論は存在しません（無限濃度の任意の構造Ｍ，Ｍをモデルにもつ任意の理論Ｔ，言語の濃度以上の任意の濃度ｋに対して，Ｔは濃度ｋの（Ｍと初等的同値な）モデルをもつことが，レーベンハイム－スコーレムの定理（ https://en.wikipedia.org/wiki/L%C3%B6wenheim%E2%80%93Skolem_theorem ）として知られています）．

最近の話題から

HOList with HOL Light
https://sites.google.com/view/holist/home

TacticToe with HOL4
https://www.thibaultgauthier.fr/tactictoe.html

さらに
http://aitp-conference.org/2019/
http://arg.ciirc.cvut.cz/teaching/mlr19/index.html
http://ai4reason.org/demos.html

CoqGym with Coq
https://github.com/princeton-vl/CoqGym

MetaGen with MetaMath
https://openreview.net/pdf?id=BJxiqxSYPB

PVS は．．．
https://github.com/nasa/vscode-pvs

数理論理３：構文論

今回は
・言語に対して，その言語の定理式の全体が定まること
をＬＫと呼ばれる流儀で述べます．

以下，言語，その言語の論理式の集合Σを任意に固定します．

（定義３－１）論理式の任意の集合の対（Ψ，Ω）をシーケントと呼び，Σから導出可能なシーケントの全体は，次の１．から16．（３．から16．を推論規則と呼びます）を満たす最小の集合です．以下，この集合に（Ψ，Ω）が属することを Ψ $\longrightarrow$ Ω で表します．

ｘが変数記号，ｔが項，Ａ，Ｂが論理式，ＣがΣの元，Ｘ，Ｙが論理式の（空でもよい）有限列ならば

１．｛｝$\longrightarrow$｛Ｃ｝
２．｛Ａ｝$\longrightarrow$｛Ａ｝

３．｛Ｘ｝$\longrightarrow$｛Ｙ｝ならば｛Ｘ｝$\longrightarrow$｛Ａ，Ｙ｝かつ｛Ａ，Ｘ｝$\longrightarrow$｛Ｙ｝
４．｛Ｘ｝$\longrightarrow$｛Ａ，Ｙ｝かつ｛Ａ，Ｘ｝$\longrightarrow$｛Ｙ｝ならば｛Ｘ｝$\longrightarrow$｛Ｙ｝

５．｛Ａ，Ｘ｝$\longrightarrow$｛Ｙ｝ならば｛Ｘ｝$\longrightarrow$｛￢Ａ，Ｙ｝
６．｛Ｘ｝$\longrightarrow$｛Ａ，Ｙ｝ならば｛￢Ａ，Ｘ｝$\longrightarrow$｛Ｙ｝

７．｛Ａ，Ｂ，Ｘ｝$\longrightarrow$｛Ｙ｝ならば｛Ａ∧Ｂ，Ｘ｝$\longrightarrow$｛Ｙ｝
８．｛Ｘ｝$\longrightarrow$｛Ａ，Ｙ｝かつ｛Ｘ｝$\longrightarrow$｛Ｂ，Ｙ｝ならば｛Ｘ｝$\longrightarrow$｛Ａ∧Ｂ，Ｙ｝

９．｛Ｘ｝$\longrightarrow$｛Ａ，Ｂ，Ｙ｝ならば｛Ｘ｝$\longrightarrow$｛Ａ∨Ｂ，Ｙ｝
10．｛Ａ，Ｘ｝$\longrightarrow$｛Ｙ｝かつ｛Ｂ，Ｘ｝$\longrightarrow$｛Ｙ｝ならば｛Ａ∨Ｂ，Ｘ｝$\longrightarrow$｛Ｙ｝

11．｛Ａ，Ｘ｝$\longrightarrow$｛Ｂ，Ｙ｝ならば｛Ｘ｝$\longrightarrow$｛Ａ→Ｂ，Ｙ｝
12．｛Ｘ｝$\longrightarrow$｛Ａ，Ｙ｝かつ｛Ｂ，Ｘ｝$\longrightarrow$｛Ｙ｝ならば｛Ａ→Ｂ，Ｘ｝$\longrightarrow$｛Ｙ｝

13．｛Ｘ｝$\longrightarrow$｛Ａ，Ｙ｝ならば｛Ｘ｝$\longrightarrow$｛∀ｘＡ，Ｙ｝
　　ただし，Ｘ，Ｙの各論理式にｘの自由出現はないとします（これを固有変数条件と呼びます）．
14．｛Ａ内のｘの全ての自由出現をｔに置き換えたもの，Ｘ｝$\longrightarrow$｛Ｙ｝ならば｛∀ｘＡ，Ｘ｝$\longrightarrow$｛Ｙ｝
　　ただし，置き換えにより新たな束縛は生じないとします（これを代入可能条件と呼びます）．

15．｛Ａ，Ｘ｝$\longrightarrow$｛Ｙ｝ならば｛∃ｘＡ，Ｘ｝$\longrightarrow$｛Ｙ｝
　　ただし，固有変数条件は満たされているとします．
16．｛Ｘ｝$\longrightarrow$｛Ａ内のｘの全ての自由出現をｔに置き換えたもの，Ｙ｝ならば｛Ｘ｝$\longrightarrow$｛∃ｘＡ，Ｙ｝
　　ただし，代入可能条件は満たされているとします．

なお，（定義３－１）も（定義１－２）のように「適当な・・・によって・・・と表せるもの」という表現も可能です．そして

・　｛Ｘ｝$\longrightarrow$｛Ｙ｝を Ｘ $\longrightarrow$ Ｙ 或いは Σ $\vdash$ Ｘ $\longrightarrow$ Ｙ と書きます．また，とくに Σ $\vdash$ $\longrightarrow$ Ａ を Σ $\vdash$ A（Σが空集合ならば $\vdash$ A）と書き，これを「ＡはΣの構文論的帰結」或いは「ＡはΣの定理式」或いは「ＡはΣから証明可能」（Σ が空集合ならば「Ａは定理式」或いは「Ａは証明可能」）と読みます．
・　（定義３－１）の集合は帰納的に定義されているので，１．または２．から｛Ｘ｝$\longrightarrow$｛Ｙ｝に至る過程に現れるΣの元は有限個です．従って，Σ $\vdash$ Ｘ $\longrightarrow$ Ｙならば，Σの有限部分集合Σ’が存在して Σ’ $\vdash$ Ｘ $\longrightarrow$ Ｙ となります．
・　固有変数条件を満たさない代入を許すと，例えば，ｘが変数記号，ｐが１項述語記号ならば，ｐｘ→∀ｘｐｘ が定理式になってしまいます．
・　代入可能条件を満たさない代入を許すと，例えば，ｘが変数記号，ｐが１項述語記号ならば，∀ｘｐｘｘ→∃ｘ∀ｙｐｘｙ が定理式になってしまいます．

（例３－１）ｘ，ｙが異なる変数記号，ｐが１項述語記号ならば
　$\longrightarrow$（￢（∀ｘｐｘ））→∃ｘ（￢ｐｘ）
となるには，11. により
　￢（∀ｘｐｘ）$\longrightarrow$∃ｘ（￢ｐｘ）
となればよく，それには，６. により
　$\longrightarrow$∀ｘｐｘ，∃ｘ（￢ｐｘ）
となればよく，それには，13. により
　$\longrightarrow$ｐｙ，∃ｘ（￢ｐｘ）
となればよく，それには，16. により
　$\longrightarrow$ｐｙ，￢ｐｙ
となればよく，それには，５. により
　ｐｙ$\longrightarrow$ｐｙ
となればよく，２. により，（￢（∀ｘｐｘ））→∃ｘ（￢ｐｘ）は定理式です．

（例３－２ https://en.wikipedia.org/wiki/Drinker_paradox ）シーケントは集合の対なので，その集合の要素を複製することが可能です．したがって，ｘ，ｙが異なる変数記号，ｐが１項述語記号ならば
　$\longrightarrow$∃ｘ（ｐｘ→∀ｘｐｘ）
となるには
　$\longrightarrow$∃ｘ（ｐｘ→∀ｘｐｘ），∃ｘ（ｐｘ→∀ｘｐｘ）
となればよく，それには
　$\longrightarrow$ｐｘ→∀ｘｐｘ，∃ｘ（ｐｘ→∀ｘｐｘ）
となればよく，それには
　ｐｘ$\longrightarrow$∀ｘｐｘ，∃ｘ（ｐｘ→∀ｘｐｘ）
となればよく，それには
　ｐｘ$\longrightarrow$ｐｙ，∃ｘ（ｐｘ→∀ｘｐｘ）
となればよく，それには
　ｐｘ$\longrightarrow$ｐｙ，ｐｙ→∀ｘｐｘ
となればよく，それには
　ｐｘ，ｐｙ$\longrightarrow$ｐｙ，∀ｘｐｘ
となればよく，それには
　ｐｙ$\longrightarrow$ｐｙ，∀ｘｐｘ
となればよく，それには
　ｐｙ$\longrightarrow$ｐｙ
となればよいので，∃ｘ（ｐｘ→∀ｘｐｘ）は定理式です.

こうした手続きを上下を逆にして次のツールが生成するような図で表したものをその定理式の証明図と呼びます．http://bach.istc.kobe-u.ac.jp/seqprover/

（参考）
https://en.wikipedia.org/wiki/Sequent_calculus#The_system_LK