# Logic#

## Chp 2: The scope of logic#

It may seem like only logicians would ignore truth and focus only on form. When else donât we care about truth, however?

When training a deep learning model, we often start with dummy data and just check that we *can* fit to something (e.g. images from some other dataset). If we canât, then we likely coded something wrong. Sometimes we are just interested in learning a library (e.g. PyTorch) rather than getting it to do something useful.

In Bayesian statistics, similarly, we generate data from our assumed data-generating distribution and then try to fit our model to it to confirm we can reproduce the model parameters.

In Chapter 2: The scope of logic, this is put in terms of a âvalidâ argument: we donât care about truth. Alternatively, you can see this as asking a âwhat ifâ question about a world that could have existed (e.g. if Abe Lincoln was from France). You could also see all this as âplayâ in the sense that it helps you understand other assumptions people have about the world. A kid could learn something about e.g. conjunction introduction on any imaginary world where we hold it to be true.

Do you only care about valid arguments, not sound arguments? Yes, when youâre trying to learn the rules of inference. No, when youâre trying to get something âdoneâ in some sense (in this case, discovering truth).

## Chp 8: Metalanguage#

See forall x Â§ Chapter 8 Use and mention for the object-language and meta-language distinction also mentioned in implication in nLab. See also Metalogic, which points to Useâmention distinction.

You can think about names as pointers in e.g. C++ as well. So if `x`

is an object, `&x`

is some number (like `0xdeadbeef`

) that we could call a pointer. You could modify `0xdeadbeef`

by adding e.g. `0x4`

to get a different pointer/name, just like you could replace âTrudeauâ with âVerlanderâ in the name âJustin Trudeauâ to get a different name. As mentioned in the text, ââJustin Trudeauââ is the name of a name, just like `&&x`

is a pointer to a pointer.

It seems likely this is related to the issue that often comes up in category theory where you can think of a word (or symbol) as either an arrow, or the thing that the arrow points to. So while âAliceâ is a word in English (e.g. an element of the set of words, an arrow into the set of people), Alice is some imaginary person (e.g. an element of the set of people).

Is referring to something without quotes the same as taking it from context? That is, using it. If you use quotes or bold then youâre defining a term (mention). Must you always mention/define before you can use, or otherwise rely on it being in context?

See also Do Periods Go Inside Quotation Marks? | The Editorâs Manual. You prefer British style, not only because it makes it clear that the punctuation is not conceptually part of the quote (it could be transferred somewhere else unchanged) but because it allows for quotes within quotes more naturally, since single quotes are actually used (not double quotes everywhere). This also matches how programming languages (e.g. Python) are written. It also gives you a standard for Python: use single quotes first and then double quotes (just like British English). Perhaps itâs not surprising that forallx is written in this style (see e.g. Chapter 4: First steps to symbolization).

If youâre American, to get used this to style you may have to think of English more like a programming language. If you write `;`

at the end of statements in C and C++, then adding . to the end of a line that ends with âââ wonât seem so strange.

But, double quotes are easier to visually distinguish from e.g. an apostrophe (see Apostrophe vs. Single Quote - SE). So prefer it first, taking what you want from both the American and British styles. In theory, you could use a triple quote if the need ever arose by combining single quotes (as in âââ), or using the dedicated symbol â´. See also What is the difference between single, double, and triple quotes in Python? - SO.

Add this to a âprefaceâ on your website? Really, everything regarding logic should come first.

What about âfully mathematicianâ for a blog title? Youâre looking for a good combination of an adjective and a noun, thatâs also memorable (like many restaurant names). This is a play on âfully human, fully divineâ that is often used in your circles. Perhaps âfully philosopherâ is a little shorter and easier to read (since itâs alliterative).

Strict quoting falls apart when applied to regular human language because we adopt words quickly. Do âYahwehâ and âHosannaâ count as English words? Almost, if youâre using them regularly in e.g. a church context and their definition is given in English words. The English language is ultimately just a collection of words from other languages; thereâs no bottom. See English language for the major influences (Hebrew is not a major influence).

## Chp 12: Semantic concepts#

How do you read A â B? Not in general, but in a context where it means Material conditional. As discussed in forall x, the best we can do in languages like TFL and FOL is âsymbolizeâ the richer English language; to say we âtranslateâ would imply we preserve meaning and we are most definitely not doing that. Therefore when we desymbolize we need to be extremely careful that we donât add additional meaning, effectively claiming that the logic that a machine (or formal language) is doing is more powerful than what it actually is doing.

What we really want here is a desymbolization that satsifies certain ground truth requirements. One of the most important requirements is when \(A\) and \(B\) are both false, as in if you assign A to the âthe Nazis won WW2â and B to âthe moon is made of green cheeseâ. Notice the contrast with LLMs here; we want to define certain words to mean certain things rather than simply measure what they mean on a large corpus of work. Weâre changing how *we* think rather (making our thoughts more precise) than telling the computer weâre always right. One column is syntax (â), and the other is semantics (âimpliesâ). Or one column is use (English), and the other is mention (FOL, TFL)? This is similar to the Alice/Bob pointers out to the real world (being Peruvian and quick). We rapidly go from English to Augmented English, then continue to augment our English indefinitely. To write pedagogical material is the process of augmenting English. See also âhomoiconicityâ in What is a âsymbolâ in Julia?.

If we all speak slightly different versions of English, then we must always translate from the variation someone else is writing in to the version we write (and hence think) in. This justifies copying and pasting content from other texts to your own, and modifying code as you read it (if only the formatting). The logic should be similar for effectively copying drawings; if you cannot build it then you do not understand it (e.g. a commutative diagram). And because we all speak different versions of English, we have to provide our own answers to questions that instructors provide. Our answer should never match the authorâs answer word-for-word, and may even take a completely different approach.

So what does the word âimplyâ really mean? When spoken about a word, it means that the word is usually used in a way that brings along additional context, the additional context being what is implied. Itâs a probabilistic statement about the word, based on the authorâs experience with the word. By supplying definitions for words we eliminate this uncertainty and allow for faster communication (because readers need to disambiguate less and consider fewer possible worlds) but also start to talk in a jargon specific to those like us. In the interest of obeying the Robustness principle weâll also likely need to read words from others who are using in an old or different way, leading to extra internal translations in our head (not as hard to deal with, if we can determine the authorâs meaning from context).

Every LLM speaks its own variation on English.

Software bugs are almost always the result of a failure to desymbolize; to not catch certain situations (âbugsâ) until theyâre uncovered by someone else.

This is closely related to âcorrelation does not imply causationâ in statistics. While the Nazis winning WW2 and the moon being made of cheese are correlated, thereâs no causal relation between them. If there were, weâd expect them both to change together (so that they would also both become true together).

### Implies#

What does implies mean, if itâs not the materical conditional? Try to use it in a few sentences. Often, it means something from the future implies something about the past. See also Implication.

See imply - Wiktionary, the free dictionary. Someone who isnât a mathematician or logician will know this word in terms of the third definition:

Although this way of using the word is common, itâs a very human custom to be polite. Itâs also quite culture-specific; see Politeness.

This is related to but not quite the same as the way the word Implicit is used. In both cases thereâs something left unsaid but derivable from the context; but the word implicit doesnât always mean something was left unsaid for the sake of being polite.

The second definition is essentially probabilistic:

(transitive, of a person) to suggest by logical inference

When I state that your dog is brown, I am notimplyingthat all dogs are brown.

That is, someone might say that a dog is brown (and list several dogs that are brown) to try to make a point that all dogs are brown or at least that most dogs are brown.

### Or not#

How about always reading it âbackwardsâ and putting âor notâ in the middle? So youâd read âA â Bâ as âB or not Aâ in these situations. That makes you read â(A â B) â Aâ as âA or not (B or not A)â (canât really avoid the parentheses) which makes it rather obvious how it reduces to âA or not Bâ assuming the law of the excluded middle. You can then read Pierceâs law i.e. ((A â B) â A) â A as âA or not (A or not B)â which reduces to the law of the excluded middle (with an âor Bâ at the end that doesnât hurt anything).

This strategy is similar to always applying Material implication (rule of inference), but also flipping the disjunction. Reading A â B as ânot A or Bâ is also acceptable, but it seems more intuitive to replace a single symbol (â) with a pair of words than adding two words in different spots. It also avoids the potential misinterpretation of ânot A or Bâ as ânot (A or B)â which is something completely different (and you canât express parentheses verbally without a lot of extra work).

This language doesnât make any claims about causality. If you assign A to the âthe Nazis won WW2â and B to âthe moon is made of green cheeseâ then A â B is true because both statements are false. This desymbolizes to âeither the moon is made of green cheese or the Nazis did not win WW2â and this is easy to agree with because we donât believe that the Nazis won WW2.

### Less than or equal (LTE)#

You could also replace A â B with A â¤ B if you donât mind seeing false as âless thanâ true. At that point, itâs trivial to desymbolize â¤ to âless than or equal toâ when moving to English. If thatâs too wordy, consider the acronym LTE (commonly used in programming and spreadsheet languages).

### Forces#

Alternatively one could read A â B as âA forces Bâ (in the sense of turning a light on) which is a bit shorter and read in the right direction, but harder to break down. It may also imply that A is the only forcer of B.

Notice the similarity between the symbol â¨ (âdouble right turnstileâ in Unicode) and the symbol âŠ (âforcesâ in Unicode). Per List of logic symbols, it seems to only be used in modal logic, but per Forcing (mathematics) it has nothing to do with modal logic. Per Boxes and Diamonds it should be read as making a formula true in either a particular world or all worlds (say âworldâ rather than âpossible worldsâ unless youâre in the alethic interpretation).

In contrast, Modal logic doesnât use âŠ at all. In Kripke semantics only âŠ is used; the â¨ symbol is never mentioned.

### Entails#

See Chapter 12 Semantic concepts Â§ 12.6 for a suggestion to avoid âimpliesâ for â¨ because of both the causal and historical issues.

How should one read â¨? It seems like the best word is âentailsâ because itâs a rather technical term. The author suggests that he may use âimpliesâ to mean entails, but in practice almost never does. Itâs likely better to never use the word âimpliesâ because of its present ambiguity. In particular, many people would read âA implies Bâ to mean that A not being true also implies that B is not true (or is at least a clue that indicates it may not be true). There are no clues in this domain; everything is true or false.

Consider the following simple example argument. While A â¨ B entails A â¨ B â¨ C, if youâre thinking about the truth tables youâll clearly see the most unambiguous way to explain their relationship is with â¤ rather than â (in English, use âentailsâ rather than âimpliesâ):

### If#

One can read A â B backwards to get âB if Aâ which appears to match a language construct of Python:

```
x = True
y = True if x else False
```

However, `y = True if x`

produces an exception. This is because weâre constructing a boolean, not taking a valuation.

### Only if#

Per paradoxes-material.pdf, using âonly ifâ is a better option than âimpliesâ because of the noted issues. For example, letâs say being good at basketball (B) requires one to be tall (T), and the converse does not hold. So youâre good at basketball *only if* youâre tall i.e. B â T. This naturally extends to predicate logic so that B â T if B(x) â T(x) for all x.

This also seems to work if two statements are equivalent. If youâre Canadian (C) youâre a citizen of Canada (U), and if youâre a citizen of Canada youâre Canadian. So we have that both C â U and U â C, and itâs still fair to say that youâre Canadian only if youâre a citizen of Canada and youâre a citizen of Canada only if youâre Canadian.

The âonly ifâ language continues to work if youâre thinking in terms of intuitionistic or constructivist mathematics, or the Curry-Howard isomorphism. To say P â Q in that context means that you can construct a P only if you can construct a Q, or that thereâs some function P â Q that can give you a Q only if you give it a P.

The language breaks down if you start to think causally. If A is that the Nazis won WW2, then A â B is vacuously true. But to say that Nazis won WW2 only if 2 + 2 = 4 is not intuitive. See similar comments in Boxes and Diamonds Â§ Paradoxes of the Material Conditional.

### Necessary and sufficient#

See Glossary of mathematical jargon Â§ Proof terminology, which points to Necessity and sufficiency.

When this article says that Q is ânecessaryâ for P if P â Q, what it means is that Q must hold (is necessary) for P to also hold. You canât have P being true (holding) unless Q also holds. When you want to use the word ânecessaryâ you must read P â Q backwards, however (similar to âQ or not Pâ).

The word âsufficientâ reads in the forward direction (P is sufficient for Q), at least. Perhaps the article should be named âSufficiency and necessityâ to reflect this.

The language breaks down if you start to think causally. Is the moon being made of green cheese sufficient for 2 + 2 = 4?. Most would say no.

If youâre looking at Modal logic, youâll see it uses the word ânecessityâ in essentially a completely different way. Avoid an overload of language for ânecessityâ when possible.

### If statement#

The âif statementâ of Conditional (computer programming) is unfortunately a false friend in this context. Most often, itâs used for control flow.

However, it could be used to create a function from the booleans to some set:

```
x = True
y = 3 if x else 4
```

```
x = True
y = "yes" if x else "no"
```

When used for control flow, it could be replaced with a function that returns a function:

```
def clean_up():
pass
def keep_working():
pass
messy = True
z = clean_up if messy else keep_working
```

See also Anti-IF Programming and Destroy All Ifs. See also Replace Conditional with Polymorphism.

## Search/replace implies#

Take the time to `git grep`

for âimpliesâ in these public notes. Replace all instances of âimpliesâ and âimplyâ with either âentailsâ or âonly ifâ or âor notâ depending on the context.

## bussproofs prooftree#

See Supported TeX/LaTeX commands â MathJax 3.2 documentation Â§ Environments for the prooftree environment, and more documentation under bussproofs â MathJax 3.2 documentation. The example from that page:

## Monotone valuation functions#

When applying inferences to propositions, we effectively expect our valuation function to be monotone. For example, we want the âgreenâ situation/arrows here rather than the red:

When this isnât the case, we have to give something up. It could be that our valuation function is wrong; the data weâve collected is wrong (and we need to fix the dashed green/red arrows). It could be that our system for coming up with inferences is wrong (and we need to fix the solid black arrows). In propositional logic we assume that the dashed arrows are always right (even definining them as ârightâ by removing meaning from the words, e.g. replacing Cloudy with \(C\)) and do whatever we need to in order to rearrange items on the left to make the function monotone. Humans get to choose what they question, which (among other things) creates politics and filter bubbles.

One solution for the system on the right is to delete the arrow Raining â Wet Ground (perhaps you have a roof or umbrella to cover the ground youâre talking about). That is, what you can you do with a contradiction in your system of logic? In almost any system youâll want to rearrange your drawing so Raining is not above Wet Ground. You could put them at the same level (ârankâ in graphviz) until you know more.

Consider the following inference system that includes Pierceâs law, however. There are three gray arrows on the diagram for the three arrows in Pierceâs law, where gray here indicates TBD. The given valuation function is shown as green because it can be made green for some choice of turning arrows on and off. Can you easily see which gray arrows need to be turned black/white?

You can come up with a working inference system based on some valuation function (deciding which arrows on the left side need to be turned on/off), but can you always come up with a green valuation function given arrows that are definitively turned on/off? What makes this question harder to âsolveâ is its recursive nature; if you only commit to one piece of âdataâ (e.g. whether a proposition is true or false) and start to check what that implies, you may discover that you need to change your original choice. What if you assign the proposition that is Pierceâs law to false to start? Your valuation function now determines the truth value of your propositions, which determines which arrows need to be on/off, which determines whether you valuation function is monotone and therefore needs to be changed.

## Heyting algebra semantics#

From Boxes and Diamonds Â§ Intuitionistic Logic Â§ Semantics:

The truth conditions for the conditional, however, differ from classical logic. \(AâB\) is known at \(w\) iff at no \(w'\) with \(Rww'\), \(A\) is known without \(B\) also being known. This is not the same as the condition that \(A\) is unknown or \(B\) is known at \(w\). For if we know neither \(A\) nor \(B\) at \(w\), there might be a future epistemic state \(w'\) with \(Rww'\) such that at \(w'\), \(A\) is known without also coming to know \(B\).

Another way to see this as a function that is written at some point, but that doesnât have any constructions to work on. In the world of programming, this would not compile. In the world of math, however, this isnât unreasonable. Many famous conjectures have had additional work done on them assuming that someday someone will come up with a proof of some of the dependencies of the proof. That is, sometimes mathematicians build \(AâB\) without having \(A\) yet.

Or consider this function defined in a file by itself:

```
def add_one(x: Integer):
x = x + 1
```

Clearly this code only has âpotentialâ without being used. Thatâs not to say it isnât something in itself, however.

## Accessible logic#

In Kripske semantics we say that a world is âaccessibleâ from another if we feel itâs possible to get there from where we are. Is this a statement about the future, or about the past? Likely neither. It seems like our imperfect knowledge of the past makes multiple histories possible given what weâre observing, as well. Are we even always more interested in the future than the past? Many problems (e.g. building a map) depend on being able to consider many possible past worlds.

Either way, the word âaccessibleâ often comes up when youâre trying to decide what to read on Wikipedia. For example, the article Heyting algebra is long and complicated. Only some sections are âaccessibleâ to your current understanding. Youâve tried to build git graphs to plan your learning, but is it better to think about this in terms of possible worlds?

One way to read is to only read chapter sections, and consider both whatâs accessible and whatâs valuable. If you read only accessible sections, youâll end up following links on Wikipedia from the categorical product to tychoffâs theorem to who the current king of England is (itâs easy to understand history and politics). If you only read whatâs valuable to solving your current problem, you may end up spending a long time reading an article and not comprehend anything at the end (or not comprehend anything long term e.g. new math).

## Valid argument#

The word âvalidâ as it is used in logic doesnât really correspond to how we use it in everyday life; see Validity and valid. However, there needs to be some word that separates the truth of individual propositions from how you reason about truth. Is it true that you can reason about truth in this way?

Why not define valid to mean âif all the premises are true, the conclusion is trueâ rather than âif it is impossible for all the premises to be true and the conclusion falseâ as in forallx? That is, so that âall premises trueâ â âconclusion is trueâ? Perhaps you can define it that way; this produces the conclusion that the argument is valid if you accept the Material conditional. Perhaps this is getting to some comments on the modal logic about âknowing that you know thatâ which otherwise seem rather crazy. To some extent this is also about âdefaultsâ in the presence of uncertainty: do you conclude that A implies B if you have no evidence that A has led to B (because you have no record of A ever being true)? The material conditional can only be T/F so it must choose either T or F, and someone somewhere seems to have decided that it defaults to T. This seems wrong: from a constructivist perspective we should only accept that something is true if we can prove that it is true. It should have âdefaultedâ to false. Said another way, absence of evidence (see Argument from ignorance) says nothing about the truth of a matter (see also Evidence of absence, which links to the last article).

What if you saw material implication not as that itâs true that A causes B, but that itâs possible that A causes B? This feels like going from a strict inequality to a non-strict inequality. Or perhaps as if A is true, then B is possible.

Perhaps an even better way to define this (more generally) is that it is impossible that an increase in X does not lead to an increase in Y. This is effectively what arrows mean on a causal diagram; they indicate that an increase in the source of the arrow leads to an increase in the target of an arrow. In the simple case of T/F, this reduces to the definition of entailment (or material conditional). Because T is as high as you can get, and F is as low as you can get, if you see X equal to T and Y equal to F then clearly no increase in X leads to any increase in Y.

This seems quite similar to an adjoint pair, in that x â¤ y iff f(x) â¤ f(y). An increase (or no change) from x to y must always correspond to an increase (or no change) from f(x) to f(y).

See also Wason selection task. In the first example, you can distinguish between the rule being *obeyed* or *causative* relative to being *likely*. If a card shows an even number on one face, is it *likely* the opposite face is blue? In that case, you need to flip all the cards to get more evidence about whether the rule holds. If you flip an odd number and see blue, it may be the case that *all* colored sides are blue. If thatâs the case, then the rule that there is an even number on one face means the other side is blue isnât really correct: it may be technically true but itâs far from the full story (and you could come up with a simpler rule). Why not prefer simpler theories, if you believe in Occamâs razor? The existence of the red card excludes the possibility of this rule being true, but many people (experimentally-minded rather than theoretically-minded) will simply start collecting evidence before even thinking about theories.

Another explanation could simply be that in regular English we assume that âifâ means âiffâ in many cases. See this same point being made in Chapter 5 Connectives.

If we had simply stopped âconstructingâ (making statements about truth, such as whether an argument is valid) when we saw a contradiction in our assumptions, then we could have avoided reaching a conclusion that may be âtrueâ in some sense but isnât useful (that the argument is actually valid). That is, the world doesnât have to be valid or invalid: it could have been left neither.

We often feel that we need to organize our notes to remove contradictions. Itâs not that weâre doing this for the sake of avoiding an explosion in conclusions; weâre simplying doing it to avoid reaching different but incompatible conclusions in different areas of our notes. We want one, single, complex model. In particular, we want to avoid coming to simple conclusions in some areas because we arenât considering enough possibilities (possible worlds).

## Chp 17: Basic Rules for TFL#

TFL is based on Truth functions; see the redirect Truth-functional logic.

### Practice exercises#

Part C.

```
0 J â ÂŹJ â´ ÂŹJ
1 J â ÂŹJ PR
2 J AS
3 ÂŹJ âE 1,2
4 âĽ ÂŹE 3,2
5 ÂŹJ ÂŹI 2-4
```

```
0 Q â (Q â§ ÂŹQ) â´ ÂŹQ
1 Q â (Q â§ ÂŹQ) PR
2 Q AS
3 Q â§ ÂŹQ âE 1,2
4 ÂŹQ â§E 3
5 âĽ ÂŹE 2,4
6 ÂŹQ ÂŹI 2-5
```

```
0 A â (B â C) â´ (A â§ B) â C
1 A â (B â C) PR
2 A â§ B AS
3 A â§E 2
4 B â§E 2
5 B â C âE 1,3
6 C âE 5,4
7 (A â§ B) â C âI 2-6
```

Letâs take this third example and rewrite it as a String diagram. We convert objects (propositions) to wires, and morphisms (inference rules) to boxes:

For this particular example, we can view the same diagram (taking propositions to types per the curry-howard isomorphism) as a description of a function that takes a function of type \(Aâ(BâC)\) and returns a function of type \((Aâ§B)âC\) (or in the category of sets \((AĂB)âC\)). That is, this expresses uncurrying.

For the next few examples, we also provide the possible worlds (each cell being a possible world) associated with parts of the proof. These are essentially the same as the truth tables:

Natural deduction in TFL is very much like how you already do proofs. It feels like a geographical search, where you have as âtruthâ what you are trying to prove, and like a geographical âproofâ of how to get from A to B there is often more than one way to do so (but sometimes only one). You could see your intended proof (your goal) as minimizing the loss in machine learning, or maximizing some utility function, but in this case reaching the proof is the end because thereâs only one thing to show (only one âgroundâ truth example). In ML you set a bunch of parameters; in this context we fill out a truth table.

Part of the problem is that you can go in circles, i.e. with:

```
A â B
A
B
A â B
```

With a natural deduction system, the large number of basic and derived rules give you many directions you can take at any possible point. The less natural a system, the fewer options/choices you have. The advantage to a natural deduction system is that your proofs can be much shorter, and arguably easier to comprehend (as long as you agree with and understand all the additional rules i.e. have them memorized).

You donât look at the proof for the same reason a machine learning model doesnât look at the truth when itâs running inference (the term inference now makes a ton of sense, see Inference). We want to check it comes to the same conclusion (e.g. true or false) about a particular set of premises that we do. If it had the truth as an input, it could just feed that all the way through, from being a premise to being the conclusion.

If proofs are programs, then automated theorem proving is automated program writing.

## Chp 20: Proof-theoretic concepts#

Notice how the title of this chapter is symmetric with the title of Chp 12: Semantic concepts. Weâll see in Chp 22 how the âsemanticâ (truth table) concepts relate to the âsyntaticâ (proof-theoretic) concepts (e.g. both define a notion of equivalence). For now, ignore how familiar all the language looks.

### Practice exercises#

Exercise A2âs answer was covered in more detail in 18.6 Indirect proof of excluded middle.

For Exercise A4 weâll try a more systematic answer search. In the following, red arrows to the right indicate searching backwards using IP. Red arrows going down indicate searching backwards using some kind of introduction rule. Green arrows going left indicate searching forwards using some kind of elimination rule.

The same proof as a String diagram:

## Propositions from propositions#

When you see âif youâre in the rain, youâre going to get wetâ you see A â B with the obvious fill-ins. But why donât you see this as a proposition in itself, that is, a C that can be true or false? You could see it as either adding another object to your preorder of propositions, or you could see it as equivalent to an existing object (equivalent in the sense of iff i.e. an arrow in both directions).

## Chp 22: Sound and complete#

See Chapter 22 Soundness and completeness âŁ Part IV Natural deduction for TFL âŁ forall x: Calgary. An Introduction to Formal LogicâŁ Part IV Natural deduction for TFL âŁ forall x: Calgary. An Introduction to Formal Logic for some suggestions about when to use truth tables vs. logic.

Sound and complete to some degree means you can use both data and logic to solve a problem. Each is better in some situation. For ill-defined problems, itâs often to collect a bunch of data and do machine learning (truth tables). For cleaner problems, you can write code.

## Chp 23: Building blocks of FOL#

How do you code the ânecessaryâ truths discussed in previous chapters? Letâs say you believe itâs true that if Jenny is mean, then Jenny will kick the dog. Similarly, you think that if George is mean, then George will kick the dog. It seems like youâd have to codify/model this as two different implications JM â JK and GM â GK. How do you deal with specifying this for all possible people, though? While itâs true that JM â JK, you could make it a ânecessary truthâ by coming up with some rule where XM â XK where X is any person. This way, you donât have to specify so many individual rules. Itâs only possible to code something like this once you move to FOL (or a programming language).

## Chp 24: Sentences with one quantifier#

See Syllogism Â§ Types for more on syllogisms and these examples.

## Why past possible worlds?#

If you think of the world like a computer i.e. in a deterministic way, then itâs hard to fathom the value in past possible worlds. How would we get to a point where Abraham Lincoln was born in France? It seems silly; what would you have to change farther back in the past to make that happen? Convince his parents to move?

One possible resolution is that we need past possible worlds because really have imperfect information about the past, just like we have imperfect information about the future. How do you know that Abraham Lincoln wasnât born in France? You think it quite unlikely that historians and the US government would lie about that, but itâs possible.

Another possible resolution is that we need to accept that those living in the past didnât have perfect information about what their future would be. Did they make the best decision based on the information that was available to them? Thatâs often a more important question than how history actually turned out; you can only go on the information you have. Leaders are often criticized despite the fact that they made the best decision they could given the information they had.

## Possible worlds vs. world states#

We sometimes think of different rows in a database as possible worlds, where each column is associated with a propositional variable. Other times we think of each row as a state of the same world, just evolving over time. For example, think of all your paystubs you get over the year as being related to the state of your checking and other accounts over the year. These transactional databases (like logs) usually have rows ordered by time.

The second kind of row is like the first, but with an explicit timestamp. Does that mean the first kind of row/world is considered timeless? If you think of there being a causal relationship between columns (or that weâre looking for one), youâre also going to run into trouble when timestamps are associated with rows because one row will cause effects in other rows.

## Standard compression#

TFL is obviously a lossy compression. If youâre going to use it, however, then you need a standard way to compress into it. That is, you essentially need a standard functor from natural language sentences to TFL, which will necessarily not be injective.

In Chp5 of forallx you can see many examples of compressions you may not agree with, but they are standard in the context of this text. The author is doing his best given the system.

For example, you code âJean is in France only if Jean is in Paris.â to F â P. If you switch this to âJean is in Paris only if Jean is in France.â itâd be coded P â F (although P â F seems true, the coding still seems wrong). Really, youâd like to use the biconditional here, if anything. Is the speaker saying that Jean may or may not have had a layover in France, but if he did then it was in Paris? You almost want to refuse to encode this, but it might work in some cases. Itâs an example of ambiguity in language where you really need to ask the original speaker what they meant (ask for more context).

Another nasty one (see Necessity and sufficiency) is all of these being coded to the same thing, namely P â F:

For Jean to be in Paris, it is necessary that Jean be in France.

It is a necessary condition on Jeanâs being in Paris that she be in France.

For Jean to be in France, it is sufficient that Jean be in Paris.

It is a sufficient condition on Jeanâs being in France that she be in Paris.

Just as we have nasty standards/defaults for the material conditional when the antecedent is false, we have to live with some of these compression standards if weâre using TFL.

## Law of exclude middle#

Is like arguing with someone and they find some small contradiction in something you said once. They use that to conclude everything you say is wrong and their conclusion is right. Or perhaps this is closer to the principle of explosion?

Either way, it feels similar to exceptions in programming languages. You âexplodeâ when things donât logically fit together (give up on any kind of inference).

## Propositions as types#

One of the primary insights that came out of the CurryâHoward correspondence is the analogy between propositions and types. Hereâs an example isomorphism, originating from the example type hierarchy on the right:

When we expand to thinking in terms of the CurryâHowardâLambek correspondence/isomorphism (see CurryâHoward correspondence Â§ CurryâHowardâLambek correspondence), we interpret category-theoretic objects as types or propositions. From this perspective an âAnimalâ is an object in a category, and the isomorphism between the categories is (partially) shown as the dashed arrows.

## Turnstile symbol â˘#

Notice â˘ (âright tackâ) is used for both syntactic consequence (see Logical consequence Â§ Syntactic consequence) and Adjoint functors. Is this just a coincidence? It seems likely that syntactic consequence is part of an adjunction (based on the syntax alone, itâs the right adjoint).

Some evidence for this is that the propositions we can derive as being true given some propositions that we assume are generally not speaking not equivalent to our assumed propositions. Since the left side of the syntactic consequence operator takes a set of propositions, this may be the upper closure operation \(A^{âX}\) defined in Upper set.

## Open/closed set as proposition#

Could you see a set being defined as âopenâ or âclosedâ like a proposition in the language of modal logic? That is, \(V(p)\) assigns certain worlds to every proposition. Those sets/worlds that are open could be represented by the letter `o`

so that \(V(o)\) picks them out.

## Kripke semantics#

Take the relational models of Kripke semantics. The \(R\) (accessibility relation) is clearly the âcategoryâ because you can draw a relation in one way or another as a bunch of arrows, and the \(W\) are the objects in the category. The relation must be reflexive and transitive (T and 4) for it to be a category, however. The T stands for the truth axiom in epistemic modal logic.

Still, this means much of category theory must correspond to modal frames with certain properties. If you have a symmetric relation (think of a symmetric monoidal preorder) then you add a B (for Brouwer).

## Is the modal frame the sheaf morphism for true?#

The modal frame decides what is possible.

## Possible world (alethic) semantics#

See Possible world; not to be confused with Kripke semantics (despite the fact that Modal logic is about possibilities).

See section 7.4.3 of SSC. Looking at the mapping of each element of a section as an aspect of a possible world, in this example each personâs opinion is an aspect of the world allowed by \(S\).

You can see this as limiting subobjects. In our people example, there are some subsheafs that are not legitimate subsheafs of the people sheaf. For example, if Bob was not alive in 1921 then we cannot provide a subsheaf that says that Bob liked the weather in 1921. That is, we donât allow that possible world.

People can disagree about whatâs possible, and if something isnât possible in the mind of one person they wonât bother to think about it in the models they produce. This could be seen as an optimization as well as a statement about whatâs real; someone may refuse to think about a particular possibility because it would require rewriting too much of what they already know (e.g. an older adult).

The subobjects of the terminal object 1 are essentially a list of all possible worlds.

We donât allow some worlds i.e. consider them impossible (level one), we allow some worlds (level two), we allow world aspects (level three). Do we also allow for world aspects to be of different kinds?

Agreement on the overlap for a particular matching family is then agreement on the shared aspects of the possible worlds.

When we consider only a subset U of X we are cutting down all our possible worlds to fewer world aspects. That is, fewer columns in a table (assuming rows are observations, columns are features).

Can you see the following as sections over a timeline?:

Can you see the propositions-as-types insight as both propositions and types corresponding to a range of possible worlds? A type (such as an integer) can take on e.g. 2^32 possible values (possible worlds). A proposition (such as whether aristotle is a man) can take on a certain number of possible values (possible worlds) such as true or false. When you extend to Heyting logic, youâre allowing for more than two possible worlds.

Throwing away uncertainty then becomes a matter of engineering; how much do you want to throw away? It depends on your meta-uncertainty; perhaps you arenât sure how uncertain you are and so only bother to split the possible worlds into true and false (as a first step).

## Define dual#

See also Define dual, which ends with the observation that the âinterior of the complementâ (or ÂŹ according to our author) is a right adjoint to the âcomplement of the closureâ (not defined specially here). To preserve **m**eets we need a **r**ight adjoint (see Proposition 1.111 in Section 1.4). Therefore we expect that \(ÂŹ(xâ§y) = ÂŹxâ§ÂŹy\); this is not true however.

## Example: Kitchen topology#

A reasonable example of a topology might be a kitchen, which potentially has multiple rooms (e.g. a walk-in pantry, additional dining room) each of which will have many cupboards/drawers/shelves, each of which may have many utensils, pans, etc. Use this to think about Topological indistinguishability. Perhaps using a house is even better; there are more names. Itâs also not clear what word the pantry and kitchen add up to together: places we store food? We could also store food in dining room cupboards, or at least dishes. Perhaps this should be part of a house design? A Topological map. But for that, you could use real distances?

In this topology youâd describe where something is by saying e.g. what room itâs in, and then e.g. what shelves it is not on (to limit a search). It may be helpful to have such a topology for a house only for the sake of naming all the rooms and shelves.

## Topological subobjects#

A topological subobject (see also Subobject) would be a Subspace topology.

## Avoid SSC auto-numbering#

See Prefer descriptive headings. We can expect that the original 7S PDF wonât have its numbering changed anytime soon, unless the authors upload something new to arxiv.org (which seems unlikely). Instead, the minds of readers and their commentary are a âforkâ of the content; we can refer to an old version of the PDF (if necessary) to help others relate the website content to the PDF. This way, even if the authors create yet another version with new numbering (theyâve already done this, kinda too late) others can still share content. We canât help other readers if theyâre using a new numbering scheme; theyâll have to do the mapping themselves anyway we look at it.

So create titles that are descriptive and help anyone who only speaks English and memorizes words better than numbers find what they need quickly in the TOC. We can mention exercise numbers in plain text (an *addition* to the headings, and less prominent).

## Deemphasizing SSC content#

Weâre never planning to rework the PDF to the point that we e.g. remove a bunch of original research or remove content that simply isnât helpful. Instead, just fail to quote or recommend those sections in our own academic courses on the topic. Put those sections into their own documents and then âburyâ the document (effectively archive it) by only linking to it. Youâd offend the original authors (Fong/Spivak) by removing the content we donât agree with or donât see much promise in (they put a lot of work into it). Instead, just fail to quote it.

Itâs still acceptable to remove content from a personal fork of the PDF; the authors should not mind this kind of change. If someone accidentally quotes a personal copy of the PDF, they should only accidentally quote *less* than the original content. These direct changes to the PDF may also be helpful to the original authors; if they see consensus that several readers donât find value in a particular section then they may be more willing to remove it.

## Enrich English#

When deciding whether to use quotes, see Useâmention distinction. Avoid quotes unless you are making this distinction.

If youâre trying to emphasize something, it really is OK to use italic. Not using italic (or using quotes instead) is potentially confusing and may change the meaning of the sentence. See the âYou canât give these plants too much waterâ example in Alethic modality.

When youâre trying to define something, use bold.