We write 'If A, then B' to mean that if A is true, then B must be true because B is a logical consequence of A i.e. it is impossible for A to be true but B to be false.
Let us consider one such statement:
'If S1 , then S2' is true, where S1, S2 are expressions.
Let it also be the case that : 'If Si , then S2' is true, and let there be many such Si. For all such Si and S1, assume they do not contradict each other, and indeed there is a finite deduction from all Si and S1 to S2.
Now for a given S2, I want to generate a finite conjunction of expressions which, so to speak, encodes necessary properties of the premises so that the conclusion (S2 in this case) is the logical consequence of the premise (all such Si). Ideally, this expression must take in some input, and yield some Si, and with appropriate set of constraints, we should be able to generate all Si. (For sufficiency, we may append some disjunction expressions as well if need be).
Is there a method to generate such an expression?