Skip to main content
MathOverflow

Return to Question

summarize my understanding of one of the answers
Source Link
ttbo
ttbo
  • 163
  • 7

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.

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.

Became Hot Network Question
Source Link
ttbo
ttbo
  • 163
  • 7

Is there a semantics for intuitionistic logic that is meta-theoretically "self-hosting"?

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.