How to Recover a Set from its Closure under Logical Consequence Let $S$ be a set of sentences from first order logic that is closed under logical consequence. Letting $C$ denote the logical closure operator, we have $S=C(S)$. 
Suppose that there is a set $A$ of sentences from first order logic such that $A$ is finite and $C(A)=S$. 
Is there a way to determine $A$ from $S$?
In other words, is there an algorithm for determining which elements of $S$ are also elements of $A$?
 A: If you had a specific $A$ that led to $S$, then no, you cannot recover $A$ from $S$, even if you knew that $A$ is finite ($S$, of course, will be infinite, because there are infinitely many tautologies that will all be in $S$).
For example, if you had $P \land Q \in S$, you don't know whether you had $P \land Q \in A$, or both $P \in A$ and $Q \in A$, or maybe all three, or maybe both $P$ and $P \land Q$, or maybe both $Q$ and $P \land Q$, or maybe just $Q \land P$, or ...
Something you could do, is to find a kind of 'minimal' set whose closure is $S$. See prime implicants for one way to think about that. However, the techniques discussed there are for propositional logic, and for first-order logic things will get a lot more complicated ... indeed, you may well run into the problem of the undecidability of first-order logic when trying to find such a 'minimal' set.
Finally, as I said, $S$ will be of infinite size, so there are some serious practical considerations to deal with here as well!
