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 four-tuple

Π=(τ,ϕ,𝒫,S).\Pi=(\tau,\phi,\mathcal{P},S). (24.1)

Here τ\tau, ϕ\phi, 𝒫\mathcal{P} and SS have specific meanings

  • •
    ​

    The set SS 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 τ:S→{0,1}\tau:S\to\{0,1\} defines whether a given statement is true or not (as eone might guess, if τ⁢(x)=1\tau(x)=1, then the statement xx is true, and otherwise it is false.

  • •
    ​

    The function ϕ:S×𝒫→{0,1}\phi:S\times\mathcal{P}\to\{0,1\} is called a verification function and takes a proof 𝒫\mathcal{P} for a statement SS and returns 11 if this is a valid proof of SS, 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∈S,p∈𝒫s\in S,p\in\mathcal{P} such that

ϕ⁢(s,p)=1,\phi(s,p)=1, (24.2)

the statement ss is true, i.e.

τ⁢(s)=1.\tau(s)=1. (24.3)

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∈Ss\in S such that

τ⁢(s)=1,\tau(s)=1, (24.4)

there exists some p∈𝒫p\in\mathcal{P} which is a proof of ss - that is, for this pp

ϕ⁢(s,p)=1.\phi(s,p)=1. (24.5)

This is less useful than soundness, but it is still an interesting property to think about.