This is a nice definition of (one notion of?) impredicativity and is mentioned directly here and in one of the sections of the answer here (although I'm probably misinterpreting Andrej Bauer's answer).
To make my question as concrete as possible:
- In order to assess whether a formal system is impredicative or not, how do we construct its lattice?
- For what kinds of mathematical objects does the complete lattice definition of impredicativity make sense?
What follow is a concrete example of simple subsystem of classical first-order logic that I'm investigating, but have so far failed to prove the predicativity of one way or another. I'm curious how the definition of (im)predicativity translates to this setting.
Also, I suspect this system really is predicative (since monadic FOL is decidable, which intuitively feels like a much stronger property). I would be grateful if anyone could provide an argument for showing the existence of glbs and lubs.
The specific system I'm interested in the subset of classical FOL constrained to have unary predicates only. This simple system is called monadic first-order logic and it's decidable.
I'm going to do something naive and just say that $\le$ is a special case of the consequence relation $\models$, (i.e. $\varphi \le \psi$ if and only if $\varphi \models \psi$).
I think proving this system is predicative would be equivalent to showing the following:
- for every set of wffs $S$, the set of all wffs that serve as lower bounds $\Phi := \{ \varphi : \varphi \models \min(S) \}$ has a supremum.
- for every set of wffs $S$, the set of all wffs that serve as upper bounds $\Phi := \{ \varphi : \max(S) \models \varphi \}$ has an infimum.
where $\min$ is $\bigwedge$ and $\max$ is $\bigvee$.
I'm curious whether this is the right way to build the lattice of whether I need to do something like mod out by the equivalence relation $\varphi, \psi \mapsto (\varphi \le \psi \;\; \text{and} \;\; \psi \le \varphi)$ or something (I think that equivalence relation might sometimes fail to be a congruence though (?)).