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

Replace maximal consistency with completeness #38

Closed
rzach opened this Issue Mar 11, 2015 · 3 comments

Comments

Projects
None yet
1 participant
@rzach
Member

rzach commented Mar 11, 2015

In the completeness proof, we should extend to a complete set, ie, one which contains A or ~A for every A. Easier to understand than max consistency. (ht greg restall's videos)

@rzach rzach added the enhancement label Mar 11, 2015

@rzach

This comment has been minimized.

Show comment
Hide comment
@rzach

rzach Sep 15, 2016

Member

Additional reason/perk of this approach: A direct proof of compactness would then follow the completeness construction closely, and could perhaps even be given as a (series of) exercise(s).

Member

rzach commented Sep 15, 2016

Additional reason/perk of this approach: A direct proof of compactness would then follow the completeness construction closely, and could perhaps even be given as a (series of) exercise(s).

@rzach

This comment has been minimized.

Show comment
Hide comment
@rzach

rzach Jul 11, 2017

Member

Hey @nicolewyatt @GillRussell @marcusrossberg do you agree that this would be better?

Does anyone want to retain maximal consistency? The more I think about it the less it seems to me that maximal consistency is an interesting target and I can't think of any application where something is true for maximal consistent but not for complete consistent sets (or is easier to prove). The aim of Lindenbaum's Lemma is to generate a complete set.

Member

rzach commented Jul 11, 2017

Hey @nicolewyatt @GillRussell @marcusrossberg do you agree that this would be better?

Does anyone want to retain maximal consistency? The more I think about it the less it seems to me that maximal consistency is an interesting target and I can't think of any application where something is true for maximal consistent but not for complete consistent sets (or is easier to prove). The aim of Lindenbaum's Lemma is to generate a complete set.

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

@rzach

This comment has been minimized.

Show comment
Hide comment
@rzach

rzach Jul 12, 2017

Member

My proposed changes are in http://people.ucalgary.ca/~rzach/static/open-logic/branches/issue38/
and there's a pull request you can comment on/see the diffs: #143

Member

rzach commented Jul 12, 2017

My proposed changes are in http://people.ucalgary.ca/~rzach/static/open-logic/branches/issue38/
and there's a pull request you can comment on/see the diffs: #143

@rzach rzach self-assigned this Jul 12, 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