-
Notifications
You must be signed in to change notification settings - Fork 4
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Strong Completeness of Normal Modal Logic #15
Conversation
remain: lindenbaum, completeness_def
レビュー終わり次第マージ可能です. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
レビューしたと思ったが公開されていなかった。申し訳ない。
Logic/Logic/HilbertStyle2.lean
Outdated
@@ -3,99 +3,183 @@ import Logic.Logic.Calculus | |||
|
|||
namespace LO | |||
|
|||
class Deduction {F : Type u} [LogicSymbol F] (Bew : Set F → F → Sort*) where | |||
axm : ∀ {f}, f ∈ T → Bew T f | |||
class Deduction {F : Type u} [LogicSymbol F] (Bew : Finset F → F → Sort*) where |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
公理をFinsetではなく集合にしたほうが良いと思う(普通の導出関係を考えるならば同等のはずで、それならばより一般的な集合のほうが良いと思う)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Hilbert流で最初からSet
を許容すると,例えば演繹定理で
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
それはおそらく次の補題を用いれば問題ないと思う.
証明で使用する公理は有限個なので帰納法で以下に相当する補題が証明できるはず
def Deduction.compact : T ⊢ p → (t : { t : Finset F // t ⊆ T }) × (t ⊢ p)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
修正しました.
TODO
completeness_def