Recursion contradicts to induction within Lukasiewicz Logic

拙論 国際会議 logic

私の発表は11:15-11:50。内容はHajekの定理の証明の簡略化について。かなり興味を持ってもらえた様子です。発表の要旨は以下の通り（ご興味がある方はこちらをご覧ください）。

Set theory:

  • CL0 with the comprehension principle within Lukasiewicz predicate logic L∀.
  • H with the comprehension principle within Lukasiewicz infinite-valued predicate logic (L∀ is weaker than Lukasiewicz infinite-valued predicate logic).

A known result:

  • Mathematical induction on ω implies a contradiction in CL0 by a very long proof [1].
  • Mathematical induction on ω implies a contradiction in H by a simple proof [2].

We will show mathematical induction on ω implies a contradiction in CL0 by a simple proof.
This result suggests the general form of recursive definition contradicts to mathematical induction, though they looks similar in an arithmetic within classical logic.

  1. Petr Hajek. On arithmetic in the Cantor-Lukasiewicz fuzzy set theory. AML 44(6), pp.339-346.
  2. Shunsuke Yatabe. Distinguishing non-standard natural numbers in a set theory within ukasiewicz logic. AML 46, pp281-287.

発表の最中、ソフトがエラーを起こしたりしましたが、落ち着いて発表できたと思います。質問は以下の通り。

    1. この定理はMTLで証明できるか。これはチェコのB氏から。考えてませんでした。ちなみに、午前の部終了直後、B氏から声をかけられ、「同僚のCiと相談したんだけど、さっきの質問、解けたよ。というのも･･･だからで、簡単なこと聞いてすまないね」。･･･国際会議は怖い、と改めて思った。
    2. 体系CL0がω-矛盾であることが、どのような哲学的意味を持つのか。これはM氏から。「幾人かの哲学者の意見に反し、超準数を人間は排除できないと言うことだ」と答えておきました。こちらも後日談があり、最終日に路上でM氏に聞くと、彼は標準的なLukasiewicz logic の意味論が量化子を持つ文の真理値の決め方について問題を持つせいだと考えているらしく、いろいろと貴重な関連事実を教わりました。
    3. 外延性と、ωの一意性について。こちらはAv氏から。私がちゃんと答える前に、B氏に助け船を出してもらって終了。助かりました。
    4. 発表者（私）は、この定理から「数学的帰納法が矛盾を導く」と結論しているようだけど、この定理から「自然数の定義が間違っている」と結論することだって出来るのではないか。これは質問時間ではなく、昼食時にCi氏から。するどい。もちろんGirard-TeruiのLight Linear logic における、modal operatorを使用して自然数を定義し、weak induction を定理として得るという、私の方法とは相反する結果も既に出ていますし。とりあえず、私は厳格有限主義（自然数の本質は後者関数に関して閉じていることであり、数学的帰納法は間違っていると主張）に強い興味を持ち、その結論をモデル化することもこの定理の証明の動機の一つだ、と答えておきました。彼は納得してくれたけれど、でも、この件に関してはもっと考察が必要でしょう。