24.1 Proof systems
In Chapter 6 a lot of methods for proving things were given, but it was kind of given that these work, and are valid methods of proof. This begs the question (well if it doesn’t, them I’m begging it now) - \saycan we prove our proof techniques?
First we can try to develop a system for telling us if something is true. There are multiple ways in which we can try to do this, but one specific idea is that we can define a \sayproof system, which is a mathematical construct that allows us to reason about proofs.
A proof system is a four-tuple
Here , , and have specific meanings
The set of all possible statements in our proof system.
The set is the set of all possible proofs in our proof system.
The function defines whether a given statement is true or not (as eone might guess, if , then the statement is true, and otherwise it is false.
The function is called a verification function and takes a proof for a statement and returns if this is a valid proof of , and false if it is not.
There are two key attributes of proof systems that we are primarily interested in; these are soundness and completeness.
A proof system is sound if and only if for every such that
the statement is true, i.e.
In natural language, I would read this as \saya proof system is sound if and only if every statement for which there is a valid proof is true. This is the property that we most interested in; as the name suggests unsound proof systems are not particularly useful!
A proof system is complete if there is a proof for every true statement; that is for every such that
there exists some which is a proof of - that is, for this
This is less useful than soundness, but it is still an interesting property to think about.