Quantification theory and empty individual-domains

1953 ◽  
Vol 18 (3) ◽  
pp. 197-200 ◽  
Author(s):  
Theodore Hailperin
Keyword(s):  
Functional Calculus ◽  
Modus Ponens ◽  
Quantification Theory ◽  
First Order ◽  
Complete Set ◽  
Universal Quantification

In a recent paper by Mostowski [1] we find an investigation of those formulas of quantification theory which are valid in all domains of individuals, including the empty domain. Mostowski gives a complete set of axioms for such a first order functional calculus (the system is called “”) and a comparison is made with a form of the usual calculus, Church's in [2]. It is pointed out that is much less elegant; in particular, the distributivity laws for quantifiers (e.g., (x){A . B) .{x)A . (x)B) do not hold in general, and likewise the rule of modus ponens does not preserve validity in all cases.In this paper we show that a not inelegant system is obtained if one modifies Mostowski's approach in two respects; and once this is done a somewhat neater proof of completeness can be given.The first respect in which we diverge from Mostowski is in the treatment of vacuous quantifiers. For him if p has no free x, then (x)p and (∃x)p are both to have the same value (interpretation) as p1. But this is not the only way to assign values to vacuous quantifications. For when universal quantification is viewed as a generalized conjunction, the formula (x)Fx has the significance of Fa . Fb…. for as many conjunctands as there are individuals in the domain, and if Fx should have the “constant” value p, then (x)p is to mean the conjunction of p with itself for as many times as there are individuals in the domain (compare the arithmetical ).

On the definition of ‘formal deduction’

1956 ◽  
Vol 21 (2) ◽  
pp. 129-136 ◽  
Author(s):  
Richard Montague ◽  
Leon Henkin
Keyword(s):  
Functional Calculus ◽  
Modus Ponens ◽  
Formal Proof ◽  
Axiom Schema ◽  
First Order ◽  
Individual Variable ◽  
Individual Variables ◽  
Definition Of ◽  
Formal Rules

The following remarks apply to many functional calculi, each of which can be variously axiomatized, but for clarity of exposition we shall confine our attention to one particular system Σ. This system is to have the usual primitive symbols and formation rules of the pure first-order functional calculus, and the following formal axiom schemata and formal rules of inference.Axiom schema 1. Any tautologous wff (well-formed formula).Axiom schema 2. (a) A ⊃ B, where A is any wff, a and b are any individual variables, and B arises from A by replacing all free occurrences of a by free occurrences of b.Axiom schema 3. (a)(A ⊃ B)⊃(A⊃ (a)B). where A and B are any wffs, and a is any individual variable not free in A.Rule of Modus Ponens: applies to wffs A and A ⊃ B, and yields B.Rule of Generalization: applies to a wff A and yields (a)A, where a is any individual variable.A formal proof in Σ is a finite column of wffs each of whose lines is a formal axiom or arises from two preceding lines by the Rule of Modus Ponens or arises from a single preceding line by the Rule of Generalization. A formal theorem of Σ is a wff which occurs as the last line of some formal proof.

Some theorems on definability and decidability

1952 ◽  
Vol 17 (3) ◽  
pp. 179-187 ◽  
Author(s):  
Alonzo Church ◽  
W. V. Quine
Keyword(s):  
Number Theory ◽  
Functional Calculus ◽  
Natural Numbers ◽  
Quantification Theory ◽  
First Order ◽  
Dyadic Relation ◽  
Truth Value ◽  
Individual Variables

In this paper a theorem about numerical relations will be established and shown to have certain consequences concerning decidability in quantification theory, as well as concerning the foundation of number theory. The theorem is that relations of natural numbers are reducible in elementary fashion to symmetric ones; i.e.:Theorem I. For every dyadic relation R of natural numbers there is a symmetric dyadic relation H of natural numbers such that R is definable in terms of H plus just truth-functions and quantification over natural numbers.To state the matter more fully, there is a (well-formed) formula ϕ of pure quantification theory, or first-order functional calculus, which meets these conditions:(a) ϕ has ‘x’ and ‘y’ as sole free individual variables;(b) ϕ contains just one predicate letter, and it is dyadic;(c) for every dyadic relation R of natural numbers there is a symmetric dyadic relation H of natural numbers such that, when the predicate letter in ϕ is interpreted as expressing H, ϕ comes to agree in truth-value with ‘x bears R to y’ for all values of ‘x’ and ‘y’.

On Theses of the First-Order Functional Calculus

1961 ◽  
Vol 7 (11-14) ◽  
pp. 175-184
Author(s):  
Juliusz Reichbach
Keyword(s):  
Functional Calculus ◽  
First Order

Scattering of elastic waves near an explosion

1993 ◽  
Vol 83 (4) ◽  
pp. 1277-1293
Author(s):  
Donald Leavy
Keyword(s):  
Displacement Field ◽  
Elastic Waves ◽  
Near Field ◽  
Static Solution ◽  
Simple Relation ◽  
Perturbation Solution ◽  
First Order ◽  
Scattering Of Elastic Waves ◽  
Harmonic Decomposition ◽  
Complete Set

Abstract We use the method of small perturbation to study the scattered waves generated by an arbitrary 3D inhomogeneous medium around a spherically symmetric compressional source. We consider two models of the medium inside the source: a homogeneous solid and a fluid. The results from these two models differ only when scattering occurs within a few source's radii from the explosion. We find that there is a simple relation between the structure of the first order scattered waves and the structure of the medium, namely that a given harmonic of the medium parameters excites only the same harmonic of the two spheroidal potentials. When scattering occurs within a wavelength from the source, we find that the quadrantal terms in the spherical harmonic decomposition of the field have the lowest frequency dependence. They depend on frequency only through the spectrum of the source. Thus, in the far field, the dominant scattered waves generated near an explosion are similar to the primary waves generated by an earthquake. However, when the displacement field is observed in the near field of the explosion, the static solution reveals that a complete set of harmonics may be required to properly account for the displacement field. We compare the perturbation solution with the exact solution of the scattering by a sphere located within a wavelength from the source. This suggests that the perturbation solution has a fairly wide domain of practical applicability. We attempt to apply these results to the Love wave generated near the Boxcar nuclear explosion.

A derivation of number theory from ancestral theory

1952 ◽  
Vol 17 (3) ◽  
pp. 192-197 ◽  
Author(s):  
John Myhill
Keyword(s):  
Number Theory ◽  
Functional Calculus ◽  
Natural Numbers ◽  
Class Inclusion ◽  
First Order ◽  
Free Variables

Martin has shown that the notions of ancestral and class-inclusion are sufficient to develop the theory of natural numbers in a system containing variables of only one type.The purpose of the present paper is to show that an analogous construction is possible in a system containing, beyond the quantificational level, only the ancestral and the ordered pair.The formulae of our system comprise quantificational schemata and anything which can be obtained therefrom by writing pairs (e.g. (x; y), ((x; y); (x; (y; y))) etc.) for free variables, or by writing ancestral abstracts (e.g. (*xyFxy) etc.) for schematic letters, or both.The ancestral abstract (*xyFxy) means what is usually meant by ; and the formula (*xyFxy)zw answers to Martin's (zw; xy)(Fxy).The system presupposes a non-simple applied functional calculus of the first order, with a rule of substitution for predicate letters; over and above this it has three axioms for the ancestral and two for the ordered pair.

scholarly journals Decidability of Definability

2013 ◽  
Vol 78 (4) ◽  
pp. 1036-1054 ◽  
Author(s):  
Manuel Bodirsky ◽  
Michael Pinsker ◽  
Todor Tsankov
Keyword(s):  
Random Graph ◽  
Topological Dynamics ◽  
Homogeneous Structure ◽  
First Order ◽  
Computational Problem ◽  
Random Tournament ◽  
Universal Quantification ◽  
Countably Infinite ◽  
Existential Quantification

AbstractFor a fixed countably infinite structure Γ with finite relational signature τ, we study the following computational problem: input are quantifier-free τ-formulas ϕ0, ϕ1, …, ϕn that define relations R0, R1, …, Rn over Γ. The question is whether the relation R0 is primitive positive definable from R1, …, Rn, i.e., definable by a first-order formula that uses only relation symbols for R1, …, Rn, equality, conjunctions, and existential quantification (disjunction, negation, and universal quantification are forbidden).We show decidability of this problem for all structures Γ that have a first-order definition in an ordered homogeneous structure Δ with a finite relational signature whose age is a Ramsey class and determined by finitely many forbidden substructures. Examples of structures Γ with this property are the order of the rationals, the random graph, the homogeneous universal poset, the random tournament, all homogeneous universal C-relations, and many more. We also obtain decidability of the problem when we replace primitive positive definability by existential positive, or existential definability. Our proof makes use of universal algebraic and model theoretic concepts, Ramsey theory, and a recent characterization of Ramsey classes in topological dynamics.

A system of logic for partial functions under existence-dependent kleene equality

1988 ◽  
Vol 53 (3) ◽  
pp. 834-839 ◽  
Author(s):  
H. Andréka ◽  
W. Craig ◽  
I. Németi
Keyword(s):  
Practical Interest ◽  
Order Logic ◽  
First Order Logic ◽  
Basic Relation ◽  
Equational Logic ◽  
Partial Functions ◽  
First Order ◽  
Complete Set ◽  
The Subject ◽  
Relationship Of

Ordinary equational logic is a connective-free fragment of first-order logic which is concerned with total functions under the relation of ordinary equality. In [AN] (see also [AN1]) and in [Cr] it has been extended in two equivalent ways into a near-equational system of logic for partial functions. The extension given in [Cr] deals with partial functions under two relationships: a relationship of existence-dependent existence and one of existence-dependent Kleene equality. For the language that involves both relationships a set of rules was given that is complete. Those rules in the set that involve only existence-dependent existence turned out to be complete for the sublanguage that involves this relationship only. In the present paper we give a set of rules that is complete for the other sublanguage, namely the language of partial functions under existence-dependent Kleene equality.This language lacks a certain, often needed, power of expressing existence and fails, in particular, to be an extension of the language that underlies ordinary equational logic. That it possesses a fairly simple complete set of rules is therefore perhaps more of theoretical than of practical interest. The present paper is thus intended to serve as a supplement to [Cr] and, less directly, to [AN]. The subject is further rounded out, and some contrast is provided, by [Rob]. The systems of logic treated there are based on the weaker language in which partial functions are considered under the more basic relation of Kleene equality.

Sign in / Sign up

Export Citation Format

Share Document