9
$\begingroup$

First-order order classical logic with standard semantics has a proof theory: it is complete, sound and effective.

In higher order logic with standard semantics one cannot obtain a proof theory - it cannot be simulateously complete, sound and effective.

Now, the internal language of a topos is higher order typed intuitionistic logic. Presumably like higher order classical logic it won't have nice meta-logical properties either.

Is there a nice characterisation for toposes with these nice properties for its internal language?

Improve this question
$\endgroup$
6
  • 1
    $\begingroup$ Hi, I don't really understand what you mean by completeness and soundness in this context. Maybe you should clarify your thought ? For classical logic (or higher order logic) these properties make sense because the logic is defined by a set of rules and axiome and you can indeed show that "something is true if and only if it is provable" but for the internal logic of a precise topos $T$ there is no such set (or at least not a canonical one ! ) $\endgroup$
    – Simon Henry
    Commented Jun 3, 2013 at 8:25
  • $\begingroup$ I am unsure how to interpret "effectivity". How can completeness be a problem for ineffective logics? $\endgroup$
    – Wouter Stekelenburg
    Commented Jun 3, 2013 at 9:42
  • $\begingroup$ I agree that completeness and effectivity fail for classical higher-order logics, but why do you say that soundness fails? If one chooses axioms and rules of inference in a reasonable way, soundness should hold. $\endgroup$
    – Andreas Blass
    Commented Jun 3, 2013 at 13:08
  • $\begingroup$ I tihnk he means the combination soudness+completeness+effectivness with respect to set-theoretic semantics. $\endgroup$
    – Andrej Bauer
    Commented Jun 3, 2013 at 13:12
  • $\begingroup$ I think Andrej is correct. The OP is probably referring to what I described in this earlier answer - mathoverflow.net/questions/71344/… $\endgroup$
    – François G. Dorais
    Commented Jun 3, 2013 at 16:59

1 Answer 1

Reset to default
18
$\begingroup$

The undesirable properties of higher-order logic are created by an insufficient notion of model. That is, we cannot have all three, soundness, completeness and effectivness (decidability of proof checking), if we insist that formulas be interpreted in the "standard" set-theoretic way. Henkin semantics does not suffer from this defficiency.

What this says is not that something is wrong with higher-order logic, but that something is wrong with those who refuse to look at semantic models, even when they are right in front of their faces, because these models are "unintended", "philosophically unacceptable", "not what mathematicians think", etc. This phenomenon of refusing to accept new interpretations of old theories is quite persistent, and always very harmful. Didn't someone stall progress in noneuclidean geometry because it was unthinkable that there would be strange new models? Aren't imaginary numbers so called because they were unthinkable and did not "really exist"? Doesn't higher-order classical logic suffer because it is being denied its natural notion of models on the grounds that they are non-standard?

The natural notion of model for intuitionistic higher-order logic (IHOL) is that of a topos. With respect to topos semantics, it is a standard result that IHOL enjoys soundness, completeness and effectivness.

We may specialize this standard fact to classical higher-order logic (CHOL). The result then is that, with respect to Boolean topos semantics, CHOL enjoys soundness, completeness and effectivness. From here on, we may prove various technical theorems which allow us to cut down on the class of Boolean toposes which is stil sufficient for completeness. And then it is not much of a surprise that we cannot cut down just to a single topos known as classical sets, which is called "Paradise" by its prisioners.

Improve this answer
$\endgroup$
17
  • 3
    $\begingroup$ I think you are a bit too polemic here. Studying higher order logic gets interesting by enforcing standard semantics, there is nothing wrong about such research. Henkin semantics make HOL very similar to FOL and it loses its genuine interesting properties (which include a higher degree of undecidability, non-compactness, and special properties of the universal, existential and monadic second-order-fragments), although I agree with you that such philosophical arguments for standard models in the context of foundations as mentioned by you are very dubious. $\endgroup$
    – The User
    Commented Jun 3, 2013 at 15:07
  • 2
    $\begingroup$ Indeed. There is nothing higher-order about the logic of Henkin semantics, it is just multi-sorted first-order logic with a light touch of syntactic sugar, and it would save unnecessary confusion if people called it as such. $\endgroup$
    – Emil Jeřábek
    Commented Jun 3, 2013 at 19:14
  • 2
    $\begingroup$ @TheUser: the standard models are insufficient for a very simple reason, namely that they do not give completeness. Yes, you can insist on staring just as standard models, but in my experience lack of completeness indicates one of two things: you forgot an axiom, or you forgot some models. Since we like effectivness, in the case of CHOL it has to be the latter. $\endgroup$
    – Andrej Bauer
    Commented Jun 4, 2013 at 5:02
  • 1
    $\begingroup$ The fact that more general semantics makes HOL look more like first-order logic is good, not bad! It gives standard meta-theoretic properties, it allows us to prove things, it gives a wealth of models, etc. I really do not understand the fascination with studying only a very specific situation in HOL, but that must be because I am not a Platonist. $\endgroup$
    – Andrej Bauer
    Commented Jun 4, 2013 at 5:04
  • 2
    $\begingroup$ @Mozibur You can give a second-order formula such that all models are isomorphic to the natural numbers. In first-order logic that is obviously not possible because of completeness/compactness/Löwenheim-Skolem. @Andrej I am not a Platonist and in fact I think that HOL with standard semantics is irrelevant for foundations/philosophy of mathematics. @François I think it was wrong to say “most”, however, model theory of second-order logic gets interesting by enforcing standard semantics. Model theory of Henkin semantics is just FO model theory (which is of course more fruitful, but not HOL). $\endgroup$
    – The User
    Commented Jun 4, 2013 at 8:34

You must log in to answer this question.

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