A proof is a method for establishing the truth. In every day life you could do this by:

- Jury trial. The most voted sentence is accepted as being true.
- “I don’t see why not”. The sentence is true unless a counter-example is provided.
- Intimidation. Truth is imposed by someone with whom disagreement seems unwise.
- Etc.

In mathematics, a proof is a verification of a proposition by a chain of logical deductions from a base set of axioms. [1]

A proposition is a statement that is either true or false.

Examples: “1+2 = 3”; “The sky is blue.”; “Water is made out of two parts of Hydrogen and one part of Helium.”.

You can easily spot the true and false ones here. But to a computer this isn’t straightforward. It might not be able to tell you if the latter proposition is true or false at first, but if you tell it that “water is H2O” and that “H2O means two parts Hydrogen and one part Oxygen”, you can write a program to determine – deduce – the truth of our statement; in this case false.

An axiom is a simple statement that you believe to be true. It is the starting point for your algorithms.

In math class, when you begin to solve a problem you are given a set of known facts from which you start your reasonings. For instance: “You have three apples. Nina eats one of them. How many apples do you have now?”. In this scenario you know that initially you have three apples and you use this in order to find out how many apples you have left after Nina eats one of them. An axiom is very similar, only it represents general knowledge, that is known to be true and it doesn’t need to be proven when you start solving the problem. The general fact present in our problem and on which you are relying when you solve it is that by substracting one from three is always equal to two – and you do not need to prove this.

Examples: “If a=b and b=c then a=c.”, “Two shapes that fill exactly the same space are the same shape.”, “If you divide a number by anything more than 1, the quotient (result) will be less than the original number.”.

How far should you go? Drawing a line between what can be assumed and what should be proven is not always a simple task. There are true statements that cannot be proved (e.g. Goldbach’s conjecture – “Every even integer greater than 2 can be expressed as the sum of two primes.”), but usually you can use your common sense.

A logical deduction combines axioms and true statements in order to form new true propositions.

Examples: “All men are mortal. Socrates is a man. Therefore, Socrates is mortal.”

The following example is valid (from a computer’s point of view), but it is not sound: “Everyone who goes to college owns a computer. Lisa goes to college. Therefore, Lisa owns a computer.”. The first premise is false – not everyone who goes to college owns a computer. The argument is valid because if both premises are true then the conclusion is also true. In other words, if the conclusion is false then the premises cannot be true.

These aspects have to be considered from a computer's point of view. Even if some concepts are clear to us - humans, the computer has no capability of distinguishing between right or wrong, true or false, other than the capabilities that you define. This applies very well in the fields of artificial intelligence and machine learning - consequently to robotics as well. For example, given the two propositions:

- “Drinking vodka and water makes you drunk.”
- “Drinking gin and water makes you drunk.”

The program might notice that “water” is the common term in the two propositions and deduce that “water makes you drunk”. This might be valid if the rules defined determine this behaviour, but no human being would believe a study that makes such claims.

The soundness and completeness of the proofs, as well as axioms, laws and logical deductions are the object of study in boolean algebra.

A sophism is a specious argument used for deceiving someone.

Example: “Socrates is a spider (Spiders have 8 legs. Socrates has eight legs). Socrates is a living being. Therefore any living being has 8 legs.”

Tautology refers to a conclusion is true in all cases, regardless of the truth value of the premises.

Given the premises you must assert them all the truth combinations possible in order to verify the truth value of a conclusion.

Why do we do this?

- A statement is considered to be proved if it is a tautology. It might also occur that some statements are true in special cases, which should be treated in a different manner by our program (branching – if-else and switch statements in C/C++).
- If we have a problem that is too complex to prove/solve and requires tedious work, by proving the logical equivalence with a different, more accessible problem (called in programming the act of reducing a problem to an other) we can considerably lessen the amount of work we have to do by proving/solving the latter one. In many cases, the simpler problem might be a known, solved problem which we needn’t work on any more.
- This is often done in programming. If you have a problem you have to solve you can do this in many ways, varying from very efficient to highly inefficient. Therefore, it is wise to try and build your solution on top of known, efficient algorithms and in order to do that you have to be able to reduce your problem to the specifics of the known algorithm.

The operators we commonly use are:

- Identity

p | p |
---|---|

T | T |

F | F |

- NOT

p | ¬p |
---|---|

T | F |

F | T |

- AND

Notations: p AND q, p ∧ q, p & q, p ∙ q

p | q | p ∧ q |
---|---|---|

T | T | T |

T | F | F |

F | T | F |

F | F | F |

- OR

Notations: p OR q, p ∨ q, p || q, p + q

p | q | p ∨ q |
---|---|---|

T | T | T |

T | F | T |

F | T | T |

F | F | F |

- XOR (Exclusive OR – “one or the other are true, but not both”)

Notations: p XOR q, p ⊕ q, p ≠ q

p | q | p ⊕ q |
---|---|---|

T | T | F |

T | F | T |

F | T | T |

F | F | F |

- Implication

Notations: if p then q, p → q

p | q | p → q |
---|---|---|

T | T | T |

T | F | F |

F | T | T |

F | F | T |

- Equality (NXOR)

Notations: p XNOR q, p ↔ q, p ⇔ q, p = q, p ≡ q

p | q | p ⇔ q |
---|---|---|

T | T | T |

T | F | F |

F | T | F |

F | F | T |

Venn diagrams illustrate all the possible logical relations between a finite number of sets.

In our case, the sets are the propositions. If an item belongs to a set then it can be associated with the value “true” from the truth tables. If it does not belong in a set, it corresponds to the “false” value. The operators used on these sentences reveal different regions in the diagrams.

In the following examples, the red region corresponds to the items in the sets that evaluate the expression as “true”, whereas the white region represents a “false” value. Each circle represents a proposition (like “p” and “q”). The outer region of the circles is considered as not belonging to either statement.

- AND – Intersection of two sets (an item belongs to both sets)

- OR – Union of two sets (an item belongs to one of the sets)

- XOR (an item belongs to one of the sets, but not to both at the same time)

“Mathematics for Computer Science” by E. Lehman, T. Leighton