13
$\begingroup$

One can study the standard semantics of classical propositional logic within classical logic set theory, so we can say that the semantics of classical logic is meta-theoretically "self-hosting". This property is probably a big part of why classical logic is so easy to accept as the default/implicit background/foundational logic for mathematics.

In contrast, classical logic set theory is also used in the presentation of the mainstream semantic interpretations of propositional intuitionistic logic such as Kripke semantics and Heyting algebra. For example, in Kripke semantics our structures are triples $M = \langle W, \leq, v\rangle$ where $W \neq \varnothing$, $\leq$ is a preorder on $W$, and $v$ is a set function from the set of atomic propositions to the powerset of $W$, where $v$ must satisfy: for every $w_1,w_2 \in W$, for every atomic proposition $p$, if $w_1 \leq w_2$ and $w_1 \in v(p)$, then $w_2 \in v(p)$. So far, it seems that we could assume that we are working in some kind of intuitionistic set theory setting, however when we get to the definition of interpretation of formulas, it seems like there are some problems with using an intuitionistic meta-theory: \begin{array}{lll} M,w \vDash p &\text{ iff } &w \in v(p)\\ M,w \vDash \top\\ M,w \nvDash \bot\\ M,w \vDash \phi_1 \to \phi_2 &\text{ iff } &\text{for every } w'\in W.\text{ if } w \leq w' \text{ and } M,w' \vDash \phi_1 \text{ then } M,w' \vDash \phi_2\\ M,w \vDash \phi_1 \lor \phi_2 &\text{ iff } & M,w \vDash \phi_1 \text{ or } M,w \vDash \phi_2\\ M,w \vDash \phi_1 \land \phi_2 &\text{ iff } & M,w \vDash \phi_1 \text{ and } M,w \vDash \phi_2 \end{array} First off: now that we are interpreting this presentation in some kind of intuitionistic meta-theory, we will no longer necessarily have $w \vDash \phi$ or $w \nvDash \phi$, whereas before this would be true of every formula $\phi$, thanks to the law of excluded middle in classical logic. It seems like this may cause this semantics to determine a different logic than intuitionistic logic, when the meta-theory is taken to be intuitionistic.

Furthermore, in my experience with this semantic interpretation, there are many times where a formula is found to be semantically valid based on some use of the law of excluded middle. For example, you might observe that there must exist some future world $w$ such that $w \vDash \phi$, or else for every future world $w$ we must have $w \nvDash \phi$. This also indicates to me that using an intuitionistic meta-theory may cause the resulting logic to be different.

I haven't been able to find an example of a formula that would be intuitionistically valid, but not valid in the logic determined by Kripke semantics as interpreted within an intuitionistic meta-theory, but it seems like such a thing might exist.

Can anyone point me to any work that studies this issue in depth? Or point me to work that studies the more general issue of meta-theoretic "leakage" with respect to semantics?

Finally, if this is indeed a problem with Kripke/Heyting semantics, has anyone discovered a "self-hosting" intuitionistic semantics? Specifically: a semantic interpretation of intuitionistic propositional logic that assumes a meta-theory based on some kind of intuitionistic set theory, and is sound and complete with respect to a standard intuitionistic proof system.

Edit: If I understand correctly, Mike Shulman's answer claims that something like the following will be a semantic interpretation of propositional intuitionistic logic, as long as the meta-theory is intuitionistic.

Let $M$ be a function from the set of atomic propositions to the set $\{0,1\}$, and then interpret formulas recursively by: \begin{array}{lll} M \vDash p &= &M(p) = 1\\ M \vDash \top &= &\text{Triv.}\\ M \vDash \bot &= &\text{Abs.}\\ M \vDash \phi_1 \to \phi_2 &= & M \vDash \phi_1 \text{ implies } M \vDash \phi_2\\ M \vDash \phi_1 \lor \phi_2 &= & M \vDash \phi_1 \text{ or } M \vDash \phi_2\\ M \vDash \phi_1 \land \phi_2 &= & M \vDash \phi_1 \text{ and } M \vDash \phi_2 \end{array} This is my best attempt to adapt simple 2-value "classical" logic semantics to the situation of an intuitionistic meta-theory. The only changes I had to make was to avoid careless references to $\nvDash$, and to specify the meaning of implication separately, instead of defining it as $\neg \phi_1 \lor \phi_2$. I also changed the use of "iff" to equality to emphasize that I think we now need to think of the statements in a way that is closer to type theory. For example, for the meaning of an atomic proposition I think we are essentially saying "a proof of $M\vDash p$ is equivalent to a proof that $M(p) = 1$". For the meaning of $\bot$ we are saying "a proof of $M\vDash \bot$ is equivalent to a proof of absurdity". These two together mean that (defining $\neg \phi \equiv \phi \to \bot$) the meaning of $\neg p$ is essentially "a proof of $M \vDash \neg p$ is equivalent to a proof that $M \vDash p$ implies (meta-theoretic) absurdity". Now finally, since we are in intuitionistic meta-theory, we know that it is not given that for any atomic proposition $p$ we must have a proof of $M(p) = 1$ or a proof of $M(p) \neq 1$. This means that we can't conclude that there is always a proof of $M \vDash p \lor \neg p$ like we could in a classical meta-theory context.

$\endgroup$
7
  • 1
    $\begingroup$ Maybe not an answer, but the meaning explanation of type theory comes to mind. This is due to Per Martin-Löf. I think it is almost surely the case that people have considered your question before, but I don't know where or who (see also: Jonathan Sterling, Type Theory and its Meaning Explanations, arXiv:1512.01837) $\endgroup$ Feb 19 at 9:22
  • 3
    $\begingroup$ Quite related: mathoverflow.net/q/320186/36103 $\endgroup$
    – cody
    Feb 19 at 14:51
  • 4
    $\begingroup$ You should not be using $\{0, 1\}$ for truth values. Use the powerset of $\{1\}$ instead. $\endgroup$ Feb 23 at 12:40
  • 2
    $\begingroup$ The power set of $\{1\}$ contains all subsingleton sets $\{1|φ\}$. Asserting that every subsingleton is either $0$ or $1$ is asserting excluded middle for every such $φ$. $\endgroup$
    – Dan Doel
    Feb 24 at 18:21
  • 3
    $\begingroup$ Those two sets are isomorphic, yes. The problem is that neither of those is isomorphic to the powerset of a singleton. The more obvious is the latter, where: $x \in \{\varnothing,\{1\}\} → x = \varnothing ∨ x = \{1\}$. If $\mathcal P\{1\}$ were that set, then we would have $\{1|φ\} = \varnothing ∨ \{1|φ\} = \{1\}$, which is equivalent to $¬φ ∨ φ$. Your semantics are actually classical as given, because $M(p) = 0 ∨ M(p) = 1$. By using a powerset, you could give a value for $p$ that is a subsingleton whose equality with $1$ is equivalent to an undecidable proposition. $\endgroup$
    – Dan Doel
    Feb 25 at 3:31
12
$\begingroup$

I would argue that intuitionistic logic is perfectly self-hosting: working in an intuitionistic set theory, one can define a sound semantics of intuitionistic logic relative to models built out of plain sets in the (intuitionistic) metatheory, without any need for Kripke-ness or anything complicated. Just as the interpretation by set-models in a classical metatheory is the "intended" meaning of classical logic, a word-for-word interpretation by set-models in an intuitionistic metatheory is the intended meaning (or, at least, an intended meaning) of intuitionistic logic.

What forms of completeness theorem are intuitionistically provable is a separate question, which I would argue doesn't impact on the self-hostingness of intuitionistic logic. But I believe the forms of completeness that are true for intuitionistic logic — which are arguably best expressed in terms of models in arbitrary categories or hyperdoctrines of the appropriate sort, including Kripke models as the special case of presheaf categories — can certainly be proven in an intuitionistic metatheory. For instance, Part D of Johnstone's Sketches of an Elephant proves these categorical completeness results for various fragments of logic, including full first-order intuitionistic logic, and generally uses intutionistically valid reasoning.

$\endgroup$
3
  • 1
    $\begingroup$ I tried to semi-formalize the first part of your answer, as far as I understood it, and updated my question with the results. Can you let me know if I said anything wrong, or if I didn't get your meaning properly? Thanks. $\endgroup$
    – ttbo
    Feb 23 at 7:51
  • 2
    $\begingroup$ Yes, you got it right, except that as Andrej says, the set of intuitionistic truth values is not just $\{0,1\}$. $\endgroup$ Feb 23 at 15:09
  • $\begingroup$ If one understands completeness of the self-hosting semantics for IPC as the claim that every Heyting algebra is the algebra of all truth values in some elementary topos, then this has been proven by Pataraia but still unpublished (for which, I must admit, I am responsible). $\endgroup$ Jun 29 at 14:09
9
$\begingroup$

See Palmgren, Constructive Sheaf Semantics for a completeness proof for sheaf semantics within a constructive (and predicative) metatheory. The introduction also mentions several references to earlier approaches that are generalised by sheaf semantics. I recommend particularly Troelstra and Van Dalen, Constructivism in mathematics, vol 2 as a standard reference containing various results about the semantics of constructive mathematics.

$\endgroup$
8
$\begingroup$

Comment environment was acting funny, so I am writing an "answer". Here is a good place to start:

Harry de Swart's PhD from the University of Nijmegen (the Netherlands) was about this kind of topic:

H.C.M. de Swart: Intuitionistic logic in intuitionistic metamathematics, Dissertation, 1976, University of Nijmegen. https://core.ac.uk/reader/43594080

He has since left this field, so I do not know if he will answers questions via email.

$\endgroup$
1
  • $\begingroup$ Thanks, the de Swart dissertation seems interesting. $\endgroup$
    – ttbo
    Feb 24 at 1:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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