all

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.

Solve

**Deadline ** 21 Feb 2020 17:00:00 EST

Solve

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:

- 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.

- 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

Solve

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.

Solve

**Deadline ** 22 Apr 2020 23:59:00 EST

Solve

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.)

Solve

Solve

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.)

Solve

Solve

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.)

Solve

Solve

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.)

Solve

Solve

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.)

Solve

Solve

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.)

Solve

Solve

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.)

Solve

Solve

Explosion

Here your task is to prove the explosion inference schema/rule
in HyperSlate^{TM}; 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.)

Solve

Solve

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.)

Solve

Solve

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.)

Solve

Solve

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.)

Solve

Solve

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.)

Solve

Solve

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.)

Solve

Solve

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$.

Solve

**Deadline ** 22 Apr 2020 23:59:59 EST

Solve

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$.

Solve

**Deadline ** 22 Apr 2020 23:59:59 EST

Solve

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.)

Solve

Solve