自然演繹の矛盾規則の意味するところが分かりません。

すみません。趣味で数学やっております。

自然演繹のところで、矛盾が出てきた時点で、任意の式を結論付けても良い。

⊥
--------------------
A
A　任意の式

という推論規則があるかと思います。

自然演繹は、人間の推論、論理思考を記号で形式的にモデル化したもので、直感的に理解しやすい推論体系という理解で良いでしょうか？

そのもとで、上の推論規則が何を意味してるのか考えてみたのですが、（直感的に理解しやすい自然な思考である以上、無機質なただの変形ルールというより、意味合いを考えれるのではないか？と考えました。）

私の考えは、

証明を進める上で、矛盾した結論が出た以上、それ以上推論を進めることにはもはや意味がない。
なので、任意の式を矛盾が生じた時点で書いても良いことにする。（書いたとしても矛盾がすでに生じてる訳だから、特にその式が成立してることにはならない）

このように考えました。
ご意見願えないでしょうか？

質問者からの補足コメント

• 構文論的に捉えると、定められた演繹ルール。記号を繋ぐための機械的操作のひとつですね。
  
  あの後、私のテキストに、他の演繹ルールとして、背理法の規則が導入されてました。
  
  ￢ A 仮定
  .
  .
  ⊥　　矛盾
  ---------------------------------
  A
  矛盾規則は、この規則で、仮定￢Aを一度も使わない場合とあり、それで納得しました。つまり、矛盾規則で導入したい任意式の否定を背理法で仮定したと言うことでしょう。
  　　続き→

  No.1の回答に寄せられた補足コメントです。 補足日時：2021/10/22 14:20

• 背理法規則は、高校数学の√2の無理数性を示すための論理そのものなので、形式的操作とはいえ、自然演繹が人間の推論思考をモデル化したものであることを踏まえると、納得しやすいというか、ただの意味を持たない変形ルールなのだろうけど、馴染み易いと感じました。
  
  自然演繹以外だと、仰る通り、本当になぜこのような操作を思い付いた？というような演繹ルールも沢山出てくるのでしょうね。
  
  とにかく、取っつきやすい背理法ルールの特別ケースとして納得することにしました。

    補足日時：2021/10/22 14:25

No.1 ベストアンサー 回答者： ありものがたり 回答日時： 2021/10/21 18:07

形式論理を意味で考えることにそもそも意味がない。