If we choose the first alternative, then we may go on to identify any two propositions that can be transformed into each other by Boolean identities. In the second alternative we will want the extensional forms of the same laws. When we get to quantification a similar choice will arise, but if we choose the first alternative, it will be undecideable whether two expressions denote the same concept. I doubt that considerations of linguistic usage or usefulness in AI will unequivocally recommend one alternative, so both will have to be studied. Actually there are more than two alternatives.
Similar possibilities arise in modal logic.
We will write the rest of our modal axioms in extensional form.