Name
Abstract | ||
|---|---|---|
In constructive mathematics it is of interest to consider a more general, but classically equivalent, notion of linear order, a so-called pseudo-order. The prime example is the order of the constructive real numbers. We examine two kinds of constructive completions of pseudo-orders: order completions of pseudo-orders and Cauchy completions of (non-archimedean) ordered groups and fields. It is shown how these can be predicatively defined in type theory, also when the underlying set is non-discrete. Provable choice principles, in particular a generalisation of dependent choice, are used for showing set-representability of cuts. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1016/j.apal.2004.12.005 | Annals of Pure and Applied Logic |
Keywords | Field | DocType |
03F60,06A05,06B23,06F20,12J15,12J25 | Prime (order theory),Discrete mathematics,Constructive proof,Combinatorics,Constructivism (mathematics),Constructive,Generalization,Type theory,Cauchy distribution,Real number,Mathematics | Journal |
Volume | Issue | ISSN |
135 | 1 | 0168-0072 |
Citations | PageRank | References |
2 | 0.58 | 2 |
Authors | ||
1 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Erik Palmgren | 1 | 233 | 43.17 |