問題タブ [verifiable-c]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
32 問題
0
投票する
0
に答える
18
参照
verifiable-c - 含意述語
単純な方法でシークエントを分離ロジックに埋め込むことは不可能だと確信していますか?
PLCC の 100 ページに、 ifP [|-] Qが「すべての世界wに対して 、 if w |= Pthenw |= Qであることを意図している」と記載されているが、それは証明できないため機能しない(P [|-] Q) |-- |> (P [|-] Q).
!!(P |-- Q)特にそれを証明するのは簡単で
!!(P |-- Q) |-- |> !!(P |-- Q)あり、証明するのはそれほど難しくないので、それを as として埋め込むことが機能しない理由がわかりません
!!(P |-- Q) |-- !!(|> P |-- |> Q)。