4
$\begingroup$

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.

Improve this question
$\endgroup$
2
  • $\begingroup$ I've had some good answers to some of the questions so far, but am still looking for further clarification on the others/additions to the existing answers. Thanks. $\endgroup$
    – Noldorin
    Commented Aug 5, 2010 at 7:46
  • $\begingroup$ I will set a bounty on this question if there are no more updates in a few days... my reputation points are pretty meager at the moment, but we'll see. $\endgroup$
    – Noldorin
    Commented Aug 11, 2010 at 9:53

2 Answers 2

Reset to default
9
$\begingroup$

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.

Improve this answer
$\endgroup$
6
  • $\begingroup$ @Andrej: Cheers for the reply. Your discussion of categorical logic is interesting, though my plan was generally to stay clear of it. It seems to be used more in the role of meta-mathematics rather than proof theory. I believe one can create proof calculi for higher-order logic using only type theory, and without category theory (though it is useful for understanding structure). By valid interpretation, I pretty much mean one that 'works' (creates a sound and complete proof theory capable of expressing as the maximal set of proofs). $\endgroup$
    – Noldorin
    Commented Jul 26, 2010 at 13:20
  • $\begingroup$ Also, would you mind elaborating on the dependence of semantics on the formulation of set theory? Full semantics I have heard described as "set theory in sheep's clothing", but what does Henkin semantics have to do with set theory directly? $\endgroup$
    – Noldorin
    Commented Jul 26, 2010 at 13:21
  • $\begingroup$ Ah, the "which" in "which depends on the idea..." in my reply refers (confusingly) to "full" semantics, not Henkin semantics. And of course, you don't really need any semantics to develop proof theory (although I wonder if that's a sensible thing to do). $\endgroup$
    – Andrej Bauer
    Commented Jul 27, 2010 at 6:26
  • $\begingroup$ @Andrej: Oh I see. Clearly, when one designs proof calculus, semantics is not at all in mind. However, can one then interpret the formal system using "full" semantics and things work? Surely completeness is then lost? $\endgroup$
    – Noldorin
    Commented Jul 27, 2010 at 7:33
  • $\begingroup$ Sorry for bothering you, but do you know where is the description of semantics as a fibered category in Bart Jacobs's book you mentioned? $\endgroup$
    – user40276
    Commented Oct 13, 2014 at 21:07
4
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • $\begingroup$ @Stefan: Thanks for the reply. It does make things slightly clearly, though I'm thinking a concrete example might help... $\endgroup$
    – Noldorin
    Commented Jul 26, 2010 at 13:14

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .