Danko Ilik

Gödel’s completeness theorem for classical first-order logic is one of the most basic theorems of logic. Central to any foundational course in logic, it connects the notion of valid formula, i.e., a formula satisfied in all models, to the notion of provable formula. We survey a few standard formulations and proofs of the completeness theorem before focusing on the formal description of a slight modification of Henkin’s proof within intuitionistic second-order arithmetic. It is usual, in the context of the completeness of intuitionistic logic with respect to various semantics, such as Kripke or Beth semantics, to follow the Curry–Howard correspondence and to interpret the proofs of completeness as programs which turn proofs of validity for these semantics into proofs of derivability. We apply this approach to Henkin’s proof to phrase it as a program which transforms any proof of validity with respect to Tarski semantics into a proof of derivability. By doing so, we hope to shed some “effective” light on the relation between Tarski semantics and syntax: proofs of validity are syntactic objects with which we can compute.

G{ö}del's completeness theorem for classical first-order logic is one of the most basic theorems of logic. Central to any foundational course in logic, it connects the notion of valid formula to the notion of provable formula.We survey a few standard formulations and proofs of the completeness theorem before focusing on the formal description of a slight modification of Henkin's proof within intuitionistic second-order arithmetic.It is standard in the context of the completeness of intuitionistic logic with respect to various semantics such as Kripke or Beth semantics to follow the Curry-Howard correspondence and to interpret the proofs of completeness as programs which turn proofs of validity for these semantics into proofs of derivability.We apply this approach to Henkin's proof to phrase it as a program which transforms any proof of validity with respect to Tarski semantics into a proof of derivability.By doing so, we hope to shed an effective light on the relation between Tarski semantics and syntax: proofs of validity are syntactic objects with which we can compute.

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

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 completeness of the 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 exploits the type information of terms substantially and this often allows us to obtain a canonical representation of terms without performing a sophisticated term analyses.

We consider the problem of characterizing isomorphisms of types, or, equivalently, constructive cardinality of sets, in the simultaneous presence of disjoint unions, Cartesian products, and exponentials. Mostly relying on results about polynomials with exponentiation that have not been used in our context, we derive: that the usual finite axiomatization known as High-School Identities (HSI) is complete for a significant subclass of types; that it is decidable for that subclass when two types are isomorphic; that, for the whole of the set of types, a recursive extension of the axioms of HSI exists that is complete; and that, for the whole of the set of types, the question as to whether two types are isomorphic is decidable when base types are to be interpreted as finite sets. We also point out certain related open problems.

We present an implementation in the Coq proof assistant of type directed partial evaluation (TDPE) algorithms for call-by-name and call-by-value versions of shift and reset delimited control operators, and in presence of strong sum types. We prove that the algorithm transforms well-typed programs to ones in normal form. These normal forms can not always be arrived at using the so far known equational theories. The typing system does not allow answer-type modification for function types and allows delimiters to be set on at most one atomic type. The semantic domain for evaluation is expressed in Constructive Type Theory as a dependently typed monadic structure combining Kripke models and continuation passing style translations.Comment: In Proceedings COS 2013, arXiv:1309.092