>>551
>>543　>箱入り無数目の代表の集合は、definableではない！！
>>546　>だから固定することは不可能だと
　箱入り無数目の代表の集合が定義可能集合である必要はない
　存在すれば一意化できる（例えば、自然演繹の∃除去規則）
ja.wikipedia.org/wiki/%E8%87%AA%E7%84%B6%E6%BC%94%E7%B9%B9
(引用終り)

君は、詭弁・論点ずらし の天才だねｗ
御大からは”寝言”と見透かされているが

下記 ちょっと面白いけどな
”自然演繹 背景 1926年、ポーランドで行われた一連の講義で、ヤン・ウカシェヴィチは論理のより自然な扱いを主張した。これに触発された Stanisław Jaśkowski がより自然な演繹を定義しようと試み、1929年には図表的記法を使った方法を提案し、1934年から1935年にかけてより洗練された提案を一連の論文として発表した。しかし、その提案は一般には全く認知されなかった。現代の自然演繹の形式はそれとは独立に1935年にドイツ人数学者ゲルハルト・ゲンツェンが学位論文で提案したものである”
論点ずらしの寝言だｗ

(参考)
ja.wikipedia.org/wiki/%E8%87%AA%E7%84%B6%E6%BC%94%E7%B9%B9
自然演繹は、「自然な」ものとしての論理的推論の形式的モデルを提供する証明理論の手法であり、哲学的論理学の用語である
自然演繹論理
自然演繹論理のあるバージョンには、公理が存在しない
ジョン・レモンが開発した体系 L は、証明の構文規則に関する次のような9つの基本的規則だけを持つ
背景
自然演繹は、ヒルベルト、フレーゲ、ラッセルらに共通する命題論理的公理化に対する不満から生じた。そのような公理化の最も有名な例としては、ラッセルとホワイトヘッドの『数学原理』がある。1926年、ポーランドで行われた一連の講義で、ヤン・ウカシェヴィチは論理のより自然な扱いを主張した。これに触発された Stanisław Jaśkowski がより自然な演繹を定義しようと試み、1929年には図表的記法を使った方法を提案し、1934年から1935年にかけてより洗練された提案を一連の論文として発表した。しかし、その提案は一般には全く認知されなかった。現代の自然演繹の形式はそれとは独立に1935年にドイツ人数学者ゲルハルト・ゲンツェンが学位論文で提案したものである。「自然演繹」という用語（のドイツ語版 natürlichen Schließens）はその論文で使われたものであった。[1]
ゲンツェンは数論の一貫性を確立したいと考えており、自然演繹をさっそく応用した。彼は、その証明の複雑性に不満を持ち、1938年にはシークエント計算を新たな証明の道具として考案した。1961年と1962年の一連の講義で、Dag Prawitz は自然演繹の包括的なまとめを行った。彼の1965年の学術論文 Natural deduction: a proof-theoretical study は自然演繹の最終版ともいうべきもので、様相論理や二階述語論理への応用も含んでいた
以下で説明するのは、ゲンツェンや Prawitz の定式化に若干修正を施したものだが、ペール・マルティン＝レーフの影響もある
古典論理と様相論理
話を単純化するため、ここまでの説明では直観論理を使ってきた。古典論理は、直観論理に次の公理あるいは排中律を追加して拡張したものと言える。
「任意の命題 p について、命題 p ∨ ¬p は真である」
この文自体は、導入も除去も明確でない