This chapter currently has three sections. (It used to have four, but now it has three.) I've decided to rearrange the discussion to freeform rough chronological order so I don't have to move things to a different page when I rearrange the draft. If you have comments about any section, solutions to any of the exercises, or requests for something to add, please them to this page.
The chapter contains three sections:
(Add Comments/Solutions Here. See the Advice for Typing Proofs.)
-----(3) --- (1)
A -> B A
------(2) --------------- [->E]
B -> A B
---------------------- [->E]
A
-------- [->I,1]
A -> A
------------------ [->I,2]
(B->A) -> (A->A)
------------------------------- [->I,3]
(A->B) -> ((B->A) -> (A->A))The formula has a linear proof. — Greg
It also has a non-linear proof, using two vacuous discharges.
--- (1)
A
-------- [->I,1]
A -> A
---------------- [->,2] (vacuous discharge)
(B->A) -> (A->A)
---------------------------- [->,3] (vacuous discharge)
(A->B) -> ((B->A) -> (A->A))This seems to me to be a very different kind of proof. Can you see why I think that? — Greg 2005-03-02 05:25 UTC
(Add any requests for this chapter here, if they don't fit in the other sections. If you start a paragraph with 'TODO' followed by a colon, then it will appear on my search for things I need to do with the text.)
You can go back to the Outline of PnC, or to the main page for the book: Proof and Counterexample.
When you add yours, please date your entry, and — if you like — sign your entry so we know to whom we owe thanks.
The easiest way to sign is to simply write a string of four "plus" symbols — like this ++++ — and make sure that the "Username" field of the form contains your name. The string will be converted to your name and a datestamp.
Mar 1, 2005
Page 8, end of first paragraph. Missing "not"? "I will feel free to use expressions such as […] even though they are, strictly speaking, in FORMULA."
Mar 2, 2005
Page 8, first paragraph in the margin, it says "If you like you can think of them has…" — Olaf
(I notice that we're coming from significantly different timezones. I've added the signature extension, so we can have timestamped comments with a uniform timestamp. Insert ‘++++’ (without the curly quotes) and it will be replaced by your username and a UTC timestamp.)
Mar 3, 2005
Page 11, the paragraph beginning "I have been intentionally unspecific …" has two instances of [→ E] that should be [→ I], and the second offset proof on the page also has [→ E,1] instead of [→ I,1]. — David Scarratt 2005-03-03 02:44 UTC
Mar 3, 2005
Page 12, line -8, another [→ E] for [→ I]. — David Scarratt 2005-03-03 06:08 UTC
Mar 4, 2005
Page 13, line -4, "An counterexample". — David Scarratt 2005-03-04 04:38 UTC
Mar 5, 2005
Page 14, paragraph 2, line 5 thereof; should 'deleted' be 'discharged'? — Olaf 2005-03-05 01:48 UTC
Mar 7, 2005
Ch. 2, Exercises, Q.1, iii. Formula is missing ")" parenthesis, on the end.
Not too sure about the next one, but p.15, Example 2.9 [A simple valuation], last line thereof: "0 + 0 = 0 …". Should it not be "0 * 0 = 0", as we have not set a * b = a + b ? — Olaf 2005-03-07 08:52 UTC
Mar 9, 2005
page 16, proof of lemma 2.11, lines 6-7 of proof " Take any c E P where c |⊢ A. We wish to show that ( a * b ) * c |⊢ A → B … " The way that I understood the proof, we want to show ( a * b ) * c |⊢ B , and not the conditional formula… I hope I am not making a monkey of myself
also, one that Kate picked up on p.15, line before Example 2.9. Is the turnstyle-y thingo meant to be ' |⊢ ' rather than ' |= ' ? … sorry Kate if you think I'm trying to steal your brownie points :) — Olaf 2005-03-09 03:45 UTC and Kate by proxy
Greg, I think I would find a slightly longer or more detailed explanation of the notion of "points" quite helpful in this section; or perhaps a reference to another text that deals with it more explicitly? — Olaf 2005-03-09 03:48 UTC
Mar 11, 2005
page 13, definition of "finite multiset". "the members may be present any finite number of times" You mean to say that the number of times each member is present is a natural number (or counting number, in your words). Otherwise I would like to have a multiset with an element that is present π (or \sqrt{-1}) times! No one would be confused with the present wording, but it doesn't seem (to me) quite right to drop to such a level of informality here.
After that you start omitting the word "finite" and talk about "multisets". Perhaps you had better make it explicit that when you say "multiset" you always mean "finite multiset".
The definition in the margin as a function is my preferred definition (being a computer scientist), but here we come up against this ambiguity - you say "you can also define a multiset" but do you mean to give an alternative definition of "finite multiset"? If so, you have to include an extra clause of the form "where f(A) is non-zero for only a finite number of A \in FORMULA". — Richard Walker 2005-03-11 04:14 UTC
Mar 12, 2005
This is definitely the clearest treatment of discharge I've seen yet: the formal notation gives excellent intuition without cluttering the proof-trees. (I'm hoping it carries over to proofs by contradiction, too.) However, I did find the margin-note next to definition 2.2 ("Now is a good time to try some of the exercises") a bit jarring; because I eagerly turned to do so, only to find that the material covered up to that point only allowed half of Question 1 to be done (ignoring the request for counterexamples). Tentative suggestion: why not split Q1 into two questions, the first giving the list of theorems to be proven, and the second asking for counterexamples? Or put the suggestion a bit later. — Benet 2005-03-12 04:42 UTC
Mar 14, 2005
As I work through this section, I'm wondering how much mathematical maturity is expected/assumed from the reader and/or student. If this is a first exposure to logic, it may also be a first exposure to the concept of induction on structure: so, particularly in Lemma 2.11 (Preservation for Conditionals), I was thinking that making some of the steps more explicit might be easier on the student, especially since this is the first non-obvious result in the book, and quite algebraic. For instance, both times when Definition 2.8 is used (before "Take any c \in P" and after "since a |⊢ A->B"), I think a brief reminder to look back to the definition would help. As to the placement, I actually think having models and counterexamples this early – immediately on the heels of defining proof – is good, unless it means having to slow down the presentation too much.
Two more very small points: these are things that might be pitfalls for readers who are more familiar with mathematics and mathematical logic. 1) It is a little bit jarring that little 'p' ranges over atoms, not over elements of big 'P'. I can't think of an ideal solution: P is the best name for the set of points, but p,q,r,.. are the traditional symbols for propositional atoms. But thought I'd make a note of it. 2) It's easy for someone used to classical model theory to keep forgetting that |⊢ is a relation on atoms and points, not a function from atoms to points. Maybe emphasize this a little bit more? — Benet 2005-03-14 00:49 UTC
Added Mar 19th, 2005 — I guess fewer things are obvious to me; I didn't think that theorem 2.7 was all that obvious. It's also a proof by induction, (isn't it?) I think novice readers may balk at "Since pi' is normal, we may assume that every formula in pi' is in sf(x, B)." I was wondering if you could change the structure of the proof so that what you are proving is that a first step containing a formula not in sf(X, A) can't be introduced through [->I] or [->E] (and of course trivially it won't be an premise.) Since every step is a premise, or the result of one of those rules, that means there's no first step containing a formula not in sf(X,A), and of course, if there were any, there would be a first one, so it follows that all the steps are such that the formulas are in sf(X,A). Maybe this is still inductive in a sense, but I think it's much more intutive for people who haven't been taught induction explicitly. (An alternative might be Graham's strategy from An Introduction to Non-classical Logic; you could explain induction in an appendix (or the introduction) and refer beginners to that when you give the first few proofs by induction.) I think it's really difficult (maybe too difficult, I don't know) and admirable to try to make the book accessible to beginners; there are so many books that start out well and then give up around page 10. — Gillian Russell 2005-03-19 19:34 UTC
Mar 16, 2005
At this point I restructured the chapter, cutting out the section on models and moving that into [PnC Chapter 4]?. — Greg 2005-03-15 14:10 UTC
Mar 16, 2005
2.3 (not sure what it is in the new version) Normal Proofs, first paragraph: "Some proofs are quite strange. Take a proof concludes with…"
and also, paragraph before Def. 2.22 [Complexity], (p.23 Old version of text): "we must will some other measure that decreases…"
paragraph after Def. 2.23 [Non-normality] (p.24 old version): "Non-normality measures are satisfy the…"
Greg, are you still interested in typo checks, seeing as you are restructuring and rewriting the chapter? — Olaf 2005-03-16 04:09 UTC
Mar 18, 2005
Hi Greg, LOVE the aims for the book, and LOVE what I've read so far. Here are a couple of comments to add to the mix:
P.8 "logic is an account of general principles of valid reasoning." If this is what you think, then it's what the book should say. But it's not what I think, and so I was wondering, is it really what you think? (For the reasons I gave at the end of the Goldfarb review.)
P.13 I found the finite multiset definition confusing. The first sentence is "A finite multiset of objects is a finite collection of those objects in which the members may be present any finite number of times." One natural way to read that is as saying that an element might be a member at one time (say, 5pm) but not be a member at a later time, but maybe be a member at a later time again (in which case it would be present twice). But at any one time they are either a member or not a member. On that reading I am a member of a multiset a finite number of times in the same sense as I visit your website a finite number of times. But on the intended reading I am a member of a multiset a finite number of times in the same sense as the letter "l" appears in "Philadelphia" a finite number of times. I know what a multiset is and I still read the first sentence the first way; I wondered whether this might be some new kind of multiset … A reader who doesn't have any idea what one is could be mislead here and that would be the first really frustrating experience in the book…I think it should be either somehow rephrased, or you could put in one of those little side notes pointing out the two possible readings and identifying the right one. — Gillian Russell 2005-03-19 06:35 UTC
OK, sorry, I'll remember the distiction in future. — Gillian Russell 2005-03-19 19:00 UTC
Mar 19, 2005
P. 15, final complete paragraph, "conjuring new arguments out of thin air" — of course we get new arguments underwritten by proofs when we introduce the conditional rules; we didn't have any rules before, so we couldn't have any proofs with steps in them. Isn't this getting new arguments out of thin air? But the conditional rules are ok, right? I'm being flatfooted here, but I also don't know what the strictly correct way to put this is.
P. 15, "if the conditional is defined by way of these rules, …" — one thing I've learned from the comments on my weblog is that not everyone gets the intuitive pull to think of the rules as defining the connective, or at least, they don't get it straight away without any explanation. I think this is the first time you've mentioned it; my hunch is that some readers will be puzzling over this antecedent unless you say more.
P. 16, definition of subformulas is very clear.
— Gillian Russell 2005-03-19 19:00 UTC
Mar 19, 2005
I took a quick peek at this chapter, and besides being quite intrigued and impressed, I had one small comment to make. On page 15 of your March 16th, 2005 draft, you use the term "critical pair" to refer to a detour in a proof, where a use of an introduction rule for a connective is followed by a use of the connective's elimination rule. In term rewriting theory, "critical pair" has a special meaning. Since term rewriting theory overlaps a bit with applied proof theory, I was wondering if you were intending to use "critical pair" here with the same meaning, or whether perhaps it was an accidental namespace clash. A quick description of the meaning in term rewriting is here (or see something like page 562 and following of the Rewriting Chapter of the Handbook of Automated Reasoning for a more detailed discussion). — Aaron Stump 2005-03-19 18:36 UTC
Further to Gillian's comment about P.8 "logic is an account of general principles of valid reasoning.", maybe a footnote summarising a range of suggested definitions would be in order to put your approach in context? FYI, the first chapter of my DPhil begins Logic is the study of arguments correct in virtue of its form. which serves as a sort of announcement of hostilities against the Tarskian view of logic. — Charles Stewart
Mar 20, 2005
Greg, I'm wondering about the relation between premises and assumptions. Section 2.1 seems to draw the distinction that proofs have assumptions, and arguments have premises; the relation being that X (therefore) A is a valid argument iff there exists some valid proof from X to A. Section 2.1 also seems to state (or at least suggest strongly) that whether in an argument or proof, the set X (resp. premises and assumptions), contains only un-discharged formulas. However, in Section 2.2 (top of p.15 in the current draft), the text speaks of a proof having "two instances of A in the premise list", and in the following figure both instances appear discharged. Furthermore, the illustration is a proof rather than an argument. (To make an even tinier quibble, if you plan later to distinguish between multisets of premises and lists, probably it's a little misleading to use list here.)
Now that I look back at the text, I note that the proof on page 11 of (A->B) states that A->(A->B) is the premise/assumption of the proof; but later, on page 13, it says ".. we have a linear proof from A->(A->B),A,A to B, but.. [no linear proof] from A->(A->B),A to B." If only undischarged assumptions ever appear in either the premise multiset or assumption multiset, I'm not quite sure I see how this distinction can be drawn, because if all the A's are discharged none can actually appear in the premise multiset under the given definition. I am quite sure that I'm missing some subtle – or, indeed, some basic – point, and my only justification for going on about it at such length is that I imagine it would be very possible for a student new to logic to miss it too. — Benet 2005-03-21 02:15 UTC
A -> (A -> B) A
-----------------
A -> B A
---------------
B --- 1
A -> (A -> B) A
-----------------
A -> B A
---------------
B
------- [->I,1]
A -> B --- 1
A -> (A -> B) A
----------------- --- 2
A -> B A
-----------------
B
------- [->I,1]
A -> B
------------- [->I,2]
A -> (A -> B)Greg, thanks for the response. It clarified a lot of my puzzlement. I think I still have some questions related to discharge and book-keeping; but I understand now how you are distinguishing between single and multiple discharge. I'm going to let these questions simmer on a back-burner for a couple more drafts and see if they are either resolved by the continuing development, or if I can put them in a concise form. — Benet 2005-03-27 05:54 UTC
Mar 21, 2005
"modest super multi-sets" — here's the most conservative suggestion I can think of: just abbreviate "multiset" to "m-set" or "mset". Admittedly, "modest super m-set" is only one syllable shorter, but "proper superset" is only one syllable shorter again and that standard piece of terminology is fine because in practice we normally talk in terms of the subset relation rather than the superset one. In practice we might end up doing the same here: y is a modest submset of x" (read: "y is a modest sub-m-set of x") rather than "x is a modest super multiset of y." (If you don't mind the idea of slightly less conservative you might decide to write "sumset" for "sub-multiset" (wheras the less-used "supermset" wouldn't be shortened.) — Gillian Russell 2005-03-21 23:51 UTC
I like it - at least as a definition of modest super multiset; but as replacement terminology (which is what you seemed to be asking for on P. 18) isn't it a bit, erm,…long? (Of course I understand about not wanting to abbreviate 'multiset'—fair enough.) — Gillian Russell 2005-03-24 10:29 UTC
Do all multisets have the same ground? (Everything's a member to some degree, possibly zero?) — Gillian Russell 2005-03-24 22:47 UTC
I'm not sure whether it would reduce or promote confusion, but 'bag' is another standard term for multiset. 'Modest super-bag' has its own problems, but has fewer syllables at least. Is 'ground' standard? I'm more familiar with 'support' as the term for those elements of the universe of discourse that have non-zero presence in a multiset (or other set generalization). (Speaking of multisets, I just wanted to introduce another teensy notational question: if you are using \box for the empty multiset, is there a possibility that will introduce confusion when you get to the later part of the book and use \box as a modal operator?) — Benet 2005-03-25 21:12 UTC
April 3, 2005
Hello, I've been reading the printing of Mar 23, and had some comments. It's very interesting to track the progress of a book; thanks for making this visible. After Chapters 2 and 3, I think I'm finally beginning to get to grips with normalization and the notion of cut; the chapters are exceptionally clear. Here's some feedback on which portions I got confused at, and some typos.
In the first pages 7 and 8 of Chapter 2, the relationship between a formula and a "conditional judgement" (the latter being described in the motivating para) is not explicitly stated, but left implicit. That is, it might make things a little clearer if there is a line somewhere stating, "Now, after setting up our formal language, we can express our notion of conditional judgement using a formula as follows …".
On page 17, in the proof of Thm 2.8, in the Introduction case, it seems that there's an implicit acceptance of the fact that a subproof of a normal proof is also normal. Perhaps that fact could be made more explicit, or even proved, somewhere close to where the notion of a normal proof is defined. Also, in the Elimination case, I think the variables X and Y were swapped midway through the para. Perhaps a marginal diagram might clarify the variables here.
In a few places, proofs of lemmas and theorems follow a page or more after they were stated. It might help searching for proofs if they were explicitly labelled, e.g. "Proof (Thm 2.10, relevant and standard case)".
In the descending sequence of non-normality measures in Example 2.14, the measure (1,3088) is not smaller than (138, 47).
— Prashanth Mundkur 2005-04-03 23:54 UTC