**argument**a set of propositions where one (the "corollary") is claimed to follow from the others (the "premises").*valid argument*one whose corollary is true whenever all the premises are true;*validation*the process of ascertaining the validity of an argument; cf proof of theorem.-
**axiom**a statement (usually a fully quantfied predicate) that is assumed to be true for the purposes of proving other statements.**axiomatic theory**a noncontradictory (i.e. not giving rise to a contradiction) set of axioms intended as a basis for proving other statements**calculus**a set of strings of symbols (i.e. fomulae) with a set of formal rules that define how a formula can be rewritten without changing its value ("calculated"). The meaning of the formulae and the justification of the rules are not part of the calculus and may not be relied upon in calculations.**(logical) connectives**words, such as "and" ,"or", "if...then..", etc., that are used to connect atomic propositions in a compound one.**contradiction**a compound proposition whose truth value is "false" irrespective of the truth values of the atomic propositions it consists of. **(partial) correctness**a program is partially correct if its postcondition is satisfied whenever it terminates. In determining partial correctness it is assumed that the precondition is satisfied. Partial correctness does not imply that the program will necessarily terminate.**(full) correctness**a program is correct if it is partially correct*and*terminates whenever the precondition is satisfied.**equivalence**the logical connective that yields*true*only when both propositions are either true or false simultaneously. It is represented as "*p*if and only if*q*" and can be understood as mutual implication: "(*p*if*q*) and (*q*if*p*)"**implication**the logical connective represented as "if...then..." or by an arrow ->. The truth vale of "if*p*then*q*" is true unless*p*is true and*q*is false.**inference rules for programs**are logical arguments that infer partial correctness of a command (in a programming language) from the partial correctness of its constituent parts.-
**instantiation**the process of replacing a variable proposition occurring in a tautology by any particular propositional statement. The result of instantiation is guaranteed to be another tautology.**laws of logic**equivalence-based tautologies which can be used for simplification of logical formulae. Examples are: de Morgan's laws, associativity of "or", etc. **Modus Ponens**also known as the "rule of detachment" and "method of affirming". An inference rule which states that if*p*implies*q*and*p*is true then so is*q*.**Modus Tollens**also known as the "method of denying". An inference rule which states that if*p*implies*q*and*q*is false, then so is*p.***operator "not"**the operator which, when applied to a propositon, inverts its truth value, i.e. makes a true proposition a false one and vice versa.**predicate**a proposition whose truth value depends on a variable. The variable may range over any class of objects (the "universe of discourse") as long as the truth value of the proposition is certain.**principle of mathematical induction (week form)**states that for a predicate*P*(*n*) with the universe of discours being all natural numbers, the fact that both*P*(1) is true and for all*n*>0*P*(*n*) implies*P*(*n*+1) constitutes a proof of the truth of*P*(*n*) for all*n*>0.**principle of mathematical induction (strong form)**states that for a predicate*P*(*n*) with the universe of discours being all natural numbers, the fact that both*P*(1) is true and the conjunction of all*P*(*k*),*k=*1..*n*implies*P*(*n*+1) constitutes a proof of the truth of*P*(*n*) for all*n*>0.**principle of well ordering**states that every set of natural numbers has the least element.**program verification**the process of proving the correctness argument for a given program with respect to a particular set of pre- and postconditions.-
**proof of a theorem**the process of validating the logical argument contained in the theorem possibly using its axioamatic theory as additional premises.**direct proof**a proof technique which assumes the truth of the theorem's premises for some unknown instance of the variables and then attempts to derive the truth of the corollary for the same instance of the variables.**contrapositive proof**a proof technique which assumes the falsehood of the theorem's corollary on some unkonwn instance of the variables and then attempts to demonstrate that at least one premise of the theorm is false on the same instance of the variables.**proof by contradiction**also known as "reductio ad absurdum", a proof technique that assumes that there exists an instance of the variables for which all the premises are true and at the same time the corollary is false. It then goes on to show that this assumption leads to a contradiction.-
**proposition**a statement with a definite truth value. *atomic proposition,*one that does not have internal structure, i.e. no smaller propositions can be identified as its parts.*compound proposition,*one that consists of one or more propositions held together by logical connectives and the operator "not".-
**quantifier**an operator applicable to a predicate and its parameter:*universal quantifier*, pronounced "for all" and denoted by the letter A written upside down. When applied to a predicate, it yields "true" if the predocate is true*everywhere*in the universe of discorse;*existential quantifier*, pronounced "there exists" and denoted by the letter E reflected about a vertical line (we have no font for this either) When applied to a predicate, it yields "true" if the predicate is true*anywhere*in the universe of discourse.-
**rules of inference**small valid arguments that involve only variable propositions. With respect to their variables, the rules of inference are tautologies. When appropriately instantiated, they are useful in proving other arguments valid.**substitution**the process of replacing a proposition that occurs in a given compound proposition by its equivalent. The result of substitution is guaranteed to be equivalent to the original compound proposition.**(Hypothetical) Syllogism**an inference rule which states that if*p*implies*q*and*q*implies*r*then*p*implies*r*.-
**tautology**a compound proposition that is true irrespective of the truth values of the atomic propositions that it consists of.**theorem**a statement claimed to be true given the truth of an axiomatic theory. A theorem is said to be stated*in*the axiomatic theory on whose truth it is dependent. All theorems should either refer to or assume the axiomatic theory they are stated in.-
**universe of discourse**see**predicate****universal generalisation**the rule in the predicate calculus that states that if a predicate*P*(*x*) is true for any*x*then it is true for all*x.*It is assumed that*x*ranges over the universe of discourse.**universal specification**the rule in the predicate calculus that state that if a predicate*P*(*x*) is true for all*x*then it is true for any given*x.*It is assumed that*x*ranges over the universe of discourse.