Classical first-order logic with no function or relation symbols is decidable. If I'm not mistaken, this is essentially because any formula (with possible free variables) has truth value uniquely determined by the partition of its free variables into "equality classes" and by the "cardinality of the model" - and furthermore, for any given partition, the answer is stable for large enough cardinality starting at some finite cardinality. So, you can write a decision procedure which recursively evaluates the set of partitions and cardinalities for which each subformula is true (which is finitely representable due to the stability condition). Then, at the end, satisfiability or tautology should be easy to read off from the result.

I recently found myself wondering whether the same thing would be true for intuitionistic first-order logic with no function or relation symbols. The above argument would certainly need some heavy-duty refinements if it were to work in this case, if it is salvageable at all. For example, the "partitions" above would need to become much more complicated objects, since there is essentially no restriction on the equality relations between free variables other than that they need to form an equivalence relation. (e.g. in a topos with subobject classifier $\Omega$, for any global section $p \in \Omega(1)$, we can form the quotient of $\{ 0, 1 \}$ by the equivalence relation $\{ (0, 0)_\top, (1, 1)_\top, (0, 1)_p, (1, 0)_p \}$ to get an object of the topos with two global sections $\bar 0$ and $\bar 1$ such that $\bar 0 = \bar 1$ is equivalent to $p$.) Similarly, in a topos, the notion of "cardinality" of the space would have to be much more involved to be of much use in classification.

Nonetheless, given that intuitionistic propositional logic is decidable, it doesn't seem completely beyond hope that maybe some sort of quantifier elimination could hold and reduce each subformula to some combination of propositions in terms of $v_i = v_j$ and some "cardinality like" conditions.

Or possibly, some mild extension of propositional sequent calculus might be able to resolve questions in this language, and still satisfy the cut elimination theorem in such a way that an automated proof search procedure can be shown to terminate in all cases. Along this line of thinking, the main addition to sequent calculus would probably be something like: given the problem $\Gamma, v_i = v_j \vdash \phi$, reduce the number of free variables by one and substitute $v_i$ in place of $v_j$ in both $\Gamma$ and $\phi$; if this $\Gamma[v_j := v_i] \vdash \phi[v_j := v_i]$ is provable, then $\Gamma, v_i = v_j \vdash \phi$ is provable. And then of course, the introduction rule $v_i = v_i$; and similarly for the $\forall$ and $\exists$ intro/elimination rules, we require in the elimination rules that the proposition being eliminated is directly in the context. This approach seems more promising, though I haven't thought too much about the details.

Just as very wild speculation for what a proof of the negative answer could potentially look like: for all I know, maybe given an instance of the group word problem, it might be possible to translate that into evaluation of tautology of some first-order sentence which is a tautology if and only if the topos of $G$-sets satisfies that sentence, if and only if that instance of the group word problem is true.


Your Answer

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

Browse other questions tagged or ask your own question.