Banishing the rule of substitution for functional variables

1953 ◽  
Vol 18 (3) ◽  
pp. 201-208 ◽  
Author(s):  
Leon Henkin
Keyword(s):  
Functional Calculus ◽  
Standard Interpretation ◽  
Substitution Instance ◽  
Deductive Systems ◽  
Functional Variable ◽  
Distinct Individual ◽  
Individual Variables ◽  
Set Up

Let and be (well-formed) formulas of the functional calculus, let c be an n-adic functional variable, and let a1, …, an be distinct individual variables. Church has defined the metalogical notation to indicate the formula resulting from when each part of of the form c{1, …, n) (such that the occurrence of c is free in ) is replaced by the formula which arises from by replacing every free occurrence of ai by i, i, = 1, …, n. (Here 1, …, n may be any individual variables or constants, not necessarily all distinct.) The notation is not defined for all , , c, a1, …, an, however, but only for those cases (specified in detail by Church) when the resulting formula constitutes a valid substitution instance of the formula according to the standard interpretation of the functional calculus.The full and correct syntactical statement of the conditions (under which this type of substitution is permissible) has proved so arduous, that it seems to have been rendered in error more often than not. Unfortunately the functional calculi are often set up as deductive systems in which this type of substitution occurs as one of the primitive rules of inference, or in one of the axiom schemata. Thus the beginning student who is introduced to the calculi through such a formulation is forced to cope from the outset with details which have proved treacherous even to the initiate. For this reason it is desirable to seek alternative formulations of the functional calculi in which this type of substitution is not mentioned.

scholarly journals Rehabilitating the ‘City of Pigs’

2018 ◽  
Vol 12 (2) ◽  
pp. 1-22
Author(s):  
Joel De Lara
Keyword(s):  
Standard Interpretation ◽  
Political Justice ◽  
Trade Specialization ◽  
False Start ◽  
The Republic ◽  
Set Up ◽  
The One ◽  
The City ◽  
Organizing Principles ◽  
Do So

In this paper, I contend that the standard interpretation of the Republic, according to which “the city of pigs” (CP) is an entirely deficient precursor to the one ideally just state, Kallipolis, is untenable. In the vital respect of unity, which for Plato is the defining condition of virtue in the soul and the city, CP is equally if not more just than Kallipolis. In part 1, I outline CP in terms of what I contend are the three organizing principles that secure its unity (“trade specialization”; “right size”; and “modesty”), before proceeding to defend this unity from some typical criticisms. The aim is to show that CP is unified and hence just, which allows us to make sense of why Socrates describes it as “complete” (telea), “true” (alêthinê), and “healthy” (hugiês), despite Glaucon’s protestations. To do so, I will have to first argue against objections from those who interpret CP as a suggestio falsi, or an exercise in playful irony, sketched only to establish the need for Kallipolis. In part 2, I then proceed to show that although Kallipolis is in certain respects superior to CP, it suffers from structural disunity relating to its heretofore unnoticed or downplayed geographical and social scissions—scissions that are requisite and unavoidable for its very organization. As such, Socrates tacitly suggests, I contend, that these scissions mark a disunity that results from reneging CP’s third organizing principle: the “modesty” principle. When Socrates, on his interlocutors’ demands, expands CP by allowing in items and conditions of luxury that provoke pleonexia (greed or covetousness) thus giving birth to the “feverish city,” he leads us to see the necessity of a kind of set-up in Kallipolis with a socially and geographically disparate class of guardians that is saturated by disunity. The overall argument of this paper is that Socrates takes us on a dialectical journey, leading us to see that unity and hence justice in each city depends upon each citizen doing her job and no more than her job (i.e., the principle of trade specialization) (433A-B). Both CP and Kallipolis are sketched for this heuristic purpose—to allow us to see this vision of justice. Socrates’ point in taking us on the dialectical journey, I contend, is to enable us to realize not just what justice is but what inhibits or threatens justice—namely, luxury, or more precisely wealth. CP is not a good model to allow us to see this, but this does not render it a suggestio falsi or an unrealistic false start. Indeed, on my reading, Socrates is not only serious when he dubs the city of pigs true and healthy, but we have to take these pronouncements seriously in order to properly accompany him on the journey and properly see his vision of political justice and injustice.

Completeness in the theory of types

1950 ◽  
Vol 15 (2) ◽  
pp. 81-91 ◽  
Author(s):  
Leon Henkin
Keyword(s):  
Functional Calculus ◽  
Formal System ◽  
Axiom System ◽  
Second Order ◽  
True Proposition ◽  
Arbitrary Domain ◽  
Individual Variables ◽  
Definition Of ◽  
The Individual ◽  
Positive Integers

The first order functional calculus was proved complete by Gödel in 1930. Roughly speaking, this proof demonstrates that each formula of the calculus is a formal theorem which becomes a true sentence under every one of a certain intended class of interpretations of the formal system.For the functional calculus of second order, in which predicate variables may be bound, a very different kind of result is known: no matter what (recursive) set of axioms are chosen, the system will contain a formula which is valid but not a formal theorem. This follows from results of Gödel concerning systems containing a theory of natural numbers, because a finite categorical set of axioms for the positive integers can be formulated within a second order calculus to which a functional constant has been added.By a valid formula of the second order calculus is meant one which expresses a true proposition whenever the individual variables are interpreted as ranging over an (arbitrary) domain of elements while the functional variables of degree n range over all sets of ordered n-tuples of individuals. Under this definition of validity, we must conclude from Gödel's results that the calculus is essentially incomplete.It happens, however, that there is a wider class of models which furnish an interpretation for the symbolism of the calculus consistent with the usual axioms and formal rules of inference. Roughly, these models consist of an arbitrary domain of individuals, as before, but now an arbitrary class of sets of ordered n-tuples of individuals as the range for functional variables of degree n. If we redefine the notion of valid formula to mean one which expresses a true proposition with respect to every one of these models, we can then prove that the usual axiom system for the second order calculus is complete: a formula is valid if and only if it is a formal theorem.

A generalization of the concept of ω-consistency

1954 ◽  
Vol 19 (3) ◽  
pp. 183-196 ◽  
Author(s):  
Leon Henkin
Keyword(s):  
Functional Calculus ◽  
Free Variable ◽  
Natural Numbers ◽  
Deductive Systems ◽  
Individual Variable ◽  
Special Cases ◽  
Definition Of ◽  
The Individual ◽  
Formal Properties ◽  
Use Of Models

In this paper we consider certain formal properties of deductive systems which, in special cases, reduce to the property of ω-consistency; and we then seek to understand the significance of these properties by relating them to the use of models in providing interpretations of the deductive systems.The notion of ω-consistency arises in connection with deductive systems of arithmetic. For definiteness, let us suppose that the system is a functional calculus whose domain of individuals is construed as the set of natural numbers, and that the system possesses individual constants ν0, ν1, ν2, … such that νi functions as a name for the number i. Such a system is called ω-consistent, if there is no well-formed formula A(x) (in which x is the only free variable) such that A(ν0), A(ν1), A(ν2), … and ∼(x)A(x) are all formal theorems of the system, where A(νi) is the formula resulting from A(x) by substituting the constant νi for each free occurrence of the individual variable x.Now consider an arbitrary applied functional calculus F, and let Γ be any non-empty set of its individual constants. In imitation of the definition of ω-consistency, we may say that the system F is Γ-consistent, if it contains no formula A(x) (in which x is the only free variable) such that ⊦ A (α) for every constant α in Γ, and also ⊦ ∼(x)A(x) (where an occurrence of “⊦” indicates that the formula which it precedes is a formal theorem). We easily see that the condition of Γ-consistency is equivalent to the condition that the system F contain no formula B(x) such that ⊦ ∼ B(α) for each α in Γ, and also ⊦ (∃x)B(x).

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.

scholarly journals Spatio-temporal reconstruction of emergent flash synchronization in firefly swarms via stereoscopic 360-degree cameras

2020 ◽  
Vol 17 (170) ◽  
pp. 20200179 ◽  
Author(s):  
Raphaël Sarfati ◽  
Julie C. Hayes ◽  
Élie Sarfati ◽  
Orit Peleg
Keyword(s):  
Natural Habitat ◽  
Three Dimensional ◽  
Strongly Correlated ◽  
The North ◽  
Long Range Interactions ◽  
Distinct Individual ◽  
Dimensional Reconstruction ◽  
Controlled Environments ◽  
Spatio Temporal ◽  
Set Up

During mating season, males of synchronous firefly species flash in unison within swarms of thousands of individuals. These strongly correlated collective displays have inspired numerous mathematical models to explain how global synchronous patterns emerge from local interactions. Yet, experimental data to validate these models remain sparse. To address this gap, we develop a method for three-dimensional tracking of firefly flashes, using a stereoscopic set-up of 360-degree cameras. We apply this method to record flashing displays of the North American synchronous species Photinus carolinus in its natural habitat as well as within controlled environments, and obtain the three-dimensional reconstruction of flash occurrences in the swarm. Our results show that even a small number of interacting males synchronize their flashes; however, periodic flash bursts only occur in groups larger than 15 males. Moreover, flash occurrences are correlated over several metres, indicating long-range interactions. While this suggests emergent collective behaviour and cooperation, we identify distinct individual trajectories that hint at additional competitive mechanisms. These reveal possible behavioural differentiation with early flashers being more mobile and flashing longer than late followers. Our experimental technique is inexpensive and easily implemented. It is extensible to tracking light communication in various firefly species and flight trajectories in other insect swarms.

scholarly journals Parity, Relevance, and Gentle Explosiveness in the Context of Sylvan's Mate Function

2018 ◽  
Vol 15 (2) ◽  
pp. 381
Author(s):  
Thomas Macaulay Ferguson
Keyword(s):  
Infinite Number ◽  
Proof Theory ◽  
Possible Worlds ◽  
Consequence Relations ◽  
Deductive Systems ◽  
First Degree Entailment ◽  
Broad Field ◽  
Soundness And Completeness ◽  
Set Up ◽  
Hallmark Feature

The Routley star, an involutive function between possible worlds or set-ups against which negation is evaluated, is a hallmark feature of Richard Sylvan and Val Plumwood's set-up semantics for the logic of first-degree entailment. Less frequently acknowledged is the weaker mate function described by Sylvan and his collaborators, which results from stripping the requirement of involutivity from the Routley star. Between the mate function and the Routley star, however, lies an broad field of intermediate semantical conditions characterizing an infinite number of consequence relations closely related to first-degree entailment. In this paper, we consider the semantics and proof theory for deductive systems corresponding to set-up models in which the mate function is cyclical. We describe modifications to Anderson and Belnap's consecution calculus LE_fde2 that correspond to these constraints, for which we prove soundness and completeness with respect to the set-up semantics. Finally, we show that a number of familiar metalogical properties are coordinated with the parity of a mate function's period, including refined versions of the variable-sharing property and the property of gentle explosiveness.

A note on direct products

1958 ◽  
Vol 23 (1) ◽  
pp. 1-6 ◽  
Author(s):  
L. Novak Gál
Keyword(s):  
Binary Relation ◽  
Direct Product ◽  
Functional Calculus ◽  
Ordered Set ◽  
Infinite Sequence ◽  
Direct Products ◽  
First Order ◽  
Individual Variables ◽  
The Individual ◽  
Infinite Sequences

By an algebra is meant an ordered set Γ = 〈V,R1, …, Rn, O1, …, Om〉, where V is a class, Ri (1 ≤ i ≤, n) is a relation on nj elements of V (i.e. Ri ⊆ Vni), and Oj (1 ≤ i ≤ n) is an operation on elements of V such that Oj(x1, … xmj) ∈ V) for all x1, …, xmj ∈ V). A sentence S of the first-order functional calculus is valid in Γ, if it contains just individual variables x1, x2, …, relation variables ϱ1, …,ϱn, where ϱi,- is nj-ary (1 ≤ i ≤ n), and operation variables σ1, …, σm, where σj is mj-ary (1 ≤, j ≤ m), and S holds if the individual variables are interpreted as ranging over V, ϱi is interpreted as Ri, and σi as Oj. If {Γi}i≤α is a (finite or infinite) sequence of algebras Γi, where Γi = 〈Vi, Ri〉 and Ri, is a binary relation, then by the direct productΓ = Πi<αΓi is meant the algebra Γ = 〈V, R〉, where V consists of all (finite or infinite) sequences x = 〈x1, x2, …, xi, …〉 with Xi ∈ Vi and where R is a binary relation such that two elements x and y of V are in the relation R if and only if xi and yi- are in the relation Ri for each i < α.

On sentences which are true of direct unions of algebras

1951 ◽  
Vol 16 (1) ◽  
pp. 14-21 ◽  
Author(s):  
Alfred Horn
Keyword(s):  
Normal Form ◽  
Wide Class ◽  
Conjunctive Normal Form ◽  
Disjunctive Normal Form ◽  
Factor Algebra ◽  
The Matrix ◽  
Distinct Individual ◽  
Direct Union ◽  
Individual Variables ◽  
Image Position

It is well known that certain sentences corresponding to similar algebras are invariant under direct union; that is, are true of the direct union when true of each factor algebra. An axiomatizable class of similar algebras, such as the class of groups, is closed under direct union when each of its axioms is invariant. In this paper we shall determine a wide class of invariant sentences. We shall also be concerned with determining sentences which are true of a direct union provided they are true of some factor algebra. In the case where all the factor algebras are the same, a further result is obtained. In §2 it will be shown that these criteria are the only ones of their kind. Lemma 7 below may be of some independent interest.We adopt the terminology and notation of McKinsey with the exception that the sign · will be used for conjunction. Expressions of the form ∼∊, where ∊ is an equation, will be called inequalities. In accordance with the analogy between conjunction and disjunction with product and sum respectively, we shall call α1, …, αn the terms of the disjunctionand the factors of the conjunctionEvery closed sentence is equivalent to a sentence in prenez normal form,where x1, …, xm distinct individual variables, Q1, …, Qm are quantifiers, and the matrix S is an open sentence in which each of the variables x1, …, xm actually occurs. The sentence S may be written in either disjunctive normal form:where αi,j is either an equation or an inequality, or in conjunctive normal form:.

An extended joint consistency theorem for a family of free modal logics with equality

1984 ◽  
Vol 49 (1) ◽  
pp. 174-183 ◽  
Author(s):  
Raymond D. Gumb
Keyword(s):  
Infinite Family ◽  
Modal Logics ◽  
Relational Semantics ◽  
Accessibility Relation ◽  
Barcan Formula ◽  
Distinct Individual ◽  
Individual Variables

In this paper, we establish an extended joint consistency theorem for an infinite family of free modal logics with equality. The extended joint consistency theorem incorporates the Craig and Lyndon interpolation lemmas and the Robinson joint consistency theorem. In part, the theorem states that two theories which are jointly unsatisfiable are separated by a sentence in the vocabulary common to both theories.Our family of free modal logics includes the free versions of I, M, and S4 studied by Leblanc [5, Chapters 8 and 9], supplemented with equality as in [3]. In the relational semantics for these logics, there is no restriction on the accessibility relation in I, while in M(S4) the restriction is reflexivity (refiexivity and transitivity). We say that a restriction on the accessibility relation countenances backward-looping if it implies a sentence of the form ∀x1 …xn(x1Rx2 &…&xn ⊃ xkRxj) (1 ≤ j < k ≤ n ≥ 2), where the xi (1 ≤ i ≤ n) are distinct individual variables. Just as reflexivity and transitivity do not countenance backward-looping, neither do any of the restrictions in our family of free modal logics. (The above terminology is derived from the effect of such restrictions on Kripke tableaux constructions.) The Barcan formula, its converse, the Fitch formula, and the formula T ≠ T′ ⊃ □T ≠ T′ do not hold in our logics.

On the rules of proof in the pure functional calculus of the first order

1951 ◽  
Vol 16 (2) ◽  
pp. 107-111 ◽  
Author(s):  
Andrzej Mostowski
Keyword(s):  
Functional Calculus ◽  
Free Variable ◽  
Propositional Function ◽  
Cartesian Power ◽  
First Order ◽  
A Value ◽  
Free Variables ◽  
Individual Variables ◽  
Definition Of

We consider here the pure functional calculus of first order as formulated by Church.Church, l.c., p. 79, gives the definition of the validity of a formula in a given set I of individuals and shows that a formula is provable in if and only if it is valid in every non-empty set I. The definition of validity is preceded by the definition of a value of a formula; the notion of a value is the basic “semantical” notion in terms of which all other semantical notions are definable.The notion of a value of a formula retains its meaning also in the case when the set I is empty. We have only to remember that if I is empty, then an m-ary propositional function (i.e. a function from the m-th cartesian power Im to the set {f, t}) is the empty set. It then follows easily that the value of each well-formed formula with free individual variables is the empty set. The values of wffs without free variables are on the contrary either f or t. Indeed, if B has the unique free variable c and ϕ is the value of B, then the value of (c)B according to the definition given by Church is the propositional constant f or t according as ϕ(j) is f for at least one j in I or not. Since, however, there is no j in I, the condition ϕ(j) = t for all j in I is vacuously satisfied and hence the value of (c)B is t.

Sign in / Sign up

Export Citation Format

Share Document