Haoyi Zeng: Research Project
The downward Löwenheim-Skolem theorem and the blurred drinker paradox
Advisors: Dominik Kirst
Summary
The Downward Löwenheim-Skolem theorem (DLS) is a fundamental meta-theorem of first-order logic, stating that any infinite model (over a countable signature) has a countably infinte elementary submodel. It is a well-known result in reverse mathematics that DLS is equivalent to dependent choice (DC) over classical foundations such as ZF set theory. In this project we reexamine this equivalence from the perspective of constructive reverse mathematics over dependent type theory, allowing for a finer analysis of the necessary logical principles.
Concretely, Over CC, the DLS theorem is equivalent to the conjunction of DC with a newly identified principle weaker than LEM that
we call the blurred drinker paradox (BDP), and without CC, the
DLS theorem is equivalent to the conjunction of BDP with similarly
blurred weakenings of DC and CC. Orthogonal to their connection
with the DLS theorem, we also study BDP and the blurred choice
axioms in their own right, for instance by showing that BDP is
LEM without some contribution of Markov’s principle and that
blurred DC is DC without some contribution of CC.
Current state
Below, you can find a document that includes definitions and results. Currently, we are in the process of drafting the preliminary version.
Resources
-
Overview of the Löwenheim-Skolem Theorem: here
-
An out-of-date Memo and Slide, where the theorem is considered on a small fragment syntax.
Legal notice, Privacy policy
