Iset axioms #423
Merged
Iset axioms #423
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Don't refer to ax-3. Revise truth table text for intuitionistic logic. Rewording to reflect additional propositional logic axioms.
Bring over the comment from set.mm about "obsolete" and "New usage is discouraged". Remove text about logical redundancy; that has not (yet at least) been proved for intuitionistic logic. Change two proofs to use ax16 instead of ax-16, since we consider the latter to be obsolete.
Bring over text from set.mm about "obsolete" and "New usage is discouraged"
- Add propositional logic axioms - List the axioms which are unchanged - Remove ax-i11e because that is no longer an axiom in iset.mm.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This is a bit more tidying of iset.mm axioms, mostly in the comments but also:
In ax-16 vs ax16
In the "intuitionistic logic" section of set.mm (where we prove the iset.mm axioms from set.mm axioms).