Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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.

share|improve this question
    
See also the nice HOL overview article "The Seven Virtues of Simple Type Theory" by. W. Farmer (imps.mcmaster.ca/doc/seven-virtues.pdf) –  Makarius Mar 8 '13 at 14:06
add comment

3 Answers

up vote 4 down vote accepted

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.

share|improve this answer
    
I think you caught what I'm asking. In essence, the whole concept of "full semantics" is what troubles me. How can it be taken as a "well-defined" term, if higher order logics which fulfill categoricity need a FO meta-theory of set-theoretical flavour to prove the categoricity of what "they say" with their "more expressive power"? Where does the "expressivity" come from, if you've used a non-categorical set theory to prove it? If I get it right, it seems to be nearly the same problem as when considering the "standard universe" of set theory. It's just intuition? What's "formal" about that? –  Mono Jul 30 '12 at 14:57
    
Right, higher-order logic with full semantics is not "formal" in that sense, and the issue is very related to the issue of the "standard model" of set theory. –  Carl Mummert Jul 30 '12 at 15:13
    
Thank you very much. This question was related to another which I cite in the first paragraph; the sense of the word "fundamental" I used there, is more or less the same we've discussed here under the adjective "formal", except for the added meaning of being able to "simulate" other logics from a mathematical point of view (e.g. fuzzy logics can be formalized in a FO mathematical theory which supports the real numbers, and define the "fuzzy membership" as an ordered pair). –  Mono Jul 30 '12 at 15:51
    
I'd really appreciate if you could leave an answer there, because I didn't find any of the current ones satisfactory. –  Mono Jul 30 '12 at 15:52
add comment

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.

share|improve this answer
    
The claim "FOL cannot express transitive closure" is somewhat vague. ZFC can certainly define the transitive closure of a relation, and is a first order theory. Anything that can be expressed in HOL can be expressed, by exactly the same sentence, in FOL. The only difference is in semantics - but HOL has several semantics, the weakest of which has the same strength as FOL. Everything Isabelle does is compatible with these semantics; Isabelle has no way to tell what semantics I use to interpret its output. If I use Henkin semantics, Isabelle will have the same semantic limitations as FOL. –  Carl Mummert Jul 30 '12 at 12:12
    
@Carl Mummert: I suppose I should make a distinction. While in ZF you can express the transitive closure of a relation between sets, it can't express the closure of logical relations such at $\in$; FOL can't do that. On the other hand, Isabelle/HOL doesn't have this problem. Likewise, Isabelle/HOL does not just encode Henkin's higher order calculus; it also includes extensions such as the axiom of choice. Isabelle/HOL can be embedded to ZFC, but that's not the same being embeddable in FOL simpliciter (like Henkin's higher order calculus can). –  Matt W-D Jul 30 '12 at 12:30
    
Henkin's method works with arbitrary choice and comprehension axioms added in; indeed these are typically used in second-order logic, even with Henkin semantics. Furthermore, it is certainly possible to express, within ZFC, the transitive closure of an arbitrary set or class $A$ under the $\in$ relation: a set $b$ is in the transitive closure of $A$ if and only if there is a finite chain $b \in a_n+1 \in a_n \in \cdots \in a_1$ where $a_1 \in A$. That can be written as a single sentence of ZFC. –  Carl Mummert Jul 30 '12 at 12:36
1  
(That's the transitive closure in the set theoretic sense. For the transitive closure in the order theoretic sense, we would put $b \in^* a$ if there is a finite chain $b \in a_{n+1} \in \cdots \in a_1 = a$ where $a_{n+1}, a_n, \ldots, a_1$ are all in $A$. This is again a single sentence of ZFC. In general, if we can define the transitive closure of any relation $R$ then we can define the transitive closure of $\in$ by just replacing $R$ with $\in$ in the definition.) –  Carl Mummert Jul 30 '12 at 12:46
1  
I think the issue is that FOL is not a single logic. There are many "first order" logics with slightly different syntax. They are all first order in the sense that they have effective deductive systems, semantics using ordinary first-order structures, and completeness theorems. The FOL that people usually see first doesn't have types, $\lambda$ terms, or set quantifiers, but these are easy to add while preserving completeness. Usually $\lambda$ terms are only seen in proof theory or computational settings, for example in higher-order arithmetic, as in Kohlenbach's Applied Proof Theory. –  Carl Mummert Jul 30 '12 at 14:06
show 2 more comments

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).

share|improve this answer
    
What confuses me is that, even if your argument is absoltely sound (computers only follow syntactical rules and don't care about semantics), then it seems to follow that every logic of a higher order than FOL is necessarily computed like if it was a many-sorted FOL (i.e. doesn't recognizing, for example, that second-order variables range over subsets of the same set which first-order variables range over). I suspect I'm missing something here, though. –  Mono Jul 29 '12 at 20:41
    
@Mono: It is true that the syntactic character of proof checking for HOL is the same as for a many-sorted FOL. What characterizes HOL is that there are usually specific logical axioms and/or rules of inference dealing with higher-order variables and ensuring, for example, that everything that is definable an an explicit formula is also considered when we quantify a higher-order variable of an appropriate signature. ...(contd) –  Henning Makholm Jul 29 '12 at 20:49
    
... We're free to consider these special rules to be part of the theory proper instead of part of the logic, and the result would be a first-order theory that could prove the same thing -- essentially the original higher-order theory would be embedded in a (possibly weak) version of first-order set theory. The position that all higher-order logic is just an abbreviation for set theory was championed by Quine, and largely carried the day until the advent of practical computer proof systems made clear how cumbersome it is to reduce everything explicitly to first order all the time. –  Henning Makholm Jul 29 '12 at 20:53
    
Note also that the fact the the logical axioms for higher-order variables are always the same (in contrast to if they were just incidental parts of the subject theory) makes it more practical for developers of proof assistants to provide special-cased general strategies for using them which allow users to specify common reasoning patterns easily. –  Henning Makholm Jul 29 '12 at 20:55
1  
@Mono: It's unclear to me why you're suddenly speaking about categoricity and models -- those are semantic properties which proof checkers/assistants don't care about. All they care about is the existence of a valid proof in some formal system; whether the formal system corresponds to any semantic notion of model is not their problem. –  Henning Makholm Jul 30 '12 at 11:17
show 6 more comments

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.