Semantics of Higher-Order Logics 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.
 A: Here are some further possibilites:


*

*Propositional logic: can be interpreted in any Boolean algebra (assuming you are talking about classical logic here), but perhaps your notion of truth assignment allows for truth values as elements of Boolean algebras. Alternatively, via the Curry-Howard correspondence propositions may be interpreted as types and proofs as terms of those types.

*Predicate logic (first-order and higher-order): can in general be interpreted in suitable categories or fibrations. For example, higher-order logic can be interpreted in a topos (which must be Boolean if your logic is classical).
In general, if you are looking for interpretations of various kinds of logic in ways other than first-order model theory, you should look at categorical logic. There various possibilities (multi-sorted vs. single-sorted, intuitionistic vs. classical, etc) are systematically considered. Also, the ad-hoc distinction between "full" vs. "Henkin-style" semantics (which depends on the idea that there is a "true" set theory in the background, as far as I can tell) is replaced with a much more advanced notions (such as properties of fibrations that are used to interpret logic). A place to start looking would be Bart Jacob's "Categorical logic and type theory", although it's not an easy reading. There should be some lecture notes on the internet that are more accessible, perhaps someone can suggest them?
I am not sure what you mean by "valid interpretation". If you just mean soundness (provable things are valid) then all of the possibilities mentiond are "valid". But I suspect you mean something else.
A: I just say something about your fourth question.  In many-sorted logic you have a partition of the domain of your structure into different sorts.  An example would be the disjoint union of a vector space over a field $K$ and the field $K$ itself.  Both sorts (vectors and scalars) 
carry their usual structure (abelian group resp. field) and there is the scalar multiplication
that connects the two.  
Now a structure for Henkin semantics can be constructed as a many-sorted first order structure as follows. 
Assume we have a logic that is first order + quantification over subsets of the first order structure.  The usual Henkin semantics for this would use first order structures 
together with a collection of "internal" subsets of the structure, which are the sets that the 
second order quantifiers run over.
Instead we consider a two-sorted structure in which the first sort is isomorphic to the first order structure above and there is a second sort, namely the collection of all internal subset
as used in the Henkin semantics model.  The two sorts are connected by a binary relation,
the relation $\in$.  Now quantification over subsets of the first order structure is emulated by first-order quantification over the elements of the second sort.  
Semantics for higher order logics can be handled in a similar fashion.
I hope this clarifies this part of your question.
