タブローの方法は無限集合に使えませんハイ終〜〜〜了〜〜〜

タブローの方法 - Wikipedia
https://ja.wikipedia.org/wiki/%E3%82%BF%E3%83%96%E3%83%AD%E3%83%BC%E3%81%AE%E6%96%B9%E6%B3%95
> タブローの方法(英 tableau([1]) method)とは、真理の木(truth tree)あるいは意味論的タブロー(semantic tableau)または分析タブロー(analytic tableau)と呼ばれるものを用いて､
> 論証の妥当性や、論理式が矛盾しているかやトートロジーであるかを機械的に調べる判定手続き(decision procedure)の一種である｡
> ヤーッコ・ヒンティッカらのモデル集合という考え方を応用して作られ、レイモンド・スマリヤンによって広められた｡
> タブローの方法は命題論理や一引数の一階述語論理において決定可能である。つまり有限ステップで必ず判定を行える｡
> しかし、多引数の一階述語論理において決定不可能である。つまり有限ステップで判定できない可能性がある｡