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

Use standard sequent calculus with sequents #145

Closed
rzach opened this Issue Jul 13, 2017 · 2 comments

Comments

Projects
None yet
2 participants
@rzach
Member

rzach commented Jul 13, 2017

The sequent calculus is presented with sequents being sets of formulas. Switch to sequences so it is more standard and allows future expansion by discussion of substructural logics.

@nicolewyatt

This comment has been minimized.

Show comment
Hide comment
@nicolewyatt

nicolewyatt Jul 13, 2017

Contributor

How time consuming will this fix be? I would like this for the Fall but I realize time is getting short.

Contributor

nicolewyatt commented Jul 13, 2017

How time consuming will this fix be? I would like this for the Fall but I realize time is getting short.

@rzach

This comment has been minimized.

Show comment
Hide comment
@rzach

rzach Jul 13, 2017

Member

Should be doable; the harder part will be to fix arithmetization of syntax for LK, but you don't need that.

Member

rzach commented Jul 13, 2017

Should be doable; the harder part will be to fix arithmetization of syntax for LK, but you don't need that.

@rzach rzach self-assigned this Jul 13, 2017

rzach added a commit that referenced this issue Jul 17, 2017

improve sequent calculus chapter (fixes issue #74 and part of issue #145
); avoid \Proves \lfalse for inconsistency (fixes issue #147)

rzach added a commit that referenced this issue Jul 17, 2017

rzach added a commit that referenced this issue Aug 8, 2017

completeness via complete sets and clearer more detailed proofs; stan…
…dard sequent calculus w/ sequences; better soundness proof for LK; standard natural deduction rules (fixes issues #38, #74, #144, #145, #147) (#143)

completeness via complete sets and clearer more detailed proofs; standard sequent calculus w/ sequences; better soundness proof for LK; standard natural deduction rules (fixes issues #38, #74, #144, #145, #147)

@rzach rzach closed this Aug 8, 2017

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment