Natural Deduction Rule Induction Ambiguity Simultaneous Induction
1
Natural Deduction and Rule Induction
Dr. Liam O’Connor
University of Edinburgh LFCS UNSW, Term 3 2020
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
Formalisation
To talk about languages in a mathematical way, we need to formalise them. Formalisation
Formalisation is the process of giving a language a formal, mathematical description.
Typically, we describe the language in another language, called the meta-language. For implementations, it may be a programming language such as Haskell, but for formalisations it is usually a minimal logic called a meta-logic.
2
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
Learning from History
What sort of meta logic should we use? There are a number of things to formalise:
Scoping
Static Semantics
Typing
Cost Models
Dynamic Semantics
Runtime Behaviour
3
Parsing
Syntax
Grammar
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
Learning from History
Logicians in the early 20th century had much the same desire to formalise logics. Scoping
Well Formedness
Typing
Proof Models
Logical Models
Truth Models
4
Ambiguity
Syntax
Grammar
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
Learning from History
In this course, we will use a meta-logic based on Natural Deduction and inductive inference rules, originally invented for formalising logics by Gerhard Gentzen in the mid 1930s.
5
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
Judgements
A judgement is a statement asserting a certain property for an object.
Example (Informal Judgements)
3 + 4 × 5 is a valid arithmetic expression.
The string madam is a palindrome.
The string snooze is a palindrome
=⇒ Judgements do not have to hold.
Unary Judgements
Formally, we denote the judgement that a property A holds for an object s by writing s A.
Typically, s is a string when describing syntax, and s is a term when describing semantics.
6
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
Proving Judgements
We define how a judgement may be proven by providing a set of inference rules. Inference Rules
An inference rule is written as:
J1 J2 … Jn J
This states that in order to prove judgement J (the conclusion), it suffices to prove all judgements J1 through to Jn (the premises).
Rules with no premises are called axioms. Their conclusions always hold.
7
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
Examples
Example (Natural Numbers)
0 NatN1
0 is a natural number
n Nat
(S n) NatN2
if n is a natural number, then the successor of n is a natural number.
8
What terms are in the set {n | n Nat}?
{0,(S 0),(S (S 0)),(S (S (S 0))),…}
n Nat
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
Examples
Example (Even and Odd Numbers)
n Even
0 EvenE1 (S (S n)) EvenE2
The Proof Video Game
n Even
(S n) OddO1
9
n Even
To show that a judgement s A holds:
1 Find a rule whose conclusion matches s A.
2 The preconditions of the applied rules become new proof obligations.
3 Rince and repeat until all obligations are proven up to axioms.
n Odd
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
Examples
Example (Even and Odd Numbers)
0 EvenE1
n Even
(S (S n)) EvenE2
n Even
(S n) OddO1
n Even
n Odd
0 EvenE1
(S (S 0)) EvenE2
10
(S (S (S (S 0)))) EvenE2
(S (S (S (S (S 0))))) OddO1
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
Defining Languages
Example (Bracket Matching Language)
M ::= ε|MM|(M) Examples of strings: ε, (), (()), ()(), (()()), . . .
11
Three rules:
Axiom Nesting
Juxtaposition
The empty string is in M
Any string in M can be surrounded by parentheses, giving a new string in M
Any two strings in M can be concatenated to give a new string in M
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
With Rules
The Language M
εM E
(s)M N
ε MME
s1s2M J
M
s M M s1 M s2 MM
εMME
()MMN (())M MN
MJ
()M MN
12
sM
()(()) M
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
Getting Stuck
If we had started with rule MN instead, we would have gotten stuck:
???
)(() M ()(()) MMN
Takeaway
13
Getting stuck does not mean what you’re trying to prove is false!
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
Consider the following rule:
Derivability
sM ((s)) M
Does adding this rule change M? (i.e. is it not admissible to M)?
No, because we could always use rule MN twice instead. Rules that are compositions of existing rules are called derivable:
sM
(s) MMN
((s)) M MN
We can prove rules as well as judgements, by deriving the conclusion of the rule while taking the premises as local axioms.
14
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
Is this rule derivable?
We can derive it like so:
sM (s)s M
sM
(s) MMN
(s)s M
Derivability
s M
MJ
15
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
Is this rule derivable?
Derivability
(s) M
Q sM
It is not admissible, let alone derivable, as it adds strings to M: ε MME ε MME
() M MN
() M MN )( M
MJ
Q
()() M
16
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
Derivability
Is this rule admissible? If so, is it derivable?
()s M sM
It is admissible, as it doesn’t let us prove any new judgements about M.
It is not derivable, as it is not made up of the composition of existing rules. We will see how to prove these sorts of rules are admissible later on.
17
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
Hypothetical Derivations
We can write a rule in a horizontal format as well:
A
is the same as A ⊢ B B
This allows us to neatly make rules premises of other rules, called hypothetical derivations:
Example
A⊢B C
Read as: If assuming A we can derive B, then we can derive C.
18
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
Specifying Logic
With hypotheticals we can specify logic, which was the original purpose of natural deduction. Let A True be the judgement that the proposition A is true.
Example (And and Implies)
A True B True A∧BTrue ∧I
ATrue⊢B True A⇒BTrue ⇒I
A∧B True ATrue ∧E1 A⇒B True
BTrue
A∧B True BTrue ∧E2
ATrue ⇒E
19
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
Specifying Logic, Continued
Example (Or, True, False and Not)
A True B True A∨B True∨I1 A∨B True∨I2
ATrue⊢C True B True⊢C True C True
⊥ True
A True⊥E ¬A True
A∨B True
∨E
⊤ True⊤I A True ⊢ ⊥ True
¬A True ¬I
A True
B True ¬E
20
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
Minimal Definitions
M s M M s1 M s2 MM εM E (s)M N s1s2M J
The above rules are the smallest set of rules to define every string in M. Therefore
If we know that a string s M, it must have been through one of these rules. This is called an inductive definition of M.
21
sM
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
Rule Induction
Suppose we want to show that a property P(s) of strings s holds for any string s M. We will use rule induction.
ε MME sM
(s) MMN
s1 M s2 MMJ
If we show that P(ε) holds, and
P(s) implies P((s)), and
P(s1) and P(s2) implies P(s1s2) Then we have shown P(s) for all s M.
22
s1s2 M
These assumptions are called inductive hypotheses.
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
Rule Induction
Example (Counting Parens)
23
Let op(s) denote the number of opening parentheses in s, and cl(s) denote the number of closing parentheses. We shall prove that
s M =⇒ op(s) = cl(s) by doing rule induction on s M.
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
Example (Counting Parens)
ε MME sM
(s) MMN
s1 M s2 MMJ s1s2 M
Rule Induction
Base Case: op(ε) = 0 = cl(ε) Inductive Case: Assuming I.H:
op(s) = cl(s)
op((s)) = op(s) + 1 = cl(s) + 1 = cl((s))
Inductive Case: Assuming I.Hs:
op(s1) = cl(s1) and op(s2) = cl(s2) op(s1s2) = op(s1) + op(s2) = cl(s1s2)
24
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
Rule Induction in General
Rule Induction Method
Given a set of rules R, we may prove a property P inductively for all judgements that can be inferred with R by showing, for each rule of the form
J1 J2 … Jn J
that if P holds for each of J1 …Jn, then P holds for J.
Therefore, axioms are the base cases of the induction, all other rules form inductive cases, and the premises of each rule give rise to inductive hypotheses.
25
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
Structural Induction
Conventional structural induction such as that on natural numbers, which we have encountered before, is a special case of rule induction.
Natural Number Induction
To show a property P(n) for all n ∈ N, it suffices to:
0 Nat
n Nat (S n) Nat
Show that P(0) holds, and
Assuming P(n), show P(n + 1).
26
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
Recall our definition of even numbers:
0 EvenE1
We could define odd numbers differently:
′ (S 0) Odd′O1
n Even
(S (S n)) EvenE2
Another Example
27
Let’s prove the original Odd rule, but for Odd′ (to whiteboard): n Even
n Even
n Odd′
n Odd′
(S (S n)) Odd′O2
(S n) Odd′
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
Arithmetic
Example (Arithmetic Expression)
Arith ::= i | Arith × Arith | Arith + Arith | (Arith) i ∈Z a Arith b Arith a Arith b Arith
i ArithL a×b Arith P a+b Arith S Infer 1 + 2 × 3 Arith (both ways) to whiteboard
(i ∈ Z)
a Arith (a) Arith
28
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
Ambiguity
Arith is ambiguous, which means that there are multiple ways to derive the same judgement.
For syntax, this is a big problem, as different interpretations of syntax can lead to semantic inconsistency:
2∈Z 3∈Z 1∈Z 2∈Z
1 ∈ Z 2 Arith 3 Arith 1 Arith 2×3 Arith
1+2×3 Arith
1 Arith 2 Arith 3 ∈ Z 1+2 Arith 3 Arith
1+2×3 Arith
29
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
Second Attempt
We want to specify Arith in such a way that enforces order of operations. Here we will use multiple judgements:
Example (Arithmetic Expression)
Atom ::= PExp ::= SExp ::=
i | (SExp) (i ∈ Z) Atom | PExp × PExp PExp | SExp + SExp
i ∈ Z i Atom a PExp
a SExp (a) Atom b PExp
e Atom
e PExp a SExp
e PExp e SExp
30
a×b PExp Consider: Is there still any ambiguity here?
b SExp a+b SExp
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
1 ∈ Z 1 Atom 1 PExp
2 Atom 3 Atom 2 PExp 3 PExp 2×3 PExp
1 Atom 2 Atom 1 PExp 2 PExp 1×2 PExp
3 ∈ Z 3 Atom 3 PExp
More ambiguity
2∈Z 3∈Z 1∈Z 2∈Z
31
1×2×3 PExp
This ambiguity seems harmless, but it would not be harmless for some other
operations. Which ones? Operators that are not associative. We have to specify the associativity of operators. How?
1×2×3 PExp
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
32
Associativities
Operators have various associativity constraints:
Associative Left-Associative Right-Associative
All associativities are equal.
A⊙B⊙C =(A⊙B)⊙C A⊙B⊙C =A⊙(B⊙C)
Try to think of some examples!
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
Enforcing associativity
We force the grammar to accept a smaller set of expressions on one side of the operator only. Show how this works on the whiteboard.
Example (Arithmetic Expression)
Atom ::= PExp ::= SExp ::=
i | (SExp) (i ∈ Z) Atom | Atom × PExp PExp | PExp + SExp
i ∈ Z i Atom a Atom
a SExp (a) Atom b PExp
e Atom
e PExp a PExp
e PExp e SExp
b SExp a+b SExp
33
a×b PExp
Here we made multiplication and addition right associative. How would we do left?
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
Bring Back Parentheses The Parenthetical Language
M s M M s1 M s2 MM εM E (s)M N s1s2M J
Is this language ambiguous? to whiteboard
34
sM
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
Ambiguity in Parentheses
Not only is it ambiguous, it is infinitely so. Strings like ()()() could be split at two different locations by rule MJ, but if we use ε, then even the string () is ambiguous:
ε MME εMME εMME ()M MN
() M MN
() M
ε MME ()M MN
MJ
ε MME
εMME () M
MJ
() M
MJ
35
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
We will eliminate the ambiguity by once again splitting M into two judgements, N and L.
The crucial observation is that terms in M are a list (L) of terms nested within parentheses (N).
Example (Unambiguous Parentheses)
sL
L sLN s1Ns2LL ε L E (s) N N s1s2 L J
sN
36
Natural Deduction Rule Induction Ambiguity Simultaneous Induction
Proving Equivalence
Now we shall prove M = L. There are two cases, each dispatched with rule induction: sM sL
sL sM
The first case requires proving a lemma. The second requires simultaneous induction. These proofs will be carried out on the “board” (iPad). A properly typeset PDF of the proof will also be uploaded.
37