SnO₂WMaN @sno2wman@fedibird.com

Lean4はNixでも環境構築できる( https://leanprover.github.io/lean4/doc/setup/nix.html )という旨が書かれて入るが内容の通りかなり実験的な状態で，少なくともこれに書かれたテンプレートを用いると毎回最新のLean4をビルドする羽目になって大変なことになる気がする（lean-toolchainは無視される）のと，Lean側で依存しているライブラリ等もNIxで明示的に記載しなければならず二度手間になる上に場合に依っては出来ないケースもある（Mathlib4がそうでNix Flakeを提供していないため）#要調査

https://scrapbox.io/sno2wman/2023.07.26#64c0a27113a1580000c95a55

Lean4を汎用的な関数型プログラミング言語として使うのならCIとかもちゃんとしないとダメだなと思ってGitHub Actionsを用意してみたが，Mathlibに依存していると凄まじく時間がかかり，どうにかしようとしたが結局よくわからなかった（何をキャッシュすればよいのだろう？）

https://scrapbox.io/sno2wman/Lean_4_on_GitHub_Actions

近況としては主に戸次『数理論理学』に基づいて(最小/直観主義/古典)命題論理をLean4で形式化しているが、まだ殆ど何も示していない（せいぜいHilbert流体系について整理したのみ）

https://github.com/SnO2WMaN/lean4-propositional-logic

日報(2023.07.26)

https://scrapbox.io/sno2wman/2023.07.26

日報(2023.07.25)

https://scrapbox.io/sno2wman/2023.07.25

そういえばこの形式の論理式には驚嘆すべき帰結(Consequentia mirabilis)という名前が付いていたことを思い出す

https://en.wikipedia.org/wiki/Consequentia_mirabilis [参照]

日報(2023.07.24)

https://scrapbox.io/sno2wman/2023.07.24

日報(2023.07.23)

https://scrapbox.io/sno2wman/2023.07.23

日報(2023.07.22)

https://scrapbox.io/sno2wman/2023.07.22

日報(2023.07.21)

https://scrapbox.io/sno2wman/2023.07.21

足し算と掛け算しか無いPeano算術に原始再帰的関数全部突っ込んでも本質的には変わらないのでOKという定理ありがたすぎていいな

日報(2023.07.20)

https://scrapbox.io/sno2wman/2023.07.20

情報ありがとうございます．

https://mstdn.jp/@palalansouki/110745269567319776 [参照]

そういえばPeano算術はPAなのにRobinson算術はなぜRAとかでなくQとして表すのだろうか

ここでの投稿内容に数式入れたらKaTeXで適当に表示してくれないかな

日報(2023.07.19)

https://scrapbox.io/sno2wman/2023.07.19

A「おまえはすぐ否定から入る」
B/1「そうだ」
B/2「そんなことはない」

B/1だとするとAは誤っていたことになる
B/2だとするとBは常に否定することになってナンセンスになる

この議論を上手く形式化するとどうなるのか?