lean4-logic

lean4-logic copied to clipboard

(first-order / propositional) formulae are defined as Tait-style formula, and it is inconsistent with minimal logic, intuitionistic logic, etc. Perhaps we should modify the definition to that of an ordinary...

iehality

Currently, there is two different characterization of deduction system, `LO.System` and `LO.Deduction`, but they are redundant and should be unified.

iehality

For some reasons, it's better to adopt Strict Implication (`⥽`) than Box (`□`) for consideration intuitionistic modal logic. cf: - https://arxiv.org/abs/1708.02143

SnO2WMaN

SnO2WMaN

Proof of incompleteness theorem via derivability conditions

1

SnO2WMaN

refactor(Modal): Commonize Kripke Semantics Part.2

2

相当に時間がかかりそうなのでのんびりとしたペースで行う．

SnO2WMaN

不要に複雑なため，現状のModalでは直観主義様相論理は諦め，古典的なものだけを考える．そのために論理式の定義を変更．

SnO2WMaN

SnO2WMaN

feat(Modal): Finite frame property of `𝐆𝐫𝐳`

1

SnO2WMaN

Cache not working

1

リポジトリ移管以降、キャッシュがうまく効いていない気がする． https://github.com/FormalizedFormalLogic/Foundation/actions/runs/10236132937/job/28317834390

SnO2WMaN