Coinductive well-foundedness

Fuente: arXiv
Saved in:
Bibliographic Details
Main Author: Petrakis, Iosif
Format: Preprint
Published: 2025
Subjects:
Online Access:
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866909669652430848
author Petrakis, Iosif
author_facet Petrakis, Iosif
contents We introduce a coinductive version of the well-foundedness of N that is used in our proof within minimal logic of the constructive counterpart CLNP to the standard least number principle LNP. According to CLNP, an inhabited complemented subset of N has a least element if and only if it is downset located. The use of complemented subsets of N in the formulation of CLNP, instead of subsets of N, allows a positive approach to the subject that avoids negation. Generalising the coinductive well-foundedness of N, we define $\exists$-well-founded sets and we prove their fundamental properties.
format Preprint
id arxiv_https___arxiv_org_abs_2506_16433
institution arXiv
publishDate 2025
record_format arxiv
spellingShingle Coinductive well-foundedness
Petrakis, Iosif
Logic
We introduce a coinductive version of the well-foundedness of N that is used in our proof within minimal logic of the constructive counterpart CLNP to the standard least number principle LNP. According to CLNP, an inhabited complemented subset of N has a least element if and only if it is downset located. The use of complemented subsets of N in the formulation of CLNP, instead of subsets of N, allows a positive approach to the subject that avoids negation. Generalising the coinductive well-foundedness of N, we define $\exists$-well-founded sets and we prove their fundamental properties.
title Coinductive well-foundedness
topic Logic
url https://arxiv.org/abs/2506.16433