Forster (2003) showed, in , that if there is a finite-to-one map from 𝒫(A) to a set A, then A must be finite. With the Axiom of Choice ( ), |𝒫(A)|=|Part_n,1(A)| and |A|=|fin(A)| for any infinite set A, where Part_n,1(A) denotes the set of partitions of A whose members have exactly n elements if they are not singletons, where n is a natural number greater than 1, and fin(A) denotes the set of finite subsets of A. However, these equalities are not provable without . In this paper, we give a condition that makes Forster’s theorem provable in when 𝒫(A) is replaced by Part_n,1(A) while, under the same condition, the statement is not provable when A is replaced by fin(A) . We also show that A in Forster’s theorem cannot be replaced by fin(A) .
We define the intuitionistic logic of a binary modality, present its semantics, and prove the completeness theorem.
We prove, in ZFC, that certain Σ^1_2 functions cannot injectively embed ω _1 into a Borel class of fixed countable rank. This had been proved under determinacy or large cardinals by Harrington and Hjorth for all Σ^1_2 functions. Our contribution is to identify conditions under which the determinacy and large cardinal assumptions can be removed. These conditions are sufficient for a recent use of the non-existence of Σ^1_2 injections of ω _1 into Borel classes by Day and Marks.
We present a type-disciplined, compositional reconstruction of the diagonal strategy in Gödel’s first incompleteness theorem. The goal is not a new or “more direct” proof of incompleteness, but an explicit computational unpacking of the mechanism. The paper exhibits a concrete pipeline of code-transformers between primitive recursive syntactic domains, thereby avoiding well-definedness issues arising in Lindenbaum-quotient formulations. A central feature is the separation between a graph-mediated witness form of the Gödel sentence and a canonical normal form, connected by an internal normalization lemma formalizable in the base theory. The paper also presents the construction categorically in a category of primitive recursive code domains and morphisms, and extracts a general diagonal-flipping blueprint clarifying how type stratification distinguishes paradoxical from limitative diagonal arguments.
