arXiv subjects

Tin Lok Wong

Publications and source records attributed to Tin Lok Wong.

5 recordsLinked to original sources

arXiv2025

Definability over $\mathrm BΣ^0_2$-models

Let $\mathfrak M=(M,\mathcal X)$ be a model of $\mathsf{RCA}_0+\text{$Σ^0_2$-bounding}$ in which $Σ^0_2(A)$-induction fails for some $A\in\mathcal X$. We show that (i) if $\mathfrak M$ is a model of the combinatorial principle Ramsey's Theorem for Pairs, the Cohesive Set Theorem or the Tree Theorem, then there is a $Δ^0_1(A)$-instance of the principle with no solution in $\mathfrak M$ that is arithmetically definable relative to $A$; and (ii) any set of minimal Turing degree in $\mathfrak M$ that is arithmetically definable relative to $A$ has Turing jump equivalent to $A'$.

math.LO↗

arXiv2022

An isomorphism theorem for models of Weak König's Lemma without primitive recursion

We prove that if $(M,\mathcal{X})$ and $(M,\mathcal{Y})$ are countable models of the theory $\mathrm{WKL}^*_0$ such that $\mathrm{I}Σ_1(A)$ fails for some $A \in \mathcal{X} \cap \mathcal{Y}$, then $(M,\mathcal{X})$ and $(M,\mathcal{Y})$ are isomorphic. As a consequence, the analytic hierarchy collapses to $Δ^1_1$ provably in $\mathrm{WKL}^*_0 + \neg\mathrm{I}Σ^0_1$, and $\mathrm{WKL}$ is the strongest $Π^1_2$ statement that is $Π^1_1$-conservative over $\mathrm{RCA}^*_0 + \neg\mathrm{I}Σ^0_1$. Applying our results to the $Δ^0_n$-definable sets in models of $\mathrm{RCA}^*_0 + \mathrm{B}Σ^0_n + \neg\mathrm{I}Σ^0_n$ that also satisfy an appropriate relativization of Weak König's Lemma, we prove that for each $n \ge 1$, the set of $Π^1_2$ sentences that are $Π^1_1$-conservative over $\mathrm{RCA}^*_0 + \mathrm{B}Σ^0_n + \neg\mathrm{I}Σ^0_n$ is c.e. In contrast, we prove that the set of $Π^1_2$ sentences that are $Π^1_1$-conservative over $\mathrm{RCA}^*_0 + \mathrm{B}Σ^0_n$ is $Π_2$-complete. This answers a question of Towsner. We also show that $\mathrm{RCA}_0 + \mathrm{RT}^2_2$ is $Π^1_1$-conservative over $\mathrm{B}Σ^0_2$ if and only if it is conservative over $\mathrm{B}Σ^0_2$ with respect to $\forall Π^0_5$ sentences.

math.LO↗

arXiv2021

Ramsey's theorem for pairs, collection, and proof size

We prove that any proof of a $\forall Σ^0_2$ sentence in the theory $\mathrm{WKL}_0 + \mathrm{RT}^2_2$ can be translated into a proof in $\mathrm{RCA}_0$ at the cost of a polynomial increase in size. In fact, the proof in $\mathrm{RCA}_0$ can be found by a polynomial-time algorithm. On the other hand, $\mathrm{RT}^2_2$ has non-elementary speedup over the weaker base theory $\mathrm{RCA}^*_0$ for proofs of $Σ_1$ sentences. We also show that for $n \ge 0$, proofs of $Π_{n+2}$ sentences in $\mathrm{B}Σ_{n+1}+\exp$ can be translated into proofs in $\mathrm{I}Σ_{n} + \exp$ at polynomial cost. Moreover, the $Π_{n+2}$-conservativity of $\mathrm{B}Σ_{n+1} + \exp$ over $\mathrm{I}Σ_{n} + \exp$ can be proved in $\mathrm{PV}$, a fragment of bounded arithmetic corresponding to polynomial-time computation. For $n \ge 1$, this answers a question of Clote, Hájek, and Paris.

math.LO↗

arXiv2019

Where Pigeonhole Principles meet König Lemmas

We study the pigeonhole principle for $Σ_2$-definable injections with domain twice as large as the codomain, and the weak König lemma for $Δ^0_2$-definable trees in which every level has at least half of the possible nodes. We show that the latter implies the existence of $2$-random reals, and is conservative over the former. We also show that the former is strictly weaker than the usual pigeonhole principle for $Σ_2$-definable injections.

math.LO↗

arXiv2018

Some observations on the logical foundations of inductive theorem proving

In this paper we study the logical foundations of automated inductive theorem proving. To that aim we first develop a theoretical model that is centered around the difficulty of finding induction axioms which are sufficient for proving a goal. Based on this model, we then analyze the following aspects: the choice of a proof shape, the choice of an induction rule and the language of the induction formula. In particular, using model-theoretic techniques, we clarify the relationship between notions of inductiveness that have been considered in the literature on automated inductive theorem proving. This is a corrected version of the paper arXiv:1704.01930v5 published originally on Nov.~16, 2017.

cs.LO↗