Logic & Programming

Danko Ilik's research blog

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.

Comments @danko@mamot.fr

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.

Comments @danko@mamot.fr

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.

Comments @danko@mamot.fr

My PhD thesis has been approved for defense. You can find it here : http://tel.archives-ouvertes.fr/tel-00529021/en/

Chapter 1 gives a constructive version of a Henkin-style proof of Godel's completeness theorem. Chapter 2 introduces a notion of model similar to Kripke models using which one can give a normalization-by-evaluation style proof of completeness for classical logic. Chapter 3 does the same thing for intuitionistic logic (including disjunction and the existential). Finally, Chapter 4 presents an extension of intuitionistic logic with delimited control operators which still remains intuitionistic (preserves disjunction and existence properties) and can prove the Double Negation Shift and Markov's Principle.

Comments @danko@mamot.fr

Published on Feb. 5th, 2010 on https://speleologic.livejournal.com/2595.html

The purpose of this post is a detailed proof, following Coquand[1], of the Open Induction Principle using Decidable-Bar Induction[2].

Open induction (OI) is useful when one can not do a proof by usual well-founded induction, that is, when there is no well-founded relation that can be used. In such cases, if the space one is in is compact, and the property one wants to prove is open, one can use a non-well-founded order to do an induction proof. From the computer science perspective, this means one can build a terminating recursive program for computing a property that does not depend on a structurally decreasing criterium of termination.

In this post we concentrate on Cantor space 2N, but it is, in some sense, enough, because every compact space is an image of Cantor space. A member α of 2N is a map N → 2, i.e. an infinite stream of bits, i.e. an infinite branch of the infinite binary tree. α<β if α is “left of” β as a branch of the infinite tree, that is, α<β if they are bit streams which are equal for a finite initial segment and then at some length n of the segment α(n) is “left” while β(n) is “right”. We write αn for the finite initial segment of α of lenght n. Each node in the infinite binary tree corresponds to some initial segment, and vice-versa. Each such node, i.e. each finite bit string, is called a basic open. An open, or open subspace, of Cantor space is an arbitrary union of basic opens. Equivalently, an open is determined by a Boolean function G on arbitrary lenght, but finite, bit strings, G : 2* → 2, which is monotone: If s, s′:2*, s is an initial segment of s′, and G(s)=⊤, then also G(s′)=⊤.

Axiom 1 (Decidable-Bar Induction) For all unary predicates P and Q on 2* (finite binary strings), such that P is decidable and ∀ s. P s → Q s, if ∀ α∈2N. ∃ n∈ N. P(αn) and ∀ s∈2*. (∀ b∈ 2. Q ⟨ b::s ⟩) → Q s then Q ⟨ ⟩.

Theorem 2 (Open Induction Principle) Let U be an open set of Cantor space 2N and < be a lexicographic ordering on 2N. If ∀ α. (∀ β<α. β∈ U) → α∈ U () then ∀ α. α∈ U. Proof. Let α : 2N be given. U is open in 2N, hence given by a mapping G : 2 → 2 which is monotone w.r.t. initial segments: if s is a prefix of t, G s = ⊤ implies G t = ⊤. We say that G bars s with witness k (notation G|k s) if all k−bit-extensions of s satisfy G.

We define mutually, by (primitive) recursion on finite strings of numbers, two functions f:N* → 2* and acc:N*→ 2:

acc ⟨ ⟩ = ⊤ acc ⟨ 0::s ⟩ = acc(s) acc ⟨ n+1::s ⟩ = acc(s) ∧ G|n ⟨ ⊥::f(s) ⟩

f ⟨ ⟩ = ⟨ ⟩ f ⟨ 0::s ⟩ = ⟨ ⊥::f(s) ⟩ f ⟨ n+1::s ⟩ = ⟨ acc⟨ n+1::s ⟩::f(s) ⟩ We set

P(s) := G(f(s)) Q(s) := acc(s) → ∃ m. G|m f(s) and apply bar induction, which gives us a proof of Q(⟨ ⟩), which, since acc(⟨ ⟩)=⊤, gives an m∈ N such that any bit-string with length m satisfies G. Hence, also αm, therefore α∈ U.

The hypotheses of (D-BI) are satisfied by the following lemmas.

Lemma 3 ∀ α∈NN. ∃ n∈ N. G(f(αn)) Proof. We write f(α) for the natural exension of f to infinite sequences. The lemma states that ∀ α∈NN. f(α)∈ U. Let α be given. Apply (). Let β<f(α), that is, there is some n such that βn = ⟨ ⊥::s ⟩ and ⟨ ⊤::s ⟩ = f(α) n = f(αn) for some s∈2 (of length n−1). By the defining equations of f and app, n>0, s=f(α(n−1)), acc(s) and G|k⟨ ⊥::s ⟩, that is, G|kβn, for some k. Hence, G(β(n+k)) = ⊤ i.e. β∈ U.

Lemma 4 For any s∈N*, if (∀ n∈ N. acc⟨ n::s ⟩ → ∃ m. G|m f⟨ n::s ⟩), and acc(s), then ∃ n. G|n f(s). Proof. Since acc(s), also acc⟨ 0::s ⟩, and the hypothesis gives us an m such that G|mf⟨ 0::s ⟩, that is, G|m⟨ ⊥::f(s) ⟩. This means that acc⟨ m+1::s ⟩, which we use with the hypothesis again to get a k such that G|kf⟨ m+1::s ⟩ i.e. Gk⟨ acc⟨ m+1::s ⟩::f(s) ⟩ i.e. G|k⟨ ⊤::f(s) ⟩. We showed that G bars both ⟨ ⊤::f(s) ⟩ and ⟨ ⊥::f(s) ⟩, which means that G bars f(s) already: G|max(m,k)f(s).

Lemma 5 ∀ s∈N*. G(f(s)) → acc(s) → ∃ m. G|m f(s). Proof. G(f(s)) iff G|0 f(s).

Remark 6 The given lemmas, and the functions f and acc, are more general than needed for (D-BI), since they take input of type N* instead of 2*.

References [1] Thierry Coquand. A note on the open induction principle, 1997. [2] Anne S. Troelstra and Dirk van Dalen. Constructivism in Mathematics: An Introduction I and II, volume 121, 123 of Studies in Logic and the Foundations of Mathematics. North-Holland, 1988.

Comments @danko@mamot.fr

Published on Apr. 19th, 2009 on https://speleologic.livejournal.com/1696.html

Some time ago I came upon a mention of Ishihara's proof technique in constructive analysis and a claim:

In [6], Ishihara introduced the following two lemmas in which, surprisingly, we can use completeness to make a decision which at first sight would seem to be impossible with purely constructive techniques (that is, with intuitionistic, rather than classical, logic). (Bridges, van Dalen, Ishihara: Ishihara’s proof technique in constructive analysis)

One does not have to be interested in mathematical analysis to appreciate it, however, it is enough to think about a sequence of computation steps and a measure of “distance” between every two consecutive computation steps. If one can prove that for a sequence the distance gets smaller and smaller as time goes on we say that the computation converges or is Cauchy. When we consider these converging processes of computation as inhabitants of some universe X we can say that X is a complete metric space.

Here I want to give a simpler (more predicative) proof of Bridges-vanDalen-Ishiharas's Proposition 1, which more obviously gives rise to a program than theirs.

Proposition 1. If X is a complete metric space, X=P∪Q, (xn) is a sequence in X that converges to x and we have ∀y:X, x#y ∨ y∉Q, then we have that (∀n. xn ∈ P) or (∃ n. x_n ∈ Q).

The role of x, y as members of X is to stand for a sequence (xn), (yn) together with a proof that the sequences make progress as time progresses, i.e. they are Cauchy/converging. The relation '#' is called apartness and it means that the two computation processes are not 'the same'.

Proof. Start with a sequence (xn). Define the binary sequence λ to be 0 as far as the elements of the sequence (xn) are in P, and to become 1 forever as soon as one of the elements of (x_n) is in Q.

Now define the sequence (yn) to be x as far as λn is 0 and to become xk as soon as λn becomes 1, where k is the smallest natural number at which λ becomes 1, i.e. the k-th element of the sequence (xn) is in Q. The sequence (yn) we defined is very similar to a constant sequence: it is either x forever, or it is x for a finite number of starting elements and then it becomes x_k forever.

In any case (yn) is Cauchy, so we can think of it as an entity y from the universe X. We now use the hypothesis given in Proposition 1 and look at two cases. if x#y then there is k, the smallest number such that λk = 1, which implies xk ∈ Q if y∉Q then we can show that ¬∃n. λn = 1 and, since λ is decidable, ∀n. λn = 0, which implies ∀n. xn ∈ P QED

Apparently, in constructive analysis they use Proposition 1 (and 2, which was not shown) as constructive instances of the general law of excluded middle. Is it useful in logic and computer science?

Comments @danko@mamot.fr