Abstract Computability and Invariant Definability

1970 ◽  
Vol 34 (4) ◽  
pp. 605-633 ◽  
Author(s):  
Yiannis N. Moschovakis
Keyword(s):  
Function Symbol ◽  
Predicate Calculus ◽  
Relation Symbol ◽  
Individual Constant ◽  
And Function

By language we understand a lower predicate calculus with identity and (perhaps) relation and function symbols. It is convenient to allow for more than one sort of variable. Now each individual constant (if there are any) is of a specified sort, the formal expressions R(t1, … tn), f(t1,…, tn) are well formed only if the terms t1, …, tn are of specified sorts determined by the relation symbol R and the function symbol f, and the term f(t1, …, tn) (if well formed) is of a sort determined by f. We admit s = t as well formed, no matter what the sorts of s and t.

A reduction class containing formulas with one monadic predicate and one binary function symbol

1976 ◽  
Vol 41 (1) ◽  
pp. 45-49
Author(s):  
Charles E. Hughes
Keyword(s):  
Normal Form ◽  
Predicate Symbol ◽  
Conjunctive Normal Form ◽  
Function Symbol ◽  
Predicate Calculus ◽  
Binary Function ◽  
First Order ◽  
The Matrix ◽  
Reduction Class ◽  
Order Predicate Calculus

AbstractA new reduction class is presented for the satisfiability problem for well-formed formulas of the first-order predicate calculus. The members of this class are closed prenex formulas of the form ∀x∀yC. The matrix C is in conjunctive normal form and has no disjuncts with more than three literals, in fact all but one conjunct is unary. Furthermore C contains but one predicate symbol, that being unary, and one function symbol which symbol is binary.

scholarly journals Completeness of two theories on ordered abelian groups and embedding relations

1980 ◽  
Vol 77 ◽  
pp. 33-39 ◽  
Author(s):  
Yuichi Komori
Keyword(s):  
Binary Relation ◽  
Abelian Groups ◽  
Function Symbol ◽  
Binary Function ◽  
Relation Symbol ◽  
Unary Function ◽  
First Order ◽  
Order Language ◽  
Unary Relation ◽  
Binary Relation Symbol

The first order language ℒ that we consider has two nullary function symbols 0, 1, a unary function symbol –, a binary function symbol +, a unary relation symbol 0 <, and the binary relation symbol = (equality). Let ℒ′ be the language obtained from ℒ, by adding, for each integer n > 0, the unary relation symbol n| (read “n divides”).

On an Ackermann-type set theory

1973 ◽  
Vol 38 (3) ◽  
pp. 410-412
Author(s):  
John Lake
Keyword(s):  
Set Theory ◽  
Measurable Cardinal ◽  
Large Cardinal ◽  
Predicate Calculus ◽  
First Order ◽  
Free Variables ◽  
Individual Constant ◽  
Image Position ◽  
Order Predicate Calculus ◽  
Universal Closure

Ackermann's set theory A* is usually formulated in the first order predicate calculus with identity, ∈ for membership and V, an individual constant, for the class of all sets. We use small Greek letters to represent formulae which do not contain V and large Greek letters to represent any formulae. The axioms of A* are the universal closures ofwhere all free variables are shown in A4 and z does not occur in the Θ of A2.A+ is a generalisation of A* which Reinhardt introduced in [3] as an attempt to provide an elaboration of Ackermann's idea of “sharply delimited” collections. The language of A+ is that of A*'s augmented by a new constant V′, and its axioms are A1–A3, A5, V ⊆ V′ and the universal closure ofwhere all free variables are shown.Using a schema of indescribability, Reinhardt states in [3] that if ZF + ‘there exists a measurable cardinal’ is consistent then so is A+, and using [4] this result can be improved to a weaker large cardinal axiom. It seemed plausible that A+ was stronger than ZF, but our main result, which is contained in Theorem 5, shows that if ZF is consistent then so is A+, giving an improvement on the above results.

Natural models and Ackermann-type set theories

1975 ◽  
Vol 40 (2) ◽  
pp. 151-158 ◽  
Author(s):  
John Lake
Keyword(s):  
Set Theory ◽  
Predicate Calculus ◽  
First Order ◽  
Free Variables ◽  
Individual Constant ◽  
Image Position ◽  
Order Predicate Calculus

Our results concern the natural models of Ackermann-type set theories, but they can also be viewed as results about the definability of ordinals in certain sets.Ackermann's set theory A was introduced in [1] and it is now formulated in the first order predicate calculus with identity, using ∈ for membership and an individual constant V for the class of all sets. We use the letters ϕ, χ, θ, and χ to stand for formulae which do not contain V and capital Greek letters to stand for any formulae. Then, the axioms of A* are the universal closures ofwhere all the free variables are shown in A4 and z does not occur in the Θ of A2. A is the theory A* − A5.Most of our notation is standard (for instance, α, β, γ, δ, κ, λ, ξ are variables ranging over ordinals) and, in general, we follow the notation of [7]. When x ⊆ Rα, we use Df(Rα, x) for the set of those elements of Rα which are definable in 〈Rα, ∈〉, using a first order ∈-formula and parameters from x.We refer the reader to [7] for an outline of the results which are known about A, but we shall summarise those facts which are frequently used in this paper.

Beth's property fails in L<ω

1980 ◽  
Vol 45 (2) ◽  
pp. 284-290
Author(s):  
Lee Badger
Keyword(s):  
Predicate Calculus ◽  
Closure Condition ◽  
Relation Symbol ◽  
First Order ◽  
One To One ◽  
Order Predicate Calculus

In this paper we prove that Beth's property does not hold in L<ω. This answers a question posed by Magidor and Malitz in [8]. Beth's property is a natural closure condition on a language which says that everything implicitly definable in the language is also explicitly definable in the language. That the first-order predicate calculus (L0) has the property was first shown by Beth [4]. Lopez-Escobar proved that also has Beth's property [7]. Malitz [9] showed the Beth's property fails in Lκλ where κ ≥ λ ≥ ω1. Friedman and Silver showed that the property fails in Lκλ for κ > ω1. Also Friedman [5] showed that extensions of elementary logic using cardinality quantifiers (L)1κ do not have Beth's property.The undefined notation used here is standard. If further clarification is needed, we refer the reader to [3]. κ and λ denote infinite cardinals. cX and ȣX∣ denote the cardinality of X. cfμ will denote the cofinality of the order μ. All languages discussed are assumed to have no function or constant symbols. All structures are relational. The type of a formula is the set of relation symbols appearing in the formula (excluding equality). The type of a set of formulas is the set of all relation symbols appearing in some formula of the set of formulas. For purpose of this paper we will assume that to each n-ary relation in a structure there is associated an n-ary relation symbol and that in any given structure this association is one-to-one. Using this convention we can define the type of a structure to be the set of those relation symbols to which there is associated a relation in the structure. Sometimes we use the term predicate instead of relation.

Compactness and transfer for a fragment of L2

1977 ◽  
Vol 42 (2) ◽  
pp. 261-268
Author(s):  
M. Magidor ◽  
J. Malitz
Keyword(s):  
Function Symbol ◽  
Predicate Calculus ◽  
Infinite Cardinal ◽  
Small Fragment ◽  
First Order ◽  
Open Questions ◽  
Higher Power ◽  
Countably Compact ◽  
Order Predicate Calculus

The language Ln is obtained from the first order predicate calculus by adjoining the quantifier Qn which binds n variables. The formula Qnυ1 … υnΨ is given a κ-interpretation for each infinite cardinal κ, namely, “there is a set X of power κ such that Ψx1 … xn holds for all distinct x1 … xn ϵ X”. L<ω is the result of adjoining all the Qn quantifiers for each n ϵ ω to the first order predicate calculus.In [4] we showed that under the assumption (cf. [3]) L<ω is countably compact under the ω1-interpretation, and that any sentence σ ϵ L<ω that has a model in some κ-interpretation where κ is a regular infinite cardinal has a model in the ω1 interpretation. However, compactness for L<ω in the κ-interpretation for κ an infinite successor cardinal other than ω1 and the transfer of satisfiability from ω1 to any higher power remain open questions under any set theoretic assumptions.Here we restrict our attention to a small fragment L2− of L2 consisting of universal first order formulas along with formulas of the kind Q2υ1υ2∀υ3 … υnΨ and ¬Q2υ1υ2∀υ3 … υnφ where Ψ and φ are open and no function symbol of arity > 1 occurs in any formula. Assuming the existence of a κ-Souslin tree, this language is λ compact in the κ-interpretation when λ < κ.

Some forms of completeness

1962 ◽  
Vol 27 (3) ◽  
pp. 344-352 ◽  
Author(s):  
P. C. Gilmore
Keyword(s):  
Predicate Symbol ◽  
Constant Term ◽  
Predicate Calculus ◽  
First Order ◽  
Individual Variables ◽  
The Individual ◽  
And Function ◽  
Order Predicate Calculus

By a theory is meant an applied first-order predicate calculus with at least one predicate symbol and perhaps some individual constants and function symbols and a specified set of axioms. In addition to the terms defined by means of the individual variables, constants, and function symbols a theory may also include among its terms those constructed by means of operators such as the epsilon or iota operators; that is, expressions like (εχΡ) or (οχΡ), where P is a well formed formula (wff) of the theory, may also be terms. A constant term of a theory F is then a term in which no variable occurs free. We are interested only in theories which have at least one constant term so that if a theory doesn't have any individual constants it must necessarily admit as terms expressions constructed by means of operators. A sentence of a theory F is a closed wff.

Conformation of Ribosomes from Escherichia Coli

1974 ◽  
Vol 32 ◽  
pp. 210-211
Author(s):  
M. Boublik ◽  
W. Hellmann ◽  
F. Jenkins
Keyword(s):  
Binding Sites ◽  
Ribosomal Proteins ◽  
Fluorescent Dyes ◽  
Protein Biosynthesis ◽  
Three Dimensional ◽  
Spatial Arrangement ◽  
Dimensional Structure ◽  
Complete Understanding ◽  
And Function

The present knowledge of the three-dimensional structure of ribosomes is far too limited to enable a complete understanding of the various roles which ribosomes play in protein biosynthesis. The spatial arrangement of proteins and ribonuclec acids in ribosomes can be analysed in many ways. Determination of binding sites for individual proteins on ribonuclec acid and locations of the mutual positions of proteins on the ribosome using labeling with fluorescent dyes, cross-linking reagents, neutron-diffraction or antibodies against ribosomal proteins seem to be most successful approaches. Structure and function of ribosomes can be correlated be depleting the complete ribosomes of some proteins to the functionally inactive core and by subsequent partial reconstitution in order to regain active ribosomal particles.

The Effect of Oxidized Cholesterol on the Aorta of Rabbits- Scanning Electron Microscopic Observations

1982 ◽  
Vol 40 ◽  
pp. 340-341
Author(s):  
S. K. Pena ◽  
C. B. Taylor ◽  
J. Hill ◽  
J. Safarik
Keyword(s):  
Cholesterol Biosynthesis ◽  
Cholesterol Content ◽  
Arterial Injury ◽  
Electron Microscopic ◽  
Aortic Smooth Muscle ◽  
Oxidized Cholesterol ◽  
Initial Event ◽  
Membrane Structure And Function ◽  
Scanning Electron Microscopic ◽  
And Function

Introduction: Oxidized cholesterol derivatives have been demonstrated in various cell cultures to be very potent inhibitors of 3-hvdroxy-3- methylglutaryl Coenzyme A reductase which is a principle regulator of cholesterol biosynthesis in the cell. The cholesterol content in the cells exposed to oxidized cholesterol was found to be markedly decreased. In aortic smooth muscle cells, the potency of this effect was closely related to the cytotoxicity of each derivative. Furthermore, due to the similarity of their molecular structure to that of cholesterol, these oxidized cholesterol derivatives might insert themselves into the cell membrane, alter membrane structure and function and eventually cause cell death. Arterial injury has been shown to be the initial event of atherosclerosis.

Ultrastructure of developing visual cortical synapses in the cat superior colliculus

1991 ◽  
Vol 49 ◽  
pp. 156-157
Author(s):  
Caroline A. Miller ◽  
Laura L. Bruce
Keyword(s):  
Superior Colliculus ◽  
Phosphate Buffer ◽  
Receptive Fields ◽  
Visual Cortical Area ◽  
Cortical Synapses ◽  
Visual Cortical ◽  
And Function ◽  
Phosphate Buffered Saline ◽  
The Brain ◽  
Cat Superior Colliculus

The first visual cortical axons arrive in the cat superior colliculus by the time of birth. Adultlike receptive fields develop slowly over several weeks following birth. The developing cortical axons go through a sequence of changes before acquiring their adultlike morphology and function. To determine how these axons interact with neurons in the colliculus, cortico-collicular axons were labeled with biocytin (an anterograde neuronal tracer) and studied with electron microscopy.Deeply anesthetized animals received 200-500 nl injections of biocytin (Sigma; 5% in phosphate buffer) in the lateral suprasylvian visual cortical area. After a 24 hr survival time, the animals were deeply anesthetized and perfused with 0.9% phosphate buffered saline followed by fixation with a solution of 1.25% glutaraldehyde and 1.0% paraformaldehyde in 0.1M phosphate buffer. The brain was sectioned transversely on a vibratome at 50 μm. The tissue was processed immediately to visualize the biocytin.

Sign in / Sign up

Export Citation Format

Share Document