Logic (PHIL 2080, COMP 2620, COMP 6262) Chapter: Propositional Logic — Semantics, Semantic Tableaux, Recap/Proof Strategies
Logic (PHIL 2080, COMP 2620, COMP 6262)
Chapter: Propositional Logic
— Semantics, Semantic Tableaux, Recap/Proof Strategies
Pascal Bercher
Planning & Optimization
Yoshihiro Maruyama
Logic
Intelligent Agents
College of Engineering and Computer Science
the Australian National University (ANU)
16 & 18 March 2021
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Introduction
Pascal Bercher and Yoshihiro Maruyama 1.36
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Semantics vs. Derivations
We’ve worked with propositional formulae as the main ingredient
in sequents.
But what do formulae “mean”?
So far we only covered:
• How different formulae can be transformed into each other.
• We gave an informal explanation of what formulae mean.
In the following, we give a formal semantics – in terms of truth
tables.
Pascal Bercher and Yoshihiro Maruyama 2.36
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Semantics
Pascal Bercher and Yoshihiro Maruyama 3.36
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Truth Tables: Semantics of Propositional Logics
The formal semantics of a propositional formulae is given by truth
tables. (Which you already saw.)
Recall that truth tables formally use the values > (true) and ⊥
(false), though we use 1 and 0 for better readability.
Truth tables: (Note how they are created)
p ¬
0 1
1 0
p q ∧
0 0 0
0 1 0
1 0 0
1 1 1
p q ∨
0 0 0
0 1 1
1 0 1
1 1 1
p q →
0 0 1
0 1 1
1 0 0
1 1 1
Example implication: If the light is red (p), you must stop (q).
Pascal Bercher and Yoshihiro Maruyama 4.36
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Truth Tables: More About Truth Tables
Some “additional” truth tables:
p q →
0 0 1
0 1 1
1 0 0
1 1 1
p q ←
0 0 1
0 1 0
1 0 1
1 1 1
p q ↔
0 0 1
0 1 0
1 0 0
1 1 1
Note how (easily!) we can create formulae from truth tables, e.g.,
• ` (p ↔ q)↔ (¬p ∧ ¬q) ∨ (p ∧ q)
• ` (p → q)↔ (¬p ∧ ¬q) ∨ (¬p ∧ q) ∨ (p ∧ q)
• ` (p → q)↔ ¬(p ∧ ¬q)
• ` (p → q)↔ (¬p ∨ q)
IMPORTANT: You are not allowed to use these equivalences for
natural deduction (in the course), but you can try to prove (some
of) them via natural deduction.
Pascal Bercher and Yoshihiro Maruyama 5.36
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Truth Tables: Even More About Truth Tables
Truth tables can be used to express arbitrary truth formula, e.g.,
p ∧ ¬q
p q ¬q ∧
0 0 1 0
0 1 0 0
1 0 1 1
1 1 0 0
Recall: (p → q)↔ ¬(p ∧ ¬q),
thus: ¬¬(p ∧ ¬q) = ¬(p → q)
p q ¬(p → q)
0 0 0
0 1 0
1 0 1
1 1 0
p → (q → p) (recall the axiom ` p → (q → p)) from lecture 2
p q q → p p → (q → p)
0 0 1 1
0 1 0 1
1 0 1 1
1 1 1 1
We have just seen that
formulae which are
always true (so-called
tautologies) correspond
to axioms!
Pascal Bercher and Yoshihiro Maruyama 6.36
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Excursion: Motivation
The concepts and relation to NP-completeness and
co-NP-completeness are not relevant for this course!
(And they will actually not be explained here anyway.)
But they are just too important and famous for/in Computer
Science not to mention them. You will/can learn about that in
Foundations of Computing.
But you should know what the following terms mean:
• Satisfiable
• Unsatisfiable
• Tautology
Pascal Bercher and Yoshihiro Maruyama 7.36
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Excursion: Satisfiability
Let ϕ be any propositional formula. An important question is:
• Can ϕ be made true? (I.e., Is ϕ satisfiable?)
• In other words: Is there an interpretation (truth assignment for
atoms) that makes the formula ϕ true?
• In yet again other words: Does the truth table of the formula have
a row mapping to 1/>?
Interesting (and extremely important) fact: This problem is
NP-complete. (Because we can guess and verify.)
• Thus, it is not known whether a polynomial time algorithm exists
for all cases. (Open question: P = NP?)
• I.e., in the worst case, we currently need exponential time to
answer this question.
• For example by building the truth table! (But natural deduction and
semantic tableaux are usually quicker.)
Pascal Bercher and Yoshihiro Maruyama 8.36
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Excursion: Unsatisfiability
Let ϕ be any propositional formula. Another (but slightly less)
important question is:
• Is ϕ unsatisfiable?
• In other words: Do all interpretations make the formula ϕ false?
• In yet again other words: Does the truth table of the formula only
have rows mapping to 0/⊥?
Interesting (and important) fact: This problem is co-NP-complete.
(Because we can guess and verify.)
• Thus, it is not known whether a polynomial time algorithm exists
for all cases. (Open questions: NP = co-NP and P = co-NP?)
• I.e., in the worst case, we currently need exponential time to
answer this question.
• For example by building the truth table!
Pascal Bercher and Yoshihiro Maruyama 9.36
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Excursion: Tautologies
Let ϕ be any propositional formula. Another (quite) important
question is:
• Is ϕ a tautology? (I.e., an axiom!)
• In other words: Do all interpretations make the formula ϕ true?
• In yet again other words: Does the truth table of the formula only
have rows mapping to 1/>?
Interesting (and important) fact: This problem is co-NP-complete.
(Because we can guess and verify.)
• Thus, it is not known whether a polynomial time algorithm exists
for all cases. (Open questions: NP = co-NP and P = co-NP?)
• I.e., in the worst case, we currently need exponential time to
answer this question.
• For example by building the truth table!
Pascal Bercher and Yoshihiro Maruyama 10.36
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Semantics: Interpretations and Valid Sequents
An interpretation is an assignment of ⊥/> to atoms (except to
⊥/>, those “special atoms” cannot be interpreted differently).
Prize question: When is a sequent X ` A valid?
• We did not say! (No formal definition yet.)
• We only “claimed” that all (correct∗) sequents are valid.
(“correct” in the sense that we are able to derive A from X using
natural deduction. E.g., p ` ¬p is not a correct sequent.)
Pascal Bercher and Yoshihiro Maruyama 11.36
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Semantics: Semantically Valid Sequents
Definition: Sequent X ` A is valid if and only if:
A is true for every interpretation for which all the formulae in X are true.
Or, equivalently:
There is no interpretation that makes X true, but not A.
Note:
This is a purely semantic definition! No deduction! No rules on
connective introduction or elimination, etc., it bases only on truth
tables!
Pascal Bercher and Yoshihiro Maruyama 12.36
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Semantics: Proving a Sequent Semantically
How to prove X |= A?
Possible decision procedure: Create the proof tables!
• Create a table tX for all formulae in X (all need to be true)
• Create another table tA for A and check validity criterion.
Reminder:
Sequent X ` A is valid (i.e., X |= A) if and only if:
A is true for every interpretation for which all the formulae in X
are true.
Or, equivalently:
There is no interpretation that makes X true, but not A.
Pascal Bercher and Yoshihiro Maruyama 13.36
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Semantics: Example Proof Based on Truth Tables
Prove that
X︷ ︸︸ ︷
(p ∨ q)→ r , p `
A︷ ︸︸ ︷
(p → r) ∧ (q → r) is valid.
Table tX for premises:
p q r p ∨ q (p ∨ q)→ r X
0 0 0 0 1 0
0 0 1 0 1 0
0 1 0 1 0 0
0 1 1 1 1 0
1 0 0 1 0 0
1 0 1 1 1 1
1 1 0 1 0 0
1 1 1 1 1 1
Table tA for conclusion:
p q r p → r q → r A
0 0 0 1 1 1
0 0 1 1 1 1
0 1 0 1 0 0
0 1 1 1 1 1
1 0 0 0 1 0
1 0 1 1 1 1
1 1 0 0 0 0
1 1 1 1 1 1
Only two interpretations exist that make all x ∈ X true:
1 p = 1, q = 0, r = 1 2 p = q = r = 1
Both of them make A true! Thus, X |= A.
Pascal Bercher and Yoshihiro Maruyama 14.36
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Semantics: Issues With Proving via Truth Tables
This decision procedure has a big problem: Inefficiency!
Note that truth tables grow always exponentially, not just in the
worst case! If X ` A consists of:
• 1 atom⇒ 2 lines (like the ¬ truth table)
• 2 atoms⇒ 4 lines (like ∧, ∨, and→)
• 3 atoms⇒ 8 lines (like our previous example!)
• 4 atoms⇒ 16 lines
• 10 atoms⇒ 1.024 lines
• 20 atoms⇒ 1.048.576 lines (> 1 million)
• n atoms⇒ 2n lines
⇒ We need a proof system that is not (always) that bad!
• We saw Natural Deduction as such a proof system.
• Semantic Tableaux is another such proof system.
(Note that we write just X ` A instead of X `ST A.)
Pascal Bercher and Yoshihiro Maruyama 15.36
Introduction Semantics Semantic Tableaux Proof Strategies Summary
On Syntax and Semantics, and Proof Systems: Syntax for our Semantics
We differentiate between validity and derivability:
• X |= A (A follows semantically from X )
• X ` A (A can be derived from X )
Note that the latter refers to a derivation, i.e., to some specific
proof system. In our case, we only cover natural deduction in this
course, but there might be many, in which case one would use
different symbols, e.g.,
• X `ND A (A can be derived from X using natural deduction)
• X `RC A (A can be derived from X using the resolution calculus)
• X `ST A (A can be derived from X using semantic tableaux)
• There are many more!
Pascal Bercher and Yoshihiro Maruyama 16.36
Introduction Semantics Semantic Tableaux Proof Strategies Summary
On Syntax and Semantics, and Proof Systems: Syntax vs. Semantics
So, what’s the relation between X |= A and X ` A?
A desirable situation would be X |= A iff X ` A
But the derivation is just “some mechanism”, so what could
happen? Let `X be some proof system.
• X |= A, but X `X ¬A
→ The proof system is wrong! (Unless X |= A and X |= ¬A, which
happens if X is contradictory, i.e., unsatisfiable.)
• X |= A, but not X `X A
→ The proof system is not complete!
What we want:
Soundness Every provable sequent is valid.
Completeness Every valid sequent is provable.
Pascal Bercher and Yoshihiro Maruyama 17.36
Introduction Semantics Semantic Tableaux Proof Strategies Summary
On Syntax and Semantics, and Proof Systems: Properties of Proof Systems
Propositional Natural Deduction is sound and complete!
But how to prove that?
To prove soundness:
• Look at all rules and show, based on truth tables, that they
preserve validity.
How to prove completeness?
• Formally, we want X |= A implies X `X A for all X and A.
• This is much harder, since X can even be infinite! (So just “looking
at all x ∈ X ” can take forever.)
• Proof can be done by contradiction. Proof not relevant for the
course, but it can be found in the course notes.
Pascal Bercher and Yoshihiro Maruyama 18.36
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Semantic Tableaux
Pascal Bercher and Yoshihiro Maruyama 19.36
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Introduction: Recap and Motivation
Based on our definition of X |= A, how can we show that (so far)?
→ With truth tables!
The problem was runtime:
→ With n atoms, truth tables have 2n lines! (I.e., exponential scaling.)
Hence we exploit “smarter” proof systems, like:
• Natural Deduction (weeks 2 & 3)
• Semantic Tableaux (week 4)
• And many more!
Pascal Bercher and Yoshihiro Maruyama 20.36
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Introduction: General Idea
Recall that deciding X |= A means:
There is no interpretation that makes X true, but not A.
So we can exploit proof via contradiciton! Assume the opposite!
• Assume there is an interpretation that makes X true, but not A
• Show that this leads to a contradiction.
• Thus, our assumption was wrong, thus X |= A holds!
Technically, we assign a label to each formula: either true or false
• Start with all formulae in X , label them with true (T).
• Label A as false (F).
• Based on simplifications (simulating proof tables), either find a
contradiction or an interpretation.
I Contradiction: Shows our claim, i.e., X |= A
I Interpretation: X 6|= A (i.e., A does not follow from X )
→ So now we can even show that a formula does not follow!
(Natural deduction was not able to do so!)
Pascal Bercher and Yoshihiro Maruyama 21.36
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Proof Technique: Example (Illustrating the “Simplifications”)
p ∨ q,¬p ` q
(1) T: p ∨ q X
(2) T: ¬p X
(3) F: q
(4) F: p from (2)
(5) T: p from (1) (6) T: q from (1)
Within each path, all lines “accumulate”.
Branches branch, i.e., they split different possibilities.
If all leafs die, the tree dies: Success! Sequent is valid.
If some leaf survives, the tree lives: Failure!
• The sequent is invalid.
• We can extract an interpretation invalidating the sequent.
Pascal Bercher and Yoshihiro Maruyama 22.36
}
premises X}
conclusion A
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Proof Technique: Rule Set (And, Or, Not)
And Elimination:
T: A ∧ B
T: A , T: B
F: A ∧ B
F: A | F: B
A B ∧
0 0 0
0 1 0
1 0 0
1 1 1
Or Elimination:
T: A ∨ B
T: A | T: B
F: A ∨ B
F: A , F: B
A B ∨
0 0 0
0 1 1
1 0 1
1 1 1
Negation Elimination:
T: ¬A
F: A
F: ¬A
T: A
A ¬
0 1
1 0
Pascal Bercher and Yoshihiro Maruyama 23.36
The comma means that both lines hold in
the same branch, i.e., we can write them
below each other!
The bar (“|”) means that we branch over
different possibilities, so the lines end up
in different branches!
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Proof Technique: Rule Set (And, Or, Not)
And Elimination:
T: A ∧ B
T: A , T: B
F: A ∧ B
F: A | F: B
A B ∧
0 0 0
0 1 0
1 0 0
1 1 1
Or Elimination:
T: A ∨ B
T: A | T: B
F: A ∨ B
F: A , F: B
A B ∨
0 0 0
0 1 1
1 0 1
1 1 1
Negation Elimination:
T: ¬A
F: A
F: ¬A
T: A
A ¬
0 1
1 0
Pascal Bercher and Yoshihiro Maruyama 23.36
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Proof Technique: Rule Set (Implication)
Implication Elimination:
T: A→ B
F: A | T: B
F: A→ B
T: A , F: B
A B →
0 0 1
0 1 1
1 0 0
1 1 1
Note that X ` A iff X |= A intuitively holds, because these rules
mimic the truth tables exactly.
Also keep in mind that we only write X ` A instead of X `ND A or
X `ST A since the applied proof system is clear from context.
Pascal Bercher and Yoshihiro Maruyama 24.36
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Proof Technique: Example (for a valid Sequent)
` p → (q → p)
(1) F: p → (q → p)
X
(2) T: p from (1)
(3) F: q → p
X
from (1)
(4) T: q from (3)
(5) F: p from (3)
This sequent is valid, because all branches show a contradiction!
Here, there was no branching. Normally, all ≥ 2 branches had to
show a contradiction.
We also did not use any assumptions here (that would have been
labeled true (T)), because there weren’t any.
Pascal Bercher and Yoshihiro Maruyama 25.36
How to start the proof?
Write one line per assumption, label it true (T).
(We have none here!)
Write a line for the formula, label it false (F).
Again: Why?
X |= A means: There is no interpretation that makes X true
but not A.
We assume the opposite, i.e., that there is an interpretation
that makes X true and A false.
So once we derive a contradiction, we know that indeed
there is no such interpretation. Thus X |= A follows.
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Proof Technique: Example (for a valid Sequent)
` p → (q → p)
(1) F: p → (q → p) X
(2) T: p from (1)
(3) F: q → p X from (1)
(4) T: q from (3)
(5) F: p from (3)
This sequent is valid, because all branches show a contradiction!
Here, there was no branching. Normally, all ≥ 2 branches had to
show a contradiction.
We also did not use any assumptions here (that would have been
labeled true (T)), because there weren’t any.
Pascal Bercher and Yoshihiro Maruyama 25.36
F: A→ B
T: A , T: B
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Proof Technique: Example (for an Invalid Sequent)
Attempting to show validity of p → (q ∨ r) ` ¬(s → ¬q)→ ((p ∧ s)→ r)
(1) T: p → (q ∨ r) X
(2) F: ¬(s → ¬q)→ ((p ∧ s)→ r) X
(3) T: ¬(s → ¬q) X from (2)
(4) F: (p ∧ s)→ r X from (2)
(5) F: s → ¬q X from (3)
(6) T: p ∧ s X from (4)
(7) F: r from (4)
(8) T: s from (5)
(9) F: ¬q X from (5)
(10) T: p from (6)
(11) T: q from (9)
(12) F: p from (1)
(13) T: q ∨ r X from (1)
(14) T: q open! from (13)
(15) T: r from (13)
Pascal Bercher and Yoshihiro Maruyama 26.36
T: A→ B
F: A | T: B
F: A→ B
T: A , T: B
T: ¬A
F: A
Interpretation: r = 0, s = q = p = 1.
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Proof Technique: Comments About Previous Proof(s)
In the beginning (when only the first lines were shown) we had
the choice of which implication to simplify.
We chose line (2), because its rule does not branch, and it’s
always good to postpone branching as long as possible so we
don’t “duplicate” work.
We detected an open branch, i.e., a complete path where no
further reductions were possible.
• Via “collecting” the truth assignments to atoms along the open
branch we can construct an interpration.
• That interpretation is a witness that:
I that there exists an interpretation that makes X true as well as ¬A,
I and, thus (by definition), that A does not follow logically from X .
I This means that the sequent is invalid.
Also note that we have a contradiction whenever some formula
appears true and false within the same branch. We do not need to
wait until it is atomic.
Pascal Bercher and Yoshihiro Maruyama 27.36
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Proof Strategies
Pascal Bercher and Yoshihiro Maruyama 28.36
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Overview
The following is:
A short recap with an emphasize on proof strategies.
A collection of tips and tricks! (With many examples.)
How to show X ` A? Depends on A!
A could be . . .
B ∧ C:
derive B
derive C
∧I
B ∨ C:
assume B
assume C
∨E
B → C:
assume B
derive C
→I
¬B:
assume B
derive contradiction
use negation rules
p (atom)
Note that X ` A can also refer to sub steps!!
Pascal Bercher and Yoshihiro Maruyama 29.36
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Examples: X ` A, A is an Implication
p → ((q ∧ r)→ s) ` q → ((p ∧ r)→ s)
α1 (1) p → ((q ∧ r)→ s) A
α2 (2) q A
α3 (3) p ∧ r A
α1, α2, α3 (n-2) s
α1, α2 (n-1) (p ∧ r)→ s (n-2)[α3]→I
α1 (n) q → ((p ∧ r)→ s) (n-1)[α2]→I
Do not assume p! Use the strategies for A! (p is part of X )
As always, we can perform regression to see where to go!
Now we cannot go further via regression, so fill the gap!
Pascal Bercher and Yoshihiro Maruyama 30.36
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Examples: X ` A, A is an Implication
p → ((q ∧ r)→ s) ` q → ((p ∧ r)→ s)
α1 (1) p → ((q ∧ r)→ s) A
α2 (2) q A
α3 (3) p ∧ r A
α3 (4) p 3 ∧E
α1, α3 (5) (q ∧ r)→ s 1,4→E
α3 (6) r 3 ∧E
α2, α3 (7) q ∧ r 2,6 ∧I
α1, α2, α3 (8) s 5,7→E
α1, α2, α3 (9) (p ∧ r)→ s 8[α3]→I
α1, α2, α3 (10) q → ((p ∧ r)→ s) 9[α2]→I
α1, α2, α3 (n-2) s
α1, α2 (n-1) (p ∧ r)→ s (n-2)[α3]→I
α1 (n) q → ((p ∧ r)→ s) (n-1)[α2]→I
Pascal Bercher and Yoshihiro Maruyama 30.36
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Examples: X ` A, A is a Negation
¬(p ∨ q) ` ¬p
α1 (1) ¬(p ∨ q) A
α2 (2) p A
α2 (3) p ∨ q 2 ∨I
α1 (4) ¬p 1,3[α2] RAA
α1 (n) ¬p ?,?[α2] RAA
Pascal Bercher and Yoshihiro Maruyama 31.36
X ,B ` A Y ,B ` ¬A
X ,Y ` ¬B
RAA
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Examples: X ` A, A is a Disjunction (here: in one of the Substeps)
¬p ∧ ¬q ` ¬(p ∨ q)
α1 (1) ¬p ∧ ¬q A
α2 (2) p ∨ q A
α3 (3) p A
α4 (4) q A
α1 (5) ¬p 1 ∧E
α3 (6) ¬(¬p ∧ ¬q) 3,5[α1] RAA
α1 (7) ¬q 1 ∧E
α4 (8) ¬(¬p ∧ ¬q) 4,7[α1] RAA
α2 (9) ¬(¬p ∧ ¬q) 2,6[α3],8[α4] ∨E
α1 (10) ¬(p ∨ q) 1,9[α2] RAA
α1 (n) ¬(p ∨ q) ?,?[α2] RAA
Pascal Bercher and Yoshihiro Maruyama 32.36
X ,B ` A Y ,B ` ¬A
X ,Y ` ¬B
RAA
X ` A ∨ B Y ,A ` C Z ,B ` C
X ,Y , Z ` C
∨E
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Examples: X ` A, A is an Atom (Or: all Other Strategies Fail)
If everything else fails, assume ¬A and derive A:
X ,¬A ` A
X ` A
Closely related is the sequent from earlier: ¬p → p ` p
(p is so true that it’s even implied by its own negation!)
Example: (p → q)→ p ` p
α1 (1) (p → q)→ p A
α2 (2) ¬p A
α3 (3) p A
α2, α3 (4) ¬¬q 2,3[] RAA
α2, α3 (5) q 4 ¬¬E
α2 (6) p → q 5[α3]→I
α1, α2 (7) p 1,6→E
α1 (8) ¬¬p 2,7[α2] RAA
α1 (9) p 8 ¬¬E
Pascal Bercher and Yoshihiro Maruyama 33.36
X ,B ` A Y ,B ` ¬A
X ,Y ` ¬B
RAA
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Examples: Previous Example, shown with Semantic Tableaux
We now show (p → q)→ p ` p via Semantic Tableaux.
(p → q)→ p ` p
(1) T: (p → q)→ p X
(2) F: p
(3) F: p → q X from (1)
(5) T: p from (3)
(6) F: q from (3)
(4) T: p from (1)
The primary strategy (that often suffices to create small trees) is:
Always apply rules first that don’t branch!
Don’t forget branches!! And mark lines that are “done”.
Pascal Bercher and Yoshihiro Maruyama 34.36
T: A→ B
F: A | T: B
F: A→ B
T: A , T: B
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Summary
Pascal Bercher and Yoshihiro Maruyama 35.36
Introduction Semantics Semantic Tableaux Proof Strategies Summary
Content of this Lecture
The formal semantics of a propositional formula.
A formal notion of the validity of seqents.
Another proof system (mimicing semantics): Semantic Tableaux
A short recap on how to prove various kinds of sequents.
→ The entire Logic Notes sections:
• More about propositional logic: Truth tables
• More about propositional logic: Semantic tableaux
Pascal Bercher and Yoshihiro Maruyama 36.36
Introduction
Semantics
Truth Tables
Excursion
Semantics
On Syntax and Semantics, and Proof Systems
Semantic Tableaux
Introduction
Proof Technique
Proof Strategies
Overview
Examples
Summary