Speaker: Antoine Voizard Topic: Constructive Logic
SCW office hours: Wed morning 9-11AM Remember: project updates due 10/24
SCW: Bob states that preservation and progress hold, but I wanted to explore the details of the latter lemma. (Note: this is an unusual lemma to prove for logics; I've not seen it included in other papers on this topic.)
-
Canonical forms lemma: If p is canonical (i.e. not "ccr") and |- p : phi then from phi we know the structure of p
- |- p : True implies p is <>
- |- p : False is impossible
- |- p : phi1 /\ phi2 implies p is < p1, p2 >
- |- p : phi1 / phi2 implies p is either l . p1 or l . p2
- |- p : not phi implies p is not(k)
- |- p : phi1 -> phi2 implies p is \x. p2
If k is not "ccp" and |- k : phi then from phi we know the structure of k
- |- k : True is impossible
- |- k : False implies k is abort
- |- k : phi1 /\ phi2 implies k is either fst; k1 or snd; k2
- |- k : phi1 / phi2 implies k is case( k1; k2 )
- |- k : not phi implies k is not(p)
- |- k : phi1 -> phi2 implies k is ap(p1);k2
-
Progress lemma:
- Pick reduction system that favors (13.5h) (i.e. eager dynamics)
- if |- k # p then either k # p final or exists k' # p' s.t. k # p -> k' # p'.
Proof:
- suppose k # p is not final. Then either p is not canonical or k is not "halt phi". In the first case, then p must be ccr u. k' # p'. Then result steps by 13.5h. In the second case, p is canonical, but k is not halt. If k is ccp, then the term steps by (13.5g). Otherwise, we have |- k : phi and |- p : phi. For each form of type phi, we can use canonical forms to know more about k and p. The case when phi is True or False is impossible. Otherwise, in each case of phi, there is a rule in (13.5a)-(13.5f) that applies. Note: we didn't need to use induction in this part!
-
Why does this chapter rework everything? Why not just add classical axiom to constructive logic? Answer (in the form of a question): what is the computational content of that axiom?
What we have here: symmetry between truth and false
-
What are continuations? They are the context of evaluation?
-
This is the truly classical rule:
D,u :- phi G |- k # p ----------------------------- D G |- ccr (u. k # p) : phi -
Q: Why is "abort" called so? abort refutes that False is a theorem Proposal: maybe it should be called "done" instead
-
Note: there are no elimination forms in this calculus We only have introduction forms for refutations
We can think of "fst" as a continuation adapter --- takes a value of phi1 /\ phi2 to a value of type phi1.
-
Sums are dual to products. What is dual to functions?
-
A 'paradox' ? Things that are constructively valid need "ccr" to prove them.
Example from the book: |- p : A /\ (B /\ C) -> C /\ A
We cannot eliminate A /\ B without using ccr?
-
I didn't see elimination rules for ¬ in Chapter 13. How do we refute φ provided a proof of ¬φ?
[SCW: if we have |- p : ¬φ and we want a refutation k that shows |- k ÷ φ we can use k = ccp x. not (x) # p ]
-
So far I have been thinking of preservation as preservation on types as an expression transitions, however the theorem on preservation states:
If k ÷ phi, p : phi, and k # p |-> k' # p', then there exists phi' such that k' ÷ phi' and p' : phi'.
So I am unsure what we are preserving. The fact that we have a contradiction?
[SCW: Yes! That is exactly what we are preserving. We could restate the theorem without using phi and phi'.]
-
Progress in terms of programming languages makes sense but I don't think I get what it means for logics? What does not having progress for some logic look like?
[SCW: Progress is kinda strange for logic. It's a weak property in this context, so I'm not sure what we get from it.]
-
Section 13.2 begins like 'The price of achieving symmetry between truth and falsity in classical logic is that we must very often rely on the principle of indirect proof ... ' The examples presented henceforth all use indirect proofs. I am wondering whether there are non-trivial direct proofs (proof tree three or more layers deep) of interesting judgements in classical logic. That even judgements like 'a and b true => a true' require indirect proof shows that proof by contradiction is more prevalent than we might think.
[SCW: good question. But, what does nontrivial mean in this context? We do have direct proofs like this one:
\x.\y. l . <x,y> : A -> B -> (A /\ B) / C ]
-
What is a canonical proof? Does it mean that there is no refutation appearing in the proof?
[SCW: a canonical proof is one that is not headed by "ccr" (and there is an analogous definition for canonical refutation.) However, a canonical proof could have a contradiction inside of it, just not at the top level. A canonical proof could even have refutation inside it, if it is headed by "not". ]
-
How to correspond classical to proofs? The book says it is an abstract machine with a control stack. Could you give an example that? And could you further clarify the penalty of that?
[SCW: See chapter 28. I think Bob must have reordered things, because there are some strange forward references.]
-
When I see the first example in 13.2, I spend a lot of time trying to construct the refutation. Is there an algorithm to build indirect proof?
[SCW: An algorithm to build a proof would be a theorem prover. There is some work on polarity and focussing to structure the proof search --- ask Jennifer for details.]
-
Near the start of Section 13.2, Bob makes the point that "this proof cannot be expressed in classical logic, because classical logic lacks the elimination forms of constructive logic" I don't quite understand this point - isn't this a problem with the formalism Bob has chosen, rather than classical logic itself?
[SCW: Hmm. Yes, and no. The formalism that Bob has chosen has its own intrinsic value based on its symmetry and minimalism. So observations about this formalism are interesting. However, you are right that Bob could have picked a different formalism to start with (for example, Parigot's lambda-mu calculus) that looks more like lambda-calculus. However, then there would be a different set of issues.]
-
What does the preservation law and progress law mean for the proof dynamics defined in 13.3? Also, I would appreciate it if you can elaborate on the correspondence between classical proofs, and the interactions between expressions and context in programming.
[SCW: Good question about proof dynamics. Preservation and progress are really weak properties from a logical point of view --- they don't show the consistency of the system. For connection with programming, see Chapter 28.]
-
I'm trying to think of how the evaluation dynamics fit, especially with the claim of the "proof changing its mind" after being "caught in its lie", and of no longer needing to reveal which disjunct it proves. The whole set-up strongly suggests an interactive game, but I'm not sure how it fits with the evaluation dynamics.
If I am to take a stab at understanding this situation, it is suggested that there are two parties, the Prover and the Context. I think of the Prover's job as having to prove the claim, of course, but also that the Context's job as having to refute the claim. Initially, they both pretend to have the proof and refutation respectively, and the idea is that that they both want to keep these secret. However, it is Prover's bad luck to have to start first, and to exhibit his proof term.
The game state is k#p, where k is the Context's refutation and p is the Prover's proof term. Both are always held abstract (secret), and the point of the proof tree is to refine this term and show that it is indeed concrete. When Prover gets stuck, he/she can challenge Context by saying that if the refutation exists, then some P is true. This is invoked as ccr(u. k#p), where the Prover proves p using the "current refutation". But this proof is conditional on the Refuter's possession of u. Not wanting to be "caught in its lie", the Refuter must go on to refute P instead, by producing a refutation k. Now the burden of "proof" falls on the Refuter, who gets to play forth in a symmetric fashion. The Refuter's moves, as such, correspond to elimination forms of the syntax (specifying how to refute); and the Prover's moves correspond to introduction forms. They also nicely get to exchange proofs and refutations when there is a not. The game ends when the Prover fully exhibits the proof term.
This looks like a plausible story which would explain the book's comments partially, but perhaps not faithfully. It presents a nice symmetry between truth and falsity. "Not having to reveal which disjunct it proves" can be explained as throwing the challenge back to the Refuter, who must now instead refute the Prover-chosen disjunct. "Not waiting to be caught in its lie" now applies to both Prover and Refuter.
But the proof dynamics, while preserving this contradiction and tension between the Prover and the Refuter, does not start off with the Prover's state being abstract; it is fully concrete instead. I tried to graft the Refuter's side of the story onto the proof tree, but I'm not precisely sure of how. I also could see alternative ways of casting the whole thing as a game as such, e.g. Prover and Refuter working together to prove the goal, but the above seemed the most satisfying.
So a long story, I'm not fully understanding the proof dynamics and what the transition system really is. The transition system as presented only simplifies the interaction of the end result; e.g. for LEM, it starts with the concrete proof term on the right and the abstract refutation on the left, and then maintains the contradiction invariant. It seems to say something about the above sort of interaction that is taking place, but I have trouble fitting it completely. Is there a way to ascribe semantics to this so that the dynamics, the above sort of interaction, and the proof tree all come together?
I don't know if I have just read too much into his words and carried this imagination too far and in the wrong direction. But this perspective of game semantics is fascinating regardless, and I wonder where one can go from here.
In closing, (I believe) the law of excluded middle has a proof in the system simply by virtue of the contradiction semantics in the metatheory, rather than this concept of "lying"; because the rules of the game themselves allow one to hypothesize the existence of both proof and refutation right from the start, in the abstract secretive sense of above. Is this right?