Logic & Programming

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

https://www.lix.polytechnique.fr/Labo/Wendlasida_Tertius.OUEDRAOGO/

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

Abstract: Lambda calculi with algebraic data types lie at the core of functional programming languages and proof assistants, but conceal at least two fundamental theoretical problems already in the presence of the simplest non-trivial data type, the sum type. First, we do not know of an explicit and implemented algorithm for deciding the beta-eta-equality of terms—-and this in spite of the first decidability results proven two decades ago. Second, it is not clear how to decide when two types are essentially the same, i.e. isomorphic, in spite of the meta-theoretic results on decidability of the isomorphism. In this paper, we present the exp-log normal form of types—-derived from the representation of exponential polynomials via the unary exponential and logarithmic functions—-that any type built from arrows, products, and sums, can be isomorphically mapped to. The type normal form can be used as a simple heuristic for deciding type isomorphism, thanks to the fact that it is a systematic application of the high-school identities. We then show that the type normal form allows to reduce the standard beta-eta equational theory of the lambda calculus to a specialized version of itself, while preserving the completeness of equality on terms. We end by describing an alternative representation of normal terms of the lambda calculus with sums, together with a Coq-implemented converter into/from our new term calculus. The difference with the only other previously implemented heuristic for deciding interesting instances of eta-equality by Balat, Di Cosmo, and Fiore, is that we exploit the type information of terms substantially and this often allows us to obtain a canonical representation of terms without performing sophisticated term analyses.

http://arxiv.org/abs/1502.04634

https://conf.researchr.org/home/POPL-2017

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

Title: An Intuitionistic Formula Hierarchy Based on High-School Identities

http://arxiv.org/abs/1601.04876

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