2
$\begingroup$

In Fitting's Intuitionistic Logic Model Theory and Forcing, the following theorem is proven:

If $X$ is a formula with no universal quantifiers and $\not\vdash_I X$, then there is a countermodel $(\mathcal{G}, \leq, \vDash, \mathcal{P})$ in which $\mathcal{P}$ is a constant function.

This is Chapter 6, "Additional First Order Results", Theorem 6.1. Fitting uses some weird semantics so I've attempted to translate it into a more standard notation, as the one found on Wikipedia. I believe this is then an equivalent formulation:

If $X$ is a formula with no universal quantifiers and $\not\vdash_I X$, then there is a countermodel $(W, \leq, \{M_w\}_{w \in W})$ such that $u \leq v$ implies that $M_u$ is a substructure of $M_v$ for all $u, v \in W$.

Fitting's proof is proof-theoretical and very technically convoluted and (in my opinion) unintuitive. He basically breaks $X$ down with deduction rules into a bunch of consistent sets closed under the deduction rules and then iterates this many times in a weird way (the full proof is too big to include here). I think my reformulation presents a very intuitive and pretty model-theoretic fact, so I wonder now if there is a proof with the same attributes.

I've tried the two things that came to mind immediately: taking an existing countermodel and "cutting it down" (it doesn't work as well as I wanted it to) and an induction on the number of connectors in $X$, but it seemed at the very least very complicated and I couldn't make much of it. I'm looking for other ideas now. (Perhaps there is an another text on this with a different proof? It's hard to find texts with similar content as Fitting.)

Improve this question
$\endgroup$
5
  • 1
    $\begingroup$ Either Fitting's theorem or your reformulation of it is wrong. In the usual Kripke semantics, models such that $u\le v\implies M_u\subseteq M_v$ are exactly those that satisfy LEM for atomic (or quantifier-free) formulas. Thus, e.g., the sentence $P(c)\lor\neg P(c)$ (where $P$ is a unary predicate and $c$ is a constant) is a counterexample (it is unprovable, but valid in all models with said property). $\endgroup$
    – Emil Jeřábek
    Commented Sep 27 at 6:29
  • $\begingroup$ Or $\exists x\,(P(x)\lor\neg P(x))$ if you want a purely relational language. Or $\exists x\,Q(x)\to\exists x\,(P(x)\lor\neg P(x))$ if your logic allows empty domains. $\endgroup$
    – Emil Jeřábek
    Commented Sep 27 at 6:57
  • 1
    $\begingroup$ What might be true though is that if $\phi$ is an unprovable formula without universal quantifiers, then $\phi$ has a constant-domain counterexample. $\endgroup$
    – Emil Jeřábek
    Commented Sep 27 at 9:33
  • 2
    $\begingroup$ @EmilJeřábek: I believe that constant-domain is precisely what's going on here and so OP's translation is unfortunately wrong. $\endgroup$
    – Z. A. K.
    Commented Sep 27 at 11:12
  • 1
    $\begingroup$ After examining Fitting's definition of a model again, I think you're right. Thank you for this because this confusion would've definitely come back to stump me later on. I'm still looking for a more intuitive proof, though. $\endgroup$
    – zaq
    Commented Sep 27 at 18:56

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .