Test Problem: KK1point3Strings
This is another early, simple knights-and-knaves problem from Raymond Smullyan, the master of such puzzles; it appears as Problem 1.3 in his delightful Logical Labyrinths (2009). Anthropologist Edgar Abercrombie, Smullyan tells us, visits the Island of Knights and Knaves, on which knights always tell the truth and knaves always lie. In addition, each inhabitant of the island is either a knight or a knave. The problem is quickly stated: Abercrombie comes across two denizens of the island, $a$ and $b$; and $a$ makes the following statement: “Both of us are knaves.” Your challenge is to decide the category of each member of this pair, and prove that you are right. Actually, the underlying Slate file makes things much easier for you, as it presents you with a single pre-set goal, which conveys the identity of $a$ and $b$. But, you will have to prove that goal from the information Abercrombie has. The representaation of that information exploits the flexibility of the pure predicate calculus (= zero-order logic = $\mathscr{L}_0$) over that of the propositional calcuus. Specifically, we make use here of relations and functions, in a manner that should be obvious. There are five givens.

Deadline 21 Feb 2020 17:00:00 EST

Test Problem: EmmaHelpedToo

This problem, known as ‘Bringsjord’ 1 in the initial, motivating part of the of the Spring 2020 edition of the class, has been shown to be unsolvable by the vast majority of college students who haven‘t had sustained, effective training in formal logic.

The problem presents two givens:

1. The following three propositions are either all true, or all false.
• If Billy helped, Doreen helped.
• If Doreen helped, Frank helped.
• If Frank helped, Emma helped.
2. Billy helped.

And the question is: Does it follow deductively from these two givens that Emma helped? It seems that the minds of those pondering this question can be partitioned into three categories: The first category is composed of those who answer in the affirmative, because they simply focus on chaining through the conditionals to arrive at the conclusion that Emma helped. The second category is composed of those who realize those in the first category have failed to take account of the all-false possibility, and are quite sure that when the three conditionals are all false, it can’t be deduced that Emma helped. The third category is made up of those who are truly logical; they realize that even in the case when all three conditionals are false, it can be proved that Emma helped. The third group is correct, and hence the answer to the question is: Yes!

While as is standard you can use the PC provability oracle while working toward your solution, no remaining use of the oracle is permitted in the submitted file, if a trophy is to be won.

Deadline 21 Feb 2020 17:00:00 EST

KnightKnave_SmullyanKKProblem1.1

Here’s an early, simple knights-and-knaves problem from Raymond Smullyan, the master of such puzzles; it appears as Problem 1.1 in his educational Logical Labyrinths (2009). The context is that anthropologist Edgar Abercrombie visits the Island of Knights and Knaves, on which knights always tell the truth and knaves always lie. In addition, each inhabitant of the island is either a knight or a knave. The problem runs as follows: Abercrombie comes across three denizens of the island, $a$, $b$, and $c$. Abercrombie asks $a$: “Are you a knight or a knave?” The reply from $a$ is indecipherable. Abercrombie then asks $b$: “What did he say?” The response from $b$ is: “He said that he is a knave.” Right after this utterance, $c$ says: “Don't believe that; it’s a lie!”Your challenge is to decide the category of $b$ and of $c$, and prove that you are right. (You can try to figure out whether $a$ is a knight or a knave, but such effort is not recommended.) Actually, the pre-set HyperSlate file makes things much easier for you, as it presents you with a single goal, which conveys the identity of $b$ and $c$. But, you will have to prove that goal from the information Abercrombie has (which is provided to you in the form of seven givens). Before doing anything, you should make sure you understand, at least to a high degree, what each given is asserting.

You are permitted to use oracles as you engineer your proof, but no use of an oracle can remain in any proof that earns a trophy, and thereby confirms success.

AthenCfromAthenBandBthenC
The theorem to be proved here is a straightforward conditional: viz. $$\vdash (A \rightarrow B) \rightarrow ((B \rightarrow C) \rightarrow (A \rightarrow C)).$$ No remaining use of an oracle can be present in a proof that constitutes a solution to this problem.

Deadline 22 Apr 2020 23:59:00 EST

BiconditionalIntroByChaining
In this problem you are provided with three biconditionals, and must deduce a new one based on the endpoints of what can be regarded as the chain of the trio. One might, upon saving the maneuver in one‘s mind or one‘s library, dub the generalization of what a successful proof shows as biconditional intro by chaining (although you will no doubt be able to devise a less verbose label for the tactic in question). Expressed metalogically, your overall task is to validate: $$\{P \leftrightarrow Q, Q \leftrightarrow R, R \leftrightarrow S\} \vdash P \leftrightarrow S.$$ You are of course free to use the PC oracle during the construction of your proof, but no use of the oracle can remain in your finished, for-credit proof. (No deadline for now.)
BogusBiconditional
In this challenge you are given a peculiar biconditional, and asked to prove from it that the moon is made of green cheese (symbolized simply as $G$, as is our custom). It’s possible to obtain $G$ from the biconditional alone, but to make the problem easier, a second given, The Law of the Excluded Middle (LEM), or by its Latin name tertium non datur, is provided. We encourage ambitious students to leave aside this second given and, if they wish to use LEM, to prove it as a theorem (or more precisely, a lemma) in the course of reaching $G$. So, minimally you need to prove this: $\{ P \leftrightarrow \neg P, P \vee \neg P\} \vdash G$; but the more impressive proof would establish this: $\{ P \leftrightarrow \neg P\} \vdash G$. (No deadline for now.)
Contrapositive_NYS_2
Here you are simply asked to prove that the contrapositive of a conditional can be deduced from that conditional. This is expressed in meta-logic by this statement: $\{ \phi \rightarrow \psi \} \vdash \neg \psi \rightarrow \neg \phi$. The problem NYS 2 tested for an understanding of this statement, which when thought of as an inference rule or schema is referred to as contraposition or transposition. No use of an oracle can remain in your solution. (No deadline for now.)
Disj_Syll
This problem requires that you prove the inference schema known as disjunctive syllogism, encapsulated in meta-logic as: $\{\phi \vee \psi, \neg \phi\} \vdash \psi$. No remaining use of an oracle is permitted, but as is standard (and recommended), using the oracle to help craft your finished proof is fine. (No deadline for now.)
GreenCheeseMoon2
Is the moon made of green cheese? Apparently, if one wisely denies what would appear to be a rather crazy claim (viz. that if some proposition $P$ doesn’t hold, every proposition is implied by $P$!), it does indeed follow that the Moon is made of cheese. Your task here is to build a proof that confirms this (i.e. a proof that confirms $\{ \neg (\neg P \rightarrow (P \rightarrow Q))\} \vdash G$), where we take $G$ to symbolize that the Moon is made of green cheese. The underlying Slate file can be found here. (No deadline for now.)
HypSyll
Here you are tasked with proving the very handy hypothetical syllogism, expressed in meta-logic by this statement: $\{ \phi \rightarrow \psi, \psi \rightarrow \delta \} \vdash \phi \rightarrow \delta$. As always, you are free to use the oracle as you analyze and build your proof, but no use of the oracle can be present in your final, trophy-winnig solution. (No deadline for now.)
Modus_Tollens
Here you are asked to prove the famous inference rule modus tollens: $\{ \phi \rightarrow \psi, \neg \psi \} \vdash \neg \phi$. In natural-deduction proof systems, modus tollens isn’t given as a primitive inference rule; modus ponens (= conditional elimination in Slate) is, however, given. Cognitive scientists have established beyond any doubt via experiments involving subjects insufficiently trained in beginning deductive logic that such people are almost invariably unable to deduce even obvious one-step conclusions using modus tollens. Make sure your successful proof of modus tollens is saved as a permanent part of your library, since it’s very useful. The underlying Slate file can be found here. (No deadline for now.)
Explosion
Here your task is to prove the explosion inference schema/rule in HyperSlateTM; the schema says that from a contradiction anything whatsoever follows. Expressed in meta-logic, you are to prove $\{\phi \wedge \neg \phi\} \vdash \psi$. As explained in class, for whatever reason, while the general proof technique of reductio ad absurdum (= proof by contradiction, indirect proof, etc.) is covered in high-school math (at least it is in the textbooks, e.g. solid ones for Geometry and Algebra 2), explosion for some reason is almost invariably left aside, despite the indisputable dual fact that explosion is valid in classical logic and mathematics, and that it can be extremely useful. (No deadline for now.)
GreenCheeseMoon1
Is the Moon made of green cheese? Apparently, if one denies what would appear to be a rather crazy claim (viz. that if some proposition $P$ holds, every proposition implies $P$), it does indeed follow that the Moon is made of cheese. Your task here is to build a proof that confirms this (i.e. a proof that confirms $\{ \neg (P \rightarrow (Q \rightarrow P))\} \vdash G$), where we take $G$ to symbolize that the Moon is made of green cheese. (No deadline for now.)
Disj_Elim
This problem requires that one employ the inference schema (or rule) known as disjunction elimination, a.k.a. proof by cases. The inference schema, the hypergraphical specification of which can be found in the chapter Propositional Calculus in LAMA-BDLA, is based on the core idea that if one has a number of cases/disjuncts $\phi_1 \vee \phi_2 \vee \ldots \vee \phi_k$ to consider, and can show that $\psi$ follows from each $\phi_i$ (made as an assumption), then $\psi$ follows from the disjunction itself. (No deadline for now.)
switching_conjuncts_fine
Here one needs to provide a proof that confirms $\{\phi \wedge \psi\} \vdash \psi \wedge \phi$. Once the proof is found, this shows that the order of conjuncts is immaterial in logical consequence, for clearly the number of conjuncts could be expanded arbitrarily, so we declare that once this proof works, it's mere tedium to handle $\phi_1 \wedge \phi_2 \wedge \ldots \wedge \phi_k,$ for any $k \in \mathbb{N}$. (No deadline for now.)
NYS_1
This warmup for the infamous problems that typically follow (in Bringsjord’s demonstration that there’s a dire need to learn formal logic) was covered in the first of the two “motivating” classes, and is taken from New York State's high-school math coverage (under algebra). Viewed from the perspective of meta-logic, your task is to prove $\{\neg A \vee \neg B, B, C \rightarrow A\} \vdash \neg C$. Here, $\neg C$ is the key among a series of options; the distractors are $C, \neg B, H, A$ and NONE OF THE ABOVE. No remaining use of the oracle can be present in your trophy-winning proof. (No deadline for now.)
NYS_3
Viewed from the perspective of meta-logic, your task is to prove $\{\neg \neg C, C \rightarrow A, \neg A \vee B, B \rightarrow D, \neg (D \vee E)\} \vdash H$. Since of course $H$ here is arbitrary, and doesn't appear in the givens, what your proof will demonstrate, if valid, is that from the set of given formulae in the propositional calculus, any $\phi$ can be derived. (No deadline for now.)
RipsSaysNo1
This problem relates to the interesting book The Psychology of Proof, by psychologist L. Rips, a book that, shortly before he died, nobelist and computational-logic pioneer Herbert Simon praised as crucial to advancing automated reasoning/AI. Specifically, you are presented here with the challenge of crafting a proof that, as implied by what Rips presents in his volume, is supposed to be beyond the reach of (at least logically naïve) humans! This is quite peculiar, because as you will soon see, that which is to be proved, expressed in meta-logic, is simply this: $\{ \neg (\phi \rightarrow \psi) \} \vdash \phi$.

Deadline 22 Apr 2020 23:59:59 EST

RipsSaysNo2
This problem also relates to the interesting book The Psychology of Proof, by psychologist L. Rips. Your challenge this time is to craft a proof that, as implied by what Rips presents in his volume, is supposed to be beyond the reach of (at least logically uneducated) humans! This is quite peculiar, because as you will soon see, that which is to be proved, expressed in meta-logic, is simply this: $\{ \neg (\phi \rightarrow \psi) \} \vdash \neg \psi$.

Deadline 22 Apr 2020 23:59:59 EST

tertium_non_datur
The theorem to be proved here is tertium non datur, a.k.a. The Law of the Excluded Middle; you will need to prove this: $\vdash \phi \vee \neg \phi$. For some edifying supplementary reading, provided for the motivated, consult the SEP entry on Contradiction. (No deadline for now.)