Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory

1957 ◽  
Vol 22 (3) ◽  
pp. 269-285 ◽  
Author(s):  
William Craig
Keyword(s):  
Model Theory ◽  
Proof Theory ◽  
Functional Relationship ◽  
Elementary Proof ◽  
Expressive Power ◽  
Second Order ◽  
Order System ◽  
First Order ◽  
Herbrand’S Theorem ◽  
Opening Up

One task of metamathematics is to relate suggestive but nonelementary modeltheoretic concepts to more elementary proof-theoretic concepts, thereby opening up modeltheoretic problems to proof-theoretic methods of attack. Herbrand's Theorem (see [8] or also [9], vol. 2) or Gentzen's Extended Hauptsatz (see [5] or also [10]) was first used along these lines by Beth [1]. Using a modified version he showed that for all first-order systems a certain modeltheoretic notion of definability coincides with a certain proof theoretic notion. In the present paper the Herbrand-Gentzen Theorem will be applied to generalize Beth's results from primitive predicate symbols to arbitrary formulas and terms.This may be interpreted as showing that (apart from some relatively minor exceptions which will be made apparent below) the expressive power of each first-order system is rounded out, or the system is functionally complete, in the following sense: Any functional relationship which obtains between concepts that are expressible in the system is itself expressible and provable in the system.A second application is concerned with the hierarchy of second-order formulas. A certain relationship is shown to hold between first-order formulas and those second-order formulas which are of the form (∃T1)…(∃Tk)A or (T1)…(Tk)A with A being a first-order formula. Modeltheoretically this can be regarded as a relationship between the class AC and the class PC⊿ of sets of models, investigated by Tarski in [12] and [13].

The relative expressive power of some logics extending first-order logic

1979 ◽  
Vol 44 (2) ◽  
pp. 129-146 ◽  
Author(s):  
John Cowles
Keyword(s):  
Model Theory ◽  
Expressive Power ◽  
Second Order ◽  
Order Logic ◽  
The Other ◽  
First Order Logic ◽  
Finite Sets ◽  
Limited Ability ◽  
First Order ◽  
Second Order Logic

In recent years there has been a proliferation of logics which extend first-order logic, e.g., logics with infinite sentences, logics with cardinal quantifiers such as “there exist infinitely many…” and “there exist uncountably many…”, and a weak second-order logic with variables and quantifiers for finite sets of individuals. It is well known that first-order logic has a limited ability to express many of the concepts studied by mathematicians, e.g., the concept of a wellordering. However, first-order logic, being among the simplest logics with applications to mathematics, does have an extensively developed and well understood model theory. On the other hand, full second-order logic has all the expressive power needed to do mathematics, but has an unworkable model theory. Indeed, the search for a logic with a semantics complex enough to say something, yet at the same time simple enough to say something about, accounts for the proliferation of logics mentioned above. In this paper, a number of proposed strengthenings of first-order logic are examined with respect to their relative expressive power, i.e., given two logics, what concepts can be expressed in one but not the other?For the most part, the notation is standard. Most of the notation is either explained in the text or can be found in the book [2] of Chang and Keisler. Some notational conventions used throughout the text are listed below: the empty set is denoted by ∅.

Second-order logic, philosophical issues in

2018 ◽  
Author(s):  
Stewart Shapiro
Keyword(s):  
Mathematical Practice ◽  
Expressive Power ◽  
Deductive System ◽  
Second Order ◽  
Order Logic ◽  
Mathematical Structures ◽  
First Order ◽  
Correct Reasoning ◽  
Second Order Logic

Typically, a formal language has variables that range over a collection of objects, or domain of discourse. A language is ‘second-order’ if it has, in addition, variables that range over sets, functions, properties or relations on the domain of discourse. A language is third-order if it has variables ranging over sets of sets, or functions on relations, and so on. A language is higher-order if it is at least second-order. Second-order languages enjoy a greater expressive power than first-order languages. For example, a set S of sentences is said to be categorical if any two models satisfying S are isomorphic, that is, have the same structure. There are second-order, categorical characterizations of important mathematical structures, including the natural numbers, the real numbers and Euclidean space. It is a consequence of the Löwenheim–Skolem theorems that there is no first-order categorical characterization of any infinite structure. There are also a number of central mathematical notions, such as finitude, countability, minimal closure and well-foundedness, which can be characterized with formulas of second-order languages, but cannot be characterized in first-order languages. Some philosophers argue that second-order logic is not logic. Properties and relations are too obscure for rigorous foundational study, while sets and functions are in the purview of mathematics, not logic; logic should not have an ontology of its own. Other writers disqualify second-order logic because its consequence relation is not effective – there is no recursively enumerable, sound and complete deductive system for second-order logic. The deeper issues underlying the dispute concern the goals and purposes of logical theory. If a logic is to be a calculus, an effective canon of inference, then second-order logic is beyond the pale. If, on the other hand, one aims to codify a standard to which correct reasoning must adhere, and to characterize the descriptive and communicative abilities of informal mathematical practice, then perhaps there is room for second-order logic.

Infinitary analogs of theorems from first order model theory

1971 ◽  
Vol 36 (2) ◽  
pp. 216-228 ◽  
Author(s):  
Jerome Malitz
Keyword(s):  
Model Theory ◽  
Expressive Power ◽  
Direct Products ◽  
Order Model ◽  
Relation Symbol ◽  
First Order ◽  
Identity Symbol

The material presented here belongs to the model theory of the Lκ, λ languages. Our results are either infinitary analogs of important theorems in finitary model theory, or else show that such analogs do not exist.For example, it is well known that whenever i, and , have the same true Lω, ω sentences (i.e., are elementarily equivalent) for i = 1, 2, then the cardinal sums 1 + 2 and + have the same true Lω, ω sentences, and the direct products 1 · 2 and · have the same true Lω, ω sentences [3]. We show that this is true when ‘Lω, ω’ is replaced by ‘Lκ, λ’ if and only if κ is strongly inaccessible. For Lω1, ω this settles a question, posed by Lopez-Escobar [7].In §3 we give a complete description of the expressive power of those sentences of Lκ, λ in which the identity symbol is the only relation symbol which occurs. This extends a result by Hanf [4].

scholarly journals First order quantifiers in monadic second order logic

2004 ◽  
Vol 69 (1) ◽  
pp. 118-136 ◽  
Author(s):  
H. Jerome Keisler ◽  
Wafik Boulos Lotfallah
Keyword(s):  
Expressive Power ◽  
Second Order ◽  
Order Logic ◽  
Existential Quantifier ◽  
Reachability Problem ◽  
Open Problems ◽  
First Order ◽  
Second Order Logic ◽  
Monadic Second Order Logic ◽  
Quantifier Alternation

AbstractThis paper studies the expressive power that an extra first order quantifier adds to a fragment of monadic second order logic, extending the toolkit of Janin and Marcinkowski [JM01].We introduce an operation existsn (S) on properties S that says “there are n components having S”. We use this operation to show that under natural strictness conditions, adding a first order quantifier word u to the beginning of a prefix class V increases the expressive power monotonically in u. As a corollary, if the first order quantifiers are not already absorbed in V, then both the quantifier alternation hierarchy and the existential quantifier hierarchy in the positive first order closure of V are strict.We generalize and simplify methods from Marcinkowski [Mar99] to uncover limitations of the expressive power of an additional first order quantifier, and show that for a wide class of properties S, S cannot belong to the positive first order closure of a monadic prefix class W unless it already belongs to W.We introduce another operation alt(S) on properties which has the same relationship with the Circuit Value Problem as reach(S) (defined in [JM01]) has with the Directed Reachability Problem. We use alt(S) to show that Πn ⊈ FO(Σn), Σn ⊈ FO(∆n). and ∆n+1 ⊈ FOB(Σn), solving some open problems raised in [Mat98].

scholarly journals Local Normal Forms for First-Order Logic with Applications to Games and Automata

1999 ◽  
Vol Vol. 3 no. 3 ◽  
Author(s):  
Thomas Schwentick ◽  
Klaus Barthelmann
Keyword(s):  
Normal Forms ◽  
Winning Strategy ◽  
Expressive Power ◽  
Second Order ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Relational Structures ◽  
Second Order Logic ◽  
Monadic Second Order Logic

International audience Building on work of Gaifman [Gai82] it is shown that every first-order formula is logically equivalent to a formula of the form ∃ x_1,...,x_l, \forall y, φ where φ is r-local around y, i.e. quantification in φ is restricted to elements of the universe of distance at most r from y. \par From this and related normal forms, variants of the Ehrenfeucht game for first-order and existential monadic second-order logic are developed that restrict the possible strategies for the spoiler, one of the two players. This makes proofs of the existence of a winning strategy for the duplicator, the other player, easier and can thus simplify inexpressibility proofs. \par As another application, automata models are defined that have, on arbitrary classes of relational structures, exactly the expressive power of first-order logic and existential monadic second-order logic, respectively.

scholarly journals On Representations of Intended Structures in Foundational Theories

2021 ◽  
Author(s):  
Neil Barton ◽  
Moritz Müller ◽  
Mihai Prunescu
Keyword(s):  
Expressive Power ◽  
Second Order ◽  
Order Logic ◽  
Trade Off ◽  
First Order ◽  
Informal Mathematics ◽  
Second Order Logic

AbstractOften philosophers, logicians, and mathematicians employ a notion of intended structure when talking about a branch of mathematics. In addition, we know that there are foundational mathematical theories that can find representatives for the objects of informal mathematics. In this paper, we examine how faithfully foundational theories can represent intended structures, and show that this question is closely linked to the decidability of the theory of the intended structure. We argue that this sheds light on the trade-off between expressive power and meta-theoretic properties when comparing first-order and second-order logic.

scholarly journals Development of FOPDT and SOPDT model from arbitrary process identification data using the properties of orthonormal basis function

2018 ◽  
Vol 7 (2.21) ◽  
pp. 77 ◽  
Author(s):  
Lalu Seban ◽  
Namita Boruah ◽  
Binoy K. Roy
Keyword(s):  
Basis Function ◽  
Delay Time ◽  
Orthonormal Basis ◽  
Control Point ◽  
Second Order ◽  
Step Test ◽  
Step Response ◽  
Order System ◽  
Model Parameters ◽  
First Order

Most of industrial process can be approximately represented as first-order plus delay time (FOPDT) model or second-order plus delay time (FOPDT) model. From a control point of view, it is important to estimate the FOPDT or SOPDT model parameters from arbitrary process input as groomed test like step test is not always feasible. Orthonormal basis function (OBF) are class of model structure having many advantages, and its parameters can be estimated from arbitrary input data. The OBF model filters are functions of poles and hence accuracy of the model depends on the accuracy of the poles. In this paper, a simple and standard particle swarm optimisation technique is first employed to estimate the dominant discrete poles from arbitrary input and corresponding process output. Time constant of first order system or period of oscillation and damping ratio of second order system is calculated from the dominant poles. From the step response of the developed OBF model, time delay and steady state gain are estimated. The parameter accuracy is improved by employing an iterative scheme. Numerical examples are provided to show the accuracy of the proposed method. 

scholarly journals Critique of ideology or/and analysis of culture? Barthes and Lotman on secondary semiotic systems

2016 ◽  
Vol 44 (3) ◽  
pp. 432-451
Author(s):  
Daniele Monticelli
Keyword(s):  
System Of Systems ◽  
Second Order ◽  
Order System ◽  
Creative Potential ◽  
Cultural Discourses ◽  
First Order ◽  
Semiotic Systems ◽  
Critique Of Ideology

The article compares Roland Barthes’s and Juri Lotman’s notions of ‘second-order semiological systems’ [systemes sémiologique seconds] and ‘secondary modelling systems’ [вторичные моделирующие системы]. It investigates the shared presuppositions of the two theories and their important divergences from each other, explaining them in terms of the opposite strategic roles that the notions of ‘ideology’ and ‘culture’ play in the work of Barthes and Lotman, respectively. The immersion of secondary modelling systems in culture as a “system of systems” characterized by internal heterogeneity, allows Lotman to evidence their positive creative potential: the result of the tensions arising from cultural systemic plurality and heterogeneity may coincide with the emergence of new, unpredictable meanings in translation. The context of Barthes’s second-order semiological systems is instead provided by highly homogeneous ideological frames that appropriate the signs of the first-order system and make them into forms for significations which confirm, reproduce and transmit previously existing information generated by hegemonic social and cultural discourses. The article shows how these differences resurface and, partially, fade away in the theories of the text that Barthes and Lotman elaborated in the 1970s. The discussion is concluded by some remarks on the possible topicality of Barthes’s and Lotman’s approaches for contemporary semiotics and the humanities in general.

Sign in / Sign up

Export Citation Format

Share Document