Homotopy Type Theory UMyn8W7b (Rev #37, changes)

Showing changes from revision #36 to #37: Added | ~~Removed~~ | ~~Chan~~ged

On foundations

The natural numbers are characterized by their induction principle (in second-order logic/in a higher universe/as an inductive type). If one only has a first order theory, then one cannot have an induction principle, and instead one has a entire category of models. Thus, the first order models of arithmetic typically found in classical logic and model theory do not define the natural numbers, and this is true even of first-order Peano arithmetic.

Closed rational interval intervals arithmetic

The ~~endpoints~~ of closed rational intervals are represented by a ~~subset~~ subtype of the product type $\mathbb{Q} \times \mathbb{Q}$ , defined as:

ClosedIntervalEndpoints ℐ (ℚ) ≔ \sum_{(a, b) : ℚ \times ℚ} (a \leq b)

~~\mathrm{ClosedIntervalEndpoints}(\mathbb{Q})~~ \mathcal{I}(\mathbb{Q}) \coloneqq \sum_{(a, b):\mathbb{Q} \times \mathbb{Q}} (a \leq b)

The elements $[a, b] : ClosedIntervalEndpoints ℐ (ℚ)$ [a, ~~b]:\mathrm{ClosedIntervalEndpoints}(\mathbb{Q})~~ b]:\mathcal{I}(\mathbb{Q}) of the type are the endpoints of the closed rational ~~intervals.~~ intervals, which we shall call rational intervals for short.

There is an embedding $i:\mathbb{Q} \to \mathcal{I}(\mathbb{Q})$ defined by

i(a) \coloneqq [a, a]

Equality of rational intervals is defined as

([a, b] = [c, d]) \coloneqq (a = c) \times (b = d)

Relation to the zero interval

A positive rational interval is defined by

([0, 0] \lt [a, b]) \coloneqq (0 \lt a)

A negative rational interval is defined by

([0, 0] \gt [a, b]) \coloneqq (0 \gt b)

A indefinite rational interval is defined by

([0, 0] \sim [a, b]) \coloneqq ((0 \lt a) \to \emptyset) \times ((0 \gt b) \to \emptyset)

Ordering of the intervals

The strict order of the rational intervals is defined as

([a, b] \lt [c, d]) \coloneqq (b \lt c)

The opposite strict order of the rational intervals is defined as

([a, b] \gt [c, d]) \coloneqq (a \gt d)

The containment relation of the rational intervals is defined as

([a, b] \subseteq [c, d]) \coloneqq (a \geq c) \times (b \leq d)

The opposite containment relation of the rational intervals is defined as

([a, b] \supseteq [c, d]) \coloneqq (a \leq c) \times (b \geq d)

Equality of rational intervals is defined as

([a, b] = [c, d]) \coloneqq ([a, b] \subseteq [c, d]) \times ([a, b] \supseteq [c, d])

Arithmetic of intervals

Zero is defined by

0 \coloneqq [0, 0]

Constants are defined by

c \coloneqq [c, c]

Addition is defined by

[a, b] + [c, d] \coloneqq [a + c, b + d]

Negation is defined by

-[a, b] \coloneqq [-b, -a]

Subtraction is defined by

[a, b] - [c, d] \coloneqq [a, b] + (-[c, d]) = [a - d, b - c]

Scalar multiplication is defined by

c [a, b] \coloneqq [\min(ca, cb),\max(ca, cb)]

One is defined by

1 \coloneqq [1, 1]

Multiplication is defined by

[a, b] \cdot [c, d] \coloneqq [\min(ac, ad, bc, bd), \max(ac, ad, bc, bd)]

The reciprocal is only defined for intervals that are positive or negative: $0 \lt [a, b]$ or $0 \gt [a, b]$ , and is defined by

1/[a, b] \coloneqq [1/b, 1/a]

Division is only defined for intervals in the denominator that are positive or negative: $0 \lt [c, d]$ or $0 \gt [c, d]$ , and is defined by

[a, b]/[c, d] \coloneqq [a, b] \cdot [1/d, 1/c] = [\min(a/c, a/d, b/c, b/d), \max(a/c, a/d, b/c, b/d)]

As a result, the rational intervals are a strict quasiordered field.

Revision on May 11, 2022 at 21:10:27 by Anonymous?. See the history of this page for a list of all contributions to it.