Showing 1–50 of 80 results for author: Dowek, G

Space-time deterministic graph rewriting

Authors: Pablo Arrighi, Marin Costes, Gilles Dowek, Luidnel Maignan

Abstract: We study non-terminating graph rewriting models, whose local rules are applied non-deterministically -- and yet enjoy a strong form of determinism, namely space-time determinism. Of course in the case of terminating computation it is well-known that the mess introduced by asynchronous rule applications may not matter to the end result, as confluence conspires to produce a unique normal form. In th… ▽ More We study non-terminating graph rewriting models, whose local rules are applied non-deterministically -- and yet enjoy a strong form of determinism, namely space-time determinism. Of course in the case of terminating computation it is well-known that the mess introduced by asynchronous rule applications may not matter to the end result, as confluence conspires to produce a unique normal form. In the context of non-terminating computation however, confluence is a very weak property, and (almost) synchronous rule applications is always preferred e.g. when it comes to simulating dynamical systems. Here we provide sufficient conditions so that asynchronous local rule applications conspire to produce well-determined events in the space-time unfolding of the graph, regardless of their application orders. Our first example is an asynchronous simulation of a dynamical system. Our second example features time dilation, in the spirit of general relativity. △ Less

Submitted 8 April, 2024; originally announced April 2024.

From Rewrite Rules to Axioms in the $λ$$Π$-Calculus Modulo Theory

Authors: Valentin Blot, Gilles Dowek, Thomas Traversié, Théo Winterhalter

Abstract: The $λ$$Π$-calculus modulo theory is an extension of simply typed $λ$-calculus with dependent types and user-defined rewrite rules. We show that it is possible to replace the rewrite rules of a theory of the $λ$$Π$-calculus modulo theory by equational axioms, when this theory features the notions of proposition and proof, while maintaining the same expressiveness. To do so, we introduce in the tar… ▽ More The $λ$$Π$-calculus modulo theory is an extension of simply typed $λ$-calculus with dependent types and user-defined rewrite rules. We show that it is possible to replace the rewrite rules of a theory of the $λ$$Π$-calculus modulo theory by equational axioms, when this theory features the notions of proposition and proof, while maintaining the same expressiveness. To do so, we introduce in the target theory a heterogeneous equality, and we build a translation that replaces each use of the conversion rule by the insertion of a transport. At the end, the theory with rewrite rules is a conservative extension of the theory with axioms. △ Less

Submitted 14 February, 2024; originally announced February 2024.

Nominal semantics for predicate logic: algebras, substitution, quantifiers, and limits

Authors: Gilles Dowek, Murdoch J. Gabbay

Abstract: We define a model of predicate logic in which every term and predicate, open or closed, has an absolute denotation independently of a valuation of the variables. For each variable a, the domain of the model contains an element [[a]] which is the denotation of the term a (which is also a variable symbol). Similarly, the algebra interpreting predicates in the model directly interprets open predicate… ▽ More We define a model of predicate logic in which every term and predicate, open or closed, has an absolute denotation independently of a valuation of the variables. For each variable a, the domain of the model contains an element [[a]] which is the denotation of the term a (which is also a variable symbol). Similarly, the algebra interpreting predicates in the model directly interprets open predicates. Because of this models must also incorporate notions of substitution and quantification. These notions are axiomatic, and need not be applied only to sets of syntax. We prove soundness and show how every 'ordinary' model (i.e. model based on sets and valuations) can be translated to one of our nominal models, and thus also prove completeness. △ Less

Submitted 27 December, 2023; originally announced December 2023.

Journal ref: Proceedings of the 9th Italian Convention on Computational Logic (CILC 2012), pages 104-118, CEUR Workshop Proceedings Volume 857, ISSN 1613-0073 (urn:nbn:de:0074-857-8). https://nbn-resolving.org/urn:nbn:de:0074-857-8

Permissive-Nominal Logic (journal version)

Authors: Gilles Dowek, Murdoch J. Gabbay

Abstract: Permissive-Nominal Logic (PNL) is an extension of first-order predicate logic in which term-formers can bind names in their arguments. This allows for direct axiomatisations with binders, such as of the lambda-binder of the lambda-calculus or the forall-binder of first-order logic. It also allows us to finitely axiomatise arithmetic, and similarly to axiomatise 'nominal' datatypes-with-binding. Ju… ▽ More Permissive-Nominal Logic (PNL) is an extension of first-order predicate logic in which term-formers can bind names in their arguments. This allows for direct axiomatisations with binders, such as of the lambda-binder of the lambda-calculus or the forall-binder of first-order logic. It also allows us to finitely axiomatise arithmetic, and similarly to axiomatise 'nominal' datatypes-with-binding. Just like first- and higher-order logic, equality reasoning is not necessary to alpha-rename. This gives PNL much of the expressive power of higher-order logic, but models and derivations of PNL are first-order in character, and the logic seems to strike a good balance between expressivity and simplicity. △ Less

Submitted 27 December, 2023; originally announced December 2023.

ACM Class: F.4.1; I.2.3

Journal ref: ACM Transactions on Computational Logic, Volume 13, Number 3, Article 20, Publication date: August 2012

PNL to HOL: from the logic of nominal sets to the logic of higher-order functions

Authors: Gilles Dowek, Murdoch J. Gabbay

Abstract: Permissive-Nominal Logic (PNL) extends first-order predicate logic with term-formers that can bind names in their arguments. It takes a semantics in (permissive-)nominal sets. In PNL, the forall-quantifier or lambda-binder are just term-formers satisfying axioms, and their denotation is functions on nominal atoms-abstraction. Then we have higher-order logic (HOL) and its models in ordinary (i.e.… ▽ More Permissive-Nominal Logic (PNL) extends first-order predicate logic with term-formers that can bind names in their arguments. It takes a semantics in (permissive-)nominal sets. In PNL, the forall-quantifier or lambda-binder are just term-formers satisfying axioms, and their denotation is functions on nominal atoms-abstraction. Then we have higher-order logic (HOL) and its models in ordinary (i.e. Zermelo-Fraenkel) sets; the denotation of forall or lambda is functions on full or partial function spaces. This raises the following question: how are these two models of binding connected? What translation is possible between PNL and HOL, and between nominal sets and functions? We exhibit a translation of PNL into HOL, and from models of PNL to certain models of HOL. It is natural, but also partial: we translate a restricted subsystem of full PNL to HOL. The extra part which does not translate is the symmetry properties of nominal sets with respect to permutations. To use a little nominal jargon: we can translate names and binding, but not their nominal equivariance properties. This seems reasonable since HOL -- and ordinary sets -- are not equivariant. Thus viewed through this translation, PNL and HOL and their models do different things, but they enjoy non-trivial and rich subsystems which are isomorphic. △ Less

Submitted 25 December, 2023; originally announced December 2023.

Comments: arXiv admin note: substantial text overlap with arXiv:1111.4611

MSC Class: 03B70 (primary); 68Q55 (secondary) ACM Class: F.3.0; F.3.2

Journal ref: Theoretical Computer Science, Volume 451, 14 September 2012, Pages 38-69

Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques

Authors: Gilles Dowek, Murdoch J. Gabbay, Dominic Mulligan

Abstract: Nominal terms extend first-order terms with binding. They lack some properties of first- and higher-order terms: Terms must be reasoned about in a context of 'freshness assumptions'; it is not always possible to 'choose a fresh variable symbol' for a nominal term; it is not always possible to 'alpha-convert a bound variable symbol' or to 'quotient by alpha-equivalence'; the notion of unifier is no… ▽ More Nominal terms extend first-order terms with binding. They lack some properties of first- and higher-order terms: Terms must be reasoned about in a context of 'freshness assumptions'; it is not always possible to 'choose a fresh variable symbol' for a nominal term; it is not always possible to 'alpha-convert a bound variable symbol' or to 'quotient by alpha-equivalence'; the notion of unifier is not based just on substitution. Permissive nominal terms closely resemble nominal terms but they recover these properties, and in particular the 'always fresh' and 'always rename' properties. In the permissive world, freshness contexts are elided, equality is fixed, and the notion of unifier is based on substitution alone rather than on nominal terms' notion of unification based on substitution plus extra freshness conditions. We prove that expressivity is not lost moving to the permissive case and provide an injection of nominal terms unification problems and their solutions into permissive nominal terms problems and their solutions. We investigate the relation between permissive nominal unification and higher-order pattern unification. We show how to translate permissive nominal unification problems and solutions in a sound, complete, and optimal manner, in suitable senses which we make formal. △ Less

Submitted 25 December, 2023; originally announced December 2023.

Journal ref: Logic Journal of the IGPL, Volume 18, Issue 6, December 2010, Pages 769-822

Dedukti: a Logical Framework based on the $λ$$Π$-Calculus Modulo Theory

Authors: Ali Assaf, Guillaume Burel, Raphaël Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant, Ronan Saillard

Abstract: Dedukti is a Logical Framework based on the $λ$$Π$-Calculus Modulo Theory. We show that many theories can be expressed in Dedukti: constructive and classical predicate logic, Simple type theory, programming languages, Pure type systems, the Calculus of inductive constructions with universes, etc. and that permits to used it to check large libraries of proofs developed in other proof systems: Zenon… ▽ More Dedukti is a Logical Framework based on the $λ$$Π$-Calculus Modulo Theory. We show that many theories can be expressed in Dedukti: constructive and classical predicate logic, Simple type theory, programming languages, Pure type systems, the Calculus of inductive constructions with universes, etc. and that permits to used it to check large libraries of proofs developed in other proof systems: Zenon, iProver, FoCaLiZe, HOL Light, and Matita. △ Less

Submitted 13 November, 2023; originally announced November 2023.

Cut elimination for Zermelo set theory

Authors: Gilles Dowek, Alexandre Miquel

Abstract: We show how to express intuitionistic Zermelo set theory in deduction modulo (i.e. by replacing its axioms by rewrite rules) in such a way that the corresponding notion of proof enjoys the normalization property. To do so, we first rephrase set theory as a theory of pointed graphs (following a paradigm due to P. Aczel) by interpreting set-theoretic equality as bisimilarity, and show that in this s… ▽ More We show how to express intuitionistic Zermelo set theory in deduction modulo (i.e. by replacing its axioms by rewrite rules) in such a way that the corresponding notion of proof enjoys the normalization property. To do so, we first rephrase set theory as a theory of pointed graphs (following a paradigm due to P. Aczel) by interpreting set-theoretic equality as bisimilarity, and show that in this setting, Zermelo's axioms can be decomposed into graph-theoretic primitives that can be turned into rewrite rules. We then show that the theory we obtain in deduction modulo is a conservative extension of (a minor extension of) Zermelo set theory. Finally, we prove the normalization of the intuitionistic fragment of the theory. △ Less

Submitted 31 October, 2023; originally announced October 2023.

Relative normalization

Authors: Gilles Dowek, Alexandre Miquel

Abstract: G{ö}del's second incompleteness theorem forbids to prove, in a given theory U, the consistency of many theories-in particular, of the theory U itself-as well as it forbids to prove the normalization property for these theories, since this property implies their consistency. When we cannot prove in a theory U the consistency of a theory T , we can try to prove a relative consistency theorem, that i… ▽ More G{ö}del's second incompleteness theorem forbids to prove, in a given theory U, the consistency of many theories-in particular, of the theory U itself-as well as it forbids to prove the normalization property for these theories, since this property implies their consistency. When we cannot prove in a theory U the consistency of a theory T , we can try to prove a relative consistency theorem, that is, a theorem of the form: If U is consistent then T is consistent. Following the same spirit, we show in this paper how to prove relative normalization theorems, that is, theorems of the form: If U is 1-consistent, then T has the normalization property. △ Less

Submitted 31 October, 2023; originally announced October 2023.

Embedding Pure Type Systems in the lambda-Pi-calculus modulo

Authors: Denis Cousineau, Gilles Dowek

Abstract: The lambda-Pi-calculus allows to express proofs of minimal predicate logic. It can be extended, in a very simple way, by adding computation rules. This leads to the lambda-Pi-calculus modulo. We show in this paper that this simple extension is surprisingly expressive and, in particular, that all functional Pure Type Systems, such as the system F, or the Calculus of Constructions, can be embedded i… ▽ More The lambda-Pi-calculus allows to express proofs of minimal predicate logic. It can be extended, in a very simple way, by adding computation rules. This leads to the lambda-Pi-calculus modulo. We show in this paper that this simple extension is surprisingly expressive and, in particular, that all functional Pure Type Systems, such as the system F, or the Calculus of Constructions, can be embedded in it. And, moreover, that this embedding is conservative under termination hypothesis. △ Less

Submitted 19 October, 2023; originally announced October 2023.

Arithmetic as a theory modulo

Authors: Gilles Dowek, Benjamin Werner

Abstract: We present constructive arithmetic in Deduction modulo with rewrite rules only. We present constructive arithmetic in Deduction modulo with rewrite rules only. △ Less

Submitted 16 October, 2023; originally announced October 2023.

A linear proof language for second-order intuitionistic linear logic

Authors: Alejandro Díaz-Caro, Gilles Dowek, Malena Ivnisky, Octavio Malherbe

Abstract: We present a polymorphic linear lambda-calculus as a proof language for second-order intuitionistic linear logic. The calculus includes addition and scalar multiplication, enabling the proof of a linearity result at the syntactic level. We present a polymorphic linear lambda-calculus as a proof language for second-order intuitionistic linear logic. The calculus includes addition and scalar multiplication, enabling the proof of a linearity result at the syntactic level. △ Less

Submitted 25 January, 2024; v1 submitted 12 October, 2023; originally announced October 2023.

Comments: arXiv admin note: substantial text overlap with arXiv:2201.11221

Journal ref: (WoLLIC 2024) - LNCS 14672:18-35, 2024

A Proof Synthesis Algorithm for a Mathematical Vernacular in the Calculus of Constructions

Authors: Gilles Dowek

Abstract: We present an incomplete proof synthesis method for the Calculus of Constructions which is always terminating and a complete Vernacular for the Calculus of Constructions based on this method. We present an incomplete proof synthesis method for the Calculus of Constructions which is always terminating and a complete Vernacular for the Calculus of Constructions based on this method. △ Less

Submitted 6 October, 2023; originally announced October 2023.

Automatic Proof Checking and Proof Construction by Tactics

Authors: Gilles Dowek

Abstract: In this note we compare two kinds of systems that verify the correctness of mathematical developments: roof checking and proof construction by tactics and we propose to merge them in a single system. In this note we compare two kinds of systems that verify the correctness of mathematical developments: roof checking and proof construction by tactics and we propose to merge them in a single system. △ Less

Submitted 28 September, 2023; originally announced September 2023.

The Undecidability of Third Order Pattern Matching in Calculi with Dependent Types or Type Constructors

Authors: Gilles Dowek

Abstract: We prove the undecidability of the third order pattern matching problem in typed lambda-calculi with dependent types and in those with type constructors by reducing the second order unification problem to them. We prove the undecidability of the third order pattern matching problem in typed lambda-calculi with dependent types and in those with type constructors by reducing the second order unification problem to them. △ Less

Submitted 21 September, 2023; originally announced September 2023.

Comments: in French language

On Statman's Finite Completeness Theorem

Authors: Richard Statman, Gilles Dowek

Abstract: We give a complete self-contained proof of Statman's finite completeness theorem and of a corollary of this theorem stating that the $λ$-definability conjecture implies the higher-order matching conjecture. We give a complete self-contained proof of Statman's finite completeness theorem and of a corollary of this theorem stating that the $λ$-definability conjecture implies the higher-order matching conjecture. △ Less

Submitted 7 September, 2023; originally announced September 2023.

A Unification Algorithm for Second-Order Linear Terms

Authors: Gilles Dowek

Abstract: We give an algorithm for the class of second order unification problems in which second order variables have at most one occurrence. We give an algorithm for the class of second order unification problems in which second order variables have at most one occurrence. △ Less

Submitted 5 September, 2023; originally announced September 2023.

On the Definition of the Eta-long Normal Form in Type Systems of the Cube

Authors: Gilles Dowek, Gérard Huet, Benjamin Werner

Abstract: The smallest transitive relation < on well-typed normal terms such that if t is a strict subterm of u then t < u and if T is the normal form of the type of t and the term t is not a sort then T < t is well-founded in the type systems of the cube. Thus every term admits a eta-long normal form. The smallest transitive relation < on well-typed normal terms such that if t is a strict subterm of u then t < u and if T is the normal form of the type of t and the term t is not a sort then T < t is well-founded in the type systems of the cube. Thus every term admits a eta-long normal form. △ Less

Submitted 3 July, 2023; originally announced July 2023.

The Undecidability of Typability in the Lambda-Pi-Calculus

Authors: Gilles Dowek

Abstract: The set of pure terms which are typable in the $λ$$Π$-calculus in a given context is not recursive. So there is no general type inference algorithm for the programming language Elf and, in some cases, some type information has to be mentioned by the programmer. The set of pure terms which are typable in the $λ$$Π$-calculus in a given context is not recursive. So there is no general type inference algorithm for the programming language Elf and, in some cases, some type information has to be mentioned by the programmer. △ Less

Submitted 13 June, 2023; originally announced June 2023.

A toy model provably featuring an arrow of time without past hypothesis

Authors: Pablo Arrighi, Gilles Dowek, Amélia Durbec

Abstract: The laws of Physics are time-reversible, making no qualitative distinction between the past and the future -- yet we can only go towards the future. This apparent contradiction is known as the `arrow of time problem'. Its resolution states that the future is the direction of increasing entropy. But entropy can only increase towards the future if it was low in the past, and past low entropy is a ve… ▽ More The laws of Physics are time-reversible, making no qualitative distinction between the past and the future -- yet we can only go towards the future. This apparent contradiction is known as the `arrow of time problem'. Its resolution states that the future is the direction of increasing entropy. But entropy can only increase towards the future if it was low in the past, and past low entropy is a very strong assumption to make, because low entropy states are rather improbable, non-generic. Recent works, however, suggest we can do away with this so-called `past hypothesis', in the presence of reversible dynamical laws featuring expansion. We prove that this is the case for a toy model, set in a 1+1 discrete spacetime. It consists in graphs upon which particles circulate and interact according to local reversible rules. Some rules locally shrink or expand the graph. Generic states always expand; entropy always increases -- thereby providing a local explanation for the arrow of time. △ Less

Submitted 12 June, 2023; originally announced June 2023.

Comments: 26 pages, 18 figures

The Undecidability of Pattern Matching in Calculi where Primitive Recursive Functions are Representable

Authors: Gilles Dowek

Abstract: We prove that the pattern matching problem is undecidable in polymorphic lambda-calculi (as Girard's system F) and calculi supporting inductive types (as G{ö}del's system T) by reducing Hilbert's tenth problem to it. More generally pattern matching is undecidable in all the calculi in which primitive recursive functions can be fairly represented in a precised sense. We prove that the pattern matching problem is undecidable in polymorphic lambda-calculi (as Girard's system F) and calculi supporting inductive types (as G{ö}del's system T) by reducing Hilbert's tenth problem to it. More generally pattern matching is undecidable in all the calculi in which primitive recursive functions can be fairly represented in a precised sense. △ Less

Submitted 9 June, 2023; originally announced June 2023.

A Complete Proof Synthesis Method for the Cube of Type Systems

Authors: Gilles Dowek

Abstract: We present a complete proof synthesis method for the eight type systems of Barendregt's cube extended with $η$-conversion. Because these systems verify the proofs-as-objects paradigm, the proof synthesis method is a one level process merging unification and resolution. Then we present a variant of this method, which is incomplete but much more efficient. At last we show how to turn this algorithm… ▽ More We present a complete proof synthesis method for the eight type systems of Barendregt's cube extended with $η$-conversion. Because these systems verify the proofs-as-objects paradigm, the proof synthesis method is a one level process merging unification and resolution. Then we present a variant of this method, which is incomplete but much more efficient. At last we show how to turn this algorithm into a unification algorithm. △ Less

Submitted 9 June, 2023; originally announced June 2023.

Third Order Matching is Decidable

Authors: Gilles Dowek

Abstract: The higher order matching problem is the problem of determining whether a term is an instance of another in the simply typed $λ$-calculus, i.e. to solve the equation a = b where a and b are simply typed $λ$-terms and b is ground. The decidability of this problem is still open. We prove the decidability of the particular case in which the variables occurring in the problem are at most third order. The higher order matching problem is the problem of determining whether a term is an instance of another in the simply typed $λ$-calculus, i.e. to solve the equation a = b where a and b are simply typed $λ$-terms and b is ground. The decidability of this problem is still open. We prove the decidability of the particular case in which the variables occurring in the problem are at most third order. △ Less

Submitted 2 June, 2023; originally announced June 2023.

Automated theorem proving in first-order logic modulo: on the difference between type theory and set theory

Authors: Gilles Dowek

Abstract: Resolution modulo is a first-order theorem proving method that can be applied both to first-order presentations of simple type theory (also called higher-order logic) and to set theory. When it is applied to some first-order presentations of type theory, it simulates exactly higherorder resolution. In this note, we compare how it behaves on type theory and on set theory. Resolution modulo is a first-order theorem proving method that can be applied both to first-order presentations of simple type theory (also called higher-order logic) and to set theory. When it is applied to some first-order presentations of type theory, it simulates exactly higherorder resolution. In this note, we compare how it behaves on type theory and on set theory. △ Less

Submitted 1 June, 2023; originally announced June 2023.

Axioms vs. rewrite rules: from completeness to cut elimination

Authors: Gilles Dowek

Abstract: Combining a standard proof search method, such as resolution or tableaux, and rewriting is a powerful way to cut off search space in automated theorem proving, but proving the completeness of such combined methods may be challenging. It may require in particular to prove cut elimination for an extended notion of proof that combines deductions and computations. This suggests new interactions betwee… ▽ More Combining a standard proof search method, such as resolution or tableaux, and rewriting is a powerful way to cut off search space in automated theorem proving, but proving the completeness of such combined methods may be challenging. It may require in particular to prove cut elimination for an extended notion of proof that combines deductions and computations. This suggests new interactions between automated theorem proving and proof theory. △ Less

Submitted 1 June, 2023; originally announced June 2023.

From proof theory to theories theory

Authors: Gilles Dowek

Abstract: In the last decades, several objects such as grammars, economical agents, laws of physics... have been defined as algorithms. In particular, after Brouwer, Heyting, and Kolomogorov, mathematical proofs have been defined as algorithms. In this paper, we show that mathematical theories can be also be defined as algorithms and that this definition has some advantages over the usual definition of the… ▽ More In the last decades, several objects such as grammars, economical agents, laws of physics... have been defined as algorithms. In particular, after Brouwer, Heyting, and Kolomogorov, mathematical proofs have been defined as algorithms. In this paper, we show that mathematical theories can be also be defined as algorithms and that this definition has some advantages over the usual definition of theories as sets of axioms. △ Less

Submitted 1 June, 2023; originally announced June 2023.

The Stratified Foundations as a theory modulo

Authors: Gilles Dowek

Abstract: The Stratified Foundations are a restriction of naive set theory where the comprehension scheme is restricted to stratifiable propositions. It is known that this theory is consistent and that proofs strongly normalize in this theory. Deduction modulo is a formulation of first-order logic with a general notion of cut. It is known that proofs normalize in a theory modulo if it has some kind of many-… ▽ More The Stratified Foundations are a restriction of naive set theory where the comprehension scheme is restricted to stratifiable propositions. It is known that this theory is consistent and that proofs strongly normalize in this theory. Deduction modulo is a formulation of first-order logic with a general notion of cut. It is known that proofs normalize in a theory modulo if it has some kind of many-valued model called a pre-model. We show in this paper that the Stratified Foundations can be presented in deduction modulo and that the method used in the original normalization proof can be adapted to construct a pre-model for this theory. △ Less

Submitted 30 May, 2023; originally announced May 2023.

Binding Logic: proofs and models

Authors: Gilles Dowek, Thérèse Hardin, Claude Kirchner

Abstract: We define an extension of predicate logic, called Binding Logic, where variables can be bound in terms and in propositions. We introduce a notion of model for this logic and prove a soundness and completeness theorem for it. This theorem is obtained by encoding this logic back into predicate logic and using the classical soundness and completeness theorem there. We define an extension of predicate logic, called Binding Logic, where variables can be bound in terms and in propositions. We introduce a notion of model for this logic and prove a soundness and completeness theorem for it. This theorem is obtained by encoding this logic back into predicate logic and using the classical soundness and completeness theorem there. △ Less

Submitted 25 May, 2023; originally announced May 2023.

Comments: Colloque avec actes et comit{é} de lecture. internationale

Report number: A02-R-500 || dowek02a

Journal ref: 9th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning - LPAR'2002, Oct 2002, Tbilisi, Georgia. pp.130-144

What is a Theory ?

Authors: Gilles Dowek

Abstract: Deduction modulo is a way to express a theory using computation rules instead of axioms. We present in this paper an extension of deduction modulo, called Polarized deduction modulo, where some rules can only be used at positive occurrences, while others can only be used at negative ones. We show that all theories in propositional calculus can be expressed in this framework and that cuts can alway… ▽ More Deduction modulo is a way to express a theory using computation rules instead of axioms. We present in this paper an extension of deduction modulo, called Polarized deduction modulo, where some rules can only be used at positive occurrences, while others can only be used at negative ones. We show that all theories in propositional calculus can be expressed in this framework and that cuts can always be eliminated with such theories. △ Less

Submitted 25 May, 2023; originally announced May 2023.

Preliminary investigations on induction over real numbers

Authors: Gilles Dowek

Abstract: The induction principle for natural numbers expresses that when a property holds for some natural number a and is hereditary, then it holds for all numbers greater than or equal to a. We present a similar principle for real numbers. The induction principle for natural numbers expresses that when a property holds for some natural number a and is hereditary, then it holds for all numbers greater than or equal to a. We present a similar principle for real numbers. △ Less

Submitted 24 May, 2023; originally announced May 2023.

Confluence as a cut elimination property

Authors: Gilles Dowek

Abstract: The goal of this note is to compare two notions, one coming from the theory of rewrite systems and the other from proof theory: confluence and cut elimination. We show that to each rewrite system on terms, we can associate a logical system: asymmetric deduction modulo this rewrite system and that the confluence property of the rewrite system is equivalent to the cut elimination property of the ass… ▽ More The goal of this note is to compare two notions, one coming from the theory of rewrite systems and the other from proof theory: confluence and cut elimination. We show that to each rewrite system on terms, we can associate a logical system: asymmetric deduction modulo this rewrite system and that the confluence property of the rewrite system is equivalent to the cut elimination property of the associated logical system. This equivalence, however, does not extend to rewrite systems directly rewriting atomic propositions. △ Less

Submitted 23 May, 2023; originally announced May 2023.

A constructive proof of Skolem theorem for constructive logic

Authors: Gilles Dowek, Benjamin Werner

Abstract: If the sequent (Gamma entails forall x exists y A) is provable in first order constructive natural deduction, then the theory (Gamma, forall x (f (x)/y)A), where f is a new function symbol, is a conservative extension of Gamma. If the sequent (Gamma entails forall x exists y A) is provable in first order constructive natural deduction, then the theory (Gamma, forall x (f (x)/y)A), where f is a new function symbol, is a conservative extension of Gamma. △ Less

Submitted 17 May, 2023; originally announced May 2023.

What do we know when we know that a theory is consistent?

Authors: Gilles Dowek

Abstract: Given a first-order theory and a proof that it is consistent, can we design a proof-search method for this theory that fails in finite time when it attempts to prove the formula False? Given a first-order theory and a proof that it is consistent, can we design a proof-search method for this theory that fails in finite time when it attempts to prove the formula False? △ Less

Submitted 17 May, 2023; originally announced May 2023.

Eigenvariables, bracketing and the decidability of positive minimal predicate logic

Authors: Gilles Dowek, Ying Jiang

Abstract: We give a new proof of a theorem of Mints that the positive fragment of minimal predicate logic is decidable. The idea of the proof is to replace the eigenvariable condition of sequent calculus by an appropriate sco** mechanism. The algorithm given by this proof seems to be more practical than that given by the original proof. A naive implementation is given at the end of the paper. Another cont… ▽ More We give a new proof of a theorem of Mints that the positive fragment of minimal predicate logic is decidable. The idea of the proof is to replace the eigenvariable condition of sequent calculus by an appropriate sco** mechanism. The algorithm given by this proof seems to be more practical than that given by the original proof. A naive implementation is given at the end of the paper. Another contribution is to show that this result extends to a large class of theories, including simple type theory (higherorder logic) and second-order propositional logic. We obtain this way a new proof of the decidability of the inhabitation problem for positive types in system F. △ Less

Submitted 15 May, 2023; originally announced May 2023.

Truth values algebras and proof normalization

Authors: Gilles Dowek

Abstract: We extend the notion of Heyting algebra to a notion of truth values algebra and prove that a theory is consistent if and only if it has a B-valued model for some non trivial truth values algebra B. A theory that has a B-valued model for all truth values algebras B is said to be super-consistent. We prove that super-consistency is a model-theoretic sufficient condition for strong normalization. We extend the notion of Heyting algebra to a notion of truth values algebra and prove that a theory is consistent if and only if it has a B-valued model for some non trivial truth values algebra B. A theory that has a B-valued model for all truth values algebras B is said to be super-consistent. We prove that super-consistency is a model-theoretic sufficient condition for strong normalization. △ Less

Submitted 12 May, 2023; originally announced May 2023.

The Undecidability of Unification Modulo $σ$ Alone

Authors: Gilles Dowek

Abstract: The rewriting system sigma is the set of rules propagating explicit substitutions in the lambda-calculus with explicit substitutions. In this note, we prove the undecidability of unification modulo sigma. The rewriting system sigma is the set of rules propagating explicit substitutions in the lambda-calculus with explicit substitutions. In this note, we prove the undecidability of unification modulo sigma. △ Less

Submitted 9 May, 2023; originally announced May 2023.

Skolemization in Simple Type Theory: the Logical and the Theoretical Points of View

Authors: Gilles Dowek

Abstract: Peter Andrews has proposed, in 1971, the problem of finding an analog of the Skolem theorem for Simple Type Theory. A first idea lead to a naive rule that worked only for Simple Type Theory with the axiom of choice and the general case has only been solved, more than ten years later, by Dale Miller. More recently, we have proposed with Th{é}r{è}se Hardin and Claude Kirchner a new way to prove anal… ▽ More Peter Andrews has proposed, in 1971, the problem of finding an analog of the Skolem theorem for Simple Type Theory. A first idea lead to a naive rule that worked only for Simple Type Theory with the axiom of choice and the general case has only been solved, more than ten years later, by Dale Miller. More recently, we have proposed with Th{é}r{è}se Hardin and Claude Kirchner a new way to prove analogs of the Miller theorem for different, but equivalent, formulations of Simple Type Theory. In this paper, that does not contain new technical results, I try to show that the history of the skolemization problem and of its various solutions is an illustration of a tension between two points of view on Simple Type Theory: the logical and the theoretical points of view. △ Less

Submitted 5 May, 2023; originally announced May 2023.

Enumerating proofs of positive formulae

Authors: Gilles Dowek, Ying Jiang

Abstract: We provide a semi-grammatical description of the set of normal proofs of positive formulae in minimal predicate logic, i.e. a grammar that generates a set of schemes, from each of which we can produce a finite number of normal proofs. This method is complete in the sense that each normal proof-term of the formula is produced by some scheme generated by the grammar. As a corollary, we get a similar… ▽ More We provide a semi-grammatical description of the set of normal proofs of positive formulae in minimal predicate logic, i.e. a grammar that generates a set of schemes, from each of which we can produce a finite number of normal proofs. This method is complete in the sense that each normal proof-term of the formula is produced by some scheme generated by the grammar. As a corollary, we get a similar description of the set of normal proofs of positive formulae for a large class of theories including simple type theory and System F. △ Less

Submitted 2 May, 2023; originally announced May 2023.

On the convergence of reduction-based and model-based methods in proof theory

Authors: Gilles Dowek

Abstract: In the recent past, the reduction-based and the model-based methods to prove cut elimination have converged, so that they now appear just as two sides of the same coin. This paper details some of the steps of this transformation. In the recent past, the reduction-based and the model-based methods to prove cut elimination have converged, so that they now appear just as two sides of the same coin. This paper details some of the steps of this transformation. △ Less

Submitted 2 May, 2023; originally announced May 2023.

The physical Church-Turing thesis and non deterministic computation over the real numbers

Authors: Gilles Dowek

Abstract: On the real numbers, the notions of a semi-decidable relation and that of an effectively enumerable relation differ. The second only seems to be adequate to express, in an algorithmic way, non deterministic physical theories, where magnitudes are represented by real numbers. On the real numbers, the notions of a semi-decidable relation and that of an effectively enumerable relation differ. The second only seems to be adequate to express, in an algorithmic way, non deterministic physical theories, where magnitudes are represented by real numbers. △ Less

Submitted 19 April, 2023; originally announced May 2023.

Logipedia: a multi-system encyclopedia of formal proofs

Authors: Gilles Dowek, François Thiré

Abstract: Libraries of formal proofs are an important part of our mathematical heritage, but their usability and sustainability is poor. Indeed, each library is specific to a proof system, sometimes even to some version of this system. Thus, a library developed in one system cannot, in general, be used in another and when the system is no more maintained, the library may be lost. This impossibility of using… ▽ More Libraries of formal proofs are an important part of our mathematical heritage, but their usability and sustainability is poor. Indeed, each library is specific to a proof system, sometimes even to some version of this system. Thus, a library developed in one system cannot, in general, be used in another and when the system is no more maintained, the library may be lost. This impossibility of using a proof developed in one system in another has been noted for long and a remediation has been proposed: as we have empirical evidence that most of the formal proofs developed in one of these systems can also be developed in another, we can develop a standard language, in which these proofs can be translated, and then used in all systems supporting this standard. Logipedia is an attempt to build such a multi-system online encyclopedia of formal proofs expressed in such as standard language. It is based on two main ideas: the use of a logical framework and of reverse mathematics. △ Less

Submitted 6 April, 2023; originally announced May 2023.

Specifying programs with propositions and with congruences

Authors: Gilles Dowek

Abstract: We give a presentation of Krivine and Parigot's Second-order functional arithmetic in Deduction modulo. Expressing this theory in Deduction modulo sheds light on an original aspect of this theory: the fact that programs are specified, not with propositions, but with congruences. We give a presentation of Krivine and Parigot's Second-order functional arithmetic in Deduction modulo. Expressing this theory in Deduction modulo sheds light on an original aspect of this theory: the fact that programs are specified, not with propositions, but with congruences. △ Less

Submitted 26 April, 2023; originally announced April 2023.

Simple Type Theory as a Clausal Theory

Authors: Gilles Dowek

Abstract: We give a presentation of Simple Type Theory as a clausal rewrite system in Polarized deduction modulo. We give a presentation of Simple Type Theory as a clausal rewrite system in Polarized deduction modulo. △ Less

Submitted 26 April, 2023; originally announced April 2023.

The physical Church thesis and the sensitivity to initial conditions

Authors: Gilles Dowek

Abstract: The physical Church thesis is a thesis about nature that expresses that all that can be computed by a physical system-a machine-is computable in the sense of computability theory. At a first look, this thesis seems contradictory with the existence, in nature, of chaotic dynamical systems, that is systems whose evolution cannot be ''computed'' because of their sensitivity to initial conditions. The… ▽ More The physical Church thesis is a thesis about nature that expresses that all that can be computed by a physical system-a machine-is computable in the sense of computability theory. At a first look, this thesis seems contradictory with the existence, in nature, of chaotic dynamical systems, that is systems whose evolution cannot be ''computed'' because of their sensitivity to initial conditions. The goal of this note is to show that there exist dynamical systems that are both computable and chaotic, and thus that the existence in nature of chaotic dynamical system is not, per se, a refutation of the physical Church thesis. Thus, chaos seems to be compatible with computability, in the same way as it is compatible with determinism. △ Less

Submitted 26 April, 2023; originally announced April 2023.

On the Expressive Power of Schemes

Authors: Gilles Dowek, Ying Jiang

Abstract: We present a calculus, called the scheme-calculus, that permits to express natural deduction proofs in various theories. Unlike $λ$-calculus, the syntax of this calculus sticks closely to the syntax of proofs, in particular, no names are introduced for the hypotheses. We show that despite its non-determinism, some typed scheme-calculi have the same expressivity as the corresponding typed $λ$-calcu… ▽ More We present a calculus, called the scheme-calculus, that permits to express natural deduction proofs in various theories. Unlike $λ$-calculus, the syntax of this calculus sticks closely to the syntax of proofs, in particular, no names are introduced for the hypotheses. We show that despite its non-determinism, some typed scheme-calculi have the same expressivity as the corresponding typed $λ$-calculi. △ Less

Submitted 24 April, 2023; originally announced April 2023.

How can we prove that a proof search method is not an instance of another?

Authors: Guillaume Burel, Gilles Dowek

Abstract: We introduce a method to prove that a proof search method is not an instance of another. As an example of application, we show that Polarized resolution modulo, a method that mixes clause selection restrictions and literal selection restrictions, is not an instance of Ordered resolution with selection. We introduce a method to prove that a proof search method is not an instance of another. As an example of application, we show that Polarized resolution modulo, a method that mixes clause selection restrictions and literal selection restrictions, is not an instance of Ordered resolution with selection. △ Less

Submitted 24 April, 2023; originally announced April 2023.

A Simple Proof That Super-Consistency Implies Cut Elimination

Authors: Gilles Dowek, Olivier Hermant

Abstract: We give a simple and direct proof that super-consistency implies the cut elimination property in deduction modulo. This proof can be seen as a simplification of the proof that super-consistency implies proof normalization. It also takes ideas from the semantic proofs of cut elimination that proceed by proving the completeness of the cut-free calculus. As an application, we compare our work with th… ▽ More We give a simple and direct proof that super-consistency implies the cut elimination property in deduction modulo. This proof can be seen as a simplification of the proof that super-consistency implies proof normalization. It also takes ideas from the semantic proofs of cut elimination that proceed by proving the completeness of the cut-free calculus. As an application, we compare our work with the cut elimination theorems in higher-order logic that involve V-complexes. △ Less

Submitted 21 April, 2023; originally announced April 2023.

A theory independent Curry-De Bruijn-Howard correspondence

Authors: Gilles Dowek

Abstract: Instead of develo** a customized typed lambda-calculus for each theory, we attempt to design a general parametric calculus that permits to express the proofs of any theory. This way, the problem of expressing proofs in the lambda-calculus is separated from that of choosing a theory. Instead of develo** a customized typed lambda-calculus for each theory, we attempt to design a general parametric calculus that permits to express the proofs of any theory. This way, the problem of expressing proofs in the lambda-calculus is separated from that of choosing a theory. △ Less

Submitted 17 April, 2023; originally announced April 2023.

The principle of a finite density of information

Authors: Pablo Arrighi, Gilles Dowek

Abstract: The possibility to describe the laws of the Universe in a computational way seems to be correlated to a principle that the density of information is bounded. This principle, that is dual to that of a finite velocity of information, has already been investigated in Physics, and is correlated to the old idea that there is no way to know a magnitude with an infinite precision. It takes different form… ▽ More The possibility to describe the laws of the Universe in a computational way seems to be correlated to a principle that the density of information is bounded. This principle, that is dual to that of a finite velocity of information, has already been investigated in Physics, and is correlated to the old idea that there is no way to know a magnitude with an infinite precision. It takes different forms in classical Physics and in quantum Physics. △ Less

Submitted 17 April, 2023; originally announced April 2023.

Complementation: a bridge between finite and infinite proofs

Authors: Gilles Dowek, Ying Jiang

Abstract: When a proposition has no proof in an inference system, it is sometimes useful to build a counter-proof explaining, step by step, the reason of this non-provability. In general, this counter-proof is a (possibly) infinite co-inductive proof in a different inference system. In this paper, we show that, for some decidable inference systems, this (possibly) infinite proof has a representation as a fi… ▽ More When a proposition has no proof in an inference system, it is sometimes useful to build a counter-proof explaining, step by step, the reason of this non-provability. In general, this counter-proof is a (possibly) infinite co-inductive proof in a different inference system. In this paper, we show that, for some decidable inference systems, this (possibly) infinite proof has a representation as a finite proof in yet another system, equivalent to the previous one. △ Less

Submitted 11 April, 2023; originally announced April 2023.