Transcript CA 208 Logic - DCU School of Computing

CA 208 Logic
Propositional Logic as a Calculus: |[A]ass
:
B
------A→B
1
CA 208 Logic



Semantic consequence relation |=
Syntactic consequence relation |Flip-sides of each other ...

Logic as a calculus
Calculus unpacked as a proof system
Pure symbol manipulation (rules of proof)
No recourse to meaning

Calculus can be implemented on computer

Aside: so can truth tables for propositional logic …



2
CA 208 Logic
Syntactic consequence relation |

unpacked as a proof system
Many alternative proof systems:








Natural Deduction
Sequent Calculus
Hilbert-style systems
Tableaux Sytems
Resolution Proof systems
Active area of Computer Science (Theorem Proving)
All proof systems for propositional logic do the same work (but
differently ... a bit like different programming languages ... C, C++, Java,
Prolog, Perl, Lisp, Haskel, Fortran, Basic, ...)
E.g. some proof systems are more geared to humans doing proofs,
others are more geared to machines doing proofs …
3
CA 208 Logic











Natural Deduction ND
Gerhand Gentzen ~1930s
Why ND?
Easy to learn ...
Its nice and intuitive (for the most part)
Has (fairly) intuitive proof rules for each of the logical connectives
Close to how humans (erm, Mathematicians  ) do proofs
…
ND can be given in two formats:
Linear (sequential) … some books
(Upside-down) tree format … we’ll be using this
4
CA 208 Logic
Introduction
П1 П2
:
:
A
B
---------- (I)
AB
П
П
:
:
A
A
--------- (I) -------- (I)
AB
BA
Elimination
П
:
AB
--------- (E)
A
П
:
A B
-------- (E)
B
П
[A]ass
[B]ass
:
:
:
AB
C
C
----------------------------------------- (E)
C
5
CA 208 Logic
Introduction
П1 П2
:
:
A
B
---------- (I)
AB
П
П
:
:
A
A
--------- (I) -------- (I)
AB
BA
Elimination
П
:
AB
--------- (E)
A
П
:
A B
-------- (E)
B
П
[A]ass
[B]ass
:
:
:
AB
C
C
----------------------------------------- (E)
C
6
CA 208 Logic
Introduction
Elimination
[A]ass
:
B
------- (→I)
A→B
П1
П2
:
:
A
A→B
---------------- (→E)
B
7
CA 208 Logic
Introduction
[A]ass
:
B
------- (→I)
A→B
Elimination
П1
П2
:
:
A
A→B
---------------- (→E)
B
8
CA 208 Logic
Introduction
[A]ass
:

------- ( I)
A

----- (ex falso quod libet)
A
Elimination
П1
П2
:
:
A
A
---------------- ( E)

[A]ass
:

------A
9
CA 208 Logic
Introduction
[A]ass
:

------- ( I)
A

----- (ex falso quod libet)
A
Elimination
П1
П2
:
:
A
A
---------------- ( E)

[A]ass
:

------A
10
CA 208 Logic
Introduction
[A]ass
:

------- ( I)
A

----- (ex falso quod libet)
A
Elimination
П1
П2
:
:
A
A
---------------- ( E)

[A]ass
П
:
or
:

A
-----------A
A
or
--------A  A
11
CA 208 Logic
Lots of example proofs in ND here (on the blackboard ...)
12
CA 208 Logic
There is method in the madness ...:


Introduction rules
Elimination rules
for each connective.
Premisses are “resources” from which to construct conclusions.



Some times complex premises need to be broken apart to get at the
components (as they are used in the conclusion): elimination rules
Sometimes simple premises need to be put together into more
complex formulas (as they are used in the conclusion): introduction
rules
Sometimes you need a bit of both in a proof: elimination rules and
introduction rules
13
CA 208 Logic
There is method in the madness ...:


Introduction rules
Elimination rules
for each connective.
This gives an inherent symmetry to Natural Deduction Rules/Calculus

Some times logicians wax lyrical about this ... 
14
CA 208 Logic
{P_1, ..., P_n} |- C iff
P_1, ........., P_n
ND
C
without any open (undischarged) intermediate assumptions
15
CA 208 Logic
Good things about the Natural Deduction calculus:




Easy to learn
Intutive account for each of the connectives
Close to how humans (mathemanticians ...) do proofs
ND rules can be used to define



Minimal Logic
Intuitionistic Logic
Classical Logic
Not so good things about Natural Deduction Calculus:



ND Proofs can require quite a bit of ingenuity and expertise
ND Proofs have non-local aspect (management of open intermediate premisses ...)
NP proofs can not easily be automated
Thats why we have other Calculi (Proof Systems) with are good for e.g. Automation of
Proofs ... Thats the subject of more advanced classes in Logic, Theorem Proving, AI,
...
16
CA 208 Logic
What’s the relationship between |- and |=?


{P_1, ..., P_n} |- C
{P_1, ..., P_n} |= C
the syntactic consequence relation (ND proofs)
the semantic consequence relation (situations, truth tables ...)
For classical logics such as Propositional Logic we have that


{P_1, ..., P_n} |- C iff {P_1, ..., P_n} |= C
|- iff |=
i.e. anything (conclusion, theorem) that can be proved (in ND) is also a semantic consequence of the
same premises: if |- then |= (“soundness” of the calculus – here ND – i.e your proof rules are
good, they don’t produce rubbish)
And anything (conclusion, theorem) that is a sematic consequence of the some premises can also be
proved (with here ND) from the same premises (“completeness” of the calculus – here ND – i.e.
your proof rules allow to prove everything that can be proved)



|- iff |=  if |- then |= and if |= then |If |- then |= (Soundness)
If |= then |- (Completeness)
This is “metalogic” = looking at logic as a mathematical object and studying its properties. Soundness
and completeness proofs first given by Kurt Gödel. We don’t do that in this introduction to logic
here ……
17
CA 208 Logic
Propositional Logic as a Calculus: |[A]ass
:
B
------A→B
18