Order-type of models of PA
Nobody has claimed this yet.
Assessment
- Difficulty
- 5/5
- Estimated time
- Over a week
- Newbie friendliness
- 30/100
- Issue type
- Documentation
- Clarity
- Mostly clear
- Activity status
- Stale
- Tech stack
- tex
- Domain
- documentation
Research direction
Start with the current presentation of the proof that every non-standard model of PA has order-type N+ZxQ, especially the proposition introducing blocks. Clarify the exact statement of each result, expand the sketchy proofs, and assess where diagrams and a revised proposition sequence would improve the exposition. Done means the advanced result is technically precise without losing its intuitive presentation.
Written by the indexing model from the issue text.
Description
I'd like to do a bit of work on the proof that every non-standard model of PA has order-type N+ZxQ. Some of the proofs are quite sketchy and I'd like to add a bit more detail, but I also wondered about going beyond this and changing the overall presentation to be a bit more precise about what's being proved, and perhaps restructuring the sequence of propositions a bit.
Does this sound reasonable? My thought here is that this is a fairly advanced result by Open Logic standards, and as such if it's being taught at all then it should be ok if it's presented in a somewhat more technical manner. I don't want to lose the intuitiveness of the current presentation (and in fact it would actually be nice to add more diagrams, as I think this is a result which is particularly amenable to them) but when I was teaching this myself I found it wasn't always clear what the exact statement of a given result was (e.g. in the proposition that introduces the idea of a block).
- Dominant language
- TeX
- Stars
- 1.4k
- Forks
- 289
- PR merge metrics
- No merged PRs in 30d
Getting set up
This project ships no dev container, Dockerfile or contributing guide, so setting up is up to you: start from its README, and see our first-contribution guide for the general steps.
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
More from OpenLogicProject/OpenLogic
-
Difficulty 1/5 Under an hour Newbie friendliness 65/100
OpenLogicProject/OpenLogic#339 · 1 comment ·
-
Difficulty 4/5 3-5 days Newbie friendliness 50/100
OpenLogicProject/OpenLogic#436 ·
-
Difficulty 3/5 1-2 days Newbie friendliness 68/100
OpenLogicProject/OpenLogic#435 · 1 comment ·
-
Improve docsOpen
Difficulty 5/5 Over a week Newbie friendliness 25/100
OpenLogicProject/OpenLogic#390 ·
-
Difficulty 4/5 3-5 days Newbie friendliness 30/100
OpenLogicProject/OpenLogic#389 · 1 comment ·
All issues in OpenLogicProject/OpenLogic
Similar issues
-
Difficulty 1/5 Under an hour Newbie friendliness 85/100
carpentries/workshop-template#918 ·
-
Logo RedirectOpen
Difficulty 2/5 1-3 hours Newbie friendliness 85/100
-
Purestorage backend configuration example contains hyphens instead of underscoresPossibly taken @wilkmar claimed this today. Open
Difficulty 1/5 Under an hour Newbie friendliness 90/100
-
Difficulty 1/5 Under an hour Newbie friendliness 67/100
materialdigital/core-ontology#528 ·
Maintainers usually reply within 1 day
-
triage-needed
Difficulty 2/5 1-3 hours Newbie friendliness 76/100
MicrosoftDocs/edge-developer#3970 ·
Maintainers usually reply within 1 day