Read about our upcoming Code of Conduct on this issue

Commit dcebca5c authored by Lukas Stevens's avatar Lukas Stevens
Browse files

Extend entry Szpilrajn

parent 46026e61801e
......@@ -9049,15 +9049,19 @@ abstract =
Mathematical Logic for Computer Science.
title = Szpilrajn Extension Theorem
author = Peter Zeller <>
title = Order Extension and Szpilrajn's Extension Theorem
author = Peter Zeller <>, Lukas Stevens <>
topic = Mathematics/Order
date = 2019-07-27
notify =
abstract =
We formalize the Szpilrajn extension theorem, also known as
order-extension principal: Every strict partial order can be extended
to a strict linear order.
This entry is concerned with the principle of order extension, i.e. the extension of an order relation to a total order relation.
To this end, we prove a more general version of Szpilrajn's extension theorem employing terminology from the book "Consistency, Choice, and Rationality" by Bossert and Suzumura.
We also formalize theorem 2.7 of their book.
extra-history =
Change history:
(by Lukas Stevens) generalise Szpilrajn's extension theorem and add material from the book "Consistency, Choice, and Rationality"
title = A Formal Development of a Polychronous Polytimed Coordination Language
This diff is collapsed.
......@@ -31,3 +31,12 @@
year = 1930
ISBN = {9780674052994},
author = {Walter Bossert and Kotaro Suzumura},
title = {Consistency, Choice, and Rationality},
doi = {},
publisher = {Harvard University Press},
year = {2010}
......@@ -14,7 +14,7 @@
\title{Szpilrajn Extension Theorem}
\author{Peter Zeller}
\author{Peter Zeller and Lukas Stevens}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment