On Generalized Ordered Sets: A constructive development

TL;DR

This paper introduces a generalized order concept and a new weak order to address issues in constructive mathematics, especially regarding real numbers and strict partial orders.

Contribution

It proposes a novel generalized order and a modified weak order suitable for constructive settings, improving the handling of strict partial orders.

Findings

A new notion of generalized order is defined.

A weak order alternative is introduced for constructive mathematics.

The approach resolves issues with strict orders on real numbers.

Abstract

We propose a notion of a generalized order, which can be used for the notion of a strict partial order. We introduce a weak order to replace the usual weak order defined from a strict partial order. In a constructive setting, that usual weak order causes problems on the real numbers because their strict order cannot be proved to be trichotomous.