Timeline for Can Heyting arithmetic be axiomatized by strong induction together with some disjunction-free formulas?
Current License: CC BY-SA 4.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 31, 2021 at 6:56 | comment | added | Emil Jeřábek | (Presented in a set-up where the morphisms have to be inclusions, $M_0$ is $\mathbb N[x]$ with $f=g$ interpreted literally, and $M_1$ is $\mathbb N[x]$ with $f=g$ interpreted as $f(0)=g(0)$.) | |
| Jul 31, 2021 at 6:26 | comment | added | Emil Jeřábek | It’s a two-node model with the bottom node having the structure of the polynomial semiring $M_0=\mathbb N[x]$, the top node $M_1=\mathbb N$, and the connecting morphism $M_0\to M_1$ being the evaluation homomorphism $f(x)\mapsto f(0)$. Also, Matt F’s model above might work as well, if it indeed satisfies strong induction. | |
| Jul 30, 2021 at 22:28 | comment | added | Mohsen Shahriari | @EmilJeřábek Could you please describe the example you mentioned? I couldn't construct any such Kripke models. | |
| Jul 29, 2021 at 8:01 | comment | added | Emil Jeřábek | Let me add more generally that over an ANAAT that includes the disjunction-free sentence $\forall x\,(\neg\neg x=0\to x=0)$, HA is equivalent to the instance $\forall x\,(\neg x=0\lor\neg\neg x=0)$ of the weak law of excluded middle. Consequently, no Kripke model which is linearly ordered, or even just upwards directed, can serve as a counterexample separating ANAAT with all disjunction-free consequences of HA from HA itself. | |
| Jul 28, 2021 at 17:32 | comment | added | Emil Jeřábek | I'm not sure about induction, but it doesn't satisfy e.g. $\forall x\,(\neg\neg x=0\to x=0)$, which is a disjunction-free consequence of HA. | |
| Jul 28, 2021 at 16:34 | comment | added | user44143 | If a Kripke model on $\mathbb{N}\times\mathbb{N}$ has $\mathbf{0}=(0,0)$, $\mathbf{S}(t,x)=(t,x+1)$, $(t,x)\mathbf{+}(u,y) = (\max(t,u),x+y)$, $(t,x)\mathbf{\cdot} (u,y) = (\max(t,u),xy)$, and equality at stage $s$ given by $(t,x)\mathbf{=}(u,y) \leftrightarrow x = y \wedge(t=u \vee \max(t,u)<s)$, will that satisfy strong induction and all the disjunction-free sentences of $HA$? | |
| Jul 28, 2021 at 16:07 | comment | added | Emil Jeřábek | Hmm. It's not difficult to construct a Kripke model of the minimal ANAAT that does not satisfy HA, but I have no idea how to generalize it in the presence of arbitrary disjunction-free axioms. | |
| Jul 28, 2021 at 4:34 | history | asked | Mohsen Shahriari | CC BY-SA 4.0 |