On nonstandard models in higher order logic

1984 ◽  
Vol 49 (1) ◽  
pp. 204-219
Author(s):  
Christian Hort ◽  
Horst Osswald
Keyword(s):  
Model Theory ◽  
Type Theory ◽  
Order Logic ◽  
Elementary Embedding ◽  
Simple Type ◽  
Order Model ◽  
Higher Order Logic ◽  
First Order ◽  
Simple Type Theory ◽  
Nonstandard Models

There are two concepts of standard/nonstandard models in simple type theory.The first concept—we might call it the pragmatical one—interprets type theory as a first order logic with countably many sorts of variables: the variables for the urelements of type 0,…, the n-ary relational variables of type (τ1, …, τn) with arguments of type (τ1,…,τn), respectively. If A ≠ ∅ then 〈Aτ〉 is called a model of type logic, if A0 = A and . 〈Aτ〉 is called full if, for every τ = (τ1,…,τn), . The variables for the urelements range over the elements of A and the variables of type (τ1,…, τn) range over those subsets of which are elements of . The theory Th(〈Aτ〉) is the set of all closed formulas in the language which hold in 〈Aτ〉 under natural interpretation of the constants. If 〈Bτ〉 is a model of Th(〈Aτ〉), then there exists a sequence 〈fτ〉 of functions fτ: Aτ → Bτ such that 〈fτ〉 is an elementary embedding from 〈Aτ〉 into 〈Bτ〉. 〈Bτ〉 is called a nonstandard model of 〈Aτ〉, if f0 is not surjective. Otherwise 〈Bτ〉 is called a standard model of 〈Aτ〉.This first concept of model theory in type logic seems to be preferable for applications in model theory, for example in nonstandard analysis, since all nice properties of first order model theory (completeness, compactness, and so on) are preserved.

GLIVENKO AND KURODA FOR SIMPLE TYPE THEORY

2014 ◽  
Vol 79 (2) ◽  
pp. 485-495 ◽  
Author(s):  
CHAD E. BROWN ◽  
CHRISTINE RIZKALLAH
Keyword(s):  
Type Theory ◽  
Predicate Logic ◽  
Order Logic ◽  
First Order Logic ◽  
Simple Type ◽  
Universal Quantifier ◽  
First Order ◽  
Simple Type Theory ◽  
Glivenko’S Theorem ◽  
First Order Predicate Logic

AbstractGlivenko’s theorem states that an arbitrary propositional formula is classically provable if and only if its double negation is intuitionistically provable. The result does not extend to full first-order predicate logic, but does extend to first-order predicate logic without the universal quantifier. A recent paper by Zdanowski shows that Glivenko’s theorem also holds for second-order propositional logic without the universal quantifier. We prove that Glivenko’s theorem extends to some versions of simple type theory without the universal quantifier. Moreover, we prove that Kuroda’s negative translation, which is known to embed classical first-order logic into intuitionistic first-order logic, extends to the same versions of simple type theory. We also prove that the Glivenko property fails for simple type theory once a weak form of functional extensionality is included.

Hauptsatz for higher order logic

1968 ◽  
Vol 33 (3) ◽  
pp. 452-457 ◽  
Author(s):  
Dag Prawitz
Keyword(s):  
Finite Type ◽  
Type Theory ◽  
Predicate Logic ◽  
Higher Order ◽  
Second Order ◽  
Order Logic ◽  
Simple Type ◽  
Higher Order Logic ◽  
Simple Type Theory ◽  
Second Order Logic

I shall prove in this paper that Gentzen's Hauptsatz is extendible to simple type theory, i.e., to the predicate logic obtained by admitting quantification over predicates of arbitrary finite type and generalizing the second order quantification rules to cover quantifiers of other types. (That Gentzen's Hauptsatz is extendible to this logic has been known as Takeuti's conjecture; see [4].) Gentzen's Hauptsatz has been extended to second order logic in a recent paper by Tait [3]. However, as remarked by Tait, his proof seems not to be extendible to higher orders. The present proof is rather an extension of a different proof of the Hauptsatz for second order logic that I have presented in [1].

Resolution in type theory

1971 ◽  
Vol 36 (3) ◽  
pp. 414-432 ◽  
Author(s):  
Peter B. Andrews
Keyword(s):  
Set Theory ◽  
Type Theory ◽  
Higher Order ◽  
Order Logic ◽  
First Order Logic ◽  
Higher Order Logic ◽  
First Order ◽  
Different Types ◽  
Axiomatic Set Theory ◽  
Order Predicate Calculus

In [8] J. A. Robinson introduced a complete refutation procedure called resolution for first order predicate calculus. Resolution is based on ideas in Herbrand's Theorem, and provides a very convenient framework in which to search for a proof of a wff believed to be a theorem. Moreover, it has proved possible to formulate many refinements of resolution which are still complete but are more efficient, at least in many contexts. However, when efficiency is a prime consideration, the restriction to first order logic is unfortunate, since many statements of mathematics (and other disciplines) can be expressed more simply and naturally in higher order logic than in first order logic. Also, the fact that in higher order logic (as in many-sorted first order logic) there is an explicit syntactic distinction between expressions which denote different types of intuitive objects is of great value where matching is involved, since one is automatically prevented from trying to make certain inappropriate matches. (One may contrast this with the situation in which mathematical statements are expressed in the symbolism of axiomatic set theory.).

Logic in the 1930s: Type Theory and Model Theory

2013 ◽  
Vol 19 (4) ◽  
pp. 433-472 ◽  
Author(s):  
Georg Schiemer ◽  
Erich H. Reck
Keyword(s):  
Twentieth Century ◽  
Model Theory ◽  
Type Theory ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Gradual Transformation ◽  
Standard Framework ◽  
Theory And Model ◽  
Made In

AbstractIn historical discussions of twentieth-century logic, it is typically assumed that model theory emerged within the tradition that adopted first-order logic as the standard framework. Work within the type-theoretic tradition, in the style of Principia Mathematica, tends to be downplayed or ignored in this connection. Indeed, the shift from type theory to first-order logic is sometimes seen as involving a radical break that first made possible the rise of modern model theory. While comparing several early attempts to develop the semantics of axiomatic theories in the 1930s, by two proponents of the type-theoretic tradition (Carnap and Tarski) and two proponents of the first-order tradition (Gödel and Hilbert), we argue that, instead, the move from type theory to first-order logic is better understood as a gradual transformation, and further, that the contributions to semantics made in the type-theoretic tradition should be seen as central to the evolution of model theory.

scholarly journals Proof normalization modulo

2003 ◽  
Vol 68 (4) ◽  
pp. 1289-1316 ◽  
Author(s):  
Gilles Dowek ◽  
Benjamin Werner
Keyword(s):  
Type Theory ◽  
Cut Elimination ◽  
Simple Type ◽  
First Order ◽  
Simple Type Theory

AbstractWe define a generic notion of cut that applies to many first-order theories. We prove a generic cut elimination theorem showing that the cut elimination property holds for all theories having a so-called pre-model. As a corollary, we retrieve cut elimination for several axiomatic theories, including Church's simple type theory.

The independence of Peano's fourth axiom from Martin-Löf's type theory without universes

1988 ◽  
Vol 53 (3) ◽  
pp. 840-845 ◽  
Author(s):  
Jan M. Smith
Keyword(s):  
Type Theory ◽  
Predicate Logic ◽  
Single Element ◽  
Simple Type ◽  
Consistency Proof ◽  
Computational System ◽  
First Order ◽  
Simple Type Theory ◽  
Individual Domain ◽  
Order Arithmetic

In Hilbert and Ackermann [2] there is a simple proof of the consistency of first order predicate logic by reducing it to propositional logic. Intuitively, the proof is based on interpreting predicate logic in a domain with only one element. Tarski [7] and Gentzen [1] have extended this method to simple type theory by starting with an individual domain consisting of a single element and then interpreting a higher type by the set of truth valued functions on the previous type.I will use the method of Hilbert and Ackermann on Martin-Löf's type theory without universes to show that ¬Eq(A, a, b) cannot be derived without universes for any type A and any objects a and b of type A. In particular, this proves the conjecture in Martin-Löf [5] that Peano's fourth axiom (∀x ϵ N)¬ Eq(N, 0, succ(x)) cannot be proved in type theory without universes. If by consistency we mean that there is no closed term of the empty type, then the construction will also give a consistency proof by finitary methods of Martin-Löf's type theory without universes. So, without universes, the logic obtained by interpreting propositions as types is surprisingly weak. This is in sharp contrast with type theory as a computational system, since, for instance, the proof that every object of a type can be computed to normal form cannot be formalized in first order arithmetic.

Stratification and cut-elimination

1991 ◽  
Vol 56 (1) ◽  
pp. 213-226 ◽  
Author(s):  
Marcel Crabbé
Keyword(s):  
Set Theory ◽  
Type Theory ◽  
Cut Elimination ◽  
Simple Type ◽  
First Order ◽  
Similar Reason ◽  
Separation Axioms ◽  
Simple Type Theory ◽  
Order Language ◽  
The Universe

In this paper, we show the normalization of proofs of NF (Quine's New Foundations; see [15]) minus extensionality. This system, called SF (Stratified Foundations) differs in many respects from the associated system of simple type theory. It is written in a first order language and not in a multi-sorted one, and the formulas need not be stratifiable, except in the instances of the comprehension scheme. There is a universal set, but, for a similar reason as in type theory, the paradoxical sets cannot be formed.It is not immediately apparent, however, that SF is essentially richer than type theory. But it follows from Specker's celebrated result (see [16] and [4]) that the stratifiable formula (extensionality → the universe is not well-orderable) is a theorem of SF.It is known (see [11]) that this set theory is consistent, though the consistency of NF is still an open problem.The connections between consistency and cut-elimination are rather loose. Cut-elimination generally implies consistency. But the converse is not true. In the case of set theory, for example, ZF-like systems, though consistent, cannot be freed of cuts because the separation axioms allow the formation of sets from unstratifiable formulas. There are nevertheless interesting partial results obtained when restrictions are imposed on the removable cuts (see [1] and [9]). The systems with stratifiable comprehension are the only known set-theoretic systems that enjoy full cut-elimination.

An introduction to recursively saturated and resplendent models

1976 ◽  
Vol 41 (2) ◽  
pp. 531-536 ◽  
Author(s):  
Jon Barwise ◽  
John Schlipf
Keyword(s):  
Set Theory ◽  
Model Theory ◽  
Order Logic ◽  
First Order Logic ◽  
Saturated Model ◽  
Order Model ◽  
Special Model ◽  
First Order ◽  
Admissible Sets ◽  
Recursively Saturated

The notions of recursively saturated and resplendent models grew out of the study of admissible sets with urelements and admissible fragments of Lω1ω, but, when applied to ordinary first order model theory, give us new tools for research and exposition. We will discuss their history in §3.The notion of saturated model has proven to be important in model theory. Its most important property for applications is that if , are saturated and of the same cardinality then = iff ≅ . See, e.g., Chang-Keisler [3]. The main drawback is that saturated models exist only under unusual assumptions of set theory. For example, if 2κ = κ+ then every theory T of L has a saturated model of power κ+. (Similarly, if κ is strongly inaccessible, then every T has a saturated model of power κ.) On the other hand, a theory T like Peano arithmetic, with types, cannot have a saturated model in any power κ with ω ≤ κ ≤ .One method for circumventing these problems of existence (or rather non-existence) is the use of “special” models (cf. [3]). If κ = Σλ<κ2λ, κ < ω, then every theory T of L has a special model of power κ. Such cardinals are large and, themselves, rather special. There are definite aesthetic objections to the use of these large, singular models to prove results about first order logic.

Sign in / Sign up

Export Citation Format

Share Document