For a set of sentences $A$, denote by $\langle A\rangle$ the set of sentences which can be derived from $A$ in some formal system.
Define the equivalence relation $\sim$ on the set of finite sets of sentences as follows:
$S_1\sim S_2$ if and only if
for every sentence $s\in S_1$, $S_2\vdash s$ - i.e. $S_2\vdash S_1$
for every sentence $s\in S_2$, $S_1\vdash s$ - i.e. $S_1\vdash S_2$
Let $A_1$ and $A_2$ be consistent sets of sentences.
Is it the case that $A_1\sim A_2\implies \langle A_1\rangle=\langle A_2\rangle$
A quick proof sketch suggests that the answer is "yes," but I'd like to verify this against a more formal proof.
proof-sketch:
$A$ is an axiomatization of a theory $T$, and we write $T=\langle A\rangle$ iff $A\vdash t$ for every $t\in T$ ($A\vdash T$ for short) (def)
If $A_1\sim A_2$, then $A_1\vdash A_2$ (def)
Suppose $A_2\vdash T$. Then $\langle A_2\rangle$.
Suppose $A_1\sim A_2$. Then $A_1\vdash A_2$.
From $A_1\vdash A_2$ and $A_2\vdash T$, derive $A_1\vdash T$ (something vaguely cut elimination - this is where I'm unsure).
Either way, I imagine that this is a proven theorem somewhere, so any reference is appreciated!
Yes, this is true.
(I preseume $\langle X\rangle=\{p:X\vdash p\}$. This is generally denoted "$Ded(X)$" or "$Th(X)$.")
However, I can't really follow your proof sketch, so let me summarize the situation below (this may be what you intended):
The key point is that proofs are finite: if $A\vdash p$ then $A'\vdash p$ for some finite $A'\subseteq A$, since every proof can only use finitely many axioms. So infinite sets of axioms don't pose any difficulty here.
We can use this as follows. Suppose $X$ proves each sentence in $Y$ and $Y$ proves $p$. Then some finite $\{y_1,...,y_k\}\subseteq Y$ proves $p$. We now "paste together" the relevant $X$-proofs of $y_1,...,y_k$ to get an $X$-proof $\pi_1$ of $y_1\wedge ...\wedge y_k$; conversely, we can turn the $\{y_1,...,y_k\}$-proof of $p$ into a $\{y_1\wedge ...\wedge y_k\}$-proof $\pi_2$ of $p$. We now "compose" the proofs $\pi_1$ and $\pi_2$ to get an $X$-proof of $p$, as desired.
(Incidentally, this "composability" property is generally considered fundamental in the study of abstract logics; for example, the lovely volume "Algebraizable logics" by Blok/Pigozzi lists it as axiom $(3)$ for deductive systems.)
It's worth noting that the "semantic" version is substantially more interesting: there, we need the highly nontrivial compactness theorem (or the equally-nontrivial completeness theorem, which will let us reduce it to the straightforward "syntactic" version above).