.Open 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 .See [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. .Hole Proofs can follow any of the patterns in .See ../maths/logic_20_Proofs100.html .See ../maths/logic_25_Proofs.html .See ../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. a iff a. (a or a) iff a. (a a) iff a. not not a iff a. a or not a. not(a and not a). (a -> not a) iff not a. (not a -> a) iff a. (a or b) iff (b or a). (a or (b or c)) iff ((a or b)or c) iff (a or b or c). (a or b or c...) = or(a,b,c,...). (a b) iff (b a). (a (b c)) iff ((a b) c) iff (a b c). (a and b and c...) = and(a,b,c,...). (a (b or c)) iff ((a b) or (a c)). (a or (b c)) iff ((a or b) (a or c)). ((a or b)(c or d)) iff (a c or a d or b c or b d). ((a b)or(c d)) iff ((a or c) (a or d) (b or c) (b or d)). a (a or b) iff a or(a b) iff a. not(a or b) iff (not a and not b). not(a b) iff (not a or not b). b or not b iff true. b and not b iff false. a and true iff a iff a or false. a or (not a and b) iff a or b. (a->b) iff (not a or b) iff not( a and not b). (a->b) iff (not b -> not a). (a->(b->c)) iff (b->(a->c)) iff (a b->c). (a->b)(a->c) iff (a -> b c). (a->c)(b->c) iff((a or b)->c). (a->b)or(a->c) iff (a -> (b or c)). (a->c)or(b->c) iff(a b->c). (a iff b) iff (b iff a). (a iff b) iff ((a->b)(b->a). (a iff b) iff ((a b) or (not a)( not b)). not(a iff b) iff ((not a) iff b) iff (a iff (not b)). (a iff b) iff ((not a) iff (not b). if((a iff b)(b iff c))then (a iff c). (a iff b)(b iff c) = (a iff b iff c)=iff(a,b,c). if a then (a or b). if a b then a. if a then (b->a). if not a then (a->b). if a (a->b) then b. if a ((not a) or b) then a b. if (a->b) then (a->(b or c)). if (a->b) then (a c->b). if ((a or c)->b) then (a->b). if (a->b c) then (a->b). if ((a->b)(c->d))then (a c ->b d). if ((a->b)(c->d))then ((a or c) ->(b or d)). if((a->b)(b->c))then (a->c). .Close.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)). for all x(f(x) g(x)) iff ((all f) (all g) ) if (all f or all g) then for all x(f(x) or g(x) ). 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)). if f ==> g then all f-> all g). if f ==> g and all f then all g. if f ==> g then (some f-> some g). if f ==> g then ( no g-> no f). if all f and f==>g then all g. if some f and f==>g then some g. if f==>g and no g then no f. For f, g, f===g :=for all x(f(x) iff g(x) ) if f===g then ( all f iff all g). if f===g then ( some f iff some g). if f===g then ( no f iff no g). (for some x(f(x) or g(x))) iff (some f or some g). (for some x(f(x) -> g(x))) iff (all f -> some g). if (some f -> some g) then for some x(f(x)->g(x)). if (some f -> all g) then f==>g. if (some f and all g) then for some x(f(x) and g(x)). for all x(a and f(x)) iff a and all f. for all x(a or f(x)) iff a or all f. for all x(a -> f(x)) iff a -> all f. for all x(f(x)->a) iff some f ->a. if for all x(f(x) iff a) then (all f iff a). for all x(a) iff a. for some x(a and f(x)) iff a and some f. for some x(a or f(x)) iff a or some f. for some x(a -> f(x)) iff a -> some f. for some x(f(x)->a) iff all f ->a. if for some x(f(x) iff a) then (some f iff a). for some x(a) iff a. not for all x(f(x)) iff for some x(not f(x)). not for some x(f(x)) iff for all x(not f(x)). if for all x(not f(x)) then not for all x(f(x)). if no f then for some x(not f(x)). For all x, if all f then f(x). For all x, if f(x) then some f. if all f then some f. For h,i:T>@, predicates with two arguments/parameters. for all x,y(h(x,y)) iff for all y,x(h(x,y)). for some x,y(h(x,y)) iff for some y,x(h(x,y)). if for some x, all y(h(x,y)) then for all y, some x(h(x,y)). (for some x, all y(f(x) g(y))) iff for all y, some x(f(x) g(y)). (for some x, all y(f(x) or g(y))) iff for all y, some x(f(x) or g(y)). (for some x, all y(f(x)-> g(y))) iff for all y, some x(f(x)-> g(y)). 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))). .Close.Net .Close . Notes on MATHS Notation iff::="if and only if". if_then_ ::="material implication". some::="existencial quantifier". all::="universal quantifier". and::="conjunction operator". or::="disjunction operator". for::="prefixes quantifiers", "for quantifier variable, ...(proposition). For::="introduces parameters and the types of variables". Special characters and words are defined in .See http://www.csci.csusb.edu/dick/maths/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 .See http://www.csci.csusb.edu/dick/maths/logic_0_Intro.html plus sets, functions, relations, and other mathematical extensions. For a more rigorous description of the standard notations see STANDARD::=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 .See http://www.csci.csusb.edu/dick/maths/home.html