#LyX 1.3 created this file. For more info see http://www.lyx.org/
\lyxformat 221
\textclass article
\begin_preamble
\usepackage{color}
\usepackage{html}
\usepackage{fitch}
\usepackage{ae}
\pagecolor{white}
\end_preamble
\language english
\inputencoding auto
\fontscheme default
\graphics default
\paperfontsize default
\spacing single
\papersize Default
\paperpackage a4
\use_geometry 0
\use_amsmath 0
\use_natbib 0
\use_numerical_citations 0
\paperorientation portrait
\secnumdepth 3
\tocdepth 3
\paragraph_separation indent
\defskip medskip
\quotes_language english
\quotes_times 2
\papercolumns 1
\papersides 1
\paperpagestyle default
\layout Title
Introduction to natural deduction
\layout Author
Daniel Clemente Laboreo
\layout Date
August 2004 (reviewed at May 2005)
\layout Standard
\begin_inset LatexCommand \tableofcontents{}
\end_inset
\layout Section
Before starting...
\layout Standard
This tutorial is available in several languages:
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
htmladdnormallinkfoot{Spanish}{http://www.danielclemente.com/logica/dn.html}
\backslash
htmladdnormallink{(and PDF)}{http://www.danielclemente.com/logica/dn.pdf},
\backslash
htmladdnormallinkfoot{Esperanto}{http://www.danielclemente.com/logica/dn.eo.html}
\backslash
htmladdnormallink{(and PDF)}{http://www.danielclemente.com/logica/dn.eo.pdf},
\backslash
htmladdnormallinkfoot{Catalan}{http://www.danielclemente.com/logica/dn.ca.html}
\backslash
htmladdnormallink{(and PDF)}{http://www.danielclemente.com/logica/dn.ca.pdf}, and
\backslash
htmladdnormallinkfoot{English}{http://www.danielclemente.com/logica/dn.en.html}
\backslash
htmladdnormallink{(and PDF)}{http://www.danielclemente.com/logica/dn.en.pdf}.
\layout Standard
\layout Standard
\end_inset
\layout Standard
Formulas look much nicer in the PDF, but if it's not possible to use it,
then look at the HTML pages.
\layout Subsection
Who am I
\layout Standard
My name is Daniel Clemente Laboreo, I'm 19 years old (in 2004), I live in
Gavà (Barcelona, Spain), and I study Computer Science in the
\emph on
FIB
\emph default
(
\emph on
UPC
\emph default
, Public University of Catalonia).
There, in the subject called
\emph on
ILO
\emph default
(
\emph on
Introduction to logic
\emph default
), is where I was taught this topic.
\layout Subsection
Why do I write this
\layout Standard
Some reasons:
\layout Itemize
There's a big gap in the search
\begin_inset Quotes eld
\end_inset
\emph on
natural deduction
\emph default
\begin_inset Quotes erd
\end_inset
at Google.
I myself needed to study it before the exam, but couldn't find anything
useful which helped me.
There actually existed some tutorials, but no one was good enough (in my
opinion): some were too confusing, others had special characters which
didn't display correctly, and others didn't explain everything (as if everyone
knew all the logic concepts).
So I decided to create this tutorial which I hope it will help someone.
\layout Itemize
It's a topic I like, and can do without much problems.
\layout Itemize
It makes you think.
Maybe it hasn't got a lot of practical uses, but one really has to try
hard and spend some time in order to solve some simple problems.
\layout Itemize
Well, I confess that I wrote this to learn text processing with
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
LaTeX
\end_inset
.
You need some dedication to learn it, but the results make the work be
worth it.
\layout Subsection
Whom is it addressed to
\layout Standard
Principally, to anyone who likes logic, computer science, or mathematics.
Anyone who wants to prepare the university logic subjects will also gain
some useful concepts.
\layout Standard
This doesn't pretend to be a complete course for natural deduction, but
it will continue being an introduction.
When I learn more, I will correct it if necessary, but I won't add more
sections (I would write them on external documents).
\layout Subsection
License
\layout Standard
All the document is
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
htmladdnormallinkfoot{FDL}{http://www.gnu.org/licenses/fdl.html}
\end_inset
(like the GPL from free software, but for documents).
The source code is made with LyX (
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
htmladdnormallinkfoot{dn.en.lyx}{http://www.danielclemente.com/logica/dn.en.lyx}
\end_inset
), and uses the macros
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
htmladdnormallink{fitch.sty}{http://www.danielclemente.com/logica/fitch.sty}
\end_inset
by Johan W.
Klüwer.
I have used the program
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
htmladdnormallink{latex2html}{http://www.danielclemente.com/linux/l2h.html}
\end_inset
(slightly patched) to create the web pages.
\layout Standard
You have the right, among others, to modify it or to translate it to other
languages which you know well, and also to redistribute it, sell it, and
more.
\layout Section
Basic concepts
\layout Standard
In logic one has to be perfectly clear of the meaning of each word.
I will just remember what are and how to read the strange symbols used
in this document.
\layout Subsection
Formalization
\layout Standard
\emph on
To formalize
\emph default
means writing an expression in a standard form which anyone can understand.
\layout Standard
When working with logical algorithms, you can be thinking all the time in
phrases like
\begin_inset Quotes eld
\end_inset
\emph on
If I have a LCD screen but it has too many dead pixels, then I need another
monitor
\emph default
\begin_inset Quotes erd
\end_inset
.
You can, but they are too long.
It's better to represent each action with a letter, and write the phrase
using such letters along with simple words like
\emph on
and
\emph default
,
\emph on
or
\emph default
,
\emph on
not
\emph default
, or
\emph on
then
\emph default
.
\layout Standard
For example, we have this vocabulary:
\layout Standard
\begin_inset Formula $L$
\end_inset
:
\emph on
have a LCD (Liquid Crystal Display) monitor
\layout Standard
\begin_inset Formula $P$
\end_inset
:
\emph on
have all pixels working perfectly, with not too many fused ones
\layout Standard
\begin_inset Formula $M$
\end_inset
:
\emph on
need a new monitor
\layout Standard
The phrase
\begin_inset Quotes eld
\end_inset
\emph on
If I have a LCD screen but it has too many dead pixels, then I need another
monitor
\emph default
\begin_inset Quotes erd
\end_inset
is better expressed by
\begin_inset Quotes eld
\end_inset
\emph on
if
\begin_inset Formula $L$
\end_inset
and not
\begin_inset Formula $P$
\end_inset
, then
\begin_inset Formula $M$
\end_inset
\emph default
\begin_inset Quotes erd
\end_inset
.
\layout Standard
At natural deduction we will only use the version with letters, following
these conditions:
\layout Itemize
The letters (named
\emph on
propositional letters
\emph default
) are uppercase.
\layout Itemize
Normally
\begin_inset Formula $P$
\end_inset
,
\begin_inset Formula $Q$
\end_inset
,
\begin_inset Formula $R$
\end_inset
,
\begin_inset Formula $S$
\end_inset
, ...
are used, but anyone else is allowed.
\layout Itemize
We use some special symbols for the operators
\emph on
and
\emph default
,
\emph on
or
\emph default
,
\emph on
not
\emph default
and
\emph on
implication
\emph default
.
\layout Subsection
Used symbols
\layout Standard
To express the relation between one action and another, there exist some
international icons.
The basic operators you must know are
\begin_inset Formula $\vee$
\end_inset
,
\begin_inset Formula $\wedge$
\end_inset
,
\begin_inset Formula $\neg$
\end_inset
,
\begin_inset Formula $\Rightarrow$
\end_inset
.
The others are more complex, but here I put all of them as a reference,
to be able to find them if you were searching any of them.
\layout Standard
\begin_inset Tabular
\begin_inset Text
\layout Standard
\series bold
Symbol
\end_inset

\begin_inset Text
\layout Standard
\series bold
It's read...
\end_inset

\begin_inset Text
\layout Standard
\series bold
Description
\end_inset

\begin_inset Text
\layout Standard
\begin_inset Formula $\vee$
\end_inset
\end_inset

\begin_inset Text
\layout Standard
\emph on
or
\end_inset

\begin_inset Text
\layout Standard
\begin_inset Formula $A\vee B$
\end_inset
is true whenever one of the two, or both, are true.
\end_inset

\begin_inset Text
\layout Standard
\begin_inset Formula $\wedge$
\end_inset
\end_inset

\begin_inset Text
\layout Standard
\emph on
and
\end_inset

\begin_inset Text
\layout Standard
To make
\begin_inset Formula $A\wedge B$
\end_inset
true, both
\begin_inset Formula $A$
\end_inset
and
\begin_inset Formula $B$
\end_inset
have to be true.
\end_inset

\begin_inset Text
\layout Standard
\begin_inset Formula $\neg$
\end_inset
\end_inset

\begin_inset Text
\layout Standard
\emph on
not
\end_inset

\begin_inset Text
\layout Standard
\begin_inset Formula $\neg A$
\end_inset
only is true when
\begin_inset Formula $A$
\end_inset
is false.
\end_inset

\begin_inset Text
\layout Standard
\begin_inset Formula $\Rightarrow$
\end_inset
\end_inset

\begin_inset Text
\layout Standard
\emph on
implies
\end_inset

\begin_inset Text
\layout Standard
Shows consequence.
The expression
\begin_inset Formula $A\Rightarrow B$
\end_inset
says that when
\begin_inset Formula $A$
\end_inset
holds, so does
\begin_inset Formula $B$
\end_inset
.
In addition,
\begin_inset Formula $A\Rightarrow B$
\end_inset
is considered true except for the case
\begin_inset Formula $A$
\end_inset
true and
\begin_inset Formula $B$
\end_inset
false.
To understand that, think of an
\begin_inset Formula $A$
\end_inset
which implies
\begin_inset Formula $B$
\end_inset
and ask yourself:
\emph on
is it possible that
\begin_inset Formula $A$
\end_inset
is true but not
\begin_inset Formula $B$
\end_inset
?
\emph default
Anyway, don't worry about that, it's not important right now.
\end_inset

\begin_inset Text
\layout Standard
\begin_inset Formula $\Longleftrightarrow$
\end_inset
\end_inset

\begin_inset Text
\layout Standard
\emph on
if and only if
\end_inset

\begin_inset Text
\layout Standard
\begin_inset Formula $A\Longleftrightarrow B$
\end_inset
is the same as
\begin_inset Formula $(A\Rightarrow B)\wedge(B\Rightarrow A)$
\end_inset
.
It means that from
\begin_inset Formula $A$
\end_inset
we can deduce
\begin_inset Formula $B$
\end_inset
and viceversa, so they are equivalent.
\end_inset

\begin_inset Text
\layout Standard
\begin_inset Formula $\square$
\end_inset
\end_inset

\begin_inset Text
\layout Standard
\emph on
false
\end_inset

\begin_inset Text
\layout Standard
The empty square represents
\emph on
false
\emph default
(the binary
\emph on
0
\emph default
).
Technically, it represents
\begin_inset Formula $\{\}$
\end_inset
.
\end_inset

\begin_inset Text
\layout Standard
\begin_inset Formula $\blacksquare$
\end_inset
\end_inset

\begin_inset Text
\layout Standard
\emph on
true
\end_inset

\begin_inset Text
\layout Standard
The filled square represents
\emph on
true
\emph default
(the binary
\emph on
1
\emph default
).
Technically, it represents
\begin_inset Formula $\{<>\}$
\end_inset
.
\end_inset

\begin_inset Text
\layout Standard
\begin_inset Formula $\exists$
\end_inset
\end_inset

\begin_inset Text
\layout Standard
\emph on
exists...
\end_inset

\begin_inset Text
\layout Standard
\begin_inset Formula $\exists xPx$
\end_inset
can be read
\emph on
there exists an
\begin_inset Formula $x$
\end_inset
such that
\begin_inset Formula $P$
\end_inset
of
\begin_inset Formula $x$
\end_inset
\emph default
.
If in our domain, we can find an element (or more) which makes true the
property
\begin_inset Formula $P$
\end_inset
applied to that element, then the formula is true.
\end_inset

\begin_inset Text
\layout Standard
\begin_inset Formula $\forall$
\end_inset
\end_inset

\begin_inset Text
\layout Standard
\emph on
for all...
\end_inset

\begin_inset Text
\layout Standard
\begin_inset Formula $\forall xPx$
\end_inset
can be read
\emph on
for all
\begin_inset Formula $x$
\end_inset
,
\begin_inset Formula $P$
\end_inset
of
\begin_inset Formula $x$
\end_inset
\emph default
.
If all elements we are working with make the property
\begin_inset Formula $P$
\end_inset
become true, then the formula is true.
\end_inset

\begin_inset Text
\layout Standard
\begin_inset Formula $\vdash$
\end_inset
\end_inset

\begin_inset Text
\layout Standard
\emph on
then
\end_inset

\begin_inset Text
\layout Standard
\begin_inset Formula $\vdash$
\end_inset
is the symbol of the
\emph on
sequent
\emph default
, which is the way of saying
\begin_inset Quotes eld
\end_inset
\emph on
when all this from the left happens, then it also happens all this from
the right
\emph default
\begin_inset Quotes erd
\end_inset
.
There exist valid sequents, like
\begin_inset Formula $P\wedge Q\vdash P$
\end_inset
or like
\begin_inset Formula $P\Rightarrow Q,\ Q\Rightarrow R,\ P\vdash P\wedge R$
\end_inset
.
But there are also invalid ones, like
\begin_inset Formula $P\Rightarrow Q,\ \neg P\vdash\neg Q$
\end_inset
.
The objective of natural deduction is to prove that a sequent is valid.
\end_inset

\begin_inset Text
\layout Standard
\begin_inset Formula $\vDash$
\end_inset
\end_inset

\begin_inset Text
\layout Standard
\emph on
valid
\end_inset

\begin_inset Text
\layout Standard
\begin_inset Formula $\phi\vDash\varphi$
\end_inset
means that
\begin_inset Formula $\varphi$
\end_inset
is logical consequence of
\begin_inset Formula $\phi$
\end_inset
, but when one writes
\begin_inset Formula $A\vDash B$
\end_inset
, what we mean is that the sequent
\begin_inset Formula $A\vdash B$
\end_inset
is valid, that is, we could somehow prove it, and now is considered true
for any interpretation of the predicate symbols.
\end_inset

\begin_inset Text
\layout Standard
\begin_inset Formula $\nvDash$
\end_inset
\end_inset

\begin_inset Text
\layout Standard
\emph on
invalid
\end_inset

\begin_inset Text
\layout Standard
\begin_inset Formula $\phi\nvDash\varphi$
\end_inset
means that
\begin_inset Formula $\varphi$
\end_inset
is not logical consequence of
\begin_inset Formula $\phi$
\end_inset
.
If you can find a series of values (
\emph on
model
\emph default
) which make
\begin_inset Formula $\phi$
\end_inset
true but
\begin_inset Formula $\varphi$
\end_inset
false, then invalidity is proven.
\end_inset

\begin_inset Text
\layout Standard
\begin_inset Formula $\Vdash$
\end_inset
\end_inset

\begin_inset Text
\layout Standard
\emph on
satisfiable
\end_inset

\begin_inset Text
\layout Standard
A set of formulas is satisfiable if there exists a series of values (
\emph on
model
\emph default
) which can make all of them true at the same time.
\end_inset

\begin_inset Text
\layout Standard
\begin_inset Formula $\nVdash$
\end_inset
\end_inset

\begin_inset Text
\layout Standard
\emph on
unsatisfiable
\end_inset

\begin_inset Text
\layout Standard
A set of formulas is unsatisfiable if there isn't any combination of variables
(
\emph on
model
\emph default
) which can make all of them become true at the same time.
\end_inset

\end_inset
\layout Subsection
Precedence of operators
\layout Standard
When you see an expression, you must be able to recognise what is it.
For instance,
\begin_inset Formula $A\vee B\Rightarrow C$
\end_inset
is an implication (not a disjunction!), because
\begin_inset Formula $\Rightarrow$
\end_inset
is evaluated last (it has lower priority than
\begin_inset Formula $\vee$
\end_inset
).
\layout Standard
Here there are the operators, inversely sorted by priority:
\layout Itemize
\begin_inset Formula $\Longleftrightarrow$
\end_inset
\layout Itemize
\begin_inset Formula $\Rightarrow$
\end_inset
\layout Itemize
\begin_inset Formula $\vee$
\end_inset
and
\begin_inset Formula $\wedge$
\end_inset
(they have the same priority)
\layout Itemize
\begin_inset Formula $\neg$
\end_inset
\layout Standard
This means that
\begin_inset Formula $\neg$
\end_inset
is the one that most
\begin_inset Quotes eld
\end_inset
\emph on
sticks
\emph default
\begin_inset Quotes erd
\end_inset
to the symbol it has next.
See this example about when and where are needed the parenthesis:
\layout Standard
\begin_inset Formula $P\vee\neg Q\Rightarrow R\wedge P\Longleftrightarrow\neg(R\vee S)\wedge A\Rightarrow B$
\end_inset
is the same as
\begin_inset Formula $(\ (P\vee(\neg Q))\ \Rightarrow\ (R\wedge P)\ )\Longleftrightarrow(\ ((\neg(R\vee S))\wedge A)\Rightarrow B\ )$
\end_inset
\layout Standard
But don't panic, I won't use again expressions that long.
\layout Section
Natural deduction
\layout Standard
Now I must explain what it is, how can it be done, and whether it has any
practical use.
\layout Subsection
What it is for
\layout Standard
Natural deduction is used to try to prove that some reasoning is correct
(
\begin_inset Quotes eld
\end_inset
\emph on
to check the validity of a sequent
\emph default
\begin_inset Quotes erd
\end_inset
, says theory).
Example:
\layout Standard
I tell you:
\begin_inset Quotes eld
\end_inset
\emph on
In summer it's warm, and now we're in summer, so now it's warm
\emph default
\begin_inset Quotes erd
\end_inset
.
You start doing calculations, and finally reply:
\begin_inset Quotes eld
\end_inset
\emph on
OK, I can prove that the reasoning you just made is correct
\emph default
\begin_inset Quotes erd
\end_inset
.
That is the use of natural deduction.
\layout Standard
But it's not always so easy:
\begin_inset Quotes eld
\end_inset
\emph on
if you fail a subject, you must repeat it.
And if you don't study it, you fail it.
Now suppose that you aren't repeating it.
Then, or you study it, or you are failing it, or both of them
\emph default
\begin_inset Quotes erd
\end_inset
.
This reasoning is valid and can be proven with natural deduction.
\layout Standard
Remark that you don't have to believe nor understand what you are told.
For example, I say that:
\begin_inset Quotes eld
\end_inset
\emph on
Thyristors are tiny and funny; a pea is not tiny, so it isn't a thyristor
\emph default
\begin_inset Quotes erd
\end_inset
.
Even if you don't know what am I talking about, or think that it is stupid
(which it really is), you must be completely sure that the reasoning was
correct.
\layout Standard
So, given a supposition
\begin_inset Quotes eld
\end_inset
\emph on
if all this happens, then all that also happens
\emph default
\begin_inset Quotes erd
\end_inset
, natural deduction allows us to say
\begin_inset Quotes eld
\end_inset
\emph on
yes, that's right
\emph default
\begin_inset Quotes erd
\end_inset
.
In logical language: if you are given a sequent
\begin_inset Formula $A\vdash B$
\end_inset
, you can conclude at the end that it is
\begin_inset Formula $\vDash$
\end_inset
(
\emph on
valid
\emph default
).
Then we write
\begin_inset Formula $A\vDash B$
\end_inset
(
\begin_inset Formula $A$
\end_inset
has as consequence
\begin_inset Formula $B$
\end_inset
).
\layout Subsection
What it is not for
\layout Standard
It isn't suitable for proving
\emph on
invalidity
\emph default
of some supposition.
I might say
\begin_inset Quotes eld
\end_inset
\emph on
at daytime, it isn't night; and now it's daytime, so now it's also night
\emph default
\begin_inset Quotes erd
\end_inset
and you may pass some time trying the rules of natural deduction, but obtaining
nothing useful.
After some time, you will intuitively discover that the reasoning might
not be valid, and it's then when another methods not natural deduction
should be tried in order to prove invalidity.
They are explained later.
\layout Standard
So, natural deduction only serves for proving validity, but not invalidity.
What a pity, isn't it?
\layout Standard
Neither does it serve to provide a good answer to the question
\begin_inset Quotes eld
\end_inset
\emph on
What would happen if...?
\emph default
\begin_inset Quotes erd
\end_inset
.
When we are to prove the validity of
\begin_inset Formula $A\vdash B$
\end_inset
, we must think of things that would happen if
\begin_inset Formula $A$
\end_inset
happened, and if we discover that one of these things is
\begin_inset Formula $B$
\end_inset
, then we have finished.
But we will never be able to give a complete and finite list of all those
things.
\layout Subsection
Functioning
\layout Standard
We are asked to prove the validity of
\begin_inset Formula $\Gamma\vdash S$
\end_inset
, where
\begin_inset Formula $\Gamma$
\end_inset
(that's
\emph on
gamma
\emph default
) is a group of formulas separated by commas, and
\begin_inset Formula $S$
\end_inset
is a single formula.
\layout Standard
We start assuming that all formulas in
\begin_inset Formula $\Gamma$
\end_inset
are true, and, by continuous application of 9 concrete rules, we can go
on discovering which other things are true.
Our intention is to discover that
\begin_inset Formula $S$
\end_inset
is true; so once we achieve that, we can stop working.
\layout Standard
Sometimes we won't be able to extract truths from anywhere, and we will
have to make suppositions:
\begin_inset Quotes eld
\end_inset
\emph on
well, I'm not sure that
\begin_inset Formula $A\wedge B$
\end_inset
is always true, but if it holds that
\begin_inset Formula $C$
\end_inset
, then it surely will be
\emph default
\begin_inset Quotes erd
\end_inset
.
Then we have just discovered another truth: that
\begin_inset Formula $C\Rightarrow A\wedge B$
\end_inset
.
\layout Standard
As you can see, one has always to be thinking in where do we want to head
to, because otherwise we could discover lots of things which are indeed
true, but which we don't need at all.
For instance, with
\begin_inset Formula $A\vee B,\ \neg A\vdash B$
\end_inset
we have to achieve the truth of
\begin_inset Formula $B$
\end_inset
.
We may discover that
\begin_inset Formula $\neg(A\wedge B)$
\end_inset
,
\begin_inset Formula $A\vee B\vee C$
\end_inset
,
\begin_inset Formula $(A\vee B)\Rightarrow\neg A$
\end_inset
, and several other formulas, but what we really are interested in is
\begin_inset Formula $B$
\end_inset
and nothing else.
So, if you aren't following the right way towards the solution, you can
make a mess.
\layout Subsection
Notation
\layout Standard
There exist several ways to write the derivations done with natural deduction.
I will use the Fitch style, because it's the one I used when learning,
it's easy to understand, and occupies little space.
It's something like this:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
P
\backslash
Rightarrow Q
\backslash
\backslash
\layout Standard
Q
\backslash
Rightarrow R
\backslash
\backslash
\layout Standard
\backslash
fh P & H
\backslash
\backslash
\layout Standard
\backslash
fa Q & E$
\backslash
Rightarrow$ 1,3
\backslash
\backslash
\layout Standard
\backslash
fa R & E$
\backslash
Rightarrow$ 2,4
\backslash
\backslash
\layout Standard
\backslash
fa Q
\backslash
wedge R & I$
\backslash
wedge$ 4,5
\backslash
\backslash
\layout Standard
P
\backslash
Rightarrow Q
\backslash
wedge R & I$
\backslash
Rightarrow$ 3,6
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Standard
This is sufficient to prove the validity of
\begin_inset Formula $P\Rightarrow Q,\ Q\Rightarrow R\vdash P\Rightarrow Q\wedge R$
\end_inset
.
\layout Standard
That figure is to be done line by line, from top to the bottom.
The numbers from the left show the number of each line, and are always
in natural order.
\layout Standard
The first lines contain each of the formulas which are written in the left
part of the sequent.
In this case, they are two:
\begin_inset Formula $P\Rightarrow Q$
\end_inset
and
\begin_inset Formula $Q\Rightarrow R$
\end_inset
.
From these we will have to achieve the formula
\begin_inset Formula $P\Rightarrow Q\wedge R$
\end_inset
.
\layout Standard
On each line we write what new thing we have just discovered to be true,
and to the right we note how did we discover that.
Those symbols from the right side (
\begin_inset Formula $E$
\end_inset
and
\begin_inset Formula $I$
\end_inset
) are the abbreviations of the names of the 9 rules.
For example, here we can see
\emph on
implication elimination
\emph default
(
\begin_inset Formula $E\Rightarrow$
\end_inset
),
\emph on
conjunction introduction
\emph default
(
\begin_inset Formula $I\wedge$
\end_inset
), and
\emph on
implication introduction
\emph default
(
\begin_inset Formula $I\Rightarrow$
\end_inset
).
The numbers that go with them give us information about from where did
we extract each necessary formula which is needed to apply the rule.
They are line numbers, so, to be able to apply a rule, one has to use informati
on only from the lines already written.
\layout Standard
Finally, that vertical line which goes from line 3 to 6 it's a hypothesis
(that's why we put
\begin_inset Formula $H$
\end_inset
to the right).
Everything which is inside it, is not always true, but only when happens
\begin_inset Formula $P$
\end_inset
(the heading of the hypothesis, at line 3).
So, all of the work we do inside the hypothesis cannot be used outside
it, because it can't be assured to be always true.
\layout Standard
The procedure finishes when we discover that it's true the formula at the
right side of the sequent, in this case
\begin_inset Formula $P\Rightarrow Q\wedge R$
\end_inset
(it appears at the last line).
\layout Section
The derivation rules
\layout Standard
Here they are defined and explained the nine basic rules which are used
in natural deduction.
Their objective is to tell us when and how can we add new formulas which
continue being true.
\layout Standard
Some examples (explained) are in the next section.
\layout Subsection
Iteration
\layout Standard
This is a very simple rule:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch*}
\layout Standard
n & A
\backslash
\backslash
\layout Standard
\backslash
hline
\layout Standard
& A & IT n
\layout Standard
\backslash
end{fitch*}
\backslash
]
\end_inset
\layout Standard
Well, I know, written like this is a bit strange, but I put it this way
to make it useful as the definition of the rule.
What is contained in the above formulation is that if on line number
\begin_inset Formula $n$
\end_inset
we have written
\begin_inset Formula $A$
\end_inset
(whatever expression it is) then we have the option to write again
\begin_inset Formula $A$
\end_inset
, but in the current line, and to justify that, we must write at the right
\begin_inset Formula $IT\ n$
\end_inset
.
\layout Standard
So, why would we want that? Well, for the moment, for nothing, but it will
have its utility when we start working with hypothesis.
Since a hypothesis is
\emph on
closed
\emph default
, all rules will have to work with formulas inside the hypothesis.
If one of the formulas we want is just outside this hypothesis, we can
copy it herein by using this rule called
\emph on
iteration
\emph default
.
\layout Standard
Some people think that it's not necessary to waste a line this way, but
it's a lot clearer when this rule is used.
What isn't allowed is using it only to
\begin_inset Quotes eld
\end_inset
\emph on
bring nearer
\emph default
\begin_inset Quotes erd
\end_inset
some formula which is several lines far away: it isn't necessary to rewrite
a line if we have it already written in the current derivation.
\layout Subsection
Conjunction introduction
\layout Standard
The conjunction (that's the
\emph on
and
\emph default
) can be created easily:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch*}
\layout Standard
m & A
\backslash
\backslash
\layout Standard
n & B
\backslash
\backslash
\layout Standard
\backslash
hline
\layout Standard
& A
\backslash
wedge B & I$
\backslash
wedge$ m,n
\layout Standard
\backslash
end{fitch*}
\backslash
]
\end_inset
\layout Standard
You should be able to understand the meaning of figures like this one.
When we put a long horizontal line, normally it's to separate the
\emph on
premises
\emph default
(top) from the
\emph on
conclusion
\emph default
(bottom).
Premises are conditions which must be fulfilled in order to apply the rule,
and conclusion (or
\emph on
resolvent
\emph default
) is the result of the application of the rule.
\layout Standard
This rule says that if on one line we have written a truth, and on another
line we have another one, also true, then we can write in just a line that
both things are true.
We must then note to the right the lines from where we picked the first
and the second formulas.
\layout Standard
This is pretty logic, isn't it? if we know that really
\emph on
it's raining
\emph default
, and that it's true that
\emph on
now it's sunny
\emph default
, then there's no problem in saying that
\emph on
it's raining and sunny
\emph default
(yes, at the same time).
If something feels strange, it's not our fault; blame the one who told
us that
\emph on
it's raining
\emph default
or
\emph on
it's sunny
\emph default
.
\layout Standard
Remark that picking the lines reversed, you can obtain
\begin_inset Formula $B\wedge A$
\end_inset
, and picking the same line you can achieve
\begin_inset Formula $A\wedge A$
\end_inset
and
\begin_inset Formula $B\wedge B$
\end_inset
, which are also true.
\layout Subsection
Conjunction elimination
\layout Standard
This is just the inverse operation of the previous one.
It has two parts; firstly:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch*}
\layout Standard
n & A
\backslash
wedge B
\backslash
\backslash
\layout Standard
\backslash
hline
\layout Standard
& A & E$
\backslash
wedge$ n
\layout Standard
\backslash
end{fitch*}
\backslash
]
\end_inset
\layout Standard
And secondly, for the case you wanted
\begin_inset Formula $B$
\end_inset
:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch*}
\layout Standard
n & A
\backslash
wedge B
\backslash
\backslash
\layout Standard
\backslash
hline
\layout Standard
& B & E$
\backslash
wedge$ n
\layout Standard
\backslash
end{fitch*}
\backslash
]
\end_inset
\layout Standard
So, you can separate in several lines the
\emph on
conjunctands
\emph default
of a conjunction (yes, I think it's used that strange word).
That's why this rule is called
\emph on
conjunction elimination
\emph default
, because from one line which has conjunction symbols (
\begin_inset Formula $\wedge$
\end_inset
) you can extract several which don't have it, supposedly trying to approach
to the formula which we want proved.
\layout Subsection
Implication introduction
\layout Standard
This is more interesting, since it allows doing something useful with hypothesis
(those subdemonstrations which have a vertical bar to the left).
It's:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch*}
\layout Standard
m &
\backslash
fh A & H
\backslash
\backslash
\layout Standard
n &
\backslash
fa B
\backslash
\backslash
\layout Standard
\backslash
hline
\layout Standard
& A
\backslash
Rightarrow B & I$
\backslash
Rightarrow$ m,n
\layout Standard
\backslash
end{fitch*}
\backslash
]
\end_inset
\layout Standard
And what it does mean is that if we supposed something (call it
\begin_inset Formula $A$
\end_inset
), and we just discovered (by using the rules) that supposing
\begin_inset Formula $A$
\end_inset
made true
\begin_inset Formula $B$
\end_inset
(whatever it is), then we have something clear: we can't assure that
\begin_inset Formula $B$
\end_inset
always is true, but we can assure that
\begin_inset Formula $A$
\end_inset
implies
\begin_inset Formula $B$
\end_inset
, which is written
\begin_inset Formula $A\Rightarrow B$
\end_inset
.
\layout Standard
This allows us to end the subdemonstration and continue working with what
we were doing before.
Remember that you can't finish natural deduction inside a subdemonstration.
\layout Subsection
Implication elimination
\layout Standard
This one is simpler than the previous, since it does not deal with suppositions
but with facts:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch*}
\layout Standard
m & A
\backslash
Rightarrow B
\backslash
\backslash
\layout Standard
n & A
\backslash
\backslash
\layout Standard
\backslash
hline
\layout Standard
& B & E$
\backslash
Rightarrow$ m,n
\layout Standard
\backslash
end{fitch*}
\backslash
]
\end_inset
\layout Standard
Simply, if we are told that when
\begin_inset Formula $A$
\end_inset
also happens
\begin_inset Formula $B$
\end_inset
(that's what it means
\begin_inset Formula $A\Rightarrow B$
\end_inset
), and they also tell us that now happens
\begin_inset Formula $A$
\end_inset
, then we can assure that
\begin_inset Formula $B$
\end_inset
.
\layout Standard
This rule is also named
\emph on
modus ponens
\emph default
.
\layout Subsection
Disjunction introduction
\layout Standard
The disjunction (that's the
\emph on
or
\emph default
) is very easy but not obvious:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch*}
\layout Standard
n & A
\backslash
\backslash
\layout Standard
\backslash
hline
\layout Standard
& A
\backslash
vee B & I$
\backslash
vee$ n
\layout Standard
\backslash
end{fitch*}
\backslash
]
\end_inset
\layout Standard
Well, to be exact, I will say that it's also available in the other order:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch*}
\layout Standard
n & A
\backslash
\backslash
\layout Standard
\backslash
hline
\layout Standard
& B
\backslash
vee A & I$
\backslash
vee$ n
\layout Standard
\backslash
end{fitch*}
\backslash
]
\end_inset
\layout Standard
That's wonderful, isn't it? If we know that
\begin_inset Quotes eld
\end_inset
\emph on
it's Thursday
\emph default
\begin_inset Quotes erd
\end_inset
we also know that
\begin_inset Quotes eld
\end_inset
\emph on
it's Thursday or cows can fly
\emph default
\begin_inset Quotes erd
\end_inset
,
\begin_inset Quotes eld
\end_inset
\emph on
it's Thursday or Friday
\emph default
\begin_inset Quotes erd
\end_inset
, or even
\begin_inset Quotes eld
\end_inset
\emph on
it's Thursday...
or not
\emph default
\begin_inset Quotes erd
\end_inset
.
All of them are true.
\layout Standard
But remember that, when talking, we tend to use
\emph on
exclusive or
\emph default
(
\emph on
XOR
\emph default
), which is true if one of the
\emph on
disjunctands
\emph default
is true but not when both of them are true at the same time.
To a logician, the common phrase
\begin_inset Quotes eld
\end_inset
\emph on
it's Thursday or Friday
\emph default
\begin_inset Quotes erd
\end_inset
holds true under three situations: when
\emph on
it's Thursday
\emph default
, when
\emph on
it's Friday
\emph default
, and when
\emph on
it's Thursday and Friday at the same time
\emph default
(something difficult in the real world, but mathematicians are capable
of doing all types of suppositions...).
\layout Subsection
Disjunction elimination
\layout Standard
This is the most complicated rule, mainly because if we are given a phrase
with
\emph on
or
\emph default
, like
\begin_inset Quotes eld
\end_inset
\emph on
it's Thursday or Friday
\emph default
\begin_inset Quotes erd
\end_inset
, what can we deduce from it? That
\emph on
it's Thursday
\emph default
? No, it may be Friday.
That
\emph on
it's Friday
\emph default
? No, it may be Thursday.
That
\emph on
it's Thursday or Friday
\emph default
? Well, yes, but we already knew that...
\layout Standard
The rule (now I explain it):
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch*}
\layout Standard
m & A
\backslash
vee B
\backslash
\backslash
\layout Standard
&
\backslash
fh A & H
\backslash
\backslash
\layout Standard
n &
\backslash
fa C
\backslash
\backslash
\layout Standard
&
\backslash
fh B & H
\backslash
\backslash
\layout Standard
p &
\backslash
fa C
\backslash
\backslash
\layout Standard
\backslash
hline
\layout Standard
& C & E$
\backslash
vee$ m,n,p
\layout Standard
\backslash
end{fitch*}
\backslash
]
\end_inset
\layout Standard
We need more information besides the
\begin_inset Formula $A\vee B$
\end_inset
.
If, luckily, we happen to know
\begin_inset Formula $A\Rightarrow C$
\end_inset
, and also
\begin_inset Formula $B\Rightarrow C$
\end_inset
, then we do know what happens when
\begin_inset Formula $A\vee B$
\end_inset
: both one option and the other drive us to
\begin_inset Formula $C$
\end_inset
, so
\begin_inset Formula $C$
\end_inset
is true.
\layout Standard
This type of things only happen when the exercise is prepared so that the
\emph on
disjunction elimination
\emph default
appears, or when
\begin_inset Formula $A$
\end_inset
and
\begin_inset Formula $B$
\end_inset
are similar (then we will find some
\begin_inset Formula $C$
\end_inset
which is implied by both).
\layout Standard
Now an example: when I contracted my ADSL access to the Internet, it was
with
\emph on
Telefónica
\emph default
or
\emph on
Terra
\emph default
, but I'm not sure of with which one (even they didn't know it).
And in my country (Spain), any option was slow, awfully expensive, and
loaded with problems.
Typical Spanish.
If we call all those
\emph on
features
\emph default
\begin_inset Formula $M$
\end_inset
(for mockery, misery, ...), then basically any Internet Service Provider was
an
\begin_inset Formula $M$
\end_inset
.
Concretely,
\begin_inset Formula $Telefonica\Rightarrow M$
\end_inset
and
\begin_inset Formula $Terra\Rightarrow M$
\end_inset
, so undoubtedly my ADSL had to be
\begin_inset Formula $M$
\end_inset
, both if I had one or the other ISP.
And indeed, I needed 9 months to fully subscribe to the service...
Luckily all this happened now several years ago.
\layout Standard
This derivation rule is also called
\emph on
proof by cases
\emph default
, since we have to check each possible case to see that they all involve
the same conclusion.
\layout Subsection
Negation introduction
\layout Standard
This one is nice and interesting:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch*}
\layout Standard
m &
\backslash
fh A & H
\backslash
\backslash
\layout Standard
n &
\backslash
fa B
\backslash
\backslash
\layout Standard
p &
\backslash
fa
\backslash
neg B
\backslash
\backslash
\layout Standard
\backslash
hline
\layout Standard
&
\backslash
neg A & I$
\backslash
neg$ m,n,p
\layout Standard
\backslash
end{fitch*}
\backslash
]
\end_inset
\layout Standard
If after supposing
\begin_inset Formula $A$
\end_inset
, you achieved the conclusion that both
\begin_inset Formula $B$
\end_inset
and
\begin_inset Formula $\neg B$
\end_inset
are true, you're not lost, since you just discovered another truth: that
it's not possible for
\begin_inset Formula $A$
\end_inset
to be true, that's it,
\begin_inset Formula $\neg A$
\end_inset
it's true.
\layout Standard
For instance, I confess that
\emph on
if I use Windows, I don't profit the time I am with my computer
\emph default
.
Since some years,
\emph on
I do profit it
\emph default
, so the conclusion is that
\emph on
I don't use Windows
\emph default
.
To achieve that conclusion, the path that you would follow (maybe without
thinking) is precisely the one that this rule needs: suppose that
\emph on
I do use Windows
\emph default
, in that case
\emph on
I wouldn't profit my computer
\emph default
.
But I said that
\emph on
I do profit it
\emph default
, so that supposition must be wrong.
\layout Standard
This procedure is called
\emph on
reduction to the absurd
\emph default
(
\emph on
reductio ad absurdum
\emph default
): suppose something to achieve a contradiction and be able to assert that
what we supposed is false.
It's specially useful if you start supposing
\emph on
the contrary
\emph default
of what you want to prove: if any contradiction can be discovered, then
it's almost all done.
\layout Standard
I should note that this is an
\emph on
abuse of notation
\emph default
: following all the laws of logic, it happens that each subdemonstration
needs
\emph on
one
\emph default
conclusion (not two); and at the above hypothesis, it's not clear which
one is the conclusion (
\begin_inset Formula $B$
\end_inset
or
\begin_inset Formula $\neg B$
\end_inset
?).
The correct way to write it would be using
\emph on
conjunction introduction
\emph default
to say that
\begin_inset Formula $B\wedge\neg B$
\end_inset
, and this one is the conclusion which shows the wrongness of the initial
hypothesis.
But my teachers didn't write that line.
\layout Subsection
Negation elimination
\layout Standard
This one is too simple, but we also have to know it:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch*}
\layout Standard
n &
\backslash
neg
\backslash
neg A
\backslash
\backslash
\layout Standard
\backslash
hline
\layout Standard
& A & E$
\backslash
neg$ n
\layout Standard
\backslash
end{fitch*}
\backslash
]
\end_inset
\layout Standard
So, when we see the negation of the negation of something, we can take off
these two following negations.
\layout Standard
Remember that the negation of
\begin_inset Quotes eld
\end_inset
\emph on
this is white
\emph default
\begin_inset Quotes erd
\end_inset
is not
\begin_inset Quotes eld
\end_inset
\emph on
this is black
\emph default
\begin_inset Quotes erd
\end_inset
but
\begin_inset Quotes eld
\end_inset
\emph on
this is not white
\emph default
\begin_inset Quotes erd
\end_inset
.
\layout Subsection
No more rules
\layout Standard
That's it, there are no more basic rules.
Well, there still exist some more to deal with
\emph on
quantifiers
\emph default
and two about
\emph on
true
\emph default
and
\emph on
false
\emph default
, which I will explain later, but with the former 9 we're able to try to
prove the validity of any sequent in this document (except the ones with
quantifiers...).
\layout Standard
Remember again that there are no more rules: you can't change from
\begin_inset Formula $A\vee\neg A$
\end_inset
to
\begin_inset Formula $\blacksquare$
\end_inset
(
\emph on
true
\emph default
) directly, or from
\begin_inset Formula $\neg(A\vee B)$
\end_inset
to
\begin_inset Formula $\neg A\wedge\neg B$
\end_inset
, nor use the distributive, associative or commutative property.
You have to proceed always step by step; even the simple changes aren't
allowed (currently).
Why? Because probably they aren't that simple: you will understand it when
having to prove things like that
\begin_inset Formula $A\vee\neg A$
\end_inset
is always true...
(it's in the next section).
\layout Section
Explained exercises
\layout Standard
Exercises from several levels, explained step by step.
If you still want more examples (but without comments) look into the last
section.
What I'm trying to explain here is not the rules, but the way of thinking
so that you can devise the magic idea which solves the problem.
\layout Standard
This is what I more lacked when I had to study natural deduction.
\layout Subsection
A very simple one.
\begin_inset Formula $P,\ P\Rightarrow Q\vdash P\wedge Q$
\end_inset
\layout Standard
The solution to
\begin_inset Formula $P,\ P\Rightarrow Q\vdash P\wedge Q$
\end_inset
is:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
P
\backslash
\backslash
\layout Standard
P
\backslash
Rightarrow Q
\backslash
\backslash
\layout Standard
Q & E$
\backslash
Rightarrow$ 2,1
\backslash
\backslash
\layout Standard
P
\backslash
wedge Q & I$
\backslash
wedge$ 1,3
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Standard
Here we won't have to think much, we just have to use correctly the rules
and their justifications.
\layout Standard
Firstly, understand what has been told to us: they say that now happen
\emph on
two
\emph default
things, the first is that
\begin_inset Formula $P$
\end_inset
and the second is that
\begin_inset Formula $P\Rightarrow Q$
\end_inset
(they are the two formulas written to the left of the
\begin_inset Formula $\vdash$
\end_inset
).
These two things we will note, one on each line, since at this demonstration
they will always be true (liking it or not).
\layout Standard
The goal of this demonstration is to know that
\begin_inset Formula $P\wedge Q$
\end_inset
is also true, as we have been told that when
\begin_inset Formula $P$
\end_inset
and
\begin_inset Formula $P\Rightarrow Q$
\end_inset
are true, then
\begin_inset Formula $P\wedge Q$
\end_inset
also is, and we want to check if that's right.
Finally we achieved it, since on the last line we see the
\begin_inset Formula $P\wedge Q$
\end_inset
written.
\layout Standard
But how do we start? Remember where do we want to head to.
If
\begin_inset Formula $P\wedge Q$
\end_inset
has to be true, then both
\begin_inset Formula $P$
\end_inset
and
\begin_inset Formula $Q$
\end_inset
should be true; let's attempt to prove that they really are.
\layout Standard
\begin_inset Formula $P$
\end_inset
is true, since they said so, and we have it written on line 1.
\layout Standard
But we weren't told that
\begin_inset Formula $Q$
\end_inset
was true.
What do we know about
\begin_inset Formula $Q$
\end_inset
? Searching it on lines 1 and 2, the only we know about
\begin_inset Formula $Q$
\end_inset
is that it's true when happens
\begin_inset Formula $P$
\end_inset
(that's what says line 2).
But
\begin_inset Formula $P$
\end_inset
is true, so we can use one of the rules to deduce
\begin_inset Formula $Q$
\end_inset
from the
\begin_inset Formula $P\Rightarrow Q$
\end_inset
and
\begin_inset Formula $P$
\end_inset
.
Remark what is the most important change when we go from
\begin_inset Formula $P\Rightarrow Q$
\end_inset
to
\begin_inset Formula $Q$
\end_inset
: we stopped using the implication symbol; so the rule we will need is the
one called
\emph on
implication elimination
\emph default
.
\layout Standard
To use this rule, we look at its definition, and see that we have to write
in a new line
\begin_inset Formula $Q$
\end_inset
, and as a justification
\begin_inset Formula $E\Rightarrow\ 2,1$
\end_inset
needs to be written.
The
\begin_inset Formula $E$
\end_inset
is from
\emph on
elimination
\emph default
, the
\begin_inset Formula $\Rightarrow$
\end_inset
means
\emph on
implication
\emph default
, the first number is the one from the line which does contain the implication
(
\begin_inset Formula $P\Rightarrow Q$
\end_inset
), and the second number is from the line which has the known truth (
\begin_inset Formula $P$
\end_inset
).
It's incorrect to write them reversed (
\begin_inset Formula $E\Rightarrow\ 1,2$
\end_inset
), since the definition of the rule says that the line which has the implication
should be cited first.
\layout Standard
We have just applied the rule, and now we know three truths:
\begin_inset Formula $P$
\end_inset
,
\begin_inset Formula $P\Rightarrow Q$
\end_inset
, and
\begin_inset Formula $Q$
\end_inset
.
They are all equally true.
Now we're nearer to our objective,
\begin_inset Formula $P\wedge Q$
\end_inset
, since we know that
\begin_inset Formula $P$
\end_inset
and
\begin_inset Formula $Q$
\end_inset
are true, so
\begin_inset Formula $P\wedge Q$
\end_inset
also has to be true (it's obvious).
In the formula we search there's a conjunction sign (
\begin_inset Formula $\wedge$
\end_inset
) which we don't have, so we need to use the
\emph on
conjunction introduction
\emph default
to be able to say that
\begin_inset Formula $P\wedge Q$
\end_inset
is true because
\begin_inset Formula $P$
\end_inset
is and also
\begin_inset Formula $Q$
\end_inset
.
As a justification we write
\begin_inset Formula $I\wedge\ 1,3$
\end_inset
(the line where it says
\begin_inset Formula $P$
\end_inset
, and the one which says
\begin_inset Formula $Q$
\end_inset
).
Don't put
\begin_inset Formula $I\wedge\ 3,1$
\end_inset
, that would be to affirm that
\begin_inset Formula $Q\wedge P$
\end_inset
, which is not what we're trying to prove.
\layout Standard
Then we know 4 truths:
\begin_inset Formula $P$
\end_inset
,
\begin_inset Formula $P\Rightarrow Q$
\end_inset
,
\begin_inset Formula $Q$
\end_inset
, and
\begin_inset Formula $P\wedge Q$
\end_inset
.
We could continue finding more things which are true, but we've already
finished, since we had been told to prove that
\begin_inset Formula $P\wedge Q$
\end_inset
is true, and we just achieved that (in line 4).
So that will be the last line, and we don't have to write anything else.
\layout Standard
Ah, and an example of this derivation, but with words:
\begin_inset Quotes eld
\end_inset
\emph on
now it's summer, and in summer it's warm.
That's why now it's summer and it's warm
\emph default
\begin_inset Quotes erd
\end_inset
.
\layout Subsection
A bit more complicated.
\begin_inset Formula $P\wedge Q\Rightarrow R,\ Q\Rightarrow P,\ Q\vdash R$
\end_inset
\layout Standard
Try yourself
\begin_inset Formula $P\wedge Q\Rightarrow R,\ Q\Rightarrow P,\ Q\vdash R$
\end_inset
.
Then look the solution:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
P
\backslash
wedge Q
\backslash
Rightarrow R
\backslash
\backslash
\layout Standard
Q
\backslash
Rightarrow P
\backslash
\backslash
\layout Standard
Q
\backslash
\backslash
\layout Standard
P & E$
\backslash
Rightarrow$ 2,3
\backslash
\backslash
\layout Standard
P
\backslash
wedge Q & I$
\backslash
wedge$ 4,3
\backslash
\backslash
\layout Standard
R & E$
\backslash
Rightarrow$ 1,5
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Standard
The only way to achieve
\begin_inset Formula $R$
\end_inset
is using the first formula,
\begin_inset Formula $P\wedge Q\Rightarrow R$
\end_inset
, but we can only use it when
\begin_inset Formula $P\wedge Q$
\end_inset
is true, so we're going for that.
\layout Standard
We know that
\begin_inset Formula $Q\Rightarrow P$
\end_inset
(line 2) and also
\begin_inset Formula $Q$
\end_inset
(line 3), so we deduce
\begin_inset Formula $P$
\end_inset
.
Since
\begin_inset Formula $P$
\end_inset
is now true and also
\begin_inset Formula $Q$
\end_inset
,
\begin_inset Formula $P\wedge Q$
\end_inset
is too.
Until now it's similar to the previous exercise.
\layout Standard
Finally, we have
\begin_inset Formula $P\wedge Q\Rightarrow R$
\end_inset
, and know that
\begin_inset Formula $P\wedge Q$
\end_inset
, so we finish by saying
\begin_inset Formula $R$
\end_inset
.
\layout Subsection
Starting to make suppositions.
\begin_inset Formula $P\Rightarrow Q,\ Q\Rightarrow R\vdash P\Rightarrow Q\wedge R$
\end_inset
\layout Standard
This one,
\begin_inset Formula $P\Rightarrow Q,\ Q\Rightarrow R\vdash P\Rightarrow Q\wedge R$
\end_inset
, is more interesting:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
P
\backslash
Rightarrow Q
\backslash
\backslash
\layout Standard
Q
\backslash
Rightarrow R
\backslash
\backslash
\layout Standard
\backslash
fh P & H
\backslash
\backslash
\layout Standard
\backslash
fa Q & E$
\backslash
Rightarrow$ 1,3
\backslash
\backslash
\layout Standard
\backslash
fa R & E$
\backslash
Rightarrow$ 2,4
\backslash
\backslash
\layout Standard
\backslash
fa Q
\backslash
wedge R & I$
\backslash
wedge$ 4,5
\backslash
\backslash
\layout Standard
P
\backslash
Rightarrow Q
\backslash
wedge R & I$
\backslash
Rightarrow$ 3,6
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Standard
Note the following details:
\layout Itemize
We aren't told any information about what does happen now (we don't have
formulas like
\begin_inset Formula $P$
\end_inset
, or
\begin_inset Formula $Q\wedge R$
\end_inset
, etc.).
They only say things like that
\emph on
if happened
\begin_inset Formula $P$
\end_inset
, then
\begin_inset Formula $Q$
\end_inset
\emph default
\emph on
would also happen
\emph default
.
\layout Itemize
In the same way, what we must prove is not that
\emph on
just now happens something
\emph default
, but that
\emph on
if it happened
\begin_inset Formula $P$
\end_inset
, then
\begin_inset Formula $Q$
\end_inset
and
\begin_inset Formula $R$
\end_inset
would be true.
\layout Itemize
\begin_inset Formula $P\Rightarrow Q\wedge R$
\end_inset
is an implication (
\emph on
something implies something
\emph default
), because operator
\begin_inset Formula $\Rightarrow$
\end_inset
has less priority than
\begin_inset Formula $\wedge$
\end_inset
.
It's a big error to understand that formula as
\begin_inset Formula $(P\Rightarrow Q)\wedge R$
\end_inset
.
\layout Standard
As the formula we want is an implication (
\begin_inset Formula $P\Rightarrow Q\wedge R$
\end_inset
), we will have to use the
\emph on
implication introduction
\emph default
, but this rule needs having a subdemonstration (look it up at its definition).
\layout Standard
It isn't hard to understand why:
\begin_inset Formula $P\Rightarrow Q\wedge R$
\end_inset
says that
\emph on
if it happens
\begin_inset Formula $P$
\end_inset
, then happens
\begin_inset Formula $Q\wedge R$
\end_inset
\emph default
, so the first we should do is to suppose that
\begin_inset Formula $P$
\end_inset
really does happen.
Then we will have to discover that, in this case when
\begin_inset Formula $P$
\end_inset
is true, it is also true
\begin_inset Formula $Q\wedge R$
\end_inset
.
When we get that, we will apply the rule and write everything politely:
\begin_inset Formula $P\Rightarrow Q\wedge R$
\end_inset
.
\layout Standard
For that reason, at line 3 we make an hypothesis (justified by the
\begin_inset Formula $H$
\end_inset
at the right): suppose that
\begin_inset Formula $P$
\end_inset
is true.
Now we're starting a subdemonstration, where we will be able to use the
truths that were on the father demonstration (lines 1 and 2 in this case),
and also we can use
\begin_inset Formula $P$
\end_inset
as if it were another truth.
\layout Standard
We made this hypothesis aiming to know that
\begin_inset Formula $Q\wedge R$
\end_inset
, so we deduce it similarly to the previous exercises.
Notice that we use truths from inside and from outside the subdemonstration,
and also that, while we haven't finished it, that vertical line to the
left must be put.
\layout Standard
In line 6 we now have
\begin_inset Formula $Q\wedge R$
\end_inset
, which is what we were looking for.
Using the
\emph on
implication introduction
\emph default
rule, we can go outside this subdemonstration by saying that
\emph on
if the hypothesis is true, then what we deduced from it also is true
\emph default
.
We stop putting that vertical line, since
\begin_inset Formula $P\Rightarrow Q\wedge R$
\end_inset
is always true (it doesn't depend on whether
\begin_inset Formula $P$
\end_inset
is true or not).
The justification we used,
\begin_inset Formula $I\Rightarrow\ 3,6$
\end_inset
, says that 3 is the line where we made the supposition, and 6 the line
where we discovered something interesting which happens when we make that
supposition.
\layout Standard
\begin_inset Formula $P\Rightarrow Q\wedge R$
\end_inset
is what we wanted, so we have finished.
We finish as always, since we're outside any subdemonstration.
\layout Subsection
Using iteration.
\begin_inset Formula $P\vdash Q\Rightarrow P$
\end_inset
\layout Standard
This is a short one:
\begin_inset Formula $P\vdash Q\Rightarrow P$
\end_inset
.
Solution:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
P
\backslash
\backslash
\layout Standard
\backslash
fh Q & H
\backslash
\backslash
\layout Standard
\backslash
fa P & IT 1
\backslash
\backslash
\layout Standard
Q
\backslash
Rightarrow P & I$
\backslash
Rightarrow$ 2,3
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Standard
The way is clear: we have to suppose
\begin_inset Formula $Q$
\end_inset
, and finally see that, in that case,
\begin_inset Formula $P$
\end_inset
is true.
The trick:
\begin_inset Formula $P$
\end_inset
is always true, whether we suppose
\begin_inset Formula $Q$
\end_inset
or not.
\layout Standard
We must use
\emph on
implication introduction
\emph default
, but this needs a hypothesis, and, some lines below, the result of the
supposition.
Only then we can close the hypothesis.
\layout Standard
So after opening it (line 2), we must do something to write down that
\begin_inset Formula $P$
\end_inset
.
Since we already have it written in line 1, we simply put
\begin_inset Formula $P$
\end_inset
again and justify it with
\begin_inset Formula $IT\ 1$
\end_inset
, which means
\begin_inset Quotes eld
\end_inset
\emph on
I copied this from line 1
\emph default
\begin_inset Quotes erd
\end_inset
.
The
\begin_inset Formula $IT$
\end_inset
is for
\emph on
iteration
\emph default
.
\layout Standard
We now fulfill the requirements to apply the rule, so we apply it, closing
the subdemonstration, and we've ended.
\layout Subsection
Reduction to the absurd.
\begin_inset Formula $P\Rightarrow Q,\ \neg Q\vdash\neg P$
\end_inset
\layout Standard
This is a very useful technique.
Validity of
\begin_inset Formula $P\Rightarrow Q,\ \neg Q\vdash\neg P$
\end_inset
is proved with:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
P
\backslash
Rightarrow Q
\backslash
\backslash
\layout Standard
\backslash
neg Q
\backslash
\backslash
\layout Standard
\backslash
fh P & H
\backslash
\backslash
\layout Standard
\backslash
fa Q & E$
\backslash
Rightarrow$ 1,3
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
neg Q & IT 2
\backslash
\backslash
\layout Standard
\backslash
neg P & I$
\backslash
neg$ 3,4,5
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Standard
What has to be achieved here is
\begin_inset Formula $\neg P$
\end_inset
, which is the
\emph on
negation of something
\emph default
, so the rule which will help is the
\emph on
negation introduction
\emph default
, also known as
\emph on
reduction to the absurd
\emph default
.
\layout Standard
The way to act will be to suppose the contrary of
\begin_inset Formula $\neg P$
\end_inset
(which is
\begin_inset Formula $P$
\end_inset
) and find a contradiction (any).
Supposing
\begin_inset Formula $P$
\end_inset
will lead us to
\begin_inset Formula $Q$
\end_inset
(by
\emph on
implication elimination
\emph default
), and, as we also have
\begin_inset Formula $\neg Q$
\end_inset
, we can apply the rule.
This
\begin_inset Formula $\neg Q$
\end_inset
should be inserted in the current subdemonstration with the
\emph on
iteration
\emph default
rule, so that it is together with the
\begin_inset Formula $Q$
\end_inset
and
\emph on
inside
\emph default
the subdemonstration.
Everything which is inside the subdemonstration is consequence of
\begin_inset Formula $P$
\end_inset
, so it is important to see that both
\begin_inset Formula $Q$
\end_inset
and
\begin_inset Formula $\neg Q$
\end_inset
also are.
\layout Standard
For the
\emph on
negation introduction
\emph default
, the way to justify this rule is putting the line number of where does
the (wrong) supposition start, and the numbers of the two lines where we
saw the contradiction.
The conclusion of this rule is the contrary of what we just supposed, in
this case
\begin_inset Formula $\neg P$
\end_inset
, so we can finish the derivation here.
\layout Standard
This reasoning is actually made without much thinking.
In words it would be something like:
\begin_inset Quotes eld
\end_inset
\emph on
of course that
\begin_inset Formula $\neg P$
\end_inset
, since if it were
\begin_inset Formula $P$
\end_inset
then
\begin_inset Formula $Q$
\end_inset
, and you say that
\begin_inset Formula $\neg Q$
\end_inset
, so it can't be that
\begin_inset Formula $P$
\end_inset
\emph default
\begin_inset Quotes erd
\end_inset
.
\layout Subsection
With subdemonstrations.
\begin_inset Formula $P\Rightarrow(Q\Rightarrow R)\vdash Q\Rightarrow(P\Rightarrow R)$
\end_inset
\layout Standard
Things get harder.
Here's the solution to
\begin_inset Formula $P\Rightarrow(Q\Rightarrow R)\vdash Q\Rightarrow(P\Rightarrow R)$
\end_inset
:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
P
\backslash
Rightarrow (Q
\backslash
Rightarrow R)
\backslash
\backslash
\layout Standard
\backslash
fh Q & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fh P & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa Q
\backslash
Rightarrow R & E$
\backslash
Rightarrow$ 1,3
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa R & E$
\backslash
Rightarrow$ 4,2
\backslash
\backslash
\layout Standard
\backslash
fa P
\backslash
Rightarrow R & I$
\backslash
Rightarrow$ 3,5
\backslash
\backslash
\layout Standard
Q
\backslash
Rightarrow (P
\backslash
Rightarrow R) & I$
\backslash
Rightarrow$ 2,6
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Standard
But first: here we will only use the two rules that help adding and removing
implications, since it's the only operator appearing in the formulas.
\layout Standard
We want
\begin_inset Formula $Q\Rightarrow(P\Rightarrow R)$
\end_inset
, so we will have to do a hypothesis
\begin_inset Formula $Q$
\end_inset
inside of which we should prove that
\begin_inset Formula $P\Rightarrow R$
\end_inset
.
We now do that to simplify the problem: we open a subdemonstration at line
2.
We won't close it until we discover that
\begin_inset Formula $P\Rightarrow R$
\end_inset
is true.
\layout Standard
Now the problem is somehow easier.
We just need to prove
\begin_inset Formula $P\Rightarrow R$
\end_inset
, and we have two lines with two truths: the first says that
\begin_inset Formula $P\Rightarrow(Q\Rightarrow R)$
\end_inset
, and the second says that
\begin_inset Formula $Q$
\end_inset
.
\layout Standard
How can we achieve the
\begin_inset Formula $P\Rightarrow R$
\end_inset
? Well, as always: we must suppose
\begin_inset Formula $P$
\end_inset
, and achieve that
\begin_inset Formula $R$
\end_inset
is true, in some way.
Even if it doesn't seem very simple, it's what must be done, since
\emph on
implication introduction
\emph default
works that way.
So we're going to open another hypothesis, now supposing
\begin_inset Formula $P$
\end_inset
, and let's see if we achieve
\begin_inset Formula $R$
\end_inset
.
This will be a hypothesis inside a hypothesis, but there's no problem in
doing that.
\layout Standard
After writing line 3, and being inside a
\emph on
subsubdemonstration
\emph default
, we have available that
\begin_inset Formula $P\Rightarrow(Q\Rightarrow R)$
\end_inset
, that
\begin_inset Formula $Q$
\end_inset
, and that
\begin_inset Formula $P$
\end_inset
.
We must prove
\begin_inset Formula $R$
\end_inset
.
Now it isn't that hard, is it? If we know that
\begin_inset Formula $P$
\end_inset
, we can use
\emph on
implication elimination
\emph default
on line 1, and we will get the true formula
\begin_inset Formula $Q\Rightarrow R$
\end_inset
.
Since
\begin_inset Formula $Q$
\end_inset
is also true (line 2), we can apply that rule again to discover that
\begin_inset Formula $R$
\end_inset
.
\layout Standard
We then see that supposing
\begin_inset Formula $P$
\end_inset
leads us to the conclusion
\begin_inset Formula $R$
\end_inset
, so we can write down
\begin_inset Formula $P\Rightarrow R$
\end_inset
, which is what we wanted.
Now we've gone outside the subsubdemonstration, and we're only under the
supposition that
\begin_inset Formula $Q$
\end_inset
is true.
As we now see that this supposition implies the truth of the formula
\begin_inset Formula $P\Rightarrow R$
\end_inset
, we can end this subdemonstration concluding that
\begin_inset Formula $Q\Rightarrow(P\Rightarrow R)$
\end_inset
.
\layout Standard
\begin_inset Formula $Q\Rightarrow(P\Rightarrow R)$
\end_inset
is precisely what had to be proven, so we're finished.
\layout Subsection
One with proof by cases.
\begin_inset Formula $P\vee(Q\wedge R)\vdash P\vee Q$
\end_inset
\layout Standard
It will be needed the most complex derivation rule: the
\emph on
disjunction elimination
\emph default
.
\begin_inset Formula $P\vee(Q\wedge R)\vdash P\vee Q$
\end_inset
solved:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
P
\backslash
vee (Q
\backslash
wedge R)
\backslash
\backslash
\layout Standard
\backslash
fh P & H
\backslash
\backslash
\layout Standard
\backslash
fa P
\backslash
vee Q & I$
\backslash
vee$ 2
\backslash
\backslash
\layout Standard
\backslash
fh Q
\backslash
wedge R & H
\backslash
\backslash
\layout Standard
\backslash
fa Q & E$
\backslash
wedge$ 4
\backslash
\backslash
\layout Standard
\backslash
fa P
\backslash
vee Q & I$
\backslash
vee$ 5
\backslash
\backslash
\layout Standard
P
\backslash
vee Q & E$
\backslash
vee$ 1,3,6
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Standard
You already know the rules, so I just explain the way of thinking of a human
who doesn't know natural deduction but can think a little:
\layout Standard
We need to know that
\begin_inset Formula $P\vee Q$
\end_inset
is always true.
The expression from the left,
\begin_inset Formula $P\vee(Q\wedge R)$
\end_inset
, can be made true because of two causes:
\layout Itemize
if it's true because
\begin_inset Formula $P$
\end_inset
is true, then
\begin_inset Formula $P\vee Q$
\end_inset
is true.
\layout Itemize
if it's true because
\begin_inset Formula $Q\wedge R$
\end_inset
is true, then both
\begin_inset Formula $Q$
\end_inset
and
\begin_inset Formula $R$
\end_inset
are true, so
\begin_inset Formula $P\vee Q$
\end_inset
is true because of
\begin_inset Formula $Q$
\end_inset
.
\layout Standard
So, anyway,
\begin_inset Formula $P\vee Q$
\end_inset
is true.
\layout Standard
Well, now we just need to translate all this to logical language, following
the same order in which we thought that, and proceeding slowly.
\layout Standard
We start proving one path, then the other, and finally we apply the
\emph on
disjunction elimination
\emph default
.
To justify it we must write the line where the disjunction is in, and the
two lines from inside each subdemonstration where we saw that both supposing
one thing or supposing the other leads to the same result.
\layout Standard
Notice that, even if we discovered that
\begin_inset Formula $P\Rightarrow P\vee Q$
\end_inset
and that
\begin_inset Formula $Q\wedge R\Rightarrow P\vee Q$
\end_inset
, it isn't necessary to use
\emph on
implication introduction
\emph default
to keep this written down.
\layout Standard
The hardest thing in
\emph on
proof by cases
\emph default
is to decide which will be the expression to prove in both cases.
It must be exactly the same in both cases!
\layout Subsection
One to think.
\begin_inset Formula $L\wedge M\Rightarrow\neg P,\ I\Rightarrow P,\ M,\ I\vdash\neg L$
\end_inset
\layout Standard
Try
\begin_inset Formula $L\wedge M\Rightarrow\neg P,\ I\Rightarrow P,\ M,\ I\vdash\neg L$
\end_inset
only thinking; then write it down on paper.
It's something like:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
L
\backslash
wedge M
\backslash
Rightarrow
\backslash
neg P
\backslash
\backslash
\layout Standard
I
\backslash
Rightarrow P
\backslash
\backslash
\layout Standard
M
\backslash
\backslash
\layout Standard
I
\backslash
\backslash
\layout Standard
\backslash
fh L & H
\backslash
\backslash
\layout Standard
\backslash
fa L
\backslash
wedge M & I$
\backslash
wedge$ 5,3
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
neg P & E$
\backslash
Rightarrow$ 1,6
\backslash
\backslash
\layout Standard
\backslash
fa P & E$
\backslash
Rightarrow$ 2,4
\backslash
\backslash
\layout Standard
\backslash
neg L & I$
\backslash
neg$ 5,7,8
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Standard
I will put it by words:
\begin_inset Quotes eld
\end_inset
\emph on
if you use Linux and Mozilla as a browser, you avoid problems.
In contrast, if you use Internet Explorer you will have problems.
Now you use Mozilla, but also Internet Explorer sometimes.
Consequently, I know that you don't use Linux
\emph default
\begin_inset Quotes erd
\end_inset
.
\layout Standard
Maybe that seems evident:
\begin_inset Quotes eld
\end_inset
\emph on
of course, since IE is not on Linux
\emph default
\begin_inset Quotes erd
\end_inset
, but notice that I never said that.
There isn't the
\begin_inset Formula $I\Rightarrow\neg L$
\end_inset
anywhere.
\layout Standard
The way in which you should think when you prepare this exercise is:
\layout Enumerate
I need to prove
\begin_inset Formula $\neg L$
\end_inset
, which is the negation of something.
It can't be seen any rule of the form
\emph on
something implies
\begin_inset Formula $\neg L$
\end_inset
\emph default
which allows me to obtain it directly.
We should think of another way, for example
\emph on
negation introduction
\emph default
(
\emph on
reduction to the absurd
\emph default
): suppose that I do use Linux.
\layout Enumerate
In the case when I use Linux, I would use both Linux and Mozilla, since
I already used Mozilla before (it's the third truth which is written in
the original problem).
\layout Enumerate
Using both Linux and Mozilla, I wouldn't have computer problems, since
\begin_inset Formula $L\wedge M\Rightarrow\neg P$
\end_inset
.
\layout Enumerate
But I also used Internet Explorer (fourth truth), and since IE generates
problems, I will have problems.
\begin_inset Formula $P$
\end_inset
.
\layout Enumerate
I got a contradiction:
\begin_inset Formula $\neg P$
\end_inset
and
\begin_inset Formula $P$
\end_inset
.
So, what's happening is that the supposition I did of using Linux is wrong:
actually,
\begin_inset Formula $\neg L$
\end_inset
.
\layout Standard
Now you just have to follow the same procedure, but writing down each step,
and using the derivation rules.
What you will obtain is the figure above, which happens to have 5 procedure
lines (the first 4 are only to copy the truths).
Each line corresponds with the steps given here.
\layout Subsection
Left side empty.
\begin_inset Formula $\vdash P\Rightarrow P$
\end_inset
\layout Standard
Proving
\begin_inset Formula $\vdash P\Rightarrow P$
\end_inset
is very easy and short:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
\backslash
fh P & H
\backslash
\backslash
\layout Standard
\backslash
fa P & IT 1
\backslash
\backslash
\layout Standard
P
\backslash
Rightarrow P & I$
\backslash
Rightarrow$ 1,2
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Standard
This case didn't occur before: now it seems that the left part of the sequent
is empty.
It means that we are not given any truth from which we can deduce
\begin_inset Formula $P\Rightarrow P$
\end_inset
.
Why? Because
\begin_inset Formula $P\Rightarrow P$
\end_inset
is always true, not depending on the value of
\begin_inset Formula $P$
\end_inset
or other formulas.
\layout Standard
It's more comfortable and interesting to solve one of these demonstrations,
since you start working directly on the formula which you want to achieve.
But beware, since there are some
\emph on
absolute truths
\emph default
(always true) very hard and long to prove.
\layout Standard
Note down this: whenever the left side is empty, you must start doing a
hypothesis (what else could you do?).
\layout Standard
To achieve
\begin_inset Formula $P\Rightarrow P$
\end_inset
we do as always: suppose that
\begin_inset Formula $P$
\end_inset
and try to see that
\begin_inset Formula $P$
\end_inset
is true.
Since we just supposed it on the first line, we can use the
\emph on
iteration
\emph default
rule to copy it inside, and we finish the subdemonstration by using
\emph on
implication introduction
\emph default
.
And we're done, in only three lines.
\layout Standard
Remark that
\begin_inset Formula $P\Rightarrow P$
\end_inset
is true because
\begin_inset Formula $\blacksquare\Rightarrow\blacksquare$
\end_inset
and
\begin_inset Formula $\square\Rightarrow\square$
\end_inset
.
Well, and furthermore, remember also that
\begin_inset Formula $\square\Rightarrow\blacksquare$
\end_inset
, but
\begin_inset Formula $\blacksquare\nRightarrow\square$
\end_inset
.
\layout Subsection
Suppose the contrary.
\begin_inset Formula $\vdash\neg(P\wedge\neg P)$
\end_inset
\layout Standard
Another simple one,
\begin_inset Formula $\vdash\neg(P\wedge\neg P)$
\end_inset
.
It's done this way:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
\backslash
fh P
\backslash
wedge
\backslash
neg P & H
\backslash
\backslash
\layout Standard
\backslash
fa P & E$
\backslash
wedge$ 1
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
neg P & E$
\backslash
wedge$ 1
\backslash
\backslash
\layout Standard
\backslash
neg (P
\backslash
wedge
\backslash
neg P) & I$
\backslash
neg$ 1,2
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Standard
We all know that two contrary things can't happen at the same time, but,
how can this be proved? We must use the
\emph on
reduction to the absurd
\emph default
:
\layout Standard
Suppose that it does happen
\begin_inset Formula $P\wedge\neg P$
\end_inset
.
Then happen both
\begin_inset Formula $P$
\end_inset
and
\begin_inset Formula $\neg P$
\end_inset
, both at the same time, which is a contradiction.
So, the supposition we just done can't be true: it's false.
This way we can prove
\begin_inset Formula $\neg(P\wedge\neg P)$
\end_inset
.
\layout Standard
When you see something so
\emph on
clear
\emph default
and
\emph on
obvious
\emph default
as
\begin_inset Formula $\neg(P\wedge\neg P)$
\end_inset
, then its contrary will be
\emph on
clearly
\emph default
false and absurd.
So, it won't be too difficult to see that it doesn't hold and that it contradic
ts itself.
Once done, we can assure that the original formula is true since its contrary
is false.
\layout Subsection
This one seems easy.
\begin_inset Formula $\vdash P\vee\neg P$
\end_inset
\layout Standard
Let's see if
\begin_inset Formula $\vdash P\vee\neg P$
\end_inset
is as easy as some say:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
\backslash
fh
\backslash
neg (P
\backslash
vee
\backslash
neg P) & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fh P & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa P
\backslash
vee
\backslash
neg P & I$
\backslash
vee$ 2
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa
\backslash
neg (P
\backslash
vee
\backslash
neg P) & IT 1
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
neg P & I$
\backslash
neg$ 2,3,4
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fh
\backslash
neg P & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa P
\backslash
vee
\backslash
neg P & I$
\backslash
vee$ 6
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa
\backslash
neg (P
\backslash
vee
\backslash
neg P) & IT 1
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
neg
\backslash
neg P & I$
\backslash
neg$ 6,7,8
\backslash
\backslash
\layout Standard
\backslash
fa P & E$
\backslash
neg$ 9
\backslash
\backslash
\layout Standard
\backslash
neg
\backslash
neg (P
\backslash
vee
\backslash
neg P) & I$
\backslash
neg$ 1,5,10
\backslash
\backslash
\layout Standard
P
\backslash
vee
\backslash
neg P & E$
\backslash
neg$ 11
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Standard
One of the simplest but longest I found.
It seems even unnecessary to prove this, since everyone knows that between
\begin_inset Quotes eld
\end_inset
\emph on
today it's Thursday
\emph default
\begin_inset Quotes erd
\end_inset
and
\begin_inset Quotes eld
\end_inset
\emph on
today it's not Thursday
\emph default
\begin_inset Quotes erd
\end_inset
, one of them is true (they can't be both be false at the same time).
\layout Standard
We could start by thinking in the
\emph on
proof by cases
\emph default
method, since from
\begin_inset Formula $P$
\end_inset
we can extract
\begin_inset Formula $P\vee\neg P$
\end_inset
, and from
\begin_inset Formula $\neg P$
\end_inset
we can extract
\begin_inset Formula $P\vee\neg P$
\end_inset
, so, the same formula.
But this doesn't help, since
\emph on
proof by cases
\emph default
is the
\emph on
disjunction elimination
\emph default
, and we don't have any disjunction to eliminate; in fact, we also don't
have the truth formula
\begin_inset Formula $A\vee B$
\end_inset
in which
\begin_inset Formula $A\Rightarrow C$
\end_inset
and
\begin_inset Formula $B\Rightarrow C$
\end_inset
, as the rule needs.
Actually, we don't have any formula which we know it's true (as the left
part of the sequent is empty).
\layout Standard
We know that we must start with a hypothesis (there's no alternative).
Since it's rather clear that
\begin_inset Formula $P\vee\neg P$
\end_inset
is true, it may also be easy to prove that its contrary,
\begin_inset Formula $\neg(P\vee\neg P)$
\end_inset
, is false.
So we will use
\emph on
reduction to the absurd
\emph default
: doing that supposition on line 1, we must achieve a contradiction, any
one.
\layout Standard
I proposed myself to achieve the contradiction
\begin_inset Formula $\neg P$
\end_inset
and
\begin_inset Formula $P$
\end_inset
.
But we don't have any of these formulas; how can we obtain them? Doing
\emph on
reduction to the absurd
\emph default
again is an option: to see that
\begin_inset Formula $\neg P$
\end_inset
, suppose that
\begin_inset Formula $P$
\end_inset
and get a contradiction.
As we did in another occasions, it's very useful to profit the capabilities
of the
\emph on
disjunction introduction
\emph default
: having supposed
\begin_inset Formula $P$
\end_inset
, we can convert it to
\begin_inset Formula $P\vee\neg P$
\end_inset
to search our contradiction.
As we have the
\begin_inset Formula $\neg(P\vee\neg P)$
\end_inset
at the top, we can use it to finish by demonstrating
\begin_inset Formula $\neg P$
\end_inset
.
We can do the same to prove
\begin_inset Formula $P$
\end_inset
, but this time supposing
\begin_inset Formula $\neg P$
\end_inset
.
\layout Standard
Having obtained
\begin_inset Formula $P$
\end_inset
and
\begin_inset Formula $\neg P$
\end_inset
after supposing
\begin_inset Formula $\neg(P\vee\neg P)$
\end_inset
, we see that this formula can't be true, so its negation,
\begin_inset Formula $\neg\neg(P\vee\neg P)$
\end_inset
, is.
By
\emph on
negation elimination
\emph default
, we get our searched formula:
\begin_inset Formula $P\vee\neg P$
\end_inset
.
\layout Standard
I did it this way to make it rather symmetrical, but it can be shorter if
we search another contradiction, for instance
\begin_inset Formula $P\vee\neg P$
\end_inset
and
\begin_inset Formula $\neg(P\vee\neg P)$
\end_inset
.
Then it would be like this:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
\backslash
fh
\backslash
neg (P
\backslash
vee
\backslash
neg P) & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fh P & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa P
\backslash
vee
\backslash
neg P & I$
\backslash
vee$ 2
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa
\backslash
neg (P
\backslash
vee
\backslash
neg P) & IT 1
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
neg P & I$
\backslash
neg$ 2,3,4
\backslash
\backslash
\layout Standard
\backslash
fa P
\backslash
vee
\backslash
neg P & I$
\backslash
vee$ 5
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
neg (P
\backslash
vee
\backslash
neg P) & IT 1
\backslash
\backslash
\layout Standard
\backslash
neg
\backslash
neg (P
\backslash
vee
\backslash
neg P) & I$
\backslash
neg$ 1,6,7
\backslash
\backslash
\layout Standard
P
\backslash
vee
\backslash
neg P & E$
\backslash
neg$ 8
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Subsection
An interesting one.
\begin_inset Formula $P\vee Q,\ \neg P\vdash Q$
\end_inset
\layout Standard
Another which seems easy:
\begin_inset Formula $P\vee Q,\ \neg P\vdash Q$
\end_inset
.
Let's see:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
P
\backslash
vee Q
\backslash
\backslash
\layout Standard
\backslash
neg P
\backslash
\backslash
\layout Standard
\backslash
fh P & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fh
\backslash
neg Q & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa
\backslash
neg P & IT 2
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa P & IT 3
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
neg
\backslash
neg Q & I$
\backslash
neg$ 4,5,6
\backslash
\backslash
\layout Standard
\backslash
fa Q & E$
\backslash
neg$ 7
\backslash
\backslash
\layout Standard
\backslash
fh Q & H
\backslash
\backslash
\layout Standard
\backslash
fa Q & IT 9
\backslash
\backslash
\layout Standard
Q & E$
\backslash
vee$ 1,8,10
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Standard
It's very easy to understand by anyone: it holds
\begin_inset Formula $P\vee Q$
\end_inset
, but
\begin_inset Formula $P$
\end_inset
is false, so the truth is
\begin_inset Formula $Q$
\end_inset
.
\layout Standard
It can be done in several ways, but at some time you will have to use
\emph on
disjunction elimination
\emph default
to do something with the
\begin_inset Formula $P\vee Q$
\end_inset
.
We're going to prove that both
\begin_inset Formula $P$
\end_inset
and
\begin_inset Formula $Q$
\end_inset
lead to the same place, which will be our target formula
\begin_inset Formula $Q$
\end_inset
(since it's possible, let's go directly for
\begin_inset Formula $Q$
\end_inset
).
\layout Standard
We open subdemonstration supposing that
\begin_inset Formula $P$
\end_inset
, and we must see that
\begin_inset Formula $Q$
\end_inset
.
It isn't too hard since we have
\begin_inset Formula $\neg P$
\end_inset
on line 2; this helps contradicting anything we want.
Since what we're searching is
\begin_inset Formula $Q$
\end_inset
, we suppose
\begin_inset Formula $\neg Q$
\end_inset
and by
\emph on
reduction to the absurd
\emph default
we obtain
\begin_inset Formula $\neg\neg Q$
\end_inset
, which is
\begin_inset Formula $Q$
\end_inset
.
\layout Standard
The other path, when we suppose
\begin_inset Formula $Q$
\end_inset
true, leads us directly to
\begin_inset Formula $Q$
\end_inset
.
\layout Standard
In conclusion, both paths go to
\begin_inset Formula $Q$
\end_inset
and by
\emph on
disjunction elimination
\emph default
we get the proof that
\begin_inset Formula $Q$
\end_inset
is always certain.
\layout Subsection
I had this one in an exam.
\begin_inset Formula $A\vee B,\ A\Rightarrow C,\ \neg D\Rightarrow\neg B\vdash C\vee D$
\end_inset
\layout Standard
In the final exam of
\emph on
ILO
\emph default
they were asking
\begin_inset Formula $A\vee B,\ A\Rightarrow C,\ \neg D\Rightarrow\neg B\vdash C\vee D$
\end_inset
, and I needed a very very long time until I got it:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
A
\backslash
vee B
\backslash
\backslash
\layout Standard
A
\backslash
Rightarrow C
\backslash
\backslash
\layout Standard
\backslash
neg D
\backslash
Rightarrow
\backslash
neg B
\backslash
\backslash
\layout Standard
\backslash
fh A & H
\backslash
\backslash
\layout Standard
\backslash
fa C & E$
\backslash
Rightarrow$ 2,4
\backslash
\backslash
\layout Standard
\backslash
fa C
\backslash
vee D & I$
\backslash
vee$ 5
\backslash
\backslash
\layout Standard
\backslash
fh B & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fh
\backslash
neg D & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa
\backslash
neg B & E$
\backslash
Rightarrow$ 3,8
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa B & IT 7
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
neg
\backslash
neg D & I$
\backslash
neg$ 8,9,10
\backslash
\backslash
\layout Standard
\backslash
fa D & E$
\backslash
neg$ 11
\backslash
\backslash
\layout Standard
\backslash
fa C
\backslash
vee D & I$
\backslash
vee$ 12
\backslash
\backslash
\layout Standard
C
\backslash
vee D & E$
\backslash
vee$ 1,6,13
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Standard
Remark that the result we're searching,
\begin_inset Formula $C\vee D$
\end_inset
, is a disjunction.
Since you already know the
\emph on
disjunction introduction
\emph default
, you could simply search
\begin_inset Formula $C$
\end_inset
, and then use that rule to get
\begin_inset Formula $C\vee D$
\end_inset
.
Or if with
\begin_inset Formula $C$
\end_inset
didn't work, you could try with
\begin_inset Formula $D$
\end_inset
, since if
\begin_inset Formula $D$
\end_inset
is true, then
\begin_inset Formula $C\vee D$
\end_inset
also is, and we're done.
\layout Standard
Unfortunately,
\begin_inset Formula $C$
\end_inset
is not always true, and
\begin_inset Formula $D$
\end_inset
also isn't always true (on the other hand,
\begin_inset Formula $C\vee D$
\end_inset
is always true, and that's what we're trying to prove).
After seeing this, we must search another method which works with the two
formulas,
\begin_inset Formula $C$
\end_inset
and
\begin_inset Formula $D$
\end_inset
, at the same time, since it seems that if we take only one without looking
at the other, then it does not provide much information.
\layout Standard
To use the
\begin_inset Formula $A\vee B$
\end_inset
we must use
\emph on
proof by cases
\emph default
.
We will try to see that both
\begin_inset Formula $A$
\end_inset
and
\begin_inset Formula $B$
\end_inset
lead to
\begin_inset Formula $C\vee D$
\end_inset
, since if we can do that, we will have finished.
\layout Standard
\begin_inset Formula $A$
\end_inset
implies
\begin_inset Formula $C$
\end_inset
, and if
\begin_inset Formula $C$
\end_inset
is true then
\begin_inset Formula $C\vee D$
\end_inset
also is, so
\begin_inset Formula $A$
\end_inset
implies
\begin_inset Formula $C\vee D$
\end_inset
.
\layout Standard
With
\begin_inset Formula $B$
\end_inset
, what we know doesn't relate it to
\begin_inset Formula $C$
\end_inset
but to
\begin_inset Formula $D$
\end_inset
.
We want
\begin_inset Formula $C\vee D$
\end_inset
.
Hardly we will make true
\begin_inset Formula $C\vee D$
\end_inset
because of
\begin_inset Formula $C$
\end_inset
, so we will try to make true just the
\begin_inset Formula $D$
\end_inset
.
To do so, we will use
\emph on
reduction to the absurd
\emph default
: suppose that
\begin_inset Formula $D$
\end_inset
is false, then it holds that
\begin_inset Formula $\neg B$
\end_inset
thanks to the formula on line 3.
But we were under the supposition that
\begin_inset Formula $B$
\end_inset
was true, so our hypothesis
\begin_inset Formula $\neg D$
\end_inset
can't be true, thus
\begin_inset Formula $D$
\end_inset
is true, and so is
\begin_inset Formula $C\vee D$
\end_inset
.
\layout Standard
Since
\begin_inset Formula $A\vee B$
\end_inset
is true, and both paths lead to
\begin_inset Formula $C\vee D$
\end_inset
, we finally see that
\begin_inset Formula $C\vee D$
\end_inset
is always true.
\layout Standard
If you are skilled working with logical formulas, you will have seen that
\begin_inset Formula $\neg D\Rightarrow\neg B$
\end_inset
is
\begin_inset Formula $B\Rightarrow D$
\end_inset
.
This simplifies the problem and helps understanding it faster.
But anyway, you can't change
\begin_inset Formula $\neg D\Rightarrow\neg B$
\end_inset
to
\begin_inset Formula $B\Rightarrow D$
\end_inset
directly, you would have to do it step by step.
\layout Subsection
A
\begin_inset Quotes eld
\end_inset
short
\begin_inset Quotes erd
\end_inset
one.
\begin_inset Formula $A\Longleftrightarrow B\vdash(A\wedge B)\vee(\neg A\wedge\neg B)$
\end_inset
\layout Standard
Seems easy: if two expressions are equivalent, it's because they are both
true, or both false.
I could prove the validity of
\begin_inset Formula $A\Longleftrightarrow B\vdash(A\wedge B)\vee(\neg A\wedge\neg B)$
\end_inset
this way:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
(A
\backslash
Rightarrow B)
\backslash
wedge (B
\backslash
Rightarrow A)
\backslash
\backslash
\layout Standard
\backslash
fh
\backslash
neg (A
\backslash
vee
\backslash
neg A) & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fh A & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa A
\backslash
vee
\backslash
neg A & I$
\backslash
vee$ 3
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa
\backslash
neg (A
\backslash
vee
\backslash
neg A) & IT 2
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
neg A & I$
\backslash
neg$ 3,4,5
\backslash
\backslash
\layout Standard
\backslash
fa A
\backslash
vee
\backslash
neg A & I$
\backslash
vee$ 6
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
neg (A
\backslash
vee
\backslash
neg A) & IT 2
\backslash
\backslash
\layout Standard
\backslash
neg
\backslash
neg (A
\backslash
vee
\backslash
neg A) & I$
\backslash
neg$ 2,7,8
\backslash
\backslash
\layout Standard
A
\backslash
vee
\backslash
neg A & E$
\backslash
neg$ 9
\backslash
\backslash
\layout Standard
\backslash
fh A & H
\backslash
\backslash
\layout Standard
\backslash
fa A
\backslash
Rightarrow B & E$
\backslash
wedge$ 1
\backslash
\backslash
\layout Standard
\backslash
fa B & E$
\backslash
Rightarrow$ 12,11
\backslash
\backslash
\layout Standard
\backslash
fa A
\backslash
wedge B & I$
\backslash
wedge$ 11,13
\backslash
\backslash
\layout Standard
\backslash
fa (A
\backslash
wedge B)
\backslash
vee (
\backslash
neg A
\backslash
wedge
\backslash
neg B) & I$
\backslash
vee$ 14
\backslash
\backslash
\layout Standard
\backslash
fh
\backslash
neg A & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fh B & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa B
\backslash
Rightarrow A & E$
\backslash
wedge$ 1
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa A & E$
\backslash
Rightarrow$ 18,17
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa
\backslash
neg A & IT 16
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
neg B & I$
\backslash
neg$ 17,19,20
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
neg A
\backslash
wedge
\backslash
neg B & I$
\backslash
wedge$ 16,21
\backslash
\backslash
\layout Standard
\backslash
fa (A
\backslash
wedge B)
\backslash
vee (
\backslash
neg A
\backslash
wedge
\backslash
neg B) & I$
\backslash
vee$ 22
\backslash
\backslash
\layout Standard
(A
\backslash
wedge B)
\backslash
vee (
\backslash
neg A
\backslash
wedge
\backslash
neg B) & E$
\backslash
vee$ 10,15,23
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Standard
Firstly: we can't write
\begin_inset Formula $A\Longleftrightarrow B$
\end_inset
since we don't have rules for
\begin_inset Formula $\Longleftrightarrow$
\end_inset
.
Since it is seldom used, when a
\begin_inset Formula $\Longleftrightarrow$
\end_inset
appears we are allowed to change it to
\begin_inset Formula $(A\Rightarrow B)\wedge(B\Rightarrow A)$
\end_inset
, which is the same.
\layout Standard
Well, this is the only idea I had...
I leave as an exercise to find a shorter way to do it (if it does exist).
What I did here was to write down that
\begin_inset Formula $A\vee\neg A$
\end_inset
is true (we already did this exercise, and here I just copied the same
steps).
Once I know that
\begin_inset Formula $A\vee\neg A$
\end_inset
holds, I see that both the case
\begin_inset Formula $A$
\end_inset
and the case
\begin_inset Formula $\neg A$
\end_inset
lead to the same formula, which is the solution.
\layout Section
Wrong things
\layout Standard
Common errors you mustn't do.
Remember that a logic professor will correct your exercises with a
\emph on
true
\emph default
or a
\emph on
false
\emph default
, so learn to do this perfectly.
\layout Subsection
Introduction and elimination of
\emph on
\begin_inset Quotes eld
\end_inset
what it would be nice to have
\begin_inset Quotes erd
\end_inset
\layout Standard
The rules like
\emph on
introduction
\emph default
and
\emph on
elimination
\emph default
are not to allow you writing anything you want, but to help you using or
creating a formula with a concrete operator.
\layout Standard
That's why, if you have
\begin_inset Formula $P$
\end_inset
, you can't say
\begin_inset Quotes eld
\end_inset
\emph on
now I do
\emph default
negation introduction
\emph on
and get
\begin_inset Formula $\neg P$
\end_inset
, which is what I needed
\emph default
\begin_inset Quotes erd
\end_inset
.
There are some requisites for each rule, and if you don't fulfill them,
you can't apply that rule.
\layout Standard
For instance: the rule
\emph on
implication elimination
\emph default
doesn't allow to use the formulas in the first line this way:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
P
\backslash
Rightarrow Q
\backslash
wedge R
\backslash
\backslash
\layout Standard
Q
\backslash
wedge R & E$
\backslash
Rightarrow$ 1,1
\layout Standard
\backslash
end{fitch} {
\backslash
textcolor{red}{
\backslash
bigotimes INCORRECTO
\backslash
bigotimes}}
\backslash
]
\end_inset
\layout Standard
To be able to do this, we would need to be sure that
\begin_inset Formula $P$
\end_inset
is always true; then we could apply the rule, correctly writing the line
numbers.
\layout Subsection
Iterate something from a non attainable subdemonstration
\layout Standard
Inside the main demonstration (which goes from the first line to the last),
we can open
\emph on
child demonstrations
\emph default
(
\emph on
subdemonstrations
\emph default
).
Inside any subdemonstration we can also have a
\emph on
subsubdemonstration
\emph default
, which would have as father the subdemonstration and as grandfather the
main demonstration.
\layout Standard
To understand this, here is the solved example
\begin_inset Formula $A\vee B,\ A\Rightarrow C,\ \neg D\Rightarrow\neg B\vdash C\vee D$
\end_inset
:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
A
\backslash
vee B
\backslash
\backslash
\layout Standard
A
\backslash
Rightarrow C
\backslash
\backslash
\layout Standard
\backslash
neg D
\backslash
Rightarrow
\backslash
neg B
\backslash
\backslash
\layout Standard
\backslash
fh A & H
\backslash
\backslash
\layout Standard
\backslash
fa C & E$
\backslash
Rightarrow$ 2,4
\backslash
\backslash
\layout Standard
\backslash
fa C
\backslash
vee D & I$
\backslash
vee$ 5
\backslash
\backslash
\layout Standard
\backslash
fh B & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fh
\backslash
neg D & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa
\backslash
neg B & E$
\backslash
Rightarrow$ 3,8
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa B & IT 7
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
neg
\backslash
neg D & I$
\backslash
neg$ 8,9,10
\backslash
\backslash
\layout Standard
\backslash
fa D & E$
\backslash
neg$ 11
\backslash
\backslash
\layout Standard
\backslash
fa C
\backslash
vee D & I$
\backslash
vee$ 12
\backslash
\backslash
\layout Standard
C
\backslash
vee D & E$
\backslash
vee$ 1,6,13
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Standard
Well, any demonstration can only access the formulas from inside itself,
inside its father, inside the father of its father, inside the father of
the father of its father, ...
All these are called
\emph on
ancestors
\emph default
, so:
\emph on
a demonstration can access itself and its ancestors
\emph default
.
\layout Standard
For this reason, it we are on line 10, the derivation rules can use formulas
from the following places:
\layout Itemize
the current demonstration (lines 8 and 9 currently).
\layout Itemize
father demonstration of the 810 one, so, from line 7.
\layout Itemize
from the demonstration father of the one which starts at line 7, that's
it, lines 1 to 3.
\layout Standard
Bet never we could use the formulas from lines 4 to 6, which is the demonstratio
n
\emph on
uncle
\emph default
of the current one (brother of its father), because all that demonstration
is based on the hypothesis that
\begin_inset Formula $A$
\end_inset
(line 4), and we're not doing that supposition anymore.
\layout Standard
In logical language, one says that a formula
\begin_inset Formula $A$
\end_inset
is
\emph on
actual
\emph default
at formula
\begin_inset Formula $B$
\end_inset
if being in
\begin_inset Formula $B$
\end_inset
we can use
\begin_inset Formula $A$
\end_inset
.
For this to be true,
\begin_inset Formula $A$
\end_inset
must have been written before
\begin_inset Formula $B$
\end_inset
, and some ancestor of
\begin_inset Formula $B$
\end_inset
must be father of
\begin_inset Formula $A$
\end_inset
.
\layout Standard
So, to prove
\begin_inset Formula $P\wedge Q$
\end_inset
we can't do this:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
\backslash
fh P & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fh Q & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa P
\backslash
wedge Q & I$
\backslash
wedge$ 1,2
\backslash
\backslash
\layout Standard
P
\backslash
wedge Q & IT 3
\layout Standard
\backslash
end{fitch} {
\backslash
textcolor{red}{
\backslash
bigotimes INCORRECTO
\backslash
bigotimes}}
\backslash
]
\end_inset
\layout Subsection
Misplace parenthesis
\layout Standard
When I wrote the definitions of the rules, I used the letters
\begin_inset Formula $A$
\end_inset
and
\begin_inset Formula $B$
\end_inset
, but these can represent any expression.
\layout Standard
For instance, here we do
\emph on
negation introduction
\emph default
, in which following the rule we suppose some formula
\begin_inset Formula $A$
\end_inset
, attain a contradiction, and we conclude
\begin_inset Formula $\neg A$
\end_inset
, so, the original formula, but negated.
Let's see:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch*}
\layout Standard
1 &
\backslash
fh P
\backslash
Rightarrow Q & H
\backslash
\backslash
\layout Standard
\backslash
ldots &
\backslash
fa
\backslash
ldots
\backslash
\backslash
\layout Standard
7 &
\backslash
neg P
\backslash
Rightarrow Q & I$
\backslash
neg$ 1,
\backslash
ldots
\layout Standard
\backslash
end{fitch*} {
\backslash
textcolor{red}{
\backslash
bigotimes INCORRECTO
\backslash
bigotimes}}
\backslash
]
\end_inset
\layout Standard
I think it's clear that the
\begin_inset Formula $A$
\end_inset
which appears in the rule represents to
\begin_inset Formula $P\Rightarrow Q$
\end_inset
in this example.
The problem comes when we do the
\begin_inset Formula $\neg A$
\end_inset
.
The negation of
\begin_inset Formula $P\Rightarrow Q$
\end_inset
is not
\begin_inset Formula $\neg P\Rightarrow Q$
\end_inset
, but
\begin_inset Formula $\neg(P\Rightarrow Q)$
\end_inset
.
It's necessary that parenthesis because if not present, the negation affects
only
\begin_inset Formula $P$
\end_inset
.
\layout Standard
If you don't know when to put parenthesis, always put them, and then try
to remove the unneeded ones.
For instance, if you must write that
\begin_inset Formula $\neg P\vee R$
\end_inset
implies
\begin_inset Formula $R\wedge Q$
\end_inset
, put parenthesis around each expression and thus write
\begin_inset Formula $(\neg P\vee R)\Rightarrow(R\wedge Q)$
\end_inset
.
This way, there are absolutely no errors.
Now learn when is it possible to remove parenthesis, and take away all
that you can.
In this case, both can be suppressed and it remains
\begin_inset Formula $\neg P\vee R\Rightarrow R\wedge Q$
\end_inset
.
\layout Subsection
Finish inside a subdemonstration
\layout Standard
You can't finish the deduction inside a subdemonstration.
The last line can't have any vertical line to the left.
\layout Standard
The reason is that everything from inside the subdemonstration is valid
only when the supposition is really true, and what the original problem
asks is to prove that the formula at the right of the
\begin_inset Formula $\vdash$
\end_inset
is
\emph on
always
\emph default
true.
\layout Standard
Here's a sample of what can be tried by someone very astute who wants to
prove
\begin_inset Formula $P\wedge Q$
\end_inset
:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
\backslash
fh P & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fh Q & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa P
\backslash
wedge Q & I$
\backslash
wedge$ 1,2
\layout Standard
\backslash
end{fitch} {
\backslash
textcolor{red}{
\backslash
bigotimes INCORRECTO
\backslash
bigotimes}}
\backslash
]
\end_inset
\layout Standard
We supposed
\begin_inset Formula $P$
\end_inset
, and also
\begin_inset Formula $Q$
\end_inset
.
In that case, of course it's true that
\begin_inset Formula $P\wedge Q$
\end_inset
, but only in that case.
We can't affirm to anyone that
\begin_inset Formula $P\wedge Q$
\end_inset
is always true.
So, we should start closing the two demonstrations (first the inner one,
and then the outer one) to extract some conclusion which is always valid.
\layout Standard
Neither could we do that
\emph on
iteration
\emph default
thing at line 4.
I already explained this before.
\layout Subsection
Skip steps
\layout Standard
Even if you know equivalences between formulas, it's much better if you
don't use them.
For instance, if you have to write the negation of
\begin_inset Formula $\neg P$
\end_inset
, don't write
\begin_inset Formula $P$
\end_inset
directly, but
\begin_inset Formula $\neg\neg P$
\end_inset
.
\layout Standard
Understand that not everything is so obvious as it seems, and that someone
may ask you to prove things like
\begin_inset Formula $P\vdash\neg\neg P$
\end_inset
, where if you could use those simplifications, you would do almost no work.
\layout Standard
Another example: going from
\begin_inset Formula $\neg(A\vee B)$
\end_inset
in one line to having
\begin_inset Formula $\neg A\wedge\neg B$
\end_inset
in the next can't be justified with any of the 9 rules.
But if you succeed in proving and understanding that
\begin_inset Formula $\neg(A\vee B)\vdash\neg A\wedge\neg B$
\end_inset
, then maybe you can add that as an additional rule to use in future demonstrati
ons.
I will give some of these in the next section.
\layout Section
Making it harder
\layout Standard
Here I will finish the explanation of everything else that I was taught
about natural deduction (even if we didn't use it very much).
The quantifiers thing is really important, but more complex.
\layout Subsection
Rules about truth and false
\layout Standard
We can work directly with the values
\begin_inset Formula $\blacksquare$
\end_inset
(
\emph on
true
\emph default
) and
\begin_inset Formula $\square$
\end_inset
(
\emph on
false
\emph default
), and also introduce or eliminate them from our demonstration following
some easy rules.
\layout Subsubsection
Truth introduction
\layout Standard
This is the easiest one:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch*}
\layout Standard
\backslash
hline
\layout Standard
&
\backslash
blacksquare & I$
\backslash
blacksquare$
\layout Standard
\backslash
end{fitch*}
\backslash
]
\end_inset
\layout Standard
So, always, and with no requirements, we can write down that
\begin_inset Formula $\blacksquare$
\end_inset
is true, because it really is.
\layout Subsubsection
False elimination
\layout Standard
A funny one:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch*}
\layout Standard
n &
\backslash
square
\backslash
\backslash
\layout Standard
\backslash
hline
\layout Standard
& A & E$
\backslash
square$ n
\layout Standard
\backslash
end{fitch*}
\backslash
]
\end_inset
\layout Standard
Explanation: if we achieved the conclusion that
\begin_inset Formula $\square$
\end_inset
is true, then we have already achieved a state where we can invent anything
and affirm that it's true; at least, as true as the idea of
\begin_inset Formula $\square$
\end_inset
(
\emph on
false
\emph default
) being true.
\layout Standard
This rule is called
\emph on
ex falso quodlibet sequitur
\emph default
, something like
\begin_inset Quotes eld
\end_inset
\emph on
from false can follow anything
\emph default
\begin_inset Quotes erd
\end_inset
.
\layout Subsection
Rules about quantifiers
\layout Standard
We're too limited if we can only say things like
\begin_inset Formula $P$
\end_inset
,
\begin_inset Formula $Q$
\end_inset
,
\begin_inset Formula $R$
\end_inset
, ...
to translate phrases to logical language.
Quantifiers will allow us to do much more.
\layout Subsubsection
What's that
\layout Standard
I won't be able to explain everything, since various previous concepts are
needed, but I will try to say a little about them.
First, some changes:
\layout Standard
Now we won't talk just about general facts (
\emph on
it rains
\emph default
,
\emph on
it's warm
\emph default
, etc.), but we will have a
\emph on
domain
\emph default
of known things, and we will have to say which property is true for each
element.
\layout Standard
For instance: we have the domain
\begin_inset Formula $\{ p,\ t,\ r\}$
\end_inset
, which represent respectively to
\emph on
PROLOG
\emph default
(a logical programming language), a
\emph on
telephone
\emph default
, and a
\emph on
radio
\emph default
.
\emph on
p
\emph default
,
\emph on
t
\emph default
,
\emph on
r
\emph default
.
\layout Standard
We also add a
\emph on
predicate letter
\emph default
(they're not called
\emph on
propositional letters
\emph default
anymore)
\begin_inset Formula $E$
\end_inset
, which will have the following meaning: when we write
\begin_inset Formula $Ex$
\end_inset
(read
\begin_inset Quotes eld
\end_inset
\emph on
\begin_inset Formula $E$
\end_inset
of
\begin_inset Formula $x$
\end_inset
\emph default
\begin_inset Quotes erd
\end_inset
, but written together) we mean that
\emph on
\begin_inset Formula $x$
\end_inset
is an electronic device
\emph default
.
We will also have
\begin_inset Formula $Sx$
\end_inset
to say that
\emph on
\begin_inset Formula $x$
\end_inset
is a piece of software
\emph default
, and
\begin_inset Formula $Tx$
\end_inset
which will mean that
\emph on
\begin_inset Formula $x$
\end_inset
is a text processor
\emph default
.
\layout Standard
Now we know that are true
\begin_inset Formula $Et$
\end_inset
,
\begin_inset Formula $Er$
\end_inset
,
\begin_inset Formula $Sp$
\end_inset
and nothing else.
\layout Standard
Quantifiers make possible to write truths referring to some elements from
the domain.
There exist two quantifiers:
\layout Itemize
Universal quantifier:
\begin_inset Formula $\forall$
\end_inset
.
When we put
\begin_inset Formula $\forall xPx$
\end_inset
(
\begin_inset Quotes eld
\end_inset
\emph on
for all
\begin_inset Formula $x$
\end_inset
,
\begin_inset Formula $P$
\end_inset
of
\begin_inset Formula $x$
\end_inset
\emph default
\begin_inset Quotes erd
\end_inset
), we mean that all elements on the domain make true the property
\begin_inset Formula $P$
\end_inset
.
\layout Itemize
Existential quantifier:
\begin_inset Formula $\exists$
\end_inset
.
\begin_inset Formula $\exists xPx$
\end_inset
(
\begin_inset Quotes eld
\end_inset
\emph on
there exists
\begin_inset Formula $x$
\end_inset
such that
\begin_inset Formula $P$
\end_inset
of
\begin_inset Formula $x$
\end_inset
\emph default
\begin_inset Quotes erd
\end_inset
) we mean that at least one element from the domain makes true the property
\begin_inset Formula $P$
\end_inset
.
\layout Standard
For instance, now are true the following formulas:
\begin_inset Formula $\forall x(Ex\vee Sx)$
\end_inset
,
\begin_inset Formula $\neg\exists xTx$
\end_inset
,
\begin_inset Formula $\forall x(Tx\Rightarrow\neg Ex)$
\end_inset
,
\begin_inset Formula $\exists xEx\wedge\exists xSx$
\end_inset
and several more.
Quantifiers have the same priority as the operator
\begin_inset Formula $\neg$
\end_inset
.
\layout Standard
The rules explained here will work only with
\emph on
free substitutions
\emph default
.
Sorry for not saying what that means, but I don't want to go out of topic.
\layout Subsubsection
Existential introduction
\layout Standard
If we see a proof of its existence, we can say that a property is true for
some element:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch*}
\layout Standard
n & A
\backslash
{t/x
\backslash
}
\backslash
\backslash
\layout Standard
\backslash
hline
\layout Standard
&
\backslash
exists x A & I$
\backslash
exists$ n,t
\layout Standard
\backslash
end{fitch*}
\backslash
]
\end_inset
\layout Standard
That
\begin_inset Formula $A\{ t/x\}$
\end_inset
is a
\emph on
substitution
\emph default
(maybe read
\begin_inset Quotes eld
\end_inset
\emph on
\begin_inset Formula $t$
\end_inset
over
\begin_inset Formula $x$
\end_inset
\emph default
\begin_inset Quotes erd
\end_inset
and is done by changing
\begin_inset Formula $x$
\end_inset
to
\begin_inset Formula $t$
\end_inset
).
\layout Standard
This rule says that if we see
\begin_inset Formula $At$
\end_inset
, where
\begin_inset Formula $t$
\end_inset
is any element, we can say that
\begin_inset Formula $\exists xAx$
\end_inset
, because we know that when
\begin_inset Formula $x$
\end_inset
is
\begin_inset Formula $t$
\end_inset
then the formula is true.
\layout Subsubsection
Existential elimination
\layout Standard
Extracting some truth from a
\begin_inset Formula $\exists xPx$
\end_inset
is tricky, but it's done this way:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch*}
\layout Standard
m &
\backslash
exists x A
\backslash
\backslash
\layout Standard
n &
\backslash
fh A
\backslash
{a/x
\backslash
} & H
\backslash
\backslash
\layout Standard
p &
\backslash
fa B
\backslash
\backslash
\layout Standard
\backslash
hline
\layout Standard
& B & E$
\backslash
exists$ m,n,p,a
\layout Standard
\backslash
end{fitch*}
\backslash
]
\end_inset
\layout Standard
So, if one of the
\begin_inset Formula $A$
\end_inset
implies
\begin_inset Formula $B$
\end_inset
, then we know that
\begin_inset Formula $B$
\end_inset
, since we know that one of the
\begin_inset Formula $A$
\end_inset
is true.
No
\begin_inset Formula $a$
\end_inset
should appear in
\begin_inset Formula $B$
\end_inset
nor in any attainable hypothesis (sorry for the cryptical phrases, they
are part of the theory).
\layout Subsubsection
Universal introduction
\layout Standard
Well, this one is easy:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch*}
\layout Standard
n & A
\backslash
\backslash
\layout Standard
\backslash
hline
\layout Standard
&
\backslash
forall x A & I$
\backslash
forall$ n
\layout Standard
\backslash
end{fitch*}
\backslash
]
\end_inset
\layout Standard
So, if we know that
\begin_inset Formula $A$
\end_inset
is always true, then it is true for any value of
\begin_inset Formula $x$
\end_inset
.
No
\emph on
free
\emph default
\begin_inset Formula $x$
\end_inset
should appear in any attainable hypothesis.
\layout Subsubsection
Universal elimination
\layout Standard
Another easy one:
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch*}
\layout Standard
n &
\backslash
forall x A
\backslash
\backslash
\layout Standard
\backslash
hline
\layout Standard
& A
\backslash
{t/x
\backslash
} & E$
\backslash
forall$ n,t
\layout Standard
\backslash
end{fitch*}
\backslash
]
\end_inset
\layout Standard
If we know that
\begin_inset Formula $A$
\end_inset
always holds for any element, then we can select an element (anyone) and
we also know that
\begin_inset Formula $A$
\end_inset
is true on that element.
\layout Subsubsection
Examples
\layout Standard
At the last section there are several examples with quantifiers, but without
explanations.
Probably you will have to look for them in some logic book if you're trying
to understand them.
\layout Subsection
Derived rules
\layout Standard
In some books or tutorials more rules are allowed (apart from the basic
9) in order to deal with formulas more easily.
They represent an abstraction: stop working in the details to dedicate
our work in more complex problems (it's like the
\emph on
high level
\emph default
programming languages).
\layout Standard
If you decide to use them, you will lose a lot of interesting work to do,
but you will finish faster.
My advice is to only use a rule if you know how to prove its validity by
using the 9 basic rules.
\layout Standard
Some of the ones I found at several places are:
\layout Itemize
\emph on
Law of double negation
\emph default
: allows changing
\begin_inset Formula $A$
\end_inset
to
\begin_inset Formula $\neg\neg A$
\end_inset
and viceversa.
\layout Itemize
\emph on
Modus Tollens
\emph default
: having
\begin_inset Formula $A\Rightarrow B$
\end_inset
and
\begin_inset Formula $\neg B$
\end_inset
, then
\begin_inset Formula $\neg A$
\end_inset
.
\layout Itemize
\emph on
Disjunctive syllogism
\emph default
: if
\begin_inset Formula $A\vee B$
\end_inset
and
\begin_inset Formula $\neg A$
\end_inset
, then
\begin_inset Formula $B$
\end_inset
.
And if
\begin_inset Formula $A\vee B$
\end_inset
and
\begin_inset Formula $\neg B$
\end_inset
, then it's
\begin_inset Formula $A$
\end_inset
.
\layout Itemize
\emph on
Elimination of
\begin_inset Formula $\neg$
\end_inset
\begin_inset Formula $\Rightarrow$
\end_inset
\emph default
: if you have
\begin_inset Formula $\neg(A\Rightarrow B)$
\end_inset
, then happen both
\begin_inset Formula $A$
\end_inset
and
\begin_inset Formula $\neg B$
\end_inset
.
\layout Itemize
\emph on
Elimination of
\begin_inset Formula $\neg$
\end_inset
\begin_inset Formula $\vee$
\end_inset
\emph default
: if you have
\begin_inset Formula $\neg(A\vee B)$
\end_inset
, then
\begin_inset Formula $\neg A$
\end_inset
, and also
\begin_inset Formula $\neg B$
\end_inset
.
\layout Itemize
\emph on
Elimination of
\begin_inset Formula $\neg\wedge$
\end_inset
\emph default
: if you have
\begin_inset Formula $\neg(A\wedge B)$
\end_inset
, then
\begin_inset Formula $\neg A\vee\neg B$
\end_inset
.
\layout Itemize
\emph on
Theorems which you can use when you want
\emph default
:
\begin_inset Formula $A\Rightarrow A$
\end_inset
,
\begin_inset Formula $A\vee\neg A$
\end_inset
,
\begin_inset Formula $\neg(A\wedge\neg A)$
\end_inset
and more.
\layout Itemize
\emph on
Change of equivalent formulas
\emph default
: if
\begin_inset Formula $A\Longleftrightarrow B$
\end_inset
, then where it says
\begin_inset Formula $A$
\end_inset
you can put
\begin_inset Formula $B$
\end_inset
and viceversa.
\layout Standard
There are lots more; but if someone requests you an exercise, they will
tell you which rules are allowed and which not (for instance, in class
we were allowed to use only the basic ones).
\layout Section
Extra
\layout Standard
If you already knew everything I explained, or have doubts about other topics
unrelated to the way of doing natural deduction, stay at this section.
\layout Subsection
Why is it called natural deduction?
\layout Standard
Because the procedures to be applied are the same that the ones people use
when they think.
\layout Standard
You can see that at most solved exercises in this manual.
Express the sequents by words, tell them to someone, and after some time
he/she will be saying
\begin_inset Quotes eld
\end_inset
\emph on
of course it's like that, since ...
\emph default
\begin_inset Quotes erd
\end_inset
.
You will see that anyone is able to explain how to use some of the 9 derivation
rules, even without knowing their name or existence.
\layout Standard
For this reason, to discover the solution to a natural deduction problem,
forget about
\emph on
introduction
\emph default
and
\emph on
elimination
\emph default
rules, and think normally, changing the letters to simple actions if necessary.
It can help to think of concepts like
\emph on
it rains
\emph default
,
\emph on
it doesn't rain
\emph default
,
\emph on
it's sunny
\emph default
,
\emph on
I don't get wet
\emph default
, ...
since they are short words and, moreover, everyone has a clear understanding
of what does happen when it rains, and can rapidly relate
\emph on
not getting wet
\emph default
with
\emph on
being sunny and not raining
\emph default
, or even more complex formulas.
\layout Subsection
Is the solution unique?
\layout Standard
No.
The more complex the exercise, the more ways to solve it correctly there
are.
In the section about explained exercises, I already gave several solutions
to one of them.
\layout Standard
Of course, you can start deducing things which are absolutely unneeded,
and you will achieve a solution different from the others.
But it's better to try to solve each exercise in the minimum number of
steps.
\layout Subsection
Other ways to prove validity
\layout Standard
Natural deduction is a way to prove the validity of a sequent, but there
exist still more.
Some of them are:
\layout Subsubsection
Brute force
\layout Standard
We can list all the possible combinations of values for each variable, and
check that, for each combination, if the left part of the sequent is true
then the right part is also true.
\layout Standard
Working with
\begin_inset Formula $n$
\end_inset
variables, you will have to test
\begin_inset Formula $2^{n}$
\end_inset
cases.
\layout Standard
The problem here are quantifiers, since now there's a domain involved.
And we're not able to list some of the possible existing domains, since
a domain can have infinite elements.
\layout Subsubsection
Refutation theorem
\layout Standard
Refutation theorem says that
\begin_inset Formula $\Gamma\vDash A\Longleftrightarrow\ \nVdash\Gamma,\neg A$
\end_inset
.
\layout Standard
In words: the set of formulas
\begin_inset Formula $\Gamma$
\end_inset
(
\emph on
gamma
\emph default
) has as consequence
\begin_inset Formula $A$
\end_inset
\emph on
if and only if
\emph default
the system composed by
\begin_inset Formula $\Gamma$
\end_inset
together with
\begin_inset Formula $\neg A$
\end_inset
is unsatisfiable.
\layout Standard
That about proving
\emph on
unsatisfiability
\emph default
is a different topic, and a rather long one, like its name suggests.
One of the easiests methods to do that is using clause
\emph on
resolution
\emph default
trees.
\layout Subsection
How to prove invalidity
\layout Standard
Natural deduction provides a method to demonstrate that a reasoning is correct,
but, how can you prove that a reasoning is noncorrect? It can't be done
with natural deduction.
\layout Standard
We are in this situation: we have sequent
\begin_inset Formula $\Gamma\vdash A$
\end_inset
, and we think that there exists a
\emph on
model
\emph default
(set of values) which make true
\begin_inset Formula $\Gamma$
\end_inset

\emph on
gamma
\emph default
 but not
\begin_inset Formula $A$
\end_inset
.
Well, then we just have to find it to prove that the sequent is invalid.
This model is called
\emph on
countermodel
\emph default
, and we can find it in several ways.
I think that the simplest one is
\emph on
intuitively
\emph default
: start trying different values which we regard as possible countermodel,
until we find a good one.
\layout Standard
For instance,
\begin_inset Formula $\neg P\Rightarrow\neg Q,\ \neg Q\vdash\neg P\vee Q$
\end_inset
is invalid (
\begin_inset Formula $\nvDash$
\end_inset
), since when
\begin_inset Formula $P$
\end_inset
is true and
\begin_inset Formula $Q$
\end_inset
is false, the left part (
\emph on
antecedent
\emph default
) becomes true but the right part (
\emph on
consequent
\emph default
) is false, so
\begin_inset Formula $\neg P\vee Q$
\end_inset
is not a consequence of that from the left part.
\layout Subsection
Create your own exercises
\layout Standard
If you have already read and learnt all the examples from this document,
you did wrong! Now you lack exercises to solve by yourself.
\layout Standard
You can invent sequents and try to prove that they are valid; the problem
then is that if they are not, you will waste your time trying to prove
their validity in vain.
So you must think only of valid sequents, and then prove them correctly.
\layout Standard
Some methods I know to do that are:
\layout Itemize
If
\begin_inset Formula $A$
\end_inset
and
\begin_inset Formula $B$
\end_inset
are the same formula, but written in some different ways, then try proving
\begin_inset Formula $A\vDash B$
\end_inset
or
\begin_inset Formula $B\vDash A$
\end_inset
.
\layout Itemize
Take a truth and prove it.
For instance:
\begin_inset Formula $\vdash P\wedge P\Rightarrow P\vee P$
\end_inset
.
\layout Itemize
Take a lie, negate it, and try to prove that formula.
Example:
\begin_inset Formula $\neg(A\wedge(A\Rightarrow B)\wedge\neg B)$
\end_inset
.
This method will make you practise
\emph on
reduction to the absurd
\emph default
.
\layout Itemize
Convert some formula to its
\emph on
conjunctive normal form
\emph default
(so it is expressed like
\emph on
something
\begin_inset Formula $\wedge$
\end_inset
something
\begin_inset Formula $\wedge$
\end_inset
...
\begin_inset Formula $\wedge$
\end_inset
something
\emph default
).
Then you have several formulas which are all true at the same time: each
of the conjunctands.
You can select one of them and assert that when the original formula is
true, then that conjunctand also is.
\layout Itemize
Take several formulas at random, and suppose that all of them are true simultane
ously.
To do that, write their conjunction (
\emph on
one
\emph default
\begin_inset Formula $\wedge$
\end_inset
\emph on
other
\emph default
\begin_inset Formula $\wedge$
\end_inset
\emph on
other
\emph default
\begin_inset Formula $\wedge$
\end_inset
\emph on
...
\emph default
).
This big formula can be modified with the above methods to find some of
its consequences.
All this will be useful to practise natural deduction with
\emph on
several
\emph default
true formulas at the left part of the sequent.
\layout Subsection
Programs which do natural deduction
\layout Standard
Is there any computer program which can do all these things I explained,
but without having to think or work at all? Well, I really don't know;
I didn't find any.
All the examples in here were done manually.
\layout Standard
Maybe you can make tools like
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
htmladdnormallinkfoot{seqprover}{http://bach.istc.kobeu.ac.jp/seqprover/}
\end_inset
or
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
htmladdnormallinkfoot{pandora}{http://www.doc.ic.ac.uk/~yg/projects/AI/prover.html}
\end_inset
work.
I didn't succeed, and the few programs I found were uncomplete or were
just projects.
Probably that type of program would be hard to do, since deduction is
\emph on
natural
\emph default
(more appropriate for human brains).
Anyway, computers might apply brute force...
\layout Standard
What you can try, and works, is a
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
htmladdnormallinkfoot{game}{http://www.winterdrache.de/freeware/domino/}
\end_inset
similar to domino, with which you can prove sequents by using coloured
tiles.
It requires some learning.
\layout Section
Examples, lots of examples
\layout Standard
And finally, here is a collection of several examples (without explanation).
It was me who solved them, so if you find errors, tell me about it.
\layout Standard
The first 14 were explained (by words) on section 5.
\layout Subsection
\begin_inset Formula $P,\ P\Rightarrow Q\vdash P\wedge Q$
\end_inset
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
P
\backslash
\backslash
\layout Standard
P
\backslash
Rightarrow Q
\backslash
\backslash
\layout Standard
Q & E$
\backslash
Rightarrow$ 2,1
\backslash
\backslash
\layout Standard
P
\backslash
wedge Q & I$
\backslash
wedge$ 1,3
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Subsection
\begin_inset Formula $P\wedge Q\Rightarrow R,\ Q\Rightarrow P,\ Q\vdash R$
\end_inset
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
P
\backslash
wedge Q
\backslash
Rightarrow R
\backslash
\backslash
\layout Standard
Q
\backslash
Rightarrow P
\backslash
\backslash
\layout Standard
Q
\backslash
\backslash
\layout Standard
P & E$
\backslash
Rightarrow$ 2,3
\backslash
\backslash
\layout Standard
P
\backslash
wedge Q & I$
\backslash
wedge$ 4,3
\backslash
\backslash
\layout Standard
R & E$
\backslash
Rightarrow$ 1,5
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Subsection
\begin_inset Formula $P\Rightarrow Q,\ Q\Rightarrow R\vdash P\Rightarrow Q\wedge R$
\end_inset
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
P
\backslash
Rightarrow Q
\backslash
\backslash
\layout Standard
Q
\backslash
Rightarrow R
\backslash
\backslash
\layout Standard
\backslash
fh P & H
\backslash
\backslash
\layout Standard
\backslash
fa Q & E$
\backslash
Rightarrow$ 1,3
\backslash
\backslash
\layout Standard
\backslash
fa R & E$
\backslash
Rightarrow$ 2,4
\backslash
\backslash
\layout Standard
\backslash
fa Q
\backslash
wedge R & I$
\backslash
wedge$ 4,5
\backslash
\backslash
\layout Standard
P
\backslash
Rightarrow Q
\backslash
wedge R & I$
\backslash
Rightarrow$ 3,6
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Subsection
\begin_inset Formula $P\vdash Q\Rightarrow P$
\end_inset
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
P
\backslash
\backslash
\layout Standard
\backslash
fh Q & H
\backslash
\backslash
\layout Standard
\backslash
fa P & IT 1
\backslash
\backslash
\layout Standard
Q
\backslash
Rightarrow P & I$
\backslash
Rightarrow$ 2,3
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Subsection
\begin_inset Formula $P\Rightarrow Q,\ \neg Q\vdash\neg P$
\end_inset
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
P
\backslash
Rightarrow Q
\backslash
\backslash
\layout Standard
\backslash
neg Q
\backslash
\backslash
\layout Standard
\backslash
fh P & H
\backslash
\backslash
\layout Standard
\backslash
fa Q & E$
\backslash
Rightarrow$ 1,3
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
neg Q & IT 2
\backslash
\backslash
\layout Standard
\backslash
neg P & I$
\backslash
neg$ 3,4,5
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Subsection
\begin_inset Formula $P\Rightarrow(Q\Rightarrow R)\vdash Q\Rightarrow(P\Rightarrow R)$
\end_inset
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
P
\backslash
Rightarrow (Q
\backslash
Rightarrow R)
\backslash
\backslash
\layout Standard
\backslash
fh Q & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fh P & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa Q
\backslash
Rightarrow R & E$
\backslash
Rightarrow$ 1,3
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa R & E$
\backslash
Rightarrow$ 4,2
\backslash
\backslash
\layout Standard
\backslash
fa P
\backslash
Rightarrow R & I$
\backslash
Rightarrow$ 3,5
\backslash
\backslash
\layout Standard
Q
\backslash
Rightarrow (P
\backslash
Rightarrow R) & I$
\backslash
Rightarrow$ 2,6
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Subsection
\begin_inset Formula $P\vee(Q\wedge R)\vdash P\vee Q$
\end_inset
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
P
\backslash
vee (Q
\backslash
wedge R)
\backslash
\backslash
\layout Standard
\backslash
fh P & H
\backslash
\backslash
\layout Standard
\backslash
fa P
\backslash
vee Q & I$
\backslash
vee$ 2
\backslash
\backslash
\layout Standard
\backslash
fh Q
\backslash
wedge R & H
\backslash
\backslash
\layout Standard
\backslash
fa Q & E$
\backslash
wedge$ 4
\backslash
\backslash
\layout Standard
\backslash
fa P
\backslash
vee Q & I$
\backslash
vee$ 5
\backslash
\backslash
\layout Standard
P
\backslash
vee Q & E$
\backslash
vee$ 1,3,6
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Subsection
\begin_inset Formula $L\wedge M\Rightarrow\neg P,\ I\Rightarrow P,\ M,\ I\vdash\neg L$
\end_inset
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
L
\backslash
wedge M
\backslash
Rightarrow
\backslash
neg P
\backslash
\backslash
\layout Standard
I
\backslash
Rightarrow P
\backslash
\backslash
\layout Standard
M
\backslash
\backslash
\layout Standard
I
\backslash
\backslash
\layout Standard
\backslash
fh L & H
\backslash
\backslash
\layout Standard
\backslash
fa L
\backslash
wedge M & I$
\backslash
wedge$ 5,3
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
neg P & E$
\backslash
Rightarrow$ 1,6
\backslash
\backslash
\layout Standard
\backslash
fa P & E$
\backslash
Rightarrow$ 2,4
\backslash
\backslash
\layout Standard
\backslash
neg L & I$
\backslash
neg$ 5,7,8
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Subsection
\begin_inset Formula $\vdash P\Rightarrow P$
\end_inset
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
\backslash
fh P & H
\backslash
\backslash
\layout Standard
\backslash
fa P & IT 1
\backslash
\backslash
\layout Standard
P
\backslash
Rightarrow P & I$
\backslash
Rightarrow$ 1,2
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Subsection
\begin_inset Formula $\vdash\neg(P\wedge\neg P)$
\end_inset
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
\backslash
fh P
\backslash
wedge
\backslash
neg P & H
\backslash
\backslash
\layout Standard
\backslash
fa P & E$
\backslash
wedge$ 1
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
neg P & E$
\backslash
wedge$ 1
\backslash
\backslash
\layout Standard
\backslash
neg (P
\backslash
wedge
\backslash
neg P) & I$
\backslash
neg$ 1,2
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Subsection
\begin_inset Formula $\vdash P\vee\neg P$
\end_inset
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
\backslash
fh
\backslash
neg (P
\backslash
vee
\backslash
neg P) & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fh P & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa P
\backslash
vee
\backslash
neg P & I$
\backslash
vee$ 2
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa
\backslash
neg (P
\backslash
vee
\backslash
neg P) & IT 1
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
neg P & I$
\backslash
neg$ 2,3,4
\backslash
\backslash
\layout Standard
\backslash
fa P
\backslash
vee
\backslash
neg P & I$
\backslash
vee$ 5
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
neg (P
\backslash
vee
\backslash
neg P) & IT 1
\backslash
\backslash
\layout Standard
\backslash
neg
\backslash
neg (P
\backslash
vee
\backslash
neg P) & I$
\backslash
neg$ 1,6,7
\backslash
\backslash
\layout Standard
P
\backslash
vee
\backslash
neg P & E$
\backslash
neg$ 8
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Subsection
\begin_inset Formula $P\vee Q,\ \neg P\vdash Q$
\end_inset
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
P
\backslash
vee Q
\backslash
\backslash
\layout Standard
\backslash
neg P
\backslash
\backslash
\layout Standard
\backslash
fh P & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fh
\backslash
neg Q & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa
\backslash
neg P & IT 2
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa P & IT 3
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
neg
\backslash
neg Q & I$
\backslash
neg$ 4,5,6
\backslash
\backslash
\layout Standard
\backslash
fa Q & E$
\backslash
neg$ 7
\backslash
\backslash
\layout Standard
\backslash
fh Q & H
\backslash
\backslash
\layout Standard
\backslash
fa Q & IT 9
\backslash
\backslash
\layout Standard
Q & E$
\backslash
vee$ 1,8,10
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Subsection
\begin_inset Formula $A\vee B,\ A\Rightarrow C,\ \neg D\Rightarrow\neg B\vdash C\vee D$
\end_inset
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
A
\backslash
vee B
\backslash
\backslash
\layout Standard
A
\backslash
Rightarrow C
\backslash
\backslash
\layout Standard
\backslash
neg D
\backslash
Rightarrow
\backslash
neg B
\backslash
\backslash
\layout Standard
\backslash
fh A & H
\backslash
\backslash
\layout Standard
\backslash
fa C & E$
\backslash
Rightarrow$ 2,4
\backslash
\backslash
\layout Standard
\backslash
fa C
\backslash
vee D & I$
\backslash
vee$ 5
\backslash
\backslash
\layout Standard
\backslash
fh B & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fh
\backslash
neg D & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa
\backslash
neg B & E$
\backslash
Rightarrow$ 3,8
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa B & IT 7
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
neg
\backslash
neg D & I$
\backslash
neg$ 8,9,10
\backslash
\backslash
\layout Standard
\backslash
fa D & E$
\backslash
neg$ 11
\backslash
\backslash
\layout Standard
\backslash
fa C
\backslash
vee D & I$
\backslash
vee$ 12
\backslash
\backslash
\layout Standard
C
\backslash
vee D & E$
\backslash
vee$ 1,6,13
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Subsection
\begin_inset Formula $A\Longleftrightarrow B\vdash(A\wedge B)\vee(\neg A\wedge\neg B)$
\end_inset
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
(A
\backslash
Rightarrow B)
\backslash
wedge (B
\backslash
Rightarrow A)
\backslash
\backslash
\layout Standard
\backslash
fh
\backslash
neg (A
\backslash
vee
\backslash
neg A) & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fh A & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa A
\backslash
vee
\backslash
neg A & I$
\backslash
vee$ 3
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa
\backslash
neg (A
\backslash
vee
\backslash
neg A) & IT 2
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
neg A & I$
\backslash
neg$ 3,4,5
\backslash
\backslash
\layout Standard
\backslash
fa A
\backslash
vee
\backslash
neg A & I$
\backslash
vee$ 6
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
neg (A
\backslash
vee
\backslash
neg A) & IT 2
\backslash
\backslash
\layout Standard
\backslash
neg
\backslash
neg (A
\backslash
vee
\backslash
neg A) & I$
\backslash
neg$ 2,7,8
\backslash
\backslash
\layout Standard
A
\backslash
vee
\backslash
neg A & E$
\backslash
neg$ 9
\backslash
\backslash
\layout Standard
\backslash
fh A & H
\backslash
\backslash
\layout Standard
\backslash
fa A
\backslash
Rightarrow B & E$
\backslash
wedge$ 1
\backslash
\backslash
\layout Standard
\backslash
fa B & E$
\backslash
Rightarrow$ 12,11
\backslash
\backslash
\layout Standard
\backslash
fa A
\backslash
wedge B & I$
\backslash
wedge$ 11,13
\backslash
\backslash
\layout Standard
\backslash
fa (A
\backslash
wedge B)
\backslash
vee (
\backslash
neg A
\backslash
wedge
\backslash
neg B) & I$
\backslash
vee$ 14
\backslash
\backslash
\layout Standard
\backslash
fh
\backslash
neg A & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fh B & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa B
\backslash
Rightarrow A & E$
\backslash
wedge$ 1
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa A & E$
\backslash
Rightarrow$ 18,17
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa
\backslash
neg A & IT 16
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
neg B & I$
\backslash
neg$ 17,19,20
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
neg A
\backslash
wedge
\backslash
neg B & I$
\backslash
wedge$ 16,21
\backslash
\backslash
\layout Standard
\backslash
fa (A
\backslash
wedge B)
\backslash
vee (
\backslash
neg A
\backslash
wedge
\backslash
neg B) & I$
\backslash
vee$ 22
\backslash
\backslash
\layout Standard
(A
\backslash
wedge B)
\backslash
vee (
\backslash
neg A
\backslash
wedge
\backslash
neg B) & E$
\backslash
vee$ 10,15,23
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Subsection
\begin_inset Formula $P\vdash(P\Rightarrow Q)\Rightarrow Q$
\end_inset
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
P
\backslash
\backslash
\layout Standard
\backslash
fh P
\backslash
Rightarrow Q & H
\backslash
\backslash
\layout Standard
\backslash
fa Q & E$
\backslash
Rightarrow$ 2,1
\backslash
\backslash
\layout Standard
(P
\backslash
Rightarrow Q)
\backslash
Rightarrow Q & I$
\backslash
Rightarrow$ 2,3
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Subsection
\begin_inset Formula $P\Rightarrow Q\vdash(Q\Rightarrow R)\Rightarrow(P\Rightarrow R)$
\end_inset
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
P
\backslash
Rightarrow Q
\backslash
\backslash
\layout Standard
\backslash
fh Q
\backslash
Rightarrow R & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fh P & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa Q & E$
\backslash
Rightarrow$ 1,3
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa R & E$
\backslash
Rightarrow$ 2,4
\backslash
\backslash
\layout Standard
\backslash
fa P
\backslash
Rightarrow R & I$
\backslash
Rightarrow$ 3,5
\backslash
\backslash
\layout Standard
(Q
\backslash
Rightarrow R)
\backslash
Rightarrow (P
\backslash
Rightarrow R) & I$
\backslash
Rightarrow$ 2,6
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Subsection
\begin_inset Formula $P\Rightarrow Q,\ P\Rightarrow(Q\Rightarrow R)\vdash P\Rightarrow R$
\end_inset
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
P
\backslash
Rightarrow Q
\backslash
\backslash
\layout Standard
P
\backslash
Rightarrow (Q
\backslash
Rightarrow R)
\backslash
\backslash
\layout Standard
\backslash
fh P & H
\backslash
\backslash
\layout Standard
\backslash
fa Q & E$
\backslash
Rightarrow$ 1,3
\backslash
\backslash
\layout Standard
\backslash
fa Q
\backslash
Rightarrow R & E$
\backslash
Rightarrow$ 2,3
\backslash
\backslash
\layout Standard
\backslash
fa R & E$
\backslash
Rightarrow$ 5,4
\backslash
\backslash
\layout Standard
P
\backslash
Rightarrow R & I$
\backslash
Rightarrow$ 3,6
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Subsection
\begin_inset Formula $P\wedge Q\Rightarrow R\vdash P\Rightarrow(Q\Rightarrow R)$
\end_inset
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
P
\backslash
wedge Q
\backslash
Rightarrow R
\backslash
\backslash
\layout Standard
\backslash
fh P & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fh Q & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa P
\backslash
wedge Q & I$
\backslash
wedge$ 2,3
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa R & E$
\backslash
Rightarrow$ 1,4
\backslash
\backslash
\layout Standard
\backslash
fa Q
\backslash
Rightarrow R & I$
\backslash
Rightarrow$ 3,5
\backslash
\backslash
\layout Standard
P
\backslash
Rightarrow (Q
\backslash
Rightarrow R) & I$
\backslash
Rightarrow$ 2,6
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Subsection
\begin_inset Formula $\neg P\vdash P\Rightarrow Q$
\end_inset
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
\backslash
neg P
\backslash
\backslash
\layout Standard
\backslash
fh P & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fh
\backslash
neg Q & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa
\backslash
neg P & IT 1
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa P & IT 2
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
neg
\backslash
neg Q & I$
\backslash
neg$ 3,4,5
\backslash
\backslash
\layout Standard
\backslash
fa Q & E$
\backslash
neg$ 6
\backslash
\backslash
\layout Standard
P
\backslash
Rightarrow Q & I$
\backslash
Rightarrow$ 2,7
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Subsection
\begin_inset Formula $A\wedge(B\vee C)\vdash(A\wedge B)\vee(A\wedge C)$
\end_inset
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
A
\backslash
wedge (B
\backslash
vee C)
\backslash
\backslash
\layout Standard
A & E$
\backslash
wedge$ 1
\backslash
\backslash
\layout Standard
B
\backslash
vee C & E$
\backslash
wedge$ 1
\backslash
\backslash
\layout Standard
\backslash
fh B & H
\backslash
\backslash
\layout Standard
\backslash
fa A
\backslash
wedge B & I$
\backslash
wedge$ 2,4
\backslash
\backslash
\layout Standard
\backslash
fa (A
\backslash
wedge B)
\backslash
vee (A
\backslash
wedge C) & I$
\backslash
vee$ 5
\backslash
\backslash
\layout Standard
\backslash
fh C & H
\backslash
\backslash
\layout Standard
\backslash
fa A
\backslash
wedge C & I$
\backslash
wedge$ 2,7
\backslash
\backslash
\layout Standard
\backslash
fa (A
\backslash
wedge B)
\backslash
vee (A
\backslash
wedge C) & I$
\backslash
vee$ 8
\backslash
\backslash
\layout Standard
(A
\backslash
wedge B)
\backslash
vee (A
\backslash
wedge C) & E$
\backslash
vee$ 3,6,9
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Subsection
\begin_inset Formula $\neg A\vee B\vdash A\Rightarrow B$
\end_inset
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
\backslash
neg A
\backslash
vee B
\backslash
\backslash
\layout Standard
\backslash
fh A & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fh
\backslash
neg A & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa
\backslash
fh
\backslash
neg B & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa
\backslash
fa A & IT 2
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa
\backslash
fa
\backslash
neg A & IT 3
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa
\backslash
neg
\backslash
neg B & I$
\backslash
neg$ 4,5,6
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa B & E$
\backslash
neg$ 7
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fh B & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa B & IT 9
\backslash
\backslash
\layout Standard
\backslash
fa B & E$
\backslash
vee$ 1,8,10
\backslash
\backslash
\layout Standard
A
\backslash
Rightarrow B & I$
\backslash
Rightarrow$ 2,11
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Subsection
\begin_inset Formula $\vdash((P\Rightarrow Q)\Rightarrow P)\Rightarrow P$
\end_inset
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
\backslash
fh (P
\backslash
Rightarrow Q)
\backslash
Rightarrow P & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fh
\backslash
neg P & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa
\backslash
fh P & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa
\backslash
fa
\backslash
fh
\backslash
neg Q & H
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa
\backslash
fa
\backslash
fa P & IT 3
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa
\backslash
fa
\backslash
fa
\backslash
neg P & IT 2
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa
\backslash
fa
\backslash
neg
\backslash
neg Q & I$
\backslash
neg$ 4,5,6
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa
\backslash
fa Q & E$
\backslash
neg$ 7
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa P
\backslash
Rightarrow Q & I$
\backslash
Rightarrow$ 3,8
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa P & E$
\backslash
Rightarrow$ 1,9
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
fa
\backslash
neg P & IT 2
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
neg
\backslash
neg P & I$
\backslash
neg$ 2,10,11
\backslash
\backslash
\layout Standard
\backslash
fa P & E$
\backslash
neg$ 12
\backslash
\backslash
\layout Standard
((P
\backslash
Rightarrow Q)
\backslash
Rightarrow P)
\backslash
Rightarrow P & I$
\backslash
Rightarrow$ 1,13
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Subsection
\begin_inset Formula $Pa,\ Qa\vdash\exists x(Px\wedge Qx)$
\end_inset
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
Pa
\backslash
\backslash
\layout Standard
Qa
\backslash
\backslash
\layout Standard
Pa
\backslash
wedge Qa & I$
\backslash
wedge$ 1,2
\backslash
\backslash
\layout Standard
\backslash
exists x(Px
\backslash
wedge Qx) & I$
\backslash
exists$ 3,a
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Subsection
\begin_inset Formula $\forall x(Px\Rightarrow Qx),\ Pa\vdash Qa$
\end_inset
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
\backslash
forall x(Px
\backslash
Rightarrow Qx)
\backslash
\backslash
\layout Standard
Pa
\backslash
\backslash
\layout Standard
Pa
\backslash
Rightarrow Qa & E$
\backslash
forall$ 1,a
\backslash
\backslash
\layout Standard
Qa & E$
\backslash
Rightarrow$ 3,2
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Subsection
\begin_inset Formula $\forall x(Px\Rightarrow Qx),\ \forall x(Qx\Rightarrow Rx)\vdash\forall x(Px\Rightarrow Rx),$
\end_inset
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
\backslash
forall x(Px
\backslash
Rightarrow Qx)
\backslash
\backslash
\layout Standard
\backslash
forall x(Qx
\backslash
Rightarrow Rx)
\backslash
\backslash
\layout Standard
\backslash
fh Px & H
\backslash
\backslash
\layout Standard
\backslash
fa Px
\backslash
Rightarrow Qx & E$
\backslash
forall$ 1,x
\backslash
\backslash
\layout Standard
\backslash
fa Qx
\backslash
Rightarrow Rx & E$
\backslash
forall$ 2,x
\backslash
\backslash
\layout Standard
\backslash
fa Qx & E$
\backslash
Rightarrow$ 4,3
\backslash
\backslash
\layout Standard
\backslash
fa Rx & E$
\backslash
Rightarrow$ 5,6
\backslash
\backslash
\layout Standard
Px
\backslash
Rightarrow Rx & I$
\backslash
Rightarrow$ 3,7
\backslash
\backslash
\layout Standard
\backslash
forall x(Px
\backslash
Rightarrow Rx) & I$
\backslash
forall$ 8
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\layout Subsection
\begin_inset Formula $\exists x\forall yPxy\vdash\forall y\exists xPxy$
\end_inset
\layout Standard
\begin_inset ERT
status Collapsed
\layout Standard
\backslash
[
\backslash
begin{fitch}
\layout Standard
\backslash
exists x
\backslash
forall yPxy
\backslash
\backslash
\layout Standard
\backslash
fh
\backslash
forall yPay & H
\backslash
\backslash
\layout Standard
\backslash
fa Pay & E$
\backslash
forall$ 2,y
\backslash
\backslash
\layout Standard
\backslash
fa
\backslash
exists xPxy & I$
\backslash
exists$ 3,a
\backslash
\backslash
\layout Standard
\backslash
exists xPxy & E$
\backslash
exists$ 1,2,4,a
\backslash
\backslash
\layout Standard
\backslash
forall y
\backslash
exists xPxy & I$
\backslash
forall$ 5
\layout Standard
\backslash
end{fitch}
\backslash
]
\end_inset
\the_end