Notes

In logic, a tautology is a formula or statement that is always true whatever values replace the variables in it.

Most of these formula are translated from [Reichenbach47].

They may have been misprinted. One or two are surprising. It's likely that I've mistyped some of them. So they have been set up as unlabeled until they have been checked by someone else. The unlabeled formula can't be trusted and shouldn't be used without proof. They will be asserted and labeled when they have been checked/proved/reviewed. At that point they can be used.

If you'd like to contribute a proof or a correction I will acknowledge it. When proved I'll label the formula. [click here if you can fill this hole] Proofs can follow any of the patterns in [ ../maths/logic_20_Proofs100.html ] [ ../maths/logic_25_Proofs.html ] [ ../maths/logic_27_Tableaux.html ] or using a tool like PVS, or even truth tables.

I plan to avoid publishing the proofs because they make useful exercises when learning symbolic logic.

Propositional Tautologies


Net
For a,b,c,d: @, -- propositions.

For a, b, a->b :@=(if a then b), local short-hand.

For a,b, a b :@=(a and b), local short-hand.

1. a iff a.
2. (a or a) iff a.
3. (a a) iff a.
4. not not a iff a.
5. a or not a.
6. not(a and not a).
7. (a -> not a) iff not a.
8. (not a -> a) iff a.

9. (a or b) iff (b or a).
10. (a or (b or c)) iff ((a or b)or c) iff (a or b or c).
11. (a or b or c...) = or(a,b,c,...).

12. (a b) iff (b a).
13. (a (b c)) iff ((a b) c) iff (a b c).
14. (a and b and c...) = and(a,b,c,...).

15. (a (b or c)) iff ((a b) or (a c)).
16. (a or (b c)) iff ((a or b) (a or c)).
17. ((a or b)(c or d)) iff (a c or a d or b c or b d).
18. ((a b)or(c d)) iff ((a or c) (a or d) (b or c) (b or d)).
19. a (a or b) iff a or(a b) iff a.

20. not(a or b) iff (not a and not b).
21. not(a b) iff (not a or not b).
22. b or not b iff true.
23. b and not b iff false.
24. a and true iff a iff a or false.
25. a or (not a and b) iff a or b.

26. (a->b) iff (not a or b) iff not( a and not b).
27. (a->b) iff (not b -> not a).
28. (a->(b->c)) iff (b->(a->c)) iff (a b->c).
29. (a->b)(a->c) iff (a -> b c).
30. (a->c)(b->c) iff((a or b)->c).
31. (a->b)or(a->c) iff (a -> (b or c)).
32. (a->c)or(b->c) iff(a b->c).

33. (a iff b) iff (b iff a).
34. (a iff b) iff ((a->b)(b->a).
35. (a iff b) iff ((a b) or (not a)( not b)).
36. not(a iff b) iff ((not a) iff b) iff (a iff (not b)).
37. (a iff b) iff ((not a) iff (not b).

38. if((a iff b)(b iff c))then (a iff c).
39. (a iff b)(b iff c) = (a iff b iff c)=iff(a,b,c).

40. if a then (a or b).
41. if a b then a.
42. if a then (b->a).
43. if not a then (a->b).
44. if a (a->b) then b.
45. if a ((not a) or b) then a b.
46. if (a->b) then (a->(b or c)).
47. if (a->b) then (a c->b).
48. if ((a or c)->b) then (a->b).
49. if (a->b c) then (a->b).
50. if ((a->b)(c->d))then (a c ->b d).
51. if ((a->b)(c->d))then ((a or c) ->(b or d)).
52. if((a->b)(b->c))then (a->c).

(End of Net)



Tautologies for the Predicate calculus


Net
For a,b,c,d: @, T: Types, x,y,z:T, f,g:T>->@.

For a, b, a->b :@=(if a then b), local short-hand.

For a,b, a b :@=(a and b), local short-hand.

For f, all f :=for all x(f(x)).

For f, some f :=for some x(f(x)).

For f, no f :=for no x(f(x)).

1. for all x(f(x) g(x)) iff ((all f) (all g) )
2. if (all f or all g) then for all x(f(x) or g(x) ).
3. if for all x(f(x) or g(x) ) then ( all f or some g).

   For f,g, f==>g := for all x(if f(x) then g(x)).

4. if f ==> g then all f-> all g).
5. if f ==> g and all f then all g.
6. if f ==> g then (some f-> some g).
7. if f ==> g then ( no g-> no f).

8. if all f and f==>g then all g.
9. if some f and f==>g then some g.
10. if f==>g and no g then no f.

    For f, g, f===g :=for all x(f(x) iff g(x) )

11. if f===g then ( all f iff all g).
12. if f===g then ( some f iff some g).
13. if f===g then ( no f iff no g).

14. (for some x(f(x) or g(x))) iff (some f or some g).
15. (for some x(f(x) -> g(x))) iff (all f -> some g).
16. if (some f -> some g) then for some x(f(x)->g(x)).
17. if (some f -> all g) then f==>g.
18. if (some f and all g) then for some x(f(x) and g(x)).

19. for all x(a and f(x)) iff a and all f.
20. for all x(a or f(x)) iff a or all f.
21. for all x(a -> f(x)) iff a -> all f.
22. for all x(f(x)->a) iff some f ->a.
23. if for all x(f(x) iff a) then (all f iff a).
24. for all x(a) iff a.

25. for some x(a and f(x)) iff a and some f.
26. for some x(a or f(x)) iff a or some f.
27. for some x(a -> f(x)) iff a -> some f.
28. for some x(f(x)->a) iff all f ->a.
29. if for some x(f(x) iff a) then (some f iff a).
30. for some x(a) iff a.

31. not for all x(f(x)) iff for some x(not f(x)).
32. not for some x(f(x)) iff for all x(not f(x)).
33. if for all x(not f(x)) then not for all x(f(x)).
34. if no f then for some x(not f(x)).

35. For all x, if all f then f(x).
36. For all x, if f(x) then some f.
37. if all f then some f.

    For h,i:T><T->@, predicates with two arguments/parameters.

38. for all x,y(h(x,y)) iff for all y,x(h(x,y)).
39. for some x,y(h(x,y)) iff for some y,x(h(x,y)).

40. if for some x, all y(h(x,y)) then for all y, some x(h(x,y)).
41. (for some x, all y(f(x) g(y))) iff for all y, some x(f(x) g(y)).
42. (for some x, all y(f(x) or g(y))) iff for all y, some x(f(x) or g(y)).
43. (for some x, all y(f(x)-> g(y))) iff for all y, some x(f(x)-> g(y)).

44. if for all x, y(h(x,y) or i(x,y)) then (for some x, all y(h(x,y)) or for all x, some y(i(x,y))).

(End of Net)

Notes on MATHS Notation