A converse of the Barwise completeness theorem

1973 ◽  
Vol 38 (4) ◽  
pp. 594-612
Author(s):  
Jonathan Stavi

In this paper a converse of Barwise's completeness theorem is proved by cut-elimination considerations applied to inductive definitions. We show that among the transitive sets T satisfying some weak closure conditions (closure under primitive-recursive set-functions is more than enough), only the unions of admissible sets satisfy Barwise's completeness theorem in the form stating that if φ ∊ T is a sentence which has a derivation (in the universe) then φ has a derivation in T. See §1 for the origin of the problem in Barwise's paper [Ba].Stated quite briefly the proof is as follows (a step-by-step account including relevant definitions is given in the body of the paper):Let T be a transitive prim.-rec. closed set, and let is nonempty, transitive and closed under pairs}. For each let κ(A) be the supremum of closure ordinals of first-order positive operators on subsets of A (first-order with respect to By Theorem 1 of [BGM], it is enough to prove that rank(T) in order to obtain that T is a union of admissible sets. (The rank of a set is defined by rank(x) = supy ∊ x (rank(y) + 1); since T is prim.-rec. closed, rank(T) = smallest ordinal not in T.)Let We show how to find in T (in fact, in Lω(A)) a derivable sentence τ that has no derivation D such that rank(D) ≤ α. Thus, if τ is to have a derivation in T, rank(T) > α. α is arbitrary (< κ(A)), so rank(T) ≥ κ(A). Q.E.D.

1993 ◽  
Vol 58 (1) ◽  
pp. 291-313 ◽  
Author(s):  
Robert S. Lubarsky

Inductive definability has been studied for some time already. Nonetheless, there are some simple questions that seem to have been overlooked. In particular, there is the problem of the expressibility of the μ-calculus.The μ-calculus originated with Scott and DeBakker [SD] and was developed by Hitchcock and Park [HP], Park [Pa], Kozen [K], and others. It is a language for including inductive definitions with first-order logic. One can think of a formula in first-order logic (with one free variable) as defining a subset of the universe, the set of elements that make it true. Then “and” corresponds to intersection, “or” to union, and “not” to complementation. Viewing the standard connectives as operations on sets, there is no reason not to include one more: least fixed point.There are certain features of the μ-calculus coming from its being a language that make it interesting. A natural class of inductive definitions are those that are monotone: if X ⊃ Y then Γ (X) ⊃ Γ (Y) (where Γ (X) is the result of one application of the operator Γ to the set X). When studying monotonic operations in the context of a language, one would need a syntactic guarantor of monotonicity. This is provided by the notion of positivity. An occurrence of a set variable S is positive if that occurrence is in the scopes of exactly an even number of negations (the antecedent of a conditional counting as a negation). S is positive in a formula ϕ if each occurrence of S is positive. Intuitively, the formula can ask whether x ∊ S, but not whether x ∉ S. Such a ϕ can be considered an inductive definition: Γ (X) = {x ∣ ϕ(x), where the variable S is interpreted as X}. Moreover, this induction is monotone: as X gets bigger, ϕ can become only more true, by the positivity of S in ϕ. So in the μ-calculus, a formula is well formed by definition only if all of its inductive definitions are positive, in order to guarantee that all inductive definitions are monotone.


1976 ◽  
Vol 41 (1) ◽  
pp. 109-120
Author(s):  
Anders M. Nyberg

Introduction. The purpose of this paper is to show how results from the theory of inductive definitions can be used to obtain new compactness theorems for uncountable admissible languages. These will include improvements of the compactness theorem by J. Green [9].In [2] Barwise studies admissible sets satisfying the Σ1-compactness theorem. Our approach is to consider admissible sets satisfying what could be called the abstract extended completeness theorem, that is, sets where the consequence relation of the admissible fragment LA is Σ1-definable over A. We will call such sets Σ1-complete. For countable admissible sets, Σ1-completeness follows from the completeness theorem for LA.Having restricted our attention to Σ1-complete sets we are led to a stronger notion also true on countable admissible sets, namely what we shall call uniform Σ1-completeness. We will see that this notion can be viewed as extending to uncountable admissible sets, properties related to both the “recursion theory” and “proof theory” of countable admissible sets.By following Barwise's recent approach to admissible sets allowing “urelements,” we show that there is a natural connection between certain structures arising from the theory of inductive definability, and uniformly Σ1-complete admissible sets . The structures we have in mind are called uniform Kleene structures.


1971 ◽  
Vol 36 (2) ◽  
pp. 262-270
Author(s):  
Shoji Maehara ◽  
Gaisi Takeuti

A second order formula is called Π1 if, in its prenex normal form, all second order quantifiers are universal. A sequent F1, … Fm → G1 …, Gn is called Π1 if a formulais Π1If we consider only Π1 sequents, then we can easily generalize the completeness theorem for the cut-free first order predicate calculus to a cut-free Π1 predicate calculus.In this paper, we shall prove two interpolation theorems on the Π1 sequent, and show that Chang's theorem in [2] is a corollary of our theorem. This further supports our belief that any form of the interpolation theorem is a corollary of a cut-elimination theorem. We shall also show how to generalize our results for an infinitary language. Our method is proof-theoretic and an extension of a method introduced in Maehara [5]. The latter has been used frequently to prove the several forms of the interpolation theorem.


1991 ◽  
Vol 56 (1) ◽  
pp. 213-226 ◽  
Author(s):  
Marcel Crabbé

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.


2018 ◽  
Vol 8 (1) ◽  
pp. 49-66
Author(s):  
Monika Szuba

The essay discusses selected poems from Thomas Hardy's vast body of poetry, focusing on representations of the self and the world. Employing Maurice Merleau-Ponty's concepts such as the body-subject, wild being, flesh, and reversibility, the essay offers an analysis of Hardy's poems in the light of phenomenological philosophy. It argues that far from demonstrating ‘cosmic indifference’, Hardy's poetry offers a sympathetic vision of interrelations governing the universe. The attunement with voices of the Earth foregrounded in the poems enables the self's entanglement in the flesh of the world, a chiasmatic intertwining of beings inserted between the leaves of the world. The relation of the self with the world is established through the act of perception, mainly visual and aural, when the body becomes intertwined with the world, thus resulting in a powerful welding. Such moments of vision are brief and elusive, which enhances a sense of transitoriness, and, yet, they are also timeless as the self becomes immersed in the experience. As time is a recurrent theme in Hardy's poetry, this essay discusses it in the context of dwelling, the provisionality of which is demonstrated in the prevalent sense of temporality, marked by seasons and birdsong, which underline the rhythms of the world.


2017 ◽  
Vol 9 (3) ◽  
pp. 17-30
Author(s):  
Kelly James Clark

In Branden Thornhill-Miller and Peter Millican’s challenging and provocative essay, we hear a considerably longer, more scholarly and less melodic rendition of John Lennon’s catchy tune—without religion, or at least without first-order supernaturalisms (the kinds of religion we find in the world), there’d be significantly less intra-group violence. First-order supernaturalist beliefs, as defined by Thornhill-Miller and Peter Millican (hereafter M&M), are “beliefs that claim unique authority for some particular religious tradition in preference to all others” (3). According to M&M, first-order supernaturalist beliefs are exclusivist, dogmatic, empirically unsupported, and irrational. Moreover, again according to M&M, we have perfectly natural explanations of the causes that underlie such beliefs (they seem to conceive of such natural explanations as debunking explanations). They then make a case for second-order supernaturalism, “which maintains that the universe in general, and the religious sensitivities of humanity in particular, have been formed by supernatural powers working through natural processes” (3). Second-order supernaturalism is a kind of theism, more closely akin to deism than, say, Christianity or Buddhism. It is, as such, universal (according to contemporary psychology of religion), empirically supported (according to philosophy in the form of the Fine-Tuning Argument), and beneficial (and so justified pragmatically). With respect to its pragmatic value, second-order supernaturalism, according to M&M, gets the good(s) of religion (cooperation, trust, etc) without its bad(s) (conflict and violence). Second-order supernaturalism is thus rational (and possibly true) and inconducive to violence. In this paper, I will examine just one small but important part of M&M’s argument: the claim that (first-order) religion is a primary motivator of violence and that its elimination would eliminate or curtail a great deal of violence in the world. Imagine, they say, no religion, too.Janusz Salamon offers a friendly extension or clarification of M&M’s second-order theism, one that I think, with emendations, has promise. He argues that the core of first-order religions, the belief that Ultimate Reality is the Ultimate Good (agatheism), is rational (agreeing that their particular claims are not) and, if widely conceded and endorsed by adherents of first-order religions, would reduce conflict in the world.While I favor the virtue of intellectual humility endorsed in both papers, I will argue contra M&M that (a) belief in first-order religion is not a primary motivator of conflict and violence (and so eliminating first-order religion won’t reduce violence). Second, partly contra Salamon, who I think is half right (but not half wrong), I will argue that (b) the religious resources for compassion can and should come from within both the particular (often exclusivist) and the universal (agatheistic) aspects of religious beliefs. Finally, I will argue that (c) both are guilty, as I am, of the philosopher’s obsession with belief. 


2019 ◽  
Vol 24 (2) ◽  
pp. 343-367
Author(s):  
Roberto Paura

Transhumanism is one of the main “ideologies of the future” that has emerged in recent decades. Its program for the enhancement of the human species during this century pursues the ultimate goal of immortality, through the creation of human brain emulations. Therefore, transhumanism offers its fol- lowers an explicit eschatology, a vision of the ultimate future of our civilization that in some cases coincides with the ultimate future of the universe, as in Frank Tipler’s Omega Point theory. The essay aims to analyze the points of comparison and opposition between transhumanist and Christian eschatologies, in particular considering the “incarnationist” view of Parousia. After an introduction concern- ing the problems posed by new scientific and cosmological theories to traditional Christian eschatology, causing the debate between “incarnationists” and “escha- tologists,” the article analyzes the transhumanist idea of mind-uploading through the possibility of making emulations of the human brain and perfect simulations of the reality we live in. In the last section the problems raised by these theories are analyzed from the point of Christian theology, in particular the proposal of a transhuman species through the emulation of the body and mind of human beings. The possibility of a transhumanist eschatology in line with the incarnationist view of Parousia is refused.


2020 ◽  
Vol 2020 (12) ◽  
Author(s):  
Ke-Pan Xie ◽  
Ligong Bian ◽  
Yongcheng Wu

Abstract We study electroweak baryogenesis in the SO(6)/SO(5) composite Higgs model with the third generation quarks being embedded in the 20′ representation of SO(6). The scalar sector contains one Higgs doublet and one real singlet, and their potential is given by the Coleman-Weinberg potential evaluated from the form factors of the lightest vector and fermion resonances. We show that the resonance masses at $$ \mathcal{O}\left(1\sim 10\kern0.5em \mathrm{TeV}\right) $$ O 1 ∼ 10 TeV can generate a potential that triggers the strong first-order electroweak phase transition (SFOEWPT). The CP violating phase arising from the dimension-6 operator in the top sector is sufficient to yield the observed baryon asymmetry of the universe. The SFOEWPT parameter space is detectable at the future space-based detectors.


1981 ◽  
Vol 4 (3) ◽  
pp. 675-760
Author(s):  
Grażyna Mirkowska

The aim of propositional algorithmic logic is to investigate the properties of program connectives. Complete axiomatic systems for deterministic as well as for nondeterministic interpretations of program variables are presented. They constitute basic sets of tools useful in the practice of proving the properties of program schemes. Propositional theories of data structures, e.g. the arithmetic of natural numbers and stacks, are constructed. This shows that in many aspects PAL is close to first-order algorithmic logic. Tautologies of PAL become tautologies of algorithmic logic after replacing program variables by programs and propositional variables by formulas. Another corollary to the completeness theorem asserts that it is possible to eliminate nondeterministic program variables and replace them by schemes with deterministic atoms.


2021 ◽  
Vol 2021 (3) ◽  
Author(s):  
Sebastian Baum ◽  
Marcela Carena ◽  
Nausheen R. Shah ◽  
Carlos E. M. Wagner ◽  
Yikun Wang

Abstract Electroweak baryogenesis is an attractive mechanism to generate the baryon asymmetry of the Universe via a strong first order electroweak phase transition. We compare the phase transition patterns suggested by the vacuum structure at the critical temperatures, at which local minima are degenerate, with those obtained from computing the probability for nucleation via tunneling through the barrier separating local minima. Heuristically, nucleation becomes difficult if the barrier between the local minima is too high, or if the distance (in field space) between the minima is too large. As an example of a model exhibiting such behavior, we study the Next-to-Minimal Supersymmetric Standard Model, whose scalar sector contains two SU(2) doublets and one gauge singlet. We find that the calculation of the nucleation probabilities prefers different regions of parameter space for a strong first order electroweak phase transition than the calculation based solely on the critical temperatures. Our results demonstrate that analyzing only the vacuum structure via the critical temperatures can provide a misleading picture of the phase transition patterns, and, in turn, of the parameter space suitable for electroweak baryogenesis.


Sign in / Sign up

Export Citation Format

Share Document