2024.03.16
https://gyazo.com/342e9123a7bf060abdcafb11609bfdd9
ホワッツ
https://www.youtube.com/watch?v=UDGdPE_C9u8
知った
https://www.youtube.com/watch?v=o89uJuhqdfk
https://www.youtube.com/watch?v=Spu6OlAZHUo
メモ
愛媛と沖縄以外の名字は存在するのか
未来予知の結果アインシュタインの予言が真実だったことがわかり、世界が協力して未来を変えるために出来る限り小規模に第四次世界大戦を行おうとして結局、平和的に石と棍棒で戦うことになってしまったため予言が成就するというオチ メモ
そしてこの違いが本質的に問題となっており,形式化は失敗するかもしれない…
code:ipl.lean
inductive prf : set form → form → Prop
| ax {Γ} {p} (h : p ∈ Γ) : prf Γ p
| k {Γ} {p q} : prf Γ (p ⊃ (q ⊃ p))
| s {Γ} {p q r} : prf Γ ((p ⊃ (q ⊃ r)) ⊃ ((p ⊃ q) ⊃ (p ⊃ r)))
| exf {Γ} {p} : prf Γ (⊥ ⊃ p)
| mp {Γ} {p q} (hpq: prf Γ (p ⊃ q)) (hp : prf Γ p) : prf Γ q
| pr1 {Γ} {p q} : prf Γ ((p & q) ⊃ p)
| pr2 {Γ} {p q} : prf Γ ((p & q) ⊃ q)
| pair {Γ} {p q} : prf Γ (p ⊃ (q ⊃ (p & q)))
| inr {Γ} {p q} : prf Γ (p ⊃ (p ∨ q))
| inl {Γ} {p q} : prf Γ (q ⊃ (p ∨ q))
| case {Γ} {p q r} : prf Γ ((p ⊃ r) ⊃ ((q ⊃ r) ⊃ ((p ∨ q) ⊃ r)))
これのmp {Γ} {p q} (hpq: prf Γ (p ⊃ q)) (hp : prf Γ p) : prf Γ qは要するに$ \Gamma \vdash \varphi \to \psi \quad \Gamma \vdash \varphi \over \Gamma \vdash \psiの形をしている
しかし私の形式化はこの形である$ \Gamma_1 \vdash \varphi \to \psi \quad \Gamma_2 \vdash \varphi \over \Gamma_1 \cup \Gamma_2 \vdash \psi.
これによって帰納法の仮定が変わっていて,非常に問題になってしまっている…