# Understanding the complete lattice definition of impredicativity

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 (?)).

• I don't see the contradiction here
– Couchy
Mar 13 at 19:44
• I'm not sure but I'm guessing you can construct the glb as $\forall \phi. \phi\in S\implies\phi$?
– Couchy
Mar 13 at 20:11
• Maybe you could rephrase your question as how to find glb?
– Couchy
Mar 13 at 20:38
• This question is too basic for Math Overflow in my opinion. I'm open moving it to the Math Stack Exchange and establishing the precedent that this sort of question belongs there rather than here. I'm also open to saying this kind of question belongs in both places. Mar 14 at 0:06
• I am sorry, but I am confused by what's written. What is a "single wff"? Should I read $S \models \phi \in \Phi$ as $S \models (\phi \in \Phi)$ or as $(S \models \phi) \in \Phi$? Neither makes sense to me. It also feels like you never actually described your subsystem. Mar 14 at 7:07

• Internal completeness means that the statement "$L$ is a complete lattice" is valid in whatever formal system we're working with. External completeness means that $L$ is seen to be a complete lattice at the meta-level, but internally this may not be the case. This is analogous to "holds in the model" vs. "holds externally". Mar 14 at 22:32