Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2021
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2104.00506 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911239683178496 |
|---|---|
| author | Beeson, Michael |
| author_facet | Beeson, Michael |
| contents | NF set theory using intuitionistic logic is called iNF. We develop the theories of finite sets and their power sets and mappings, finite cardinals and their ordering, cardinal exponentiation, addition, and multiplication. We follow Rosser and Specker with appropriate constructive modifications, especially replacing ``arbitrary subset'' by ``separable subset'' in the definitions of exponentiation and order. It is not known whether iNF proves that the set of finite cardinals is infinite, so the whole development must allow for the possibility that there is a maximum integer; arithmetical computations might ``overflow'' as in a computer or odometer, and theorems about them must be carefully stated to allow for this possibility. The work presented here is intended as a substrate for further investigations of iNF, including the development of Bishop-style constructive mathematics in iNF. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2104_00506 |
| institution | arXiv |
| publishDate | 2021 |
| record_format | arxiv |
| spellingShingle | Finite sets, mappings, cardinals, and arithmetic in intuitionistic NF Beeson, Michael Logic 03E70, 03A05 NF set theory using intuitionistic logic is called iNF. We develop the theories of finite sets and their power sets and mappings, finite cardinals and their ordering, cardinal exponentiation, addition, and multiplication. We follow Rosser and Specker with appropriate constructive modifications, especially replacing ``arbitrary subset'' by ``separable subset'' in the definitions of exponentiation and order. It is not known whether iNF proves that the set of finite cardinals is infinite, so the whole development must allow for the possibility that there is a maximum integer; arithmetical computations might ``overflow'' as in a computer or odometer, and theorems about them must be carefully stated to allow for this possibility. The work presented here is intended as a substrate for further investigations of iNF, including the development of Bishop-style constructive mathematics in iNF. |
| title | Finite sets, mappings, cardinals, and arithmetic in intuitionistic NF |
| topic | Logic 03E70, 03A05 |
| url | https://arxiv.org/abs/2104.00506 |