Haoyi Zeng: Research Project
The downward LöwenheimSkolem theorem and the blurred drinker paradox
Advisors: Dominik Kirst
Summary
The Downward LöwenheimSkolem theorem (DLS) is a fundamental metatheorem of firstorder logic, stating that any infinite model (over a countable signature) has a countably infinte elementary submodel. It is a wellknown 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öwenheimSkolem Theorem: here

An outofdate Memo and Slide, where the theorem is considered on a small fragment syntax.
Legal notice, Privacy policy