6
$\begingroup$

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

Improve this question
$\endgroup$
13
  • 1
    $\begingroup$ I don't see the contradiction here $\endgroup$
    – Couchy ♦
    Mar 13 at 19:44
  • 1
    $\begingroup$ I'm not sure but I'm guessing you can construct the glb as $\forall \phi. \phi\in S\implies\phi$? $\endgroup$
    – Couchy ♦
    Mar 13 at 20:11
  • 1
    $\begingroup$ Maybe you could rephrase your question as how to find glb? $\endgroup$
    – Couchy ♦
    Mar 13 at 20:38
  • 1
    $\begingroup$ 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. $\endgroup$
    – Greg Nisbet
    Mar 14 at 0:06
  • 2
    $\begingroup$ 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. $\endgroup$
    – Andrej Bauer
    Mar 14 at 7:07

1 Answer 1

Reset to default
5
$\begingroup$

You must be careful to distinguish internal and external completeness.

First, I think you might be looking for the Lindenbaum-Tarski algebra of monadic first-order logic, and you are asking whether it is externally comlplete. This is a fine question, but it's not about impredicativity, which at least I understand to be internal completeness.

I do not see what the answer to the question is, but since you are working with classical logic, the Lindebaum-Tarski algebra will be a countable boolean algebra. Sergei Goncharov wrote a book about them.

Improve this answer
$\endgroup$
2
  • $\begingroup$ What are internal and external completeness? If we take contraclassical logics off the table, I have a very vague intuition that internal completeness means something like "externally complete and able to be proven complete using the fragment of classical logic (the background system) associated with the theory in question". Is that what it means? $\endgroup$
    – Greg Nisbet
    Mar 14 at 19:27
  • 3
    $\begingroup$ 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". $\endgroup$
    – Andrej Bauer
    Mar 14 at 22:32

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.