新しいものを表示
SnO₂WMaN さんがブースト

令和最新版のlean4環境構築について書きました!(ほとんど公式のままです)
https://zenn.dev/labbase/articles/b24dca38e0420d

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

scrapbox.io/sno2wman/2023.07.2

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

scrapbox.io/sno2wman/Lean_4_on

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

github.com/SnO2WMaN/lean4-prop

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

en.wikipedia.org/wiki/Conseque [参照]

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

SnO₂WMaN さんがブースト

Robinson算術がQなのはPの次のアルファベットだから(続いてR(Theory R), S, T(限定算術), U, V(二階論理の算術)がある)

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

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

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

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

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

古いものを表示
Fedibird

様々な目的に使える、日本の汎用マストドンサーバーです。安定した利用環境と、多数の独自機能を提供しています。