各言語の任意の論理式は，証明論においては，証明系で証明できる式，すなわち，定理式か否かに，モデル論においては，任意の構造，任意の変数への個体割り当てに対して真となる式，すなわち，恒真式か否かに，それぞれ分類されますが，その分類が同じ結果と…

「開いた式」とは「変数の自由出現（あるいは自由変数）を含む論理式」のことで，その真理値の定め方には幾つかの立場があります．言語，構造を固定した上で，伝統的（？）なのは，変数への個体割り当てを用いて立場１ 割り当て毎に真偽を与える立場２ 割り…

古典的（？）な一階の古典論理の意味論では，ドメインAは空でないとされ，その理由として，Aが空では，∀x.p(x)，つまり「任意のxについて，x∈Aならばp(x)」が真，∃x.p(x)つまり「あるxについて，x∈Aかつp(x)」が偽，したがって，定理式 ∀x.p(x)→∃x.p(x) が偽…

今更ですが，使い方です．端末から pvs とすると，emacsが起動し M-x nf でNew file name:と尋ねられ，例えばdemoe20160519と適当に入力すれば，demo20160519.pvsが demo20160519 % [ parameters ] : THEORY BEGIN % ASSUMING % assuming declarations % END…

PVSのskeepコマンドは，本来は x!1 などのように新規に導入すべきスコーレム定数を，衝突がない限り束縛されていた変数と同じ名前で導入してくれます． f1 : |------- {1} (EXISTS (x: A): (p(x))) AND (EXISTS (x: A): (q(x))) => (EXISTS (x: A): (p(x) AN…

g `!n. 8 <= n ==> (?x y. n = 3 * x + 5 * y)` ;; e( INDUCT_TAC );; e( ARITH_TAC );; e( REWRITE_TAC [LE] THEN REPEAT STRIP_TAC );; e( EXISTS_TAC `1` THEN EXISTS_TAC `1` THEN ASM_ARITH_TAC );; e( FIRST_X_ASSUM (fun t -> FIRST_ASSUM (MP_TAC o …