[Skip Navigation] [CSUSB] / [CNS] / [Comp Sci Dept] / [R J Botting] / [Samples] / tautologies
Tue Sep 18 15:27:15 PDT 2007

# Tautologies of the Propositional and Predicate Calculi

## 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

1. iff::="if and only if".
2. if_then_::="material implication".
3. some::="existencial quantifier".
4. all::="universal quantifier".
5. and::="conjunction operator".
6. or::="disjunction operator".
7. for::="prefixes quantifiers", "for quantifier variable, ...(proposition).
8. For::="introduces parameters and the types of variables".

Special characters and words are defined in [ intro_characters.html ] that also outlines the syntax of expressions and a document.

The notation used here is a formal language with syntax and semantics described using traditional formal logic [ logic_0_Intro.html ] plus sets, functions, relations, and other mathematical extensions.

For a more rigorous description of the standard notations see

9. STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html

For a complete listing of pages in this part of my site by topic see [ home.html ]