Logic & Programming

Danko Ilik's research blog
<– home page

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

The paper preciselly formalizes Martin-Löf constructive type theory with the W-type (inductive definitions) and one universe, in its intensional and extensional variants, and in its variants “à la Tarski” and “à la Russell”, as well as a version/extension of classical Kripke-Platek set theory. It is then shown how to interpret the extensional type theory into Kripke-Platek set theory, from which an upper bound on the proof-theoretic strength is obtained. Together with previous results on a lower bound for intensional type theory (and an embedding into the extensional one), one obtains as a precise characterisation for the proof-theoretic strength of all variants of type theory the ordinal ψΩ1ΩI+ω.

Actually this is the most precise and succinct formulation of type theory that I have seen and should be helpful for relative interpretations of/inside type theory as well as implementing proof tools.

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

Paper by Yoshiki Nakamura and Naosuke Matsuda

Let IL and CL denote the fragments of intutionistic and classical propositional logic having implication as the sole logical connective. Call a formula (a theorem) α of CL “minimal in CL” if α cannot be obtained by substituting in another formula β ∈ CL a propositional variable p by any formula γ. In a way, α being minimal in CL means that α is apt to be an axiom (schema) of an intermediate logic, since its form is general enough that it cannot be obtained as an instantiation of another more general axiom (schema). IL and CL themselves can be completely axiomatized by such formulas and a question was posed by Komori and Kashima whether one can axiomatize a proper intermediate logic using such a formula.

The authors show that it can be done, by displaying an explicit formula G', a variant of and equivalent to the formula G := ((a → b) → c) → ((b → a) → c) → c, which when added to IL produces the intermediate Gödel-Dummett logic. One could not simple take G to be the required formula, because it is not minimal in CL.

The authors also discuss three related open problems.

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

The paper studies the notions of continuity that arise from inductively generated neighborhood functions and from functions NN → N having a bar recursive modulus of continuity, in a strictly constructive context (constructive reverse mathematics).

The inductively generated neighborhood function (called Brouwer operations in the paper) are given by two constructors of an inductive set K, L : N → K and Sup : (N → K) → K, and an associated (primitive / structurally decreasing) recursor R satisfying the equations

Ruf (Lx) = ux Ruf (Supφ) = f φ(λx.Ruf (φx)).

A function ξ is a bar recursor for a function Y : (N → N) → N (the stopping condition for Spector’s bar recursion) if

ξGHs = Gs when Y (ˆs) < |s| ξGHs = Hs(λx.ξGH(s∗〈x〉)) when Y (ˆs) ≥ |s|.

The recursion in this case is not primitive / structurally decreasing as in the case of Brouwer operations.

While usual/general neighborhood functions can be simply be seen as continuous moduli for the functions they induce, in the strictly constructive setting, the relation between inductively generated neighborhood functions and the continuity of functions they induce is more subtle and the subject of this paper. In either classical mathematics (in presence of classical logic and dependent choice) or in intuitionistic mathematics (in presence of bar induction and strong continuity for numbers), all neighborhood functions are inductively defined. Similarly, the relation between bar induction and bar recursion has not been extensively studied in the strictly constructive setting.

A first result of the paper is that a function Y : (N → N) → N is induced by a Brouwer operation if and only if it has a bar recursive modulus of continuity (Theorem 4.15).

A second contribution of the paper is the introduction of the following equivalence-of-continuity principles.

BC: Every continuous function Y : (N → N) → N is induced by a Brouwer operation / has a bar recursive modulus.

BCc: Every continuous function Y : (N → N) → N with a continuous modulus is induced by a Brouwer operation / has a bar recursive modulus.

It is shown in Proposition 5.1 that BCc is equivalent to decidable bar induction, in the presence of the axiom of countable choice and the axiom of choice for functions N → N and quantifier-free formulas. BC is equivalent to continuous bar induction, in the presence of the axiom of countable choice and the axiom of choice for functions N → N and Π01 formulas.

A third contribution of the paper is the transposition of the previous results in the settings of Cantor space and uniform continuity.

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

The paper “Applications of the analogy between formulas and exponential polynomials to equivalence and normal forms” to be presented at PLS12 in Anogeia, Crete, Grece

We show some applications of the formulas-as-polynomials correspondence: 1) a method for (dis)proving formula isomorphism and equivalence based on showing (in)equality; 2) a constructive analogue of the arithmetical hierarchy, based on the exp-log normal form. The results are valid intuitionistically, as well as classically.

https://arxiv.org/abs/1905.07621

http://panhellenic-logic-symposium.org/12/

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

https://arxiv.org/abs/1601.04876

We revisit the notion of intuitionistic equivalence and formal proof representations by adopting the view of formulas as exponential polynomials.

After observing that most of the invertible proof rules of intuitionistic (minimal) propositional sequent calculi are formula (i.e. sequent) isomorphisms corresponding to the high-school identities, we show that one can obtain a more compact variant of a proof system, consisting of non-invertible proof rules only, and where the invertible proof rules have been replaced by a formula normalisation procedure.

Moreover, for certain proof systems such as the G4ip sequent calculus of Vorob'ev, Hudelmaier, and Dyckhoff, it is even possible to see all of the non-invertible proof rules as strict inequalities between exponential polynomials; a careful combinatorial treatment is given in order to establish this fact.

Finally, we extend the exponential polynomial analogy to the first-order quantifiers, showing that it gives rise to an intuitionistic hierarchy of formulas, resembling the classical arithmetical hierarchy, and the first one that classifies formulas while preserving isomorphism.

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

Common Criteria [ISO/IEC 15408] is an international standard for certifying the security of computer systems. When high evaluation assurance levels (EAL6 and EAL7) are required of a system, Common Criteria (CC) requires formal modelling and mechanized proofs of security properties. In this talk, we will first have an overall look at the schema for CC evaluations, after which we will concentrate on the scientific aspects relating to proofs and programming languages, and the special role that proof assistants play during these evaluations.

https://eutypes.cs.ru.nl/Meetings/Nijmegen18

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

Abstract: In this chapter, we propose some future directions of work, potentially beneficial to Mathematics and its foundations, based on the recent import of methodology from the theory of programming languages into proof theory. This scientific essay, written for the audience of proof theorists as well as the working mathematician, is not a survey of the field, but rather a personal view of the author who hopes that it may inspire future and fellow researchers.

http://arxiv.org/abs/1605.09177

http://www.collegepublications.co.uk/admin/download.php?ID=ifcolog00019

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

Talk on the topic of my POPL 2017 paper https://chocola.ens-lyon.fr/

https://chocola.ens-lyon.fr/

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