In the semantics of natural language, it is a common practice to distinguish between \(\textit{assertion}\) and \(\textit{presupposition}\) when analyzing a sentence. A theory that assigns two levels of meaning, assertion and presupposition, to a sentence is called the “two-dimensional theory.” In the analysis of sentences with indefinite subjects using the two-dimensional theory, it is known that there is no guarantee that the subject in the semantic representation of the presupposition is the same individual as that in the assertion. This problem is commonly called the “binding problem.” As a solution to the binding problem, Sudo (2012, 2014) proposed combining two-dimensional theory with Dynamic Predicate Logic and Plural Predicate Logic. This approach involves analyzing the anaphoric linking between assertion and presupposition as a case of cross-sentential anaphora. This paper points out empirical problems with Sudo’s proposal. We then propose an alternative approach to address the binding problem by using Dependent Type Semantics, an approach grounded in proof-theoretic semantics where assertion and presupposition are treated at a single level of semantic representation.