Skip navigation

Category Archives: Logic

By Anthony Cantor (University of Iowa PhD student)

Thanks to travel funds generously provided by my advisor, Aaron Stump, as well as the FLOC student travel grant, I was recently fortunate enough to spend a week in Oxford at FLOC 2018. Not only was it an enriching experience, but it was also my first time presenting research. Over the course of the pre-FLOC workshop weekend and the block 1 conferences I saw numerous thought-provoking and enlightening presentations, so I’d like to share some of the highlights here.

Term Assignment for Admissible Rules in Intuitionistic Logic
One of my favorites from my day at the Classical Logic and Computation workshop was Matteo Manighetti’s presentation of an extension of intuitionistic logic that supports admissible intuitionistic rules (with co-author Andrea Condoluci). He explained that if the provability of a formula A implies the provability of a formula B, then the rule A/B is admissible, and if the formula A→B is provable then the rule A/B is derivable. As far as I can tell, these definitions express the difference between meta-theoretic implication and object implication. In classical logic every admissible rule is derivable, but this is not the case in intuitionistic logic: apparently the rule ¬A→(B∨C) / (¬A→B)∨(¬A→C) is admissible but not derivable (this is called “Harrop’s rule”). Manighetti continued by describing an extension of intuitionistic logic obtained by adding axioms corresponding to the admissible rules, and a corresponding Curry-Howard term assignment. I’m really looking forward to reading this paper when it appears in the workshop proceedings because I’m very curious about the details of some of the proofs of theorems that Manighetti claimed during the presentation: one was the disjunction property, and the other he called a “classification” lemma. At the moment I’m quite interested in these sorts of proofs because I’m currently working with Aaron to prove a logical constructiveness result.

Proof Nets and Linear Logic
While at FLOC I attended two great presentations on the subject of proof nets: a presentation on proof nets for bi-intuitionistic linear logic by Willem Heijltjes, and a presentation on a new type of proof nets for multiplicative linear logic by Dominic Hughes. These two presentations caught my interest because of the logic under consideration in the former (bi-intuitionistic logic), and the concept of canonicity in the latter (these two topics relate to research I’ve been working on with Aaron).

Regardless of their potential relevance to my research interests, I’m happy to have attended these presentations because they both had a common property that taught me a lesson about designing slides: when possible, omit words (especially sentences) from a slide. Both of these presentations did a good job of focusing my attention on a particular point of the slide (usually some part of a proof derivation). Throughout the conference I often got lost because I was trying to read sentences on slides instead of focusing on the speaker. By omitting unnecessary words, these presentations kept my eyes on the right part of the slide, and my ears on the speaker. Interestingly, the two presentations differed greatly in terms of the their depth. Heijltjes’ presentation contained a lot details and examples, and Hughes’ stayed extremely high level.

Inspired by Heijltjes and Hughes, I’ve begun exploring linear logic and proof nets via Girard’s “Linear Logic”, a reference cited in both of their papers[1][2]. So far it’s been very rewarding. In particular, I quite liked the following observation made by Girard regarding the connection between the ⊢ relation and constructiveness:

Now, what is the meaning of the separation ⊢? The classical answer is “to separate positive and negative occurrences”. This is factually true but shallow; we shall get a better answer by asking a better question: what in the essence of ⊢ makes the two latter logics more constructive than the classical one? For this the answer is simple: take a proof of the existence or the disjunction property; we use the fact that the last rule used is an introduction, which we cannot do classically because of a possible contraction. Therefore, in the minimal and intuitionistic cases, ⊢ serves to mark a place where contraction (and maybe weakening too) is forbidden; classically speaking, the ⊢ does not have such a meaning, and this is why lazy people very often only keep the right-hand side of classical sequents. Once we have recognized that the constructive features of intuitionistic logic come from the dumping of structural rules on a specific place in the sequents, we are ready to face the consequences of this remark: the limitation should be generalized to the other rooms, i.e., weakening and contraction disappear. As soon as weakening and contraction have been forbidden, we are in linear logic.

Blockchain Verification
Grigore Rosu’s presentation on formally verifying blockchain contracts and virtual machines also stood out. In his talk Rosu advocated the use of a single framework called “K” to generate a suite of language and runtime tools related to a blockchain specification, as opposed to constructing the components first and attempting formal verification as an afterthought. The system uses a logic called “Matching Logic” to generate the components based on configurations containing semantic and syntactic rules. Rosu claimed that many previous methods for defining computational semantics have drawbacks, and that the “K” framework “keeps the advantages of those methods, but without the drawbacks”. Unfortunately he didn’t explain how exactly the “K” framework achieves this, but he did enumerate a rather impressive list of languages that are currently supported by the “K” framework, which included C, Java, and the Ethereum VM. I had a hard time following a lot of the detail about how matching logic enables auto-generation of effective language tools, but I’m at least convinced that it would probably be a lot of fun to try out his framework on a toy language.

Corrado Böhm Memorial
Finally, another standout event was most certainly the pair of talks given by Silvio Micali and Henk Barendregt in memory of Corrado Böhm. After relaying some personal memories, Barendregt presented some highlights of Böhm’s career. He first discussed some of Böhm’s early work on self compilation and bootstrapping. In particular, Böhm proved that one could start with a handwritten slow compiler, and then use that compiler to compile itself to obtain faster and faster compilers. Barendregt also touched on a few other important results achieved by Böhm, and ended by discussing Böhm’s passion for research: apparently Böhm was still stating open problems even while in his 90’s. Barendregt’s conclusion was memorable: “keeping asking questions, it keeps you young.”

[1] http://www.cs.bath.ac.uk/~wbh22/pdf/2018-bellin-heijltjes.pdf
[2] http://boole.stanford.edu/~dominic/papers/unification-nets/unification-nets-LICS-2018.pdf

Advertisements

This post is about double negation in constructive type theory.  Suppose you know that \neg(\neg A) is true; i.e., (A \to \perp)\to \perp (writing \perp for false).  In classical logic, you then know that A is true.  But of course, you are allowed no such conclusion in intuitionistic logic.  So far, so familiar.  But let us look at this now from the perspective of realizability.  Realizability semantics gives the meaning of a type as a set of some kind of realizers.  Let us consider untyped lambda calculus terms (or combinators) as realizers for purposes of this discussion.  Then the crucial clauses of the semantics for our purposes are

  • t \in [\negthinspace[ A \to B ]\negthinspace ]\ \Leftrightarrow\ \forall t' \in[\negthinspace[A]\negthinspace].\ t\ t'\in[\negthinspace[B]\negthinspace], and
  • \neg t \in [\negthinspace[\perp]\negthinspace]

Let us work through, then, when t\in[\negthinspace[(A\to\perp)\to\perp]\negthinspace] according to this definition:

\begin{array}{ll} t\in[\negthinspace[(A\to\perp)\to\perp]\negthinspace] & \Leftrightarrow \\ \forall t'\in[\negthinspace[A\to\perp]\negthinspace].\ t\ t'\in[\negthinspace[\perp]] & \Leftrightarrow \\ \forall t'.\neg(t'\in[\negthinspace[ A \to \perp]\negthinspace]) & \Leftrightarrow \\ \neg(t'\in[\negthinspace[A\to\perp]\negthinspace]) & \Leftrightarrow \\ \neg(\forall t''\in[\negthinspace[A]\negthinspace].\ t'\ t''\in[\negthinspace[\perp]\negthinspace]) & \Leftrightarrow \\ \neg(\forall t''.\neg t''\in[\negthinspace[A]\negthinspace]) & \Leftrightarrow \\ \exists t''.t''\in[\negthinspace[A]\negthinspace] &\  \end{array}

So this is saying that if [\negthinspace[A]\negthinspace] is nonempty, then [\negthinspace[(A\to\perp)\to\perp]\negthinspace] is universal (contains all terms); and otherwise (if [\negthinspace[A]\negthinspace] is empty), [\negthinspace[(A\to\perp)\to\perp]\negthinspace] is empty.

So if you have a function F, say, realizing \neg\neg A)\to B for some B, what this means is that F can make use of the fact that A is true, but not how it is true.  If F were simply given a proof of A, then it could compute with this proof.  But here, with \neg\neg A, the proof of A is hidden behind an existential quantifier (as we deduced above), and so it cannot be used.  Only if someone is reasoning at the metalevel about F, they can make use of the fact that A is true when checking that the body of F realizes B.

So semantically, \neg\neg A is news you can’t use: we know A is true, but we have no access to how it is true.  For example, if A is a disjunction, you cannot case split, within the type theory, on the disjuncts.  Only at the metalevel are you entitled to consider the behavior of a term in light of the fact that one or the other of the disjuncts must hold.

Last week I had the great pleasure of visiting the amazing PL group at Indiana University.  They are doing so much inspiring research in many different areas of programming languages research.  It was great.  The collective knowledge there was very impressive, and I got a lot of great references to follow up on now that I am back.

I gave two talks: one in the logic seminar, and one for the PL group.  In the first talk, one issue I was discussing was an argument, originally sketched by Michael Dummett and developed more fully by Charles Parsons in a paper called “The Impredicativity of Induction” (you can find a revised version of this paper in a book called “Proof, Logic, and Formalization” edited by Michael Detlefsen) — this argument claims to show that induction is impredicative.  Impredicativity, as many QA9 readers well know, is the property of a definition D of some mathematical object x that D refers to some collection or totality of which x is a member.  Philosophical constructivists must reject impredicative definitions, because they believe that the definition are constructing or creating the entities defined, and hence cannot presuppose that those entities already exist in the course of defining them.  This kind of philosophical constructivism must be distinguished from a kind of formal constructivism a type theorist is likely to care about, which I identify with a canonical forms property: every inhabitant of a type A should have a canonical form which is part of the essential nature of type A.  Computational classical type theory violates this formal canonicity property, because types like A \vee \neg A are inhabited by terms which are neither left nor right injections.

Here is Parsons’s argument as I understand (or maybe extrapolate?) it.  A philosophical constructivist must reject impredicative definitions, such as the kind one gives for the natural numbers in second-order logic (see my talk slides for this example definition).  As an alternative, one may try to say that the meaning of the natural number type is determined by introduction and elimination rules (similarly to the meanings of logical connectives).  The introduction rules are about the constructors of the type.  And the elimination rule is an induction principle for the type.  But then, Parsons and Dummett point out, this explanation of the natural number (or other) inductive type is not any better off with respect to impredicativity than the second-order definition, because the induction principle allows us to prove any property P of n, assuming as premises that Nat n holds and that the base and step cases of induction are satisfied for P.  But the predicate P could just as well be Nat itself, or some formula which quantifies over Nat.  The latter seems to provoke worries, which I do not understand.  It seems already bad enough that P could be Nat.  So just moving from a single formula defining Nat to a schematic rule defining Nat cannot save one from the charge of impredicativity.  Hence, for avoiding impredicativity, there is no reason to prefer one approach (specifically, the rule-based approach) over the other.

The alternative to this is to reject the idea that we must give a foundational explanation of the natural-number type (or predicate).  We just accept the idea of numbers and other datatypes as given, and then induction is a consequence — not part of some definition of numbers, which we are refusing to give.  This is a coherent way to avoid impredicativity, but at the cost of having to accept numbers with no deeper analysis — something that a logicist might not like, for example (though I do not know for sure how a logicist would likely view this situation).

In our seminar for the Computational Logic Group at Iowa, we have been studying Logic Programming for the past couple semesters.  We are continuing this semester, and have been reading “The Stable Model Semantics for Logic Programming” by Gelfond and Lifschitz (available on Citeseer here), which is a classic paper describing a semantics for logic programs with negation.  I was interested to read this paper, as I am interested in datatypes in type theory and programming languages with negative occurrences (in the types of the constructors) of the type being defined.  I am hoping that maybe some ideas from LP could possibly carry over to semantics for such datatypes.  This is intellectually a bit of a longshot, but the paper is quite nice reading for anyone interested in computational logic.

Anyway, I want to record here a few notes from the discussion this past Friday, of Alain Mebsout, Nestan Tsiskaridze, Ruoyu Zhang, Baoluo Meng, and myself. First, some background from the paper.  A clause is an implication where there is a conjunction, possibly empty, of literals (either atomic formulas or negated atomic formulas) in the antecedent of the implication, and a single atomic formula as the consequent.  The authors work just with ground (i.e., variable-free) clauses, since a set of nonground clauses can be modeled as the (possibly infinite) set of all its ground instances.  A program Pi is a set of clauses.  The authors define an operation which I will denote here Pi/M, where M is a set of atomic formulas.  The operation drops “not A” from the formula for every atom A which is not in M.  And it drops every clause that contains “not A” (in the antecedent) where A is in M.  The intuition is that we can pretend M is exactly the set of atoms we know to be true, and then simplify the clauses of Pi by looking at negated literals.  If you negate an atom which is in M, then you are negating something which we are pretending is true, and hence the negation is definitely false.  A clause containing such a literal is satisfied if we view M as determining a model (namely, the term model where exactly the atoms in M are made true by the interpretations of the predicates used in the atoms).  So those clauses do not add any further information and can be dropped.  From an operational perspective, such clauses would give rise to unsatisfiable (in M) subgoals, and so cannot possibly help to prove anything.  Similarly, if a clause contains “not A” where A is not in M, then the literal “not A” is true in M, and hence cannot contribute anything as an antecedent of an implication.  So that is why it is dropped from the clause.

If after performing this simplification the minimal set of atoms satisfying Pi is exactly M, then M is called a stable set for Pi.  If we suppose the atoms in M are exactly the true ones and simplify away all negated literals, then the resulting formula’s minimal model is again M.  So our assumed knowledge M is consistent with what we can deduce from it from the program.  The paper gives examples of programs which have no stable sets, and which have more than one minimal stable set (i.e., a stable set none of whose subsets is stable).

On Friday, we worked through the proof of Theorem 1 of the paper, which states that if M is a stable set of Pi, then it is also a minimal model of Pi.  This led us to consider a pair of propositions (which we did not take from the paper).  Suppose M is a stable set of Pi, and suppose M’ is another set of atoms.

Proposition 1: if M’ satisfies Pi/M, then M’ satisfies Pi.

Proposition 2: if M’ satisfies Pi, then M’ satisfies Pi/M.

We delighted ourselves by managing to refute Proposition 2 and prove Proposition 1.  For the refutation: a counterexample is if M is { p }, M’ is { q }, and Pi is {“p if not q”}.  Pi/M is then just { p }, since we will drop the “not q” from the antecedent of “p if not q”.  So M is stable, since the minimal model of Pi/M is M.  M’ does satisfy Pi, because by making q true, M’ makes “p if not q” vacuously true (since “not q” is false).  But M’ does not satisfy Pi/M, since it does not make “p” true.

For the proof of Proposition 1, we considered an arbitrary clause “A if As and not Bs” in Pi (where I am writing As for a vector of atoms and “not Bs” for a vector of negated atoms Bs).  Suppose that clause does not have a corresponding one in Pi/M.  This means that some Bi must be in M, since the operation Pi/M drops a clause if it contains a literal “not B” where B is in M.  Since M is a stable model, Pi/M must entail Bi.  If not, M would not contain Bi.  Since M’ satisfies Pi/M by assumption for Proposition 2, this means Bi is also in M’, and hence M’ also satisfies the clause we are considering from Pi.

Now suppose that the clause “A if As and not Bs” from Pi does have a corresponding clause in Pi/M.  The clause in Pi/M must be just “A if As”, since the transformation which retains a clause going from Pi to Pi/M just drops all negated literals from the clause.  Since M’ satisfies Pi/M by assumption, it satisfies this clause “A if As”.  Weakening the antecedent by conjoining in some more literals cannot change that fact. So M’ satisfies the original clause “A if As and not Bs” from Pi.  So M’ satisfies every clause in Pi, as required by Proposition 2.

Most QA9 readers will know the nonconstructive proof that there are two irrational numbers a and b such that a to the power b is rational.  There is interesting discussion about this here.  I recently came across a 2014 note by Roger Hindley about the history of how this example came to be more broadly known.  It is interesting reading.  Hindley credits a 1953 paper by Dov Jarden in Scripta Mathematica (volume 19, page 229) with the proof.  In case you do not have access to this journal in a local library, I have decided to include a scanned copy of the article below:

dov-jarden-1953

It’s a Math tweet from 1953.