Here is a question I have about first order logic using the conventions in Enderton:
First-order deductions in our proof system are obtained via 1) being a member of a set of formulas $\Gamma$, 2) being an instance of six axioms, the set of which we call $\Lambda$,
or 3) obtained via modus ponens from formulas obtained in the previous two ways. Now, consider that the first axiom is that we have an infinite set of first-order tautologies.
(1) Could we have replaced this infinite set of tautologies by a single formula? (2) Could we have replaced this infinite set of tautologies set by a single formula schema? (where we define a schema as being obtained by quantifying over all possible subformulas) i.e., some formula containing generic subformulas.
Here are my thoughts: For question (1), I believe that it is not the case that we can replace all tautologies with a single formula. The obvious candidate is the formula consisting of the conjunction of all tautologies, let's call this formula $\psi$. This formula would be of countable length, but determining whether we are able to write a given formula $\varphi$ in any deduction would no longer involve simply checking whether $\varphi \in \Lambda$. We would now need to check whether $\vdash \{\psi, \varphi\}$ or equivalently $\{\psi, \varphi\}$ is consistent, which presents an equally complicated problem and requires the use of the infinite set of tautologies to determine.
For question (2), the obvious candidate is the schema $\alpha \leftrightarrow (\beta \rightarrow \beta)$ for an atomic formula $\beta$, (which we can easily convert to the limited language provided be Enderton). We are simply providing a formula which checks whether some formula $\alpha$ is tautologically implied by a known tautology. Now, I am not certain whether verification of whether this holds requires the infinite set of tautologies.
I'd greatly appreciate any tips as to whether I'm on the right track.
Yes; there are many equivalent axiomatization of propositional calculus that needs only modus ponens as rule of inference.
A very "classic" one is the three-axioms set used by Mendelson (see e.g. this post).
You can see List of Hilbert systems for many other axiom systems, including the single-axiom systems proposed by Łukasiewicz-Tarski and Meredith (for systems with $\to$ and $\lnot$ as primitive).
Comments: the conjunction of all tautologies is not a well-formed formula of "standard" propositional and first-order logics, where a formula must have finite lenght.
The schema $α ↔ (β → β)$ is not a tautology, and thus it is not allowed as axiom, because it implies the inconsistency of the system.