[
Introduction
]
[
File Structure
]
[
#check PROP
]
[
#check PRED
]
[
#check PREDTYPES
]
[
#check TP
]
[
#check ND
]
[
#check ST
]
[
Arithmetic
]
[
Sets
]
[
#check Z
]
[
#check PC
]
[
Contributions by Students
]
[
Credits
]
Keywords
]
Arithmetic theory is a theory of predicate logic in which the functions and predicates of operations on numbers can be used in predicate logic expressions and proofs. Below is the syntax for these operators, many of which are infix operators. These can be used in any predicate logic formula.
"nat" is a keyword in george for the natural numbers type. Arithmetic operators are parsed following BEDMAS and are left associative except for exponent which is right associative.
| Syntax in george | Meaning | Syntax in george | Meaning |
|---|---|---|---|
| a + b | addition | a - b | subtraction |
| a * b | multiplication | a / b | division |
| a^b | exponentiation | ||
| a > b | greater than | a < b | less than |
| a >= b | greater than or equal to | a <= b | less than or equal to |
These operators can be used in any predicate logic formula. For example:
#check PRED // Every number that is less than 5 is also less than 10. forall x. x < 5 => x <10
In proofs, we use the rule by arith on .. to justify any transformations based on arithmetic laws. In addition, in natural deduction we have a special rule by induction on ..., which combines the universal introduction and implication introduction subproofs needed for induction (explained in lecture). Here are three examples that use induction and arithmetic reasoning:
#check ND
|- forall n:nat . 3^n >= 2^n
bc) 3^0 >= 2^0 by arith
ih) inductionstep 3^ng >= 2^ng {
2) 3^ng * 3 >= 2^ng * 2 by arith on ih
3) 3^(ng+1) >= 2^(ng+1) by arith on 2
}
4) forall n. 3^n >= 2^n by induction on bc,ih-3
#check ND
// relies on a normal definition of the summation
// sum(i,x,y,j) means the sum of j's for i=x to i=y
|-
forall n. n >= 1 => sum(i,1,n, 2 * i - 1) = n^2
1) assume 0 >= 1 {
2) !(0 >= 1) by arith
3) sum(i,1,0, 2 * i - 1) = 0^2 by not_e on 1,2
}
bc) 0 >= 1 => sum(i,1,0, 2 * i - 1) = 0^2 by imp_i on 1-3
ih) inductionstep ng >= 1 => sum(i,1,ng, 2 * i - 1) = ng^2 {
4) assume ng + 1 >= 1 {
5) ng = 0 | ng >= 1 by arith on 4
6) case ng = 0 {
7) sum(i,1,0+1, 2 * i - 1) = 2 * 1 - 1 by arith // defn of sum
8) sum(i,1,0+1, 2 * i - 1) = (0+1)^2 by arith on 7
11) sum(i,1,ng+1, 2*i -1) = (ng+1)^2 by eq_e on 6,8
}
12) case ng >= 1 {
13) sum(i,1,ng, 2 * i - 1) = ng^2 by imp_e on ih,12
15) sum(i,1,ng+1, 2 * i - 1) = 2*(ng+1) - 1 + sum(i,1,ng, 2 * i -1) by arith on 12 // and defn of sum
16) sum(i,1,ng+1, 2 * i - 1) = 2*(ng+1) - 1 + ng^2 by eq_e on 15,13
17) sum(i,1,ng+1, 2 * i - 1) = ng^2 + 2*ng +1 by arith on 16
18) sum(i,1,ng+1, 2 * i - 1) = (ng + 1)^2 by arith on 17
}
20) sum(i,1,ng+1,2* i - 1) = (ng+1)^2 by cases on 5, 6-11,12-18
}
21) ng +1 >= 1 => sum(i,1,ng+1,2* i - 1) = (ng+1)^2 by imp_i on 4-20
}
22) forall n . n >= 1 => sum(i,1,n, 2 * i - 1) = n^2 by induction on bc, ih-21
#check ND
// f(0) = 0
// f(1) = 1
// f(n) = f(n-1) + f(n-2) for n >= 2
|-
forall n . exists y . f(3*n) = 2*y
1) f(3*0) = f(0) by arith on 1
3) f(3*0) = 0 by arith on 1 // and defn of f
4) f(3*0) = 2*0 by arith on 3
bc) exists y . f(3*0) = 2 * y by exists_i on 4
ih) inductionstep exists y . f(3*ng) = 2 * y {
6) for some yu assume f(3*ng) = 2*yu {
7) 3*ng + 3 >= 2 by arith // needed to apply defn of f
8) 3*ng + 2 >= 2 by arith // needed to apply defn of f
9) f(3*(ng+1)) = f(3*ng + 3) by arith
11) f(3*(ng+1)) = f(3*ng + 2) + f(3*ng + 1) by arith on 9,7 // and defn of f
12) f(3*(ng+1)) = f(3*ng + 1) + f(3*ng) + f(3*ng +1) by arith on 11,8 // and defn of f
13) f(3*(ng+1)) = 2*f(3*ng + 1) + f(3*ng) by arith on 12
14) f(3*(ng+1)) = 2*f(3*ng + 1) + 2 * yu by eq_e on 13,6
15) f(3*(ng+1)) = 2 * f(3*ng +1 + yu) by arith on 14
17) exists y . f(3*(ng+1)) = 2 * y by exists_i on 15
}
18) exists y . f(3*(ng+1)) = 2 * y by exists_e on ih, 6-17
}
19) forall n . exists y . f(3*n) = 2*y by induction on bc, ih-18
george checks some of the arith rules but if it cannot conclude that the arith steps are correct then it treats them as magic rules. Induction rules are treated as magic rules and does not check the correctness of these, therefore george gives you a warning that these rules have been used and not checked, but for the other TP/ND rules, it checks that they have been used correctly.