1

I want to understand how logicians reason about strengths of proof systems and argue relative strengths of proof systems. I want to appreciate the validity of the reasoning by which we establish relative proof strengths. Some milestones in this area are the works by Godel, Gentzen and Turing, but I am unequipped to follow Gentzen's "Consistency Proof" or Turing's dissertation "Systems of Logic based on Ordinals".

What are the starting areas I must master to be able to understand these topics on strengths of proof systems?

Ajax
  • 1,063
  • 5
  • 13
  • There are different ways by which logicians measure "strength", [consistency strength](https://en.wikipedia.org/wiki/Equiconsistency#Consistency_strength) and [interpretability strength](https://plato.stanford.edu/entries/independence-large-cardinals/#IntHie) are the most common ones, some interrelations are discussed in this [MathOverflow post](https://mathoverflow.net/q/355384/51484). For foundations in the work of Hilbert, Gödel and Gentzen and pointers to further reading see [SEP, Proof theory](https://plato.stanford.edu/entries/proof-theory/). – Conifold Sep 20 '21 at 00:46
  • @Conifold Is proof theory different from Metamathematics? How exactly do they overlap? – Ajax Sep 20 '21 at 13:07
  • It is not entirely clear what you are asking. A proof system is normally considered to be a distinct thing from a logic. A logic might be identified with the set of its theorems, while a proof system is a formal way of determining what those theorems are. A given logic can have several proof systems. For example, propositional logic has Hilbert-style axiom systems, natural deduction systems, sequent calculus, tableau methods. These are of equal strength in the sense that they all prove the same theorems. – Bumble Sep 20 '21 at 17:29
  • Logics themselves can be of different strengths, in that one logic might have as its theorems a proper subset of the theorems of another. In this sense, minimal logic is weaker than intuitionistic logic, and intuitionistic logic is weaker than classical logic. – Bumble Sep 20 '21 at 17:29
  • Proof theory is a subfield of metamathematics, model theory is another subfield. – Conifold Sep 22 '21 at 00:47
  • 1
    Concerning what you must master to understand what you are interested in: [What should a person interested in the philosophy of mathematics know?](https://philosophy.stackexchange.com/questions/78660/what-should-a-person-interested-in-the-philosophy-of-mathematics-know) Concerning the strength of formal systems, see [this post](https://math.stackexchange.com/a/3818951/21820) (which assumes you know what is listed in the other post). – user21820 Oct 25 '21 at 08:37

0 Answers0