iaddg.net blogs

Reader

Read the latest posts from iaddg.net blogs.

from Logic & Programming

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.

 
En savoir plus...

from 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.

 
Read more...

from Logic & Programming

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.

 
En savoir plus...

from Logic & Programming

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.

 
Read more...

from Logic & Programming

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.

 
En savoir plus...