Saturated models of universal theories
type: Item
instance of: scholarly article
title: Saturated models of universal theories
zbMATH Open document ID: 1015.03040
DOI: 10.1016/S0168-0072(02)00030-1
author: Jeremy Avigad
published in: Annals of Pure and Applied Logic
publication date: 2003-03-09T00:00:00Z
review text: A number of conservation results have been proved proof-theoretically as well as model-theoretically. The author cites \(\text{I}\Sigma_1/\text{PRA}\), \(\text{WKL}_0/\text{PRA}\), \(\text{S}^1_2/\text{PV}\), \(\Sigma^1_1\text{-AC}_0/\text{PA}\), and \(\text{B}\Sigma_{k+1}/\text{I}\Sigma_k\). The tool on the proof-theory side is always the cut-elimination/Herbrand theorem (which W. Sieg refined and dubbed Herbrand analysis). On the other side, model-theorists use a variety of tools, like ultrapowers and cuts in nonstandard models. In this paper, the author develops a model-theoretic counterpart of Herbrand analysis and gives a unified proof of the above conservation results. The key is a Herbrand saturated model, that is, a model in which a principal \(U\)-type is realized if it is consistent with the \(U\)-diagram. (``\(U\)-\(\cdots\)'' means ``\(\cdots\) given by universal formulas'', and ``\(H\)-model'' stands for ``Herbrand saturated model'' in this review.) After showing that a consistent \(U\)-theory has an \(H\)-model, the author gives the following recipe for showing conservation. Given two theories \(T_1\) and \(T_2\) in the same language, with \(T_2\) being universal; if \(T_1\) holds in every \(H\)-model of \(T_2\), then \(T_1\) is conservative over \(T_2\) as to \(\forall\exists\)-sentences. So the author's proof of the \(\text{I}\Sigma_1/\text{PRA}\) conservation amounts to the verification of \(\Sigma_1\)-induction in an \(H\)-model of primitive recursive arithmetic. He indicates how to handle the other cases mentioned above. To recover the constructive aspect of Herbrand analysis, the author considers other proofs by forcing, and shows how they relate to realizability and the normalization of \(\lambda\)-terms.
Mathematics Subject Classification ID: 03C50
Mathematics Subject Classification ID: 03F25
Mathematics Subject Classification ID: 03C25
zbMATH DE Number: 1878498
zbMATH Keywords: universal theories
zbMATH Keywords: conservation theorems
zbMATH Keywords: saturation
zbMATH Keywords: model-theoretic counterpart of Herbrand analysis
zbMATH Keywords: Herbrand saturated model
MaRDI profile type: Publication
cites work: Formalizing forcing arguments in subsystems of second-order arithmetic
cites work: Interpreting classical theories in constructive ones
cites work: Algebraic proofs of cut elimination
cites work: Q4793022
cites work: Transfer principles in nonstandard intuitionistic arithmetic
cites work: A Model-Theoretic Approach to Ordinal Analysis
cites work: Q4110995
cites work: A proof-theoretic analysis of collection
cites work: Q3794177
cites work: Q4325772
cites work: Q4215631
cites work: Handbook of proof theory
cites work: Functional interpretations of feasibly constructive arithmetic
cites work: Two applications of Boolean models
cites work: A new method for establishing conservativity of classical systems over their intuitionistic version
cites work: An application of constructive completeness
cites work: Q4039813
cites work: Explicit algebraic models for constructive and classical theories with non-standard elements
cites work: Q5619071
cites work: Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
cites work: Q3140636
cites work: Q5286672
cites work: Q4001935
cites work: Remarks on Herbrand normal forms and Herbrand realizations
cites work: Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals
cites work: Q4856172
cites work: Q4215637
cites work: Fragments of arithmetic
cites work: Herbrand analyses
cites work: Q4215635
cites work: Constructivism in mathematics. An introduction. Volume I
cites work: Notes on polynomially bounded arithmetic
description: scientific article; zbMATH DE number 1878498