**Abstract**

This dissertation concerns theories of bounded arithmetic and
propositional proof systems associated with PSPACE and classes from
the exponential-time hierarchy.

The second-order viewpoint of Zambella and Cook associates
second-order theories of bounded arithmetic with various complexity
classes by studying the definable functions of strings, rather than
numbers. This approach simplifies presentation of the theories and
their propositional translations, and furthermore is applicable to
complexity classes that previously had no corresponding theories. We
adapt this viewpoint to large complexity classes from the
exponential-time hierarchy by adding a third sort, intended to
represent exponentially long strings (``superstrings''), and capable
of coding, for example, the computation of an exponential-time Turing
machine. Specifically, our main theories $W^i_1$ and $TW^i_1$ are
associated with PSPACE$^{\Sigma^p_{i-1}}$ and
EXP$^{\Sigma^p_{i-1}}$, respectively. We also develop a model for
computation in this third-order setting including a function calculus,
and define third-order analogues of ordinary complexity classes. We
then obtain recursion-theoretic characterizations of our function
classes for FP, FPSPACE and FEXP. We use our characterization of
FPSPACE as the basis for an open theory for PSPACE that is a
conservative extension of a weak PSPACE theory $HW0_1$.

Next we present strong propositional proof systems \QBP[i], which are
based on the Boolean program proof system \BPLK but additionally with
quantifiers on function symbols. We exhibit a translation of theorems
of $W^i_1$ into polynomial-sized proofs in \QBP[i].

**Table of Contents**

1. Introduction 2. Preliminaries and Related Work 3. The Third-Order Viewpoint 4. Third-Order Theories 5. Definability in the Theories 6. A Universal Conservative Extension of $HW0_1$ 7. Witnessing Theorems 8. Propositional Translations 9. Future Work