Logic & Programming

The paper studies the algebraic notion of Jacobson radical as a set theoretic notion. For a logician, it seems easiest to understand the Jacobson radical logically : the radical $\text{Jac}(T)$ of a theory $T$ is the set of all propositions $a$, such that an inconsistency of $a$ with a proposition $b$ translates to an inconsistency of $T$ with the proposition $b$: $$ \text{Jac}(T) = \{ a ~|~ \forall b(a,b\vdash\bot \to T,b\vdash\bot)\}. $$It is a concept used in logic, for instance, in the construction of maximally consistent extensions in the proof of the completeness theorem.

The paper studies a generalized set-theoretic formulation of the Jacobson radical and shows how it is applicable both in algebra and in logic. The generalization is obtained by replacing the algebraic statement $1\in\langle a,b\rangle$ and the logical $a,b\vdash\bot$ by a predicate $R(a,b)$ on subsets $a,b$ of the universe, called an ``inconsistency predicate''.

It is shown (Theorem 1) that the membership to the Jacobson radical is an inductively generated relation, and that this holds constructively, in CZF.

In Theorem 2, it is shown, via Theorem 1, Raoult's Open Induction principle and classical logic, that $\text{Jac}(U)$ is equal to the intersection of all possible maximally consistent extensions of $U$; this holds in ZFC.

The paper then gives application to algebra and logic, among which that the universal closure of Theorem 2 is equivalent to the axiom of choice (Proposition 3) and the derivation of Glivenko's theorem for propositional logic.

Comment here: @danko@mamot.fr Follow using the Fediverse ID: @danko@blog.iaddg.net