Notes Hoofdstuk 1 & deel Hoofdstuk 2
Hoofdstuk 1:
Given a formula in propositional logic p, we can check when p holds for all possible values of its
atomic propositional variables that occur in that formula whether the formule holds under a certain
assignment of false and true– this is what we do when we write a truth table.
We can also give a ‘proof sketch’ using proof strategies – but we haven’t made precise what these
strategies are, relying on an informal diagrammatic description. Can we define a set of all proofs of
some propositional logic formula? After all, we managed to define the syntax of propositional logic
as inductively defined set – can we do the same for its semantics?
We can define the syntax of propositional logic using BNF, we have different way to build a
propositional formula as follows:
p, q ::= true | false | P | ¬p | p ∧ q | p ∨ q | p ⇒ q | p ⇔ q
So far, we have seen the BNF notation for inductively defined sets. But what notation should we use
for inductively defined relations? For example, we defined the ⩽ relation between Peano natural
numbers using the following rules:
− for all n ∈ N, 0 ⩽ n;
− if n ⩽ m, then s(n) ⩽ s(m)
Inductively defined relations are often given by means of inference rules:
Here we have two inference rules, named Base and Step; these rules together
define a relation (⩽) ⊆ N × N. The statements above the horizontal line are the
premises - the assumptions that you must establish in order to use this rule; the
statement under the horizontal line is the conclusion that you can draw from
these assumptions.
These rules state that there are two ways to prove that n ⩽ m:
− if n = 0 the ⩽-Base rule tells us that 0 ⩽ n – for any n;
− if we can show n ⩽ m, we can use the ⩽-Step rule to prove s(n) ⩽ s(m).
A rule without premises is called an axiom.
Example:
By repeatedly applying these rules, we can write larger proofs.
For example, to give a formal proof that 2 ⩽ 5 we write:
We can read these rules top-to-bottom or bottom-to-top. Such a
proof is sometimes referred to a as derivation. Each of the
inference rules gives a different ‘lego piece’ that we can use to
write bigger proofs.
, Example of even numbers: We can use this inference rule notation to write all
kinds of relations. For example, we may want to define the unary relation
isEven – that proves that a given number is even.
Example of isSorted array: Similarly, we can define inference rules that
make precise when a list of numbers is sorted. Note that we can require
more than one hypothesis – as in the isSorted-Step rule.
A word over an alphabet Σ is called a palindrome if it reads the
same backward as forward. Examples include: ‘racecar’, ‘radar’, or
‘madam’. Give a inference rules that characterise a unary relation
on words, capturing the fact that they are a palindrome.
Hoofdstuk 2 Natural Deduction
Given the following set of propositional logical formulas over a set of atomic variables P: p, q ::= true
| false | P | ¬p | p ∧ q | p ∨ q | p ⇒ q | p ⇔ q Can we give inference rules that capture precisely the
tautologies? Yes! These inference rules, sometimes called natural deduction, formalize the proof
strategies that we have seen previously.
Conjunction introduction and elimination
Conjunction introduction:
The proof strategy for conjunction introduction
and the inference rule for conjunction
introduction.
Hoofdstuk 1:
Given a formula in propositional logic p, we can check when p holds for all possible values of its
atomic propositional variables that occur in that formula whether the formule holds under a certain
assignment of false and true– this is what we do when we write a truth table.
We can also give a ‘proof sketch’ using proof strategies – but we haven’t made precise what these
strategies are, relying on an informal diagrammatic description. Can we define a set of all proofs of
some propositional logic formula? After all, we managed to define the syntax of propositional logic
as inductively defined set – can we do the same for its semantics?
We can define the syntax of propositional logic using BNF, we have different way to build a
propositional formula as follows:
p, q ::= true | false | P | ¬p | p ∧ q | p ∨ q | p ⇒ q | p ⇔ q
So far, we have seen the BNF notation for inductively defined sets. But what notation should we use
for inductively defined relations? For example, we defined the ⩽ relation between Peano natural
numbers using the following rules:
− for all n ∈ N, 0 ⩽ n;
− if n ⩽ m, then s(n) ⩽ s(m)
Inductively defined relations are often given by means of inference rules:
Here we have two inference rules, named Base and Step; these rules together
define a relation (⩽) ⊆ N × N. The statements above the horizontal line are the
premises - the assumptions that you must establish in order to use this rule; the
statement under the horizontal line is the conclusion that you can draw from
these assumptions.
These rules state that there are two ways to prove that n ⩽ m:
− if n = 0 the ⩽-Base rule tells us that 0 ⩽ n – for any n;
− if we can show n ⩽ m, we can use the ⩽-Step rule to prove s(n) ⩽ s(m).
A rule without premises is called an axiom.
Example:
By repeatedly applying these rules, we can write larger proofs.
For example, to give a formal proof that 2 ⩽ 5 we write:
We can read these rules top-to-bottom or bottom-to-top. Such a
proof is sometimes referred to a as derivation. Each of the
inference rules gives a different ‘lego piece’ that we can use to
write bigger proofs.
, Example of even numbers: We can use this inference rule notation to write all
kinds of relations. For example, we may want to define the unary relation
isEven – that proves that a given number is even.
Example of isSorted array: Similarly, we can define inference rules that
make precise when a list of numbers is sorted. Note that we can require
more than one hypothesis – as in the isSorted-Step rule.
A word over an alphabet Σ is called a palindrome if it reads the
same backward as forward. Examples include: ‘racecar’, ‘radar’, or
‘madam’. Give a inference rules that characterise a unary relation
on words, capturing the fact that they are a palindrome.
Hoofdstuk 2 Natural Deduction
Given the following set of propositional logical formulas over a set of atomic variables P: p, q ::= true
| false | P | ¬p | p ∧ q | p ∨ q | p ⇒ q | p ⇔ q Can we give inference rules that capture precisely the
tautologies? Yes! These inference rules, sometimes called natural deduction, formalize the proof
strategies that we have seen previously.
Conjunction introduction and elimination
Conjunction introduction:
The proof strategy for conjunction introduction
and the inference rule for conjunction
introduction.
