Some relations between classical and constructive mathematics

1978 ◽  
Vol 43 (2) ◽  
pp. 228-246 ◽  
Author(s):  
Michael Beeson
Keyword(s):  
Number Theory ◽  
Historical Context ◽  
Mathematical Practice ◽  
General Question ◽  
Constructive Mathematics ◽  
Main Question ◽  
Double Negation ◽  
Formal Systems ◽  
First Time ◽  
Classical Proof

This paper is devoted to the general question, which assertions φ have the property,if φ is provable classically, then φ is(*) provable constructively.More generally, we consider the question, what is the “constructive content” of a given classical proof? Our aim is to formulate rules in a form applicable to mathematical practice. Often a mathematician has the feeling that there will be no difficulty constructivizing a certain proof, only a number of routine details; although it can be quite laborious to set them all out. We believe that most such situations will come quite easily under the scope of the rules given here; the metamathematical machinery will then take care of the details.This basic idea is not new; it has been discussed by Gödel and by Kreisel. Kreisel's investigations [Kr] were based on Herbrand's theorem; in unpublished memoranda he has also used Gödel's methods on some examples. These methods of Gödel (the double-negation and Dialectica interpretations) lie at the root of our work here. Previous work, however, has been limited to traditional formal systems of number theory and analysis. It is only recently that formal systems adequate to formalize constructive mathematics as a whole have been developed. Thus, for the first time we are in a position to formulate logical theorems which are easily applicable to mathematical practice. It is this program which we here carry out.Now that the work has been placed in some historical context, let us return to the main question: which φ have the property (*)? Upon first considering the problem, one might guess that any φ which makes no existential assertions (including disjunctions) should have the property (*).

A generalization of the concept of ω-completeness

1957 ◽  
Vol 22 (1) ◽  
pp. 1-14 ◽  
Author(s):  
Leon Henkin
Keyword(s):  
Number Theory ◽  
Functional Calculus ◽  
General Setting ◽  
Con A ◽  
Formal Systems ◽  
Individual Variable ◽  
Free Variables

The concepts of ω-consistency and ω-completeness are closely related. The former concept has been generalized to notions of Γ-consistency and strong Γ-consistency, which are applicable not only to formal systems of number theory, but to all functional calculi containing individual constants; and in this general setting the semantical significance of these concepts has been studied. In the present work we carry out an analogous generalization for the concept of ω-completeness.Suppose, then, that F is an applied functional calculus, and that Γ is a non-empty set of individual constants of F. We say that F is Γ-complete if, whenever B(x) is a formula (containing the single free individual variable x) such that ⊦ B(α) for every α in Γ, then also ⊦ (x)B(x). In the paper “Γ-con” a sequence of increasingly strong concepts, Γ-consistency, n = 1,2, 3,…, was introduced; and it is possible in a formal way to define corresponding concepts of Γn-completeness, as follows. We say that F is Γn-complete if, whenever B(x1,…, xn) is a formula (containing exactly n distinct free variables, namely x1…, xn) such that ⊦ B(α1,…,αn) for all α1,…,αn in Γ, then also ⊦ (X1)…(xn)B(x1,…,xn). However, unlike the situation encountered in the paper “Γ-con”, these definitions are not of interest – for the simple reason that F is Γn-complete if and only if it is Γ-complete, as one easily sees.

scholarly journals СТРУКТУРУВАННЯ КОМПОЗИЦІЙНИХ ТА КОНСТРУКТИВНИХ ЗАСОБІВ ПРОЕКТУВАННЯ ОДЯГУ ДЛЯ ВАГІТНИХ

2019 ◽  
pp. 40-47
Author(s):  
І. В. Давиденко ◽  
Т. В. Ніколаєва ◽  
І. Л. Гайова
Keyword(s):  
Pregnant Women ◽  
System Analysis ◽  
Historical Context ◽  
Costume Design ◽  
Literary Analysis ◽  
Practical Significance ◽  
European Tradition ◽  
Technological Means ◽  
Visual Graphic ◽  
First Time

The  purpose  of  the  research  is  to  analyze  and  improve  the  structure  of  the  composition  and constructive  means  of  costume  design  for  future  mothers  through  the  prism  of  the  historical perspective of its development. In the process of doing the work used modern methods of research: literary analysis, historiography, systematic structural, morphological analysis and classification of artistic and composition elements. On the basis of literary and visual-graphic sources, an analysis of the evolution of constructive-technological means of creating clothes for pregnant women in the European tradition of the 15th-20th centuries is carried out and systematized design solutions for certain historical periods to satisfy the ergonomic, utilitarian, hygienic functions of the respective costume,  the  creation  of  psychological  comfort,  as  well  as  the  provision  of  social,  artistic  and aesthetic  functions. Next was the structuring  of composition and constructive means of creating comfortable clothes for pregnant women. Analysis of composition decisions was carried out on the basis of both historical and modern costumes. It was investigated that the use of the principles of transformation in pregnant clothes increases the versatility of products and extends the life of the work. The scientific novelty of research lies in the fact that for the first time a system analysis of the means of shaping and artistic expressiveness in designing special clothes for pregnant women was carried out based on an analysis of the evolution of the shaping of this type of costume in a historical context. It has been determined, systematized and structured the modern constructive-composite means of the design process of promising collections of clothes for pregnant women. The practical significance of the work lies in the development of scientifically based means of shaping special clothes for pregnant women to create collections of modern women’s suits that represent special clothes for pregnant women with improved functional and aesthetic qualities.

More than ‘skimble-skamble stuff’: the Medieval Welsh Poetry Associated with Owain Glyndŵr

2012 ◽  
Author(s):  
Gruffydd Aled Williams
Keyword(s):  
Discrete Group ◽  
Historical Context ◽  
High Status ◽  
Postcolonial Criticism ◽  
Henry Iv ◽  
First Time

In Shakespeare's Henry IV, Part 1, Hotspur refers to the partiality of Owain Glyndŵr (Glendower) for prophecies, which he characterises dismissively as ‘skimble-skamble stuff’. Whilst there is a virtual scholarly consensus that Glyndŵr inspired prophecies and utilised them, no verse prophecies certainly dateable to the revolt have survived, and the poetry surveyed in the lecture consists of eulogies by high-status poets, all but one of them composed before the outbreak of the revolt in 1400. Though used as a source by the historians J. E. Lloyd and R. R. Davies in their volumes on Glyndŵr, this corpus of poems is for the first time examined in detail in English as a discrete group, one that now includes a unique poem – a hybrid displaying elements of eulogy and of vaticination – composed during the revolt and restored to the canon of Glyndŵr poems since the two historians wrote. The poems, some of which are of Scottish interest – they reflect Glyndŵr's participation in Richard II's invasion of Scotland in 1385 – are examined in historical context and in relation to medieval Welsh poetic convention. Drawing on R. R. Davies' perception of post-Conquest Wales as an English colony, insights derived from modern postcolonial criticism are applied to the depiction of Owain in some of the poems, revealing their value in charting his evolution from a seemingly conformist ‘colonial mimic’ to the leader of a national revolt.

Introduction

2021 ◽  
pp. 1-25
Author(s):  
Ulrike Elisabeth Stockhausen
Keyword(s):  
Republican Party ◽  
Historical Context ◽  
The United States ◽  
First Century ◽  
Significant Shift ◽  
Main Question ◽  
Line Position ◽  
Political Debate ◽  
Immigrant And Refugee ◽  
Evangelical Theology

The introduction outlines how American evangelical Christians have responded to refugees and immigrants to the United States since the early 1960s and into the twenty-first century. It sketches the evangelical theology of hospitality, which drove this activism into the late 1980s, and notes the significant shift which took place in evangelical immigration attitudes in the 1990s. While political leanings have always shaped evangelicals’ practical responses and political positions on immigration, mainstream evangelicals’ alliance with the Republican Party profoundly impacted their theology of hospitality as the Grand Old Party shifted toward a hard-line position on immigration. The introduction provides historical context for this activism and introduces the main question which drives the book: Why did evangelicals for many years embrace an immigrant- and refugee-friendly theology, only to replace their scriptural convictions with a more skeptical interpretation of the biblical record once the issue became subject to a deeply polarized political debate?

The Patterns of Large Numbers

2019 ◽  
pp. 43-66
Author(s):  
Steven J. Osterlind
Keyword(s):  
Probability Theory ◽  
Central Limit Theorem ◽  
Limit Theorem ◽  
French Revolution ◽  
Central Limit ◽  
Historical Context ◽  
Binomial Theorem ◽  
The Central Limit Theorem ◽  
Large Numbers ◽  
First Time

This chapter advances the historical context for quantification by describing the climate of the day—social, cultural, political, and intellectual—as fraught with disquieting influences. Forces leading to the French Revolution were building, and the colonists in America were fighting for secession from England. During this time, three important number theorems came into existence: the binomial theorem, the law of large numbers, and the central limit theorem. Each is described in easy-to-understand language. These are fundamental to how numbers operate in a probability circumstance. Pascal’s triangle is explained as a shortcut solving some binomial expansions, and Jacob Bernoulli’s Ars Conjectandi, which presents the study of measurement “error” for the first time, is discussed. In addition, the central limit theorem is explained in terms of its relevance to probability theory, and its utility today.

Towards a consistent set-theory

1951 ◽  
Vol 16 (2) ◽  
pp. 130-136 ◽  
Author(s):  
John Myhill
Keyword(s):  
Number Theory ◽  
Real Number ◽  
Set Theory ◽  
Mathematical Practice ◽  
Axiom Of Choice ◽  
Small Fragment ◽  
Real Numbers ◽  
The Real ◽  
Classical Construction

In a previous paper, I proved the consistency of a non-finitary system of logic based on the theory of types, which was shown to contain the axiom of reducibility in a form which seemed not to interfere with the classical construction of real numbers. A form of the system containing a strong axiom of choice was also proved consistent.It seems to me now that the real-number approach used in that paper, though valid, was not the most fruitful one. We can, on the lines therein suggested, prove the consistency of axioms closely resembling Tarski's twenty axioms for the real numbers; but this, from the standpoint of mathematical practice, is a pitifully small fragment of analysis. The consistency of a fairly strong set-theory can be proved, using the results of my previous paper, with little more difficulty than that of the Tarski axioms; this being the case, it would seem a saving in effort to derive the consistency of such a theory first, then to strengthen that theory (if possible) in such ways as can be shown to preserve consistency; and finally to derive from the system thus strengthened, if need be, a more usable real-number theory. The present paper is meant to achieve the first part of this program. The paragraphs of this paper are numbered consecutively with those of my previous paper, of which it is to be regarded as a continuation.

How connected is the intuitionistic continuum?

1997 ◽  
Vol 62 (4) ◽  
pp. 1147-1150 ◽  
Author(s):  
Dirk Van Dalen
Keyword(s):  
Real Function ◽  
Peculiar Feature ◽  
Constructive Mathematics ◽  
Fan Theorem ◽  
First Time ◽  
Uniformly Continuous ◽  
Intuitionistic Mathematics ◽  
Excluded Middle ◽  
Do So ◽  
The Continuum

In the twenties Brouwer established the well-known continuity theorem “every real function is locally uniformly continuous,” [3, 2, 5]. From this theorem one immediately concludes that the continuum is indecomposable (unzerlegbar), i.e., if ℝ = A ∪ B and A ∩ B = ∅ (denoted by ℝ = A + B), then ℝ = A or ℝ = B.Brouwer deduced the indecomposability directly from the fan theorem (cf. the 1927 Berline Lectures, [7, p. 49]).The theorem was published for the first time in [6], it was used to refute the principle of the excluded middle: ¬∀x ∈ ℝ (x ∈ ℚ ∨ ¬x ∈ ℚ).The indecomposability of ℝ is a peculiar feature of constructive universa, it shows that ℝ is much more closely knit in constructive mathematics, than in classically mathematics. The classically comparable fact is the topological connectedness of ℝ. In a way this characterizes the position of ℝ: the only (classically) connected subsets of ℝ are the various kinds of segments. In intuitionistic mathematics the situation is different; the continuum has, as it were, a syrupy nature, one cannot simply take away one point. In the classical continuum one can, thanks to the principle of the excluded third, do so. To put it picturesquely, the classical continuum is the frozen intuitionistic continuum. If one removes one point from the intuitionistic continuum, there still are all those points for which it is unknown whether or not they belong to the remaining part.

Sign in / Sign up

Export Citation Format

Share Document