 Let us define the concepts that are needed to understand this intended interpretation of GLB. An arithmetical theory \(T\) is defined to be \(\omega\)-consistent if and only if for all formulas A with free variable \(x\), \(T\vdash \neg\, A(I_n)\) for all \(n\) implies that \(T \not\vdash \exists x \, A(x)\); here, \(I_n\) is the numeral of \(n\), i.e., the term \(\bs\bs\ldots\bs 0\) with \(n\) occurrences of the successor operator \(\bs\). Peano Arithmetic (PA) is the most well-known example of an \(\omega\)-consistent theory (see also  Gödel’s incompleteness theorems).  Now let PA\(^+\) be the arithmetical theory whose axioms are those of PA together with all sentences \(\forall x \, \neg \, A(x)\) such that for every \(n\), PA\(\vdash \neg \, A(I_n)\). Now \(\omega\)-provability is simply provability in PA\(^+\), so it is the dual of \(\omega\)-consistency.