See UNISA – Summary of 2010 Posts for a list of related UNISA posts. This post is one of three summary posts I will be building up over the next couple of months, so if you are following this topic or completing the same course as I this year, you may want to bookmark this post and come back occasionally for a peek and to give “candid” feedback.
** UNDER CONSTRUCTION ** Last change: 20100405
Summary
The eye of this excursion is the firstorder logic (FOL) language which goes back to Aristotle and is used by a variety of environments such as mathematics, philosophy, linguistics and artificial intelligence.
The two examples above are referred to in the terminology summary below:
Terminology  Description  Example 
Arity  Defines how many namesconstants a predicate needs. Unary = 1, Binary = 2, … 
LeftOf(x,y) … Arity = 2 Planet(pluto) … Arity = 1 
Atomic Sentence  Is a predicate followed by the right number (arity) of names  Bigger(saturn,pluto)
Sentence –> Pluto is a planet 
Constant  Symbols used to refer to a specific object, analogous to names, and written in lowercase.  pluto 
Conclusion  Is a logical consequence of premises.  
Conjunctive Normal Form (CNF)  A sentence is in conjunctive normal form (CNF) is it is a conjunction of one or more disjunctions of one or more literals.  See UNISA Chatter – Formal Logic: Propositional Logic Proofs for a proof  an example. 
Disjunctive Normal Form (DNF)  A sentence is in disjunctive normal form (DNF) is it is a disjunction of one or more conjunctions of one or more literals.  See UNISA Chatter – Formal Logic: Propositional Logic Proofs for a proof  an example. 
Identity Introduction  Rule that embodies the reflexity of identity   n = n = Intro 
Identity Elimination  Rule that embodies indiscernibility of identicals   1. P(n)  2. n = m  3. P(m) = Elim 1,2 
Indiscernibility of identicals  Also known as substitution.  If b = c, then anything is true of b is also true of c. 
Infix Notation  With infix notation the predicate appears between two arguments  x = y 
Informal proofs of nonconsequence  Possible situation were premises are true, but conclusion is false.
See UNISA Chatter – Formal Logic: Propositional Logic Examples for more examples. 
 Nearly all soccer players are funny true  Grumpy plays soccer true   Grumpy is funny false 
Logical Truth  Necessity  X is logically necessary if and only if it is impossible for X to be false.  See UNISA Chatter – Formal Logic: Propositional Logic Proofs for a proof  an example. 
Logical Equivalence  X and Y are logically equivalent if and only if it is impossible for either of them to be true and the other false.  See UNISA Chatter – Formal Logic: Propositional Logic Proofs for a proof  an example. 
Logical Consequence  X is a logical consequence of Y1, Y2, …Yn if and only if it is impossible for Y1, Y2, … Yn to be true and X is false.  See UNISA Chatter – Formal Logic: Propositional Logic Proofs for a proof  an example. 
Negative Normal Form (NNF)  A sentence is in negative normal form (NNF) if all occurrences of Ø apply directly to atomic sentences.  See UNISA Chatter – Formal Logic: Propositional Logic Proofs for a proof  an example. 
Object  Anything that we can make claims about  Jupiter, Pluto, Carola 
Prefix Notation  With prefix notation the predicate precedes the arguments  Equal(x,y) 
Predicate  Expresses properties of an object or relations between objects  Equal, LeftOf, … 
Proof  A stepstep demonstration that a conclusion follows from some premises, using either a formal or informal style.  Informal proof Since CTOS is an operating system and all operating systems crash, it follows that CTOS will crash. Formal proof  1. Square ( a )  2. a = b   3. Square ( b ) 
Quantifiers  Also see “Symbols” below
Distribution " through Ù Bound variable replacement DeMorgan Laws 
"x(P(x) Ù Q(x)) <=> "xP(x) Ù "xQ(x) Ø"xQ(x) <=> $yØQ(y) Øx($(x) Ù "Q(x)) <=> Ø$xP(x) Ú Ø"xQ(x) Ø"x(P(x) ® Q(x)) <=> $x(P(x) Ù ØQ(x)) 
Reflexity of identity  Sentences of the form a = a are always true  
Reiteration  Repeat an earlier step   1. n = n  …  2. n = n = Reit 1 
Soundness  Implies that a deductive argument is both valid and that all premises are true.
See UNISA Chatter – Formal Logic: Propositional Logic Examples for more examples. 
Valid argument, which is not sound  All proprietary operating systems are expensive  CTOS is a proprietary operating system   CTOS must be an expensive operating system … why? Because first premise is false. 
Rules 
Typical rules used as part of proofs, DNF or CNF formatting includes:

Ø[(ØA Ù B) Ú Ø(C Ú ØD)] 
Symbols  Ø Negation … not ¹ Nonidentity … is not Ù Conjunction … and, moreover, but Ú Disjuntion … or ® Conditional … if, if then « Conditional … if and only if, iff " Quantifier … all, everything $ Quantifier … something, at least one 
Ø Planet(monkey) Pluto ¹ Saturn Planet(pluto) Ù Planet(saturn) Planet(moon) Ú Planet(saturn) All P’s are in Q … "x(P(x) ® Q(x)) 
Symmetry of identity  If b = c then c = b  
Tautology  X is a tautology if and only if every row of its truth table is true.  See UNISA Chatter – Formal Logic: Propositional Logic Proofs for a proof  an example. 
Tautology Consequence  X is a tautological consequence of Y1, Y2, …Yn if and only if there is no row in the joint truth table in which Y1, Y2 … Yn are all true and X is false.  See UNISA Chatter – Formal Logic: Propositional Logic Proofs for a proof  an example. 
Tautology Equivalence  X and Y are tautologically equivalent if and only if there is no row of their joint table in which one value is true and the other is false.  See UNISA Chatter – Formal Logic: Propositional Logic Proofs for a proof  an example. 
Transitivity of identity  If a = b and b = c, then a = c  
Truth Value  The truth value value of a statement is true if the statement is true in the circumstances, else the truth value is false.  
Validity  Validity implies that there is no possibility in which premises are true and the conclusion false.
See UNISA Chatter – Formal Logic: Propositional Logic Examples for more examples. 
Valid and sound argument  LeftOf ( x, z ) ;Premise  LeftOf ( x, y ) ;Premise   LeftOf ( y, z ) ;Conclusion 
Some of these expressions and proofs are a real tongue twister … but formal logic is fun … so far 🙂
Be careful to make a distinction between Propositional Logic and Predicate (or FirstOrder) Logic: Variables, predicates with arguments and quantifiers are not part of Propositional Logic.
Regards, Ken