![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-oexpi | GIF version |
Description: Define the ordinal
exponentiation operation.
This definition is similar to a conventional definition of exponentiation except that it defines โ โo ๐ด to be 1o for all ๐ด โ On, in order to avoid having different cases for whether the base is โ or not. We do not yet have an extensive development of ordinal exponentiation. For background on ordinal exponentiation without excluded middle, see Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg, and Chuangjie Xu (2025), "Ordinal Exponentiation in Homotopy Type Theory", arXiv:2501.14542 , https://arxiv.org/abs/2501.14542 which is formalized in the TypeTopology proof library at https://ordinal-exponentiation-hott.github.io/. (Contributed by Mario Carneiro, 4-Jul-2019.) |
Ref | Expression |
---|---|
df-oexpi | โข โo = (๐ฅ โ On, ๐ฆ โ On โฆ (rec((๐ง โ V โฆ (๐ง ยทo ๐ฅ)), 1o)โ๐ฆ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | coei 6415 | . 2 class โo | |
2 | vx | . . 3 setvar ๐ฅ | |
3 | vy | . . 3 setvar ๐ฆ | |
4 | con0 4363 | . . 3 class On | |
5 | 3 | cv 1352 | . . . 4 class ๐ฆ |
6 | vz | . . . . . 6 setvar ๐ง | |
7 | cvv 2737 | . . . . . 6 class V | |
8 | 6 | cv 1352 | . . . . . . 7 class ๐ง |
9 | 2 | cv 1352 | . . . . . . 7 class ๐ฅ |
10 | comu 6414 | . . . . . . 7 class ยทo | |
11 | 8, 9, 10 | co 5874 | . . . . . 6 class (๐ง ยทo ๐ฅ) |
12 | 6, 7, 11 | cmpt 4064 | . . . . 5 class (๐ง โ V โฆ (๐ง ยทo ๐ฅ)) |
13 | c1o 6409 | . . . . 5 class 1o | |
14 | 12, 13 | crdg 6369 | . . . 4 class rec((๐ง โ V โฆ (๐ง ยทo ๐ฅ)), 1o) |
15 | 5, 14 | cfv 5216 | . . 3 class (rec((๐ง โ V โฆ (๐ง ยทo ๐ฅ)), 1o)โ๐ฆ) |
16 | 2, 3, 4, 4, 15 | cmpo 5876 | . 2 class (๐ฅ โ On, ๐ฆ โ On โฆ (rec((๐ง โ V โฆ (๐ง ยทo ๐ฅ)), 1o)โ๐ฆ)) |
17 | 1, 16 | wceq 1353 | 1 wff โo = (๐ฅ โ On, ๐ฆ โ On โฆ (rec((๐ง โ V โฆ (๐ง ยทo ๐ฅ)), 1o)โ๐ฆ)) |
Colors of variables: wff set class |
This definition is referenced by: fnoei 6452 oeiexg 6453 oeiv 6456 |
Copyright terms: Public domain | W3C validator |