binary expressions: represent anything that comes in two kinds
represent statements about the world (natural or constructed, real or imaginary) represent digital circuits
represent human behavior
theorems: represent one kind represent true statements
represent circuits with high voltage output represent innocent behavior
antitheorems: represent the other kind represent false statements
represent circuits with low voltage output represent guilty behavior
1/23
0 operands 1 operand 2 operands 3 operands
⊤ ⊥
¬x
x∧y x∨y x⇒y x⇐y x=y x⧧y if x then y else z fi
precedence and parentheses associative operators: ∧ ∨ = ⧧
x∧y∧z meanseither (x∧y)∧z or x∧(y∧z)
x∨y∨z meanseither (x∨y)∨z or x∨(y∨z) continuing operators: ⇒ ⇐ = ⧧
x=y=z means x=y ∧ y=z x⇒y⇒z means (x⇒y) ∧ (y⇒z)
big operators: = ⇒ ⇐
same as = ⇒ ⇐ but later precedence
x=y⇒z means (x=y) ∧ (y⇒z)
2/23
truth tables
⊤⊥ ¬⎪⊥⊤
⊤⊤ ⊤⊥ ⊥⊤ ⊥⊥ ∧⎪⊤⊥⊥⊥
∨⎪⊤⊤⊤⊥ ⇒⎪⊤⊥⊤⊤ ⇐⎪⊤⊤⊥⊤ =⎪⊤⊥⊥⊤ ⧧⎪⊥⊤⊤⊥
⊤⊤⊤ ⊤⊤⊥ ⊤⊥⊤ ⊤⊥⊥ ⊥⊤⊤ ⊥⊤⊥ ⊥⊥⊤ ⊥⊥⊥ if then else fi ⎪ ⊤ ⊤ ⊥ ⊥ ⊤ ⊥ ⊤ ⊥
3/23
variables are for substitution (instantiation)
• add parentheses to maintain precedence
in x∧y replace x by ⊥ and y by ⊥∨⊤ result: ⊥∧(⊥∨⊤)
• every occurrence of a variable must be replaced by the same expression in x∧x replace x by ⊥ result: ⊥∧⊥
• different variables can be replaced by the same expression or different expressions in x∧y replace x by ⊥ and y by ⊥ result: ⊥∧⊥
in x∧y replace x by ⊤ and y by ⊥ result: ⊤∧⊥
4/23
new binary expressions
(the grass is green)
(the sky is green)
(there is life elsewhere in the universe) (intelligent messages are coming from space) 1 +1 = 2
0 /0 = 5
———————————————————————————
consistent: no binary expression is both a theorem and an antitheorem (no overclassified expressions)
complete: every fully instantiated binary expression is either a theorem or an antitheorem (no unclassified expressions)
5/23
Proof Rules Axiom Rule If a binary expression is an axiom, then it is a theorem.
x+y = y+x
If a binary expression is an antiaxiom, then it is an antitheorem.
is a mathematical expression
represents a truth in an application such that
when you put quantities together, the total quantity does not depend
on the order in which you put them together is an axiom
is a theorem
is equivalent to
is true (not really)
x+y = y+x
6/23
Proof Rules Axiom Rule If a binary expression is an axiom, then it is a theorem.
If a binary expression is an antiaxiom, then it is an antitheorem.
axiom: ⊤ antiaxiom: ⊥
axiom: antiaxiom: axiom:
(the grass is green) (the sky is green)
(intelligent messages are coming from space) ⇒ (there is life elsewhere in the universe)
Evaluation Rule If all the binary subexpressions of a binary expression are classified, then it is classified according to the truth tables.
7/23
Proof Rules
Completion Rule If a binary expression contains unclassified binary subexpressions,
theorem:
theorem:
and all ways of classifying them place it in the same class, then it is in that class.
(there is life elsewhere in the universe) ∨ ⊤ (there is life elsewhere in the universe)
∨ ¬(there is life elsewhere in the universe)
(there is life elsewhere in the universe) ∧ ¬(there is life elsewhere in the universe)
antitheorem:
8/23
Proof Rules
Consistency Rule If a classified binary expression contains binary subexpressions, and
only one way of classifying them is consistent, then they are classified that way.
We are given that x and x⇒y are theorems. What is y ?
If y were an antitheorem, then by the Evaluation Rule, x⇒y would be an antitheorem. That would be inconsistent. So y is a theorem.
We are given that ¬x is a theorem. What is x ?
If x were a theorem, then by the Evaluation Rule, ¬x would be an antitheorem. That would be inconsistent. So x is an antitheorem.
No need to talk about antiaxioms and antitheorems.
9/23
Proof Rules Instance Rule If a binary expression is classified,
then all its instances have that same classification.
axiom: x = x theorem: x = x
theorem: ⊤=⊥∨⊥ = ⊤=⊥∨⊥
theorem:
=
(intelligent messages are coming from space) (intelligent messages are coming from space)
Classical Logic: Constructive Logic: Evaluation Logic:
all five rules
not Completion Rule
neither Consistency Rule nor Completion Rule
10/23
Expression and Proof Format
a∧b ∨ c NOT a ∧ b∨c ( first part
∧ second part )
C and Java convention
while (something) { various lines
in the body
of the loop }
11/23
a∧b ∨ c
( first part
∧ second part first part
= second part
expression0
= expression1
= expression2
= expression3
NOT a ∧ b∨c
)
Expression and Proof Format
means
expression0=expression1 ∧ expression1=expression2 ∧ expression2=expression3
12/23
a∧b ∨ c
( first part
∧ second part first part
= second part
expression0
= expression1
= expression2
= expression3
NOT a ∧ b∨c
)
Expression and Proof Format
hint0 hint1 hint2
13/23
Expression and Proof Format
Prove a∧b⇒c = a⇒(b⇒c) a ∧ b ⇒ c
= ¬(a ∧ b) ∨ c
= ¬a ∨ ¬b ∨ c
= a ⇒ ¬b ∨ c
= a ⇒ (b ⇒ c)
Material Implication
Duality Material Implication Material Implication
= ¬ a Instance of Material Implication: a ∧ b ⇒ c = ¬(a ∧ b) ∨ c
Material Implication: a
⇒ b
∨ b
14/23
Expression and Proof Format
Prove a∧b⇒c = a⇒(b⇒c) a ∧ b ⇒ c
= ¬(a ∧ b) ∨ c
= ¬a ∨ ¬b ∨ c
= a ⇒ ¬b ∨ c
= a⇒(b⇒c)
(a ∧ b ⇒ c =
= (¬(a∧b)∨c = ¬a∨(¬b∨c))
= (¬a ∨ ¬b ∨ c = ¬a ∨ ¬b ∨ c)
= ⊤
Material Implication
Duality Material Implication Material Implication
Material Implication 3 times Duality Reflexivity of =
a ⇒ (b ⇒ c))
15/23
Monotonicity and Antimonotonicity
covariance and varies directly as and nondecreasing and sorted and
contravariance varies inversely as nonincreasing sorted backwards
x≤y ⇒ fx≤fy
fx fx
x≤y ⇒ fx≥fy
xx
16/23
number:
x≤y
–∞≤+∞ 0≤1
x≤y ⇒ fx≤fy x≤y ⇒ fx≥fy
x⇒y
⊥ ⇒ ⊤
x⇒y ⇒ fx⇒fy
x⇒y ⇒ fx⇐fy
x is less than or equal to y smaller≤larger
f ismonotonic
as x gets larger, f x gets larger (or equal) f isantimonotonic
as x gets larger, f x gets smaller (or equal)
x implies y x is stronger than or equal to y stronger ⇒ weaker
f ismonotonic
as x gets weaker, f x gets weaker (or equal)
f isantimonotonic
as x gets weaker, f x gets stronger (or equal)
binary:
Monotonicity and Antimonotonicity
17/23
Monotonicity and Antimonotonicity
¬a
a∧b
a∨b
a⇒b
a⇐b
if a then b else c fi
¬(a ∧ ¬(a∨b))
¬(a ∧ ¬a) =⊤
antimonotonic in a monotonic in a monotonic in a
antimonotonic in a monotonic in a monotonic in b
monotonic in b monotonic in b monotonic in b
antimonotonic in b monotonic in c
⇐
use the Law of Generalization a ⇒ a∨b now use the Law of Noncontradiction
18/23
In a ∧ b , when changing a , we can assume b . a∧b
↓
= c∧b
If b is ⊤ , we have assumed correctly.
If b is ⊥ , then a ∧ b and c ∧ b are both ⊥ , so the equation is ⊤ anyway.
Context
19/23
In In
a ∧ b , when changing a ∧ b , when changing
a , we can assume b , we can assume
b . a .
=
=
= =⊤
¬(a ∧ ¬(a∨b)) ¬(a ∧ ¬(⊤∨b)) ¬(a ∧ ¬⊤) ¬(a∧⊥)
assume a to simplify ¬(a∨b) Symmetry Law and Base Law for ∨ Truth Table for ¬ BaseLawfor ∧
Context
20/23
In a ∧ b , when changing
In a ∧ b , when changing
In a ∨ b , when changing
In a ∨ b , when changing
In a ⇒ b , when changing
In a ⇒ b , when changing
In a ⇐ b , when changing
In a ⇐ b , when changing
In if a then b else c fi , when changing In if a then b else c fi , when changing In if a then b else c fi , when changing
b . a . ¬b . ¬a .
¬b .
a.
b.
¬a .
can assume b⧧c . can assume a .
a , we can assume b , we can assume a , we can assume b , we can assume
a , we can assume b , we can assume a , we can assume b , we can assume
Context
a , we
b , we
c , we can assume ¬a .
21/23
number expressions represent quantity
number expressions
0 1 2 597 1.2 1e10 ∞
–x x+y x–y x×y x/y xy
if a then x else y fi
binary expressions
x=y x⧧y x
Number Theory
22/23
Character Theory
“A” “a” “ ” “““” “”””
succ pred if then else fi
=⧧<>≤≥
23/23