What's the difference between a Proof System and a Theory?

Question

I found this question Is the axiom of induction required for proving the first G&#246;del's incompleteness theorem?
I am apparently under the (wrong) impression that a theory and a proof system are synonyms. I'm pointing this out because from the accepted answer:

Note that the term "(in)complete" is annoyingly overloaded: (in)completeness of a theory is a very different thing from (in)completeness of a proof system.

I am also currently reading a book at leisure hoping to understand the basics well enough.
In the first few pages, the book defines:

A logical system consists of the following:

An alphabet
A grammar
Propositional forms that require no proof
Rules that determine truth
Rules that are used to write proofs.

I'm not quite sure whether this definition is akin to a theory or a proof system. From where I currently stand, where the lines are drawn is very unclear. Maybe this definition describes both a theory and a proof system? Any help clearing this up would be very appreciated.
This book was recommended by one of my professors as it does cover some model theory which is what I'm hoping to learn. Well, in honesty my goal is to have a very clear idea of what people are talking about when discussing the "good" stuff about $ZFC$, $Q$, $PA$, etc. I decided to look into how the book introduces the fundamentals, mostly because I've already covered first-order logic in a previous CS unit about formal languages.

Mauro ALLEGRANZA · Answer

What's the difference between a Proof System and a Theory?

A proof system is the "logical machinery" made of logical axioms and rules of inference, like propositional calculus and predicate calculus.
A formal mathematical theory is based on axioms; see e.g. the first-order version of Peano arithmetic and Zermelo-Fraenkel set theory built using first-order logical language and using the "calculus" to prove theorems.
See Leary, page 68:

The term theory refers to a collection of propositions all surrounding a particular subject. Since different theories have different notation (think about how algebraic notation differs from geometric notation), alphabets change depending on the subject matter.

This means that we start with the basic alphabet of first-order logic [see Def.2.1.2] made of variables, logical connectives and quantifiers, and develop the theory of sets using (in addition to equality) a single "theory symbol": the binary relation symbol $in$, where $(x in y)$ reads:

"$x$ is an element of $y$".

Using examples from Leary's book, we have propositional axioms: $⊢ p→(q→p)$ [axiom FL1, page 24] and rules of inference: Modus Ponens [1.2.10], as well as rules regarding the quantifiers: $forall x p(x) to p(a)$ [Universal Instantiation, page 87].
In the development of set theory we will use them to prove mathematical theorems starting from mathematical axioms and using logical axioms and rules.

The definitions above are consistent with the terms used in the post you have linked about Gödel Incompleteness Theorem.
In that case, the post is about the formal mathematical theory $mathsf Q$, the so-called Robinson arithemtic: a first-order mathematical theory that is a fragment (sub-system) of first-order Peano arithmetic ($mathsf {PA}$).

What's the difference between a Proof System and a Theory?

One Answer

Add your own answers!

Ask a Question