Conjunctive Positive Set Constraints

原子論理式（atomic formula）ってのがなんか決まっているとき、それら原子論理式をベースに、∧（連言）、∨（選言）、¬（否定）を使って組み立てた式（formula）の全体が古典論理の式。ド・モルガンの法則を使えば、∧と∨のどちらかと¬だけでも古典論理の式はできる。

原子論理式から∧だけで組み立てた式は連言的論理（conjunctive logic）の式。だが、連言だけではいくら何でも弱いので、普通は連言＋含意（conjunctive implicative logic）まで考える。それに普通の自然演繹があれば、それでラムダ計算と同等（カリー／ハワード対応）。が、連言だけの論理も意味を持つことがある。以下のケースは連言だけを使う事例。

集合を表すつもりの定数記号や変数記号を準備して、集合の演算として∩（ミート、インターセクション）、∪（ジョイン、ユニオン）、＼（集合差）とかを考える。他に、単調な集合関数（を表す記号）を入れてもいい。定数、変数、演算、関数の各種記号を組み合わせて作った表現を項と呼ぶ。さらに、包含（inclusion）を意味する記号⊆を入れて、「項 ⊆ 項」の形を原子論理式とする。

通常の用語法とはまったく違う（論理特有だ）が、原子論理式を正リテラル、原子論理式の否定を負リテラルと呼ぶ。集合を表す項と⊆（等号を入れてもいい）から作られた正リテラル、負リテラルを set constraint という。正リテラル、つまり positive set constraint を連言∧を使って組み立てた論理式を conjunctive positive set constraints と呼ぶ。これはいわば、集合に関する連立不等式系（system of inclusion inequalities）である

conjunctive positive set constraints をCPSCと略記することにして、A、BなどでCPSCを表すとする。このとき、A、Bなどは包含関係式（集合の不等式）の集合であり、変数を含むかもしれない。CPSC Aの変数の集合をVar(A)とする。Var(A) = 空 なら変数を含まない関係式なので、定数や関数の意味が与えられれば真偽が決まる。定数や関数の意味は与えられているとして、連立不等式系としてのCPSCが解を持つとき、充足可能、変数にどんな集合を割り当てても常に成立するならそのCPSCは普遍妥当と呼ぶ。

CPSCはシーケントの左辺と似たもんだと思ってよい。が、コゥゼンのシーケント計算をそのまま採用できるかどうかはわからない（たぶん、そうはしない）。

実際には、CPSC Aに含まれる変数を2組に分けて、x₁, ..., x_n; y₁, ..., y_m として、∀x₁ ... x_n.A を満たす最小のy₁, ..., y_mを求めたいことが多い。