9
$\begingroup$

For classical theories, Henkin's completeness proof can be arithmetized. This leads to the result that for classical theories $T$ and $S$ if $\sigma$ is a formula enumerating $S$ in $T$ then $S \leq T + Con_{\sigma}$. In other words, if a classical theory can prove the consistency of another classical theory it can interpret that theory.

Can a similar thing be done for non-classical theories? I imagine if there is a way to arithmetize a completeness proof for other logics this may be possible. However, Kripke models have a more complicated truth condition so that might also be an issue. Let me know if you have seen anything about this, I have looked around and have not been able to find much information.

Improve this question
$\endgroup$
11
  • $\begingroup$ Do you have a precise definition of interpretation in mind? The answer may depend on which one you use. $\endgroup$
    – James E Hanson
    Commented Jun 1, 2023 at 22:11
  • $\begingroup$ Ah, yes sorry. I mean relative interpretation. A recursive function that commutes with logical operators and has a domain. Ideally without parameters but with parameters are fine. $\endgroup$
    – Spencer Woolfson
    Commented Jun 2, 2023 at 12:11
  • $\begingroup$ I don't know if I can fill in all of the details of this, but I feel like there's basically no way it's going to work. Here's an informal argument: Heyting arithmetic together with any true $\Pi^0_1$ sentence should still have a good realizer interpretation. Consider the theory that is $\mathsf{PA}$ together with a unary predicate $U$ together with axioms asserting that $U$ separates some pair of computably inseparable sets. $\endgroup$
    – James E Hanson
    Commented Jun 5, 2023 at 2:41
  • $\begingroup$ $\mathsf{HA}$ proves that this theory is consistent if and only if $\mathsf{PA}$ is, so if there is an arithmetized completeness theorem, $\mathsf{HA} + \mathrm{Con}(\mathsf{PA})$ will be able to interpret this expanded theory. So suppose there is such an interpretation. $\mathsf{HA}$ should be smart enough to be able to define a map from the real natural numbers to an initial segment of the interpreted model, but then $U$ will give you a predicate (satisfying excluded middle) separating two computably inseparable sets. $\endgroup$
    – James E Hanson
    Commented Jun 5, 2023 at 2:41
  • $\begingroup$ Since $\mathsf{HA}+ \mathrm{Con}(\mathsf{PA})$ still has a realizer interpretation, the proof of this would give you a program that allows you to computably separate the computably inseparable sets, which is a contradiction. $\endgroup$
    – James E Hanson
    Commented Jun 5, 2023 at 2:42

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .