I've been trying to get to grips with the various semantics commonly discussed in formal logic. Specifically, the nature and role of interpretations of first and higher-order logics is slightly unclear.

Here are a few of the specific questions that have occurred to me:

- Propositional logic only has one sensible interpretation, that is truth assignment. Correct?
- Predicate (first-order) logic has an interpretation that may be defined by the domain of discourse. For a given formal system (proof calculus), there is typically a single valid interpretation?
- Higher order logic has full semantics and Henkin semantics. Are there any other valid/commonly-used interpretations?
- What exactly is the relation between many-sorted first-order logic and Henkin semantics? Many-sorted logic looks rather akin to type theory, what differences should I be aware of?
- What are the (common) valid interpretations for higher-order logic that permit a valid proof theory. Henkin semantics is certainly one, while full semantics seems not to be - are there any others? Do Henkin semantics pose any problems (soundness/completeness)?
- Generally, what aspects of a given proof calculus are orthogonal? i.e. type of logic (classical, intuitionistic, constructive), deduction system (natural, sequent, Hilbert), semantics (full, Henkin) - these three aspects should fully specify a proof caculus if I'm not mistaken.

Explanations and clarifications regarding these questions and thoughts would be much appreciated.