interpretations between theories

Summary

Somtimes one mathematical theory T1 (e.g. set theory) is powerful enough to define the objects in and derive all the theorems of another theory T0 (e.g. Peano arithmetic). An interpretation from T0 into T1 is a systematic way of translating statements in T0 into the corresponding statements in T1.

Context

This concept has the prerequisites:

semantics of first-order logic (One must use the semantics of first-order logic to check the correctness of the interpretation procedure.)
recursion theorem (The Recursion Theorem is needed to define an interpretation function.)

Goals

Define the notion of an interpretation function from one first-order theory to another

Be able to show that an interpretation function preserves the semantics of a theory

Core resources (read/watch one of the following)

-Paid-

→ A Mathematical Introduction to Logic

An undergraduate textbook in mathematical logic, with proofs.

Location: Section 2.7, "Interpretations between theories," pages 164-172

[external website]