Maths - Proof

On these pages we look at how to do mathematical proofs and also the extent that computers can be used in proving things.

Proofs

A proof allows us to start with known information and to derive other information from it. So proofs don't create information from nothing, they are more like:

if some set of facts then some other thing

The starting information for a proof may be the results of other proofs or it may be the things that we assume to be true (known as axioms or postulates). So, ultimately, everything derives from a set of postulates, the things we assume. For a given mathematical structure it is not always clear what the postulates should be, it may be that:

we assume A and prove B from it.

or it may be that:

we assume B and prove A from it.

In some cases it could be that neither A or B is more fundamental than the other, it may come down to an arbitrary decision about which we choose to be the postulate.

In addition to the mathematical system that we are analysing we also need a system of logic a set of rules to derive things from other things. In this sense logic is used as a meta-mathematics operating on other mathematics.

Mathematical Proofs and Computers

There are computer programs that can help with doing proofs (proof assistants) and there are computer programs that can do algebra (such as solving equations). I would like an (open source) program which can do both of these things. The advantage of this is that we would only need to define a mathematical structure once to be able to do a large range of mathematics with it (and possibly to prove the programs themselves correct). The problem with this idea is that these two aspects of mathematics may be done more efficiently with different encodings.

For example, proofs about natural numbers can be done using Peano encoding, this makes inductive/recursive proofs much more practical, however this encoding is not very practical for general programming or human readability. Some programs such as Idris get round this by automatically converting between them.

This works for natural numbers but can this be used for any mathematical types? There is an encoding that applies to a wider range of structures, such as lists and trees, this is an inductively defined type. Mathematically: W-type which is free and initial.

Proof Assistant Notes Introduction
COQ   coq
Agda Agda is a proof assistant, its language is similar to Haskell Agda
Isabelle    

On these pages have included some code for the program Isabelle which is a proof assistant. I have put some information about how I installed this program on this page.

Many of the important results in mathematics have proofs that can be computerised.

Terminology

Notation Meaning
p => q infer (If p, then q)
   
   
   
   
   
   
   
   

 

 

Direct Proof

Prove a statement by a combination of established facts (existing lemmas and theorems)

Common proof rules used are modus ponens and universal instantiation.

Modus Ponens

 

Universal Instantiation

Example: "All men are mortal, Socrates is a man, therefore Socrates is a mortal."

for allx A(x) => A(a/x)

Proof by Mathematical Induction

 

Proof by Transposition

 

Proof by Construction

 

Proof by Exhaustion

 

Probabilistic Proof

 

Combinatorial Proof

 

Nonconstructive Proof

 


metadata block
see also:
Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

cover Modern Graph Theory (Graduate Texts in Mathematics, 184)

Commercial Software Shop

Where I can, I have put links to Amazon for commercial software, not directly related to the software project, but related to the subject being discussed, click on the appropriate country flag to get more details of the software or to buy it from them.

 

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2023 Martin John Baker - All rights reserved - privacy policy.