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.
Definition 24.1.1
A proof system $\Pi$ is a fourtuple
Here $\tau$, $\phi$, $\mathcal{P}$ and $S$ have specific meanings

•
The set $S$ of all possible statements in our proof system.

•
The set $\mathcal{P}$ is the set of all possible proofs in our proof system.

•
The function $\tau:S\to\{0,1\}$ defines whether a given statement is true or not (as eone might guess, if $\tau(x)=1$, then the statement $x$ is true, and otherwise it is false.

•
The function $\phi:S\times\mathcal{P}\to\{0,1\}$ is called a verification function and takes a proof $\mathcal{P}$ for a statement $S$ and returns $1$ if this is a valid proof of $S$, 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.
Definition 24.1.2
A proof system $\Pi$ is sound if and only if for every $s\in S,p\in\mathcal{P}$ such that
the statement $s$ 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!
Definition 24.1.3
A proof system is complete if there is a proof for every true statement; that is for every $s\in S$ such that
there exists some $p\in\mathcal{P}$ which is a proof of $s$  that is, for this $p$
This is less useful than soundness, but it is still an interesting property to think about.