rzach / forallx-yyc Goto Github PK

A missing qoutation sign at the very end ('B')

I hope you don't mind me reporting these minor typos! I think it is an interesting thing to have a book on github.

Please modify Appendix A to add "|"
as an alternative symbol for disjunction ("or"), both in the discussion about "or" and in
the following summary table.

This is used. For example, prover9 uses "|" for "or", "&" for "and", and so on,
as documented here:
https://www.cs.unm.edu/~mccune/prover9/manual/2009-11A/syntax.html

Thanks so much!

In 25.3, replace capital F with lowercase f in the pointwise continuous and uniformly continuous definitions.

In 31.1, spell check susbstitution.

In Chp 36, the language "provided provided" is used twice. It looks like this is a typo that got copy-pasted?

Chapter 9 specifies whether a binary connective (∧, ∨, →, ↔) is symmetrical or asymmetric. The Wikipedia page on Logical Connective lists Commutativity as a property of logical connectives and says that symmetry is a property of a binary relation.

Perhaps it is not a big deal, but what is more common for logical connectives -- commutativity or symmetry?

In Chp 33, an example uses "witness" to refer to (what I'd call) nodes on a diagram. This was not clear to me initially. Perhaps replace with "witness" with “see node” but if not NBD 👍.

Kindly please modify "Dodson" with "Dodgson", at page 408 (Glossary). The mistake is both in "forallxyyc" and "forallxyyc-f20"

hyperref doesn't produce PDF bookmarks in solutions/forallxsol.pdf for some reason

I haven't researched the literature to establish if postfix notation has been tried on TFL sentences. I have written about it here.

Summarily:

Compare, for instance, 𝒜ℬ𝒞∧∨ with 𝒜∨(ℬ∧𝒞). We can prove that the postfix notation can create unambiguous TFL Sentences (see below), but whether they will be readable is difficult to determine; it may also be subjective. Sometimes, however, I fancy thinking that postfix notation may serve the TFL Sentences well, once you get used to it.

Is it a good idea to make a passing reference to such a notation in TFL (§ 6.3)?

Chapter 32, Using interpretations, has no solutions in the solutions manual. Maybe that was an oversight in copying things over. Check original and Cambridge versions

• New cover
• Added chapters on modal logic, based on notes by Rob Trueman
• Changed syntax of FOL: Use F(x,y) instead of Fxy. Can be customized.
• Changed some notation: logical consistency is now satisfiability (and cognates), logical truths are now validities
• Fixed issue #15 and let sentence letters be atomic formulas
• Fixed issue #12 and defined satisfaction of a formula by an object, used this to define truth conditions for quantifiers

Spell check "contradition" in Chp 17.

Spell check "subroof" in Chp 18.

Spell check "apropriate" in Chp 42.

In Chp 43 the following sentence has an unmatched bracket, besides being otherwise hard to read:

In fact, we could have added rule R5 to T alone, and leave out rule R5)

In Chp 30, replace "just in case" with "if":

and stipulate that ‘R(x,y)’ is to hold of x and y just in case there is an arrow running from x to y in our diagram.

In §6.2, we formally define TFL sentence.

In the given inductive definition that constructs a TFL sentence, is "Nothing else is a sentence." needed? I doubt if it provides any constructive value. It is okay to use it for emphasis, but then it can be a part of exposition, not the definition.

Some text in the content is pink. If this is meant to communicate something (for example, that the term is a key term) that information needs to also provided in a way that doesn't rely on colour. This is for anyone who is colour blind or someone using a screen reader. For example, you could provide a list of key terms at the beginning or end of a chapter/part.

In 23.5 (“Quantifiers and Scope”), we find the pair:

15. Everyone is such that, if they are a bassist, then Lars is a bassist

and its FOL translation

[15-FOL:] ∀x(B(x) → B(l)) .

The English-sentence 15 is of course not really something anyone would say in ordinary conversation, outside a philosophy classroom. My students and I found it helpful, in thinking about what the symbolization 15-FOL actually means, to recognize that 15-FOL can be more naturally translated as “Lars is a bassist, if anyone is” or as “If anybody’s a bassist, Lars is.” (I think my students found this especially helpful, because Chapter 23 is an early-enough part of the textbook that students are still struggling to understand what basic FOL sentences are intuitively saying.)

Of course, this isn’t any kind of logical error in the text. I mention this only as a report of what my particular students found helpful in yesterday's discussion of this material. So the thought was that adding a sentence including this more idiomatic/ natural English translation of 15-FOL might be useful to some readers.

Note: Given the wider pedagogical goals of 23.5, I think it's 100% reasonable to keep 15 as it currently is, since its surface form is closer to the FOL sentence that the section wants to discuss. So I'm just suggesting that in the discussion of the FOL sentence, you could mention this other, more 'everyday' English sentence to help the students grasp the intuitive meaning.

While implementing the deductive system of both the Calgary and Cambridge for LogicPenguin (which is nearly complete), I noticed a couple oddities.

The Cambridge version lists a restriction on $∀I$ and $∃I$. It says that the variable introduced must not already occur in the statement generalized upon.

The Calgary (and Mangus's original) list no restriction at all.

Both are wrong if a quantifier with a certain variable within the scope of another quantifier with the same variable is allowed syntactically.

The Calgary version allows the inference from $∃xRxa$ to $∃x∃xRxx$, which, at least given the normal way of treating double-binding, is semantically equivalent to $∃xRxx$, which should not be provable from $∃xRxa$. (Just as an example, there are others.)

The Cambridge rule, however, is too restrictive, since it is impossible to prove something like $∀x(Fx → ∃xFx)$, which is semantically valid.

Looking at the Cambridge recursive syntactic formation rules for formulas of FOL, it looks like it disallows both vacuous binding and double binding, so maybe this isn't really a problem for it. (Though the restriction then seems redundant since the result wouldn't even be well-formed.)

However, the Calgary version needs some kind of fix. Either the syntactic rules have to change, or there needs to be a restriction on the rules, something like "c must not occur within the scope of a quantifier $∃x$ or $∀x$ already in $A(...c...c...)$."

• Rewrote 15.7 and 15.8 and combined into one section:
  • _|_I is now ~E, with order of premises reversed
  • _|_E is now called explosion (X)
  • Removed TND as a basic rule, and instead added indicrect proof (IP)
  • Renamed tertium non datur to excluded middle,TND to LEM
  • Added exercises 19.C-E

All six examples in 2.3 have this issue:

Either Mei is a mathematician or a botanist.

gives us as disjunctive alternatives a sentence and a noun, which have different grammatical functions.

per Chicago Manual of Style 5.244, for example:

Correlative conjunctions such as either–or, neither–nor, both–and, and not only–but also and some adverb pairs such as where–there, as–so, and if–then must join grammatically parallel sentence elements. It is a common error to mismatch elements framed by correlatives.

This can be fixed with the pattern

Either Mei is a mathematician or Mei is a botanist.

or the pattern

Mei is either a mathematician or a botanist.

Would you be receptive to a pull request for all the examples with one of these patterns?

Add alt text to the two images on the home page:

• Cover: Book cover for forall x: Calgary. An Introduction to Formal Logic.
  

• UofC logo: Logo for the University of Calgary Taylor Institute for Teaching and Learning.
  

First off, thank you for making this available on GH. It just helps!

I couldn't find an instruction in the book preface or the GH repo about how to submit errata. Can that be clarified somewhere (preferably the preface)? If sending a PR is the way to go, please clarify it here and close the issue. I will send a PR.

Some rules are repetitions of others. That makes memorising the rules harder. It also perhaps makes learning strategies for how to use the different rules harder. I've been trying to simplify the rules. That'll generally make proofs using them one line longer, but I don't think any more difficult.

• rule for biconditional can be simplified to simply allow moving between the biconditional and the conjunction of the two conditionals. Then rules for conditionals can be applied.
• rule TND by Law of Excluded middle: you can always write Av¬A.

I've already edited this in my version, but that's not up on GitHub because I haven't properly worked out how to use GitHub. https://uob-my.sharepoint.com/personal/cc15682_bristol_ac_uk/_layouts/15/guestaccess.aspx?docid=0ed0ef9e829a14fcebcc7b253346a8d66&authkey=ATuzcf6W48MgwwLACcjyjYM&expiration=2017-12-01T00%3a00%3a00.000Z

Someone who navigates with a keyboard can use the [Tab] key to navigate between links and buttons on the webpage. As such, there needs to be visual focus indicators when tabbing through the site so they can see where they are on the page. When I tab through the site, I can only see the focus indicators when I tab through the links in the content. I do not see focus indicators when tabbing through the table of contents side menu or the next/previous arrows. And I see only faint indicators when tabbing through the four top-menu buttons.

The sketch of the soundness proof at the end of Ch 21 is confusing and not quite correct. Rewrite it or take it out (since we have the complete soundness proof).

This observation pertains to content clarification and it could be subjective. Filing it as an issue according to the emerging guidance from #65.

I am studying from revision 79af9e0.

§3.1 is on Joint Possibility. It refers to whether given "sentences" are jointly possible.

It seems to me that if given sentences are premises of an argument, it can only be valid if the premises are jointly possible.

Should §3.1 end with a comment reflecting the above, or is it too obvious?

On ch. 17, "constructing proofs", pg. 130, practice exercises, in C.5 i think there is a typo,

(A or ~B) -> (A -> B) is not a tautology (check for instance here). It would have been, for instance, if the outermost consequent were reversed, to B -> A, having

(A or ~B) -> (B -> A)

version 2cf987e (2020-08-07)

btw, thanks for all this effort.

Add material on implicature and explain exclusive or, unless, if-then, existential import weirdness using it.

When discussing the scope of subproofs -
It is stated and explained
"Any rule whose citation requires mentioning individual lines can mention any earlier lines, except for those lines which occur within a closed subproof."
Examples are given of citing lines that are within a subproof from outside a subproof, and called 'naughty'.
However, when using the Conditional Introduction Rule, while 'discharging' a subproof, that line clearly cites lines from within the subproof.
There is no mention of why this is allowed in those circumstances - especially since the Conditional Introduction Rule is not formulated with regard to a subproof (contrast to this definition in SL from "The Logic Book" by Bergmann et al:)

Whereas in our book, it defines the Conditional Introduction Rule all within one scope.
Perhaps this should be addressed somehow?
(I am only a beginning student of logic, not an expert, but this seems unclear to me).

Via email, I said:

Mainly the problem here is that the text calls '\bot Introduction' the rule that I think of as '\neg Elimination'; there is no '\neg Elimination' rule. This breaks the nice symmetry of having two I/E rules which define each connective. I also gave students a problem about explaining why we can define '\neg P' as 'P \eif \bot'. This problem would make more sense if the insight they were expected to get was: the I/E rules for negation just become instances of the rules for the conditional.

Richard Zach said:

I agree. This shouldn't be too hard to fix: rename all the rules in
existing proofs, and rewrite 15.7 and 15.8 (probably also: reverse them)?

(I'm also not sure about using the TND rule as opposed to the classical
absurdity rule.)

There is no clear statement (inductive definition) of formulas and sentences of FOL.

In the chapter you first introduce scoped quantifiers in such style:

∃x(Fx ∧ Dx)

Yet discuss scope at the very end of the chapter, which is a bit confusing. If anything, it would make more sense to do this the other way around.

LaTeXML 0.8.7 times out on expl8 brucemiller/LaTeXML#2064 which is needed by glossaries. When that's fixed we can try to compile the glossary to HTML.

Typose reported by Daniel Hill (Liverpool):

p. 208 6 lines up. You are discussing 'if x is a bassist, then Lars is a bassist'. You write 'This sentence is false; Kim Deal is a bassist'. The semi-colon here makes it seem that you think that 'Kim Deal is a bassist' implies the falsity of 'if x is a bassist then Lars is a bassist'. You need a full stop rather than a semi-colon.

p. 216 'lots the difference' for 'lost the difference'

p. 217, line 4 closing inverted comma missing after 'k'.

p. 217, 4 lines up -- 'a love triangle' is not defined as one might think. A love triangle obtains when two rivals love a third person. I am not sure whether the third party has to reciprocate, but I think that they do, which means that your sentence is correct, but your explanation of it in the next two sentences is overkill.

The website title associated with every HTML page (used in e.g. auto-generated bookmarks and the presentation of the website in search engines) seems to have been auto-generated in an incorrect or at least non-ideal way. For example: Chapter 12 Semantic concepts ‣ Part III Truth tables ‣ forall x: Calgary. An Introduction to Formal Logic‣ Part III Truth tables ‣ forall x: Calgary. An Introduction to Formal Logic.

Should also cover functions, and mathematical examples (eg language of arithmetic)

Add material to cover structural ambiguity and how to disambiguate in TFL and FOL.

Not all rule labels are produced by macros, and the style file has two sets for them. Make that uniform.

Also as suggested in #11 by @catrincm, avoid Latin. ECQ is Explosion, TND law of excluded middle.

Allow zero-place predicates (these would naturally symbolize sentences like "it's raining"). It somehow seems more elegant to me if FOL keeps everything from TFL but just allows for more logical structure to be revealed. I don't think this would require many changes. The syntax in 26.2 is already consistent with it. For the semantics, you could just have interpretations include valuations. Maybe this makes the notion of an interpretation a bit less natural, though...

The next and previous arrows do not have a high enough colour contrast, so people may not see them. I would recommend that they be at least #565353

In 12.5 example 2 the book provides "Jan is neither bold, nor not-bold" as a limit to validity tests using TFL.

The problem described is that a possible symbolization would be: $'\neg J \wedge \neg \neg J'$ which is a contradiction.
It is explained that we could have added "Jan is on the borderline of boldness" and that is why the original sentence is possible.

Does this not mean that our symbolization was faulty to begin with? True, "Jan is bold" would probably be symbolized as some sentence letter, say 'J', but since in reality the phrase "not-bold" is not the complement of "bold", is it not a mistake to symbolize it as $'\neg J'$ to begin with? Shouldn't we have added at least one more sentence letter for "not-bold", say 'N', and get the following symbolization: $'\neg J \wedge \neg N'$ which is not a contradiction?

Now, if this example comes to show that misuse of TFL can bring us faulty test results, it is, of course, true, but it is not a limit of TFL specifically but of any possible logic language, existing or hypothetical. Wouldn't it be clearer to mention that this is a limitation that is not unique to TFL?

• Test on JAWS
• Test on NVDA
• Test on NaturalReader
• Provide recommendations for custom dictionaries ('iff')
• Check image descriptions on SVG images
• Figure out best way to load MathJax with maximal a11y support and minimal clutter

From Dirk Schlimm:

One thing that occurred to me is that the definitions are in a box, but that they still don’t stand out as much as they could. From math education research I’ve learned that especially beginners need to be taught to focus on definitions and that highlighting them can be of help for this.

Here’s an idea that I had. In forallx-yyc.sty the \factoidbox command could be redefined as follows:

\usepackage{tcolorbox}

\renewcommand{\factoidbox}[1]{\par{\centering\begin{tcolorbox}[width=.9\textwidth,colback={vltleadbeater},colbacktitle=yellow,coltitle=blue]   
#1
\end{tcolorbox}\par}}

For this to work the background color needs to be added in forallx-yyc.tex as:

\colorlet{vltleadbeater}{darkred!10}

Seems to be an error here ("Consider: Consider:"):

The truth conditions of "except" are given as the same as for "other than". But "except" is not a case of perfection, "Exeryone except Pavel" should be symbolized as Ax(~x = p <-> ...) not as Ax(x=p -> ...)`

Via email, I said:

I like that the book uses a substitutional approach rather than dealing with assignment functions. But I am finding that, as things are set up in the text, this doesn't actually buy much in terms of simplifying semantic reasoning about quantifiers, because we don't assume that every object has a name. (Compare the approach in Forbes' "Modern Logic", which just uses straight substitutional clauses for the quantifiers, because he adopts an 'alphabetic convention' that ensures every object has a name.) The net result is that when you apply the book's clauses for the quantifiers, you end up quantifying over additional interpretations in the metalanguage, rather than objects in the original interpretation, and this makes the reasoning a bit clumsy and, I think, more opaque to students.

The approach I think I've settled on for teaching this to the students next week is to keep the basic substitutional approach, but introduce a notation that makes what it means to 'extend' an interpretation a bit more obvious, and use this in the semantic clauses for the quantifiers, like

'\exists x F(...x...)' is true is an interpretation M iff: for some object \delta in the domain of M, 'F(...d...)' is true in M[d: \delta]

'\forall x F(...x...)' is true is an interpretation M iff: for every object \delta in the domain of M, 'F(...d...)' is true in M[d: \delta]

This avoids talking about assignment functions but still quantifies over the objects in the domain of M in the metalanguage, rather than over alternative interpretations M'.

Richard Zach said:

This also should not be too hard. Changes only required in 28.3, 30
passim, and 31.

An alternative would be to define what it means for an object in the
domain to satisfy a formula with a free variable (\delta satisfies A(x)
iff M[d:\delta] |= A(d)) in 28.3. From then on you can just talk about
satisfaction.

Talking about satisfaction also makes it easier to talk about expressive
power, which I'd like to do at some point. That is, I'd like to add a
section about the extensions of formulas and not just of predicates,
e.g., A(x) has as extension {\alpha : \alpha satisfies A(x)} (etc for
more than one variable).

The instructions say to clone the repo and LaTeX the book. But no matter which command I use to LaTeX it, I get no further than
! Undefined control sequence.
l.4 \Language
{en-US}

How exactly do I build the book?

0f8bdb6

Previously, the notions of extension and of stipulating an extension
were used in section 27.1, before the notion of extension was
introduced in section 27.2. This change defines an extension before
introducing the notion of an extensional language.

This is a stopgap. Probably a bigger change is ultimately called for
here: the notion of an extension and the sense in which FOL is an
extensional language should be explained before the symbolising
vs. translating discussion, not within that section.

Already put in effort to make the book easily readable, but dyslexics would benefit from additional things (typeface, line and letter spacing, type size etc). Make an accessible version.

• https://open.bccampus.ca/2017/03/08/lessons-learned-in-accessibility-through-the-bc-open-textbook-project/
• http://dyslexiahelp.umich.edu/sites/default/files/good_fonts_for_dyslexia_study.pdf
• http://www.dyslexiaaction.org.uk/page/text-formatting-best-practice
• http://bigelowandholmes.typepad.com/bigelow-holmes/2014/11/typography-dyslexia.html
• https://bdatech.org/what-technology/typefaces-for-dyslexia/

Something my students are persistently confused about is when a quantifier has to be restricted and when it doesn't have to be. E.g., in a mixed domain you want to symbolize "Someone is blah". Do you have to restrict the \exists to people or not? When do you have to restrict? Can you symbolize "someone" without restricting to people? There should perhaps be some sort of discussion on this in the book.

E.g., I received the following by email:

A question about Sec 24.4. For the following example: Someone is a dog owner.
This symbolization is given: ∃y∃x(D(x) ∧O(y,x)) But since the domain includes both animals and human beings, shouldn't '∃y' be restricted? I.e., Something like ∃y∃x(D(x) ∧ Person(y) ∧ O(y,x)).

This is well taken, but the symbolization key doesn't even include a predicate for "person". Figure out what to do here.

In the explanation of negation elimination, the current version says: "we always cite the sentence first, followed by its negation" (116). But where the rule is presented immediately above this, the negation of the sentence is cited first, followed by the sentence.

(Thanks for the fantastic resource!)

Insert a "Skip to Content" link at the top of each page on the website. This will allow screen reader users to skip the top menu directly to the beginning of the chapter content. You can see an example on this page: https://opentextbc.ca/studentsuccess/chapter/learning-action-plan/ If you start tabbing, a "Skip to content" link pops up that takes you directly to the beginning of the chapter. Here is more information: WCAG - Bypass Blocks

Figure out a good way to convert everything to HTML and ePub.