How are the full semantics of SOL and HOL specified?

Question

In relation to this question about the "fundamental" character of possible logical systems, I realized that I just had an intuitive (and so, inadequate) understanding of the way logics higher than FOL can unambiguously specify the kind of semantics which make up the intended interpretation of their formalisms, inside the formalisms themselves. This is quite a meaningful question, since the ability of an automated system of reasoning at the object-language level can only recognize what is coded in the formalism itself, at that level; and so, those approaches which start from the construction of a model at the meta-level, are a priori ruled out in the sense I'm describing here.

What I'm thinking about are computer systems reasoning with the logic, such as the HOL-based proof assistants, as Isabelle.

So, how are the intended semantics of SOL and HOL specified in a computer system?

P.S. : I have realized that this topic isn't actually new in this site, and has been brought up in other questions like this one.

Answer 1

From the point of view of derivability and syntax, there is no distinction between full higher order semantics and first-order (Henkin) semantics. This is, in one sense, the reason that there is no completeness theorem for full semantics - because the completeness theorem matches derivability with Henkin semantics, and so any genuinely different semantics will not match up with derivability. Syntactic things like proof assistants, which only care about derivability, are somewhat indifferent to semantic issues.

I believe that the main benefit of using higher order logic in proof assistants is that it makes it easier to formalize theorems that have been proven in ordinary mathematics. Even if these theorems could be formalized in, say, Peano arithmetic, by creating entirely new proofs, it is often easier to modify the existing proof to work in higher order logic.

Answer 2

As far as I'm aware, computer proof systems do not care about semantics at all. Their task is to construct and check formal proofs that follow the syntacical rules for what constitutes a valid derivation, and it is then up to the human user to convince himself that the formal system corresponds to his intuition about semantics.

(Well, some proof assistants do care about semantics some of the time, such as if they contain calculation-based decision procedures for specific theories such as ordered fields or Presburger arithmetic. But then -- depending on the level of paranoia used in the development -- the role of these semantic subparts parts is usually just to suggest a syntactic proof that can be verified independently).

Answer 3

I want to clear something up: HOL is not merely multi-sorted FOL

The key difference is in the two systems expressivity. FOL cannot express transitive closure. Here is a nice note explaining why. On the other hand, HOL can express transitive closure. Here's the source code from Isabelle/HOL's implementation if you are interested.

EDIT 1: Note the caveat in the comments: FOL extended with ZF or machinery from arithmetic can express transitive closure. That no extended calculus can do this is not the claim I'm making here, however.

EDIT 2: Likewise, it's inappropriate blindly make use of intuition from Henkin's semantics for his higher order logic, as its application to computer-based HOLs is not straight forward. For one thing, proof assistants are based off of Church's HOL, which predates Henkin's work and has its own peculiarities. Semantics for Church's HOL may given using applicative structures, as per Harvey Friedman (1975) and subsequent papers.

---

[H]ow are the intended semantics of SOL and HOL specified in a computer system?

You can't really specify the semantics, as others have noted, but there are different ways that $x \in A$ gets parsed into base syntax.

In Isabelle, you can load either Isabelle/ZF or Isabelle/HOL. Depending on which system you load, $x \in A$ gets interpreted differently.

In Isabelle/ZF, it's the meaning you learned in set theory class: $\in$ is a binary relation in FOL and it obeys the various axioms in set theory.

In Isabelle/HOL, S :: 'x set (ie, "S is a set of objects of type 'x") is really just a wrapper for an object of type f :: 'x -> bool (ie, "f is an indicator function that take 'x to True/False"). Set comprehension and membership are effectively defined by the equivalence $a \in \{x \ |\ P(x) \} \iff P(a)$. You can read about it in Isabelle/HOL's source if you're into that sort of thing.

In both Isabelle/ZF and Isabelle/HOL, the familiar syntax $\{x \in S\ |\ \phi(x)\}$ is also interpreted as syntactic sugar. In both cases, it's the parser's responsibility for compiling the extended syntax into the base syntax; and how it is done differs based on foundation.

Finally, while computer proof assistants are not generally used to reason about their own semantics, there is an exception. John Harrison developed two relative consistency proofs of HOL-Light within HOL-Light here.

He first demonstrates how to construct a full model of HOL-Light without the axiom of infinity in HOL-Light. He then shows how to construct a full model of all of HOL-Light in HOL-Light extended with a strongly inaccessible cardinal.