Proofs of non-deducibility in intuitionistic functional calculus

1948 ◽  
Vol 13 (4) ◽  
pp. 204-207 ◽  
Author(s):  
Andkzej Mostowski

It has been proved by S. C. Kleene and David Nelson that the formulais intuitionistically non-deducible, i.e., non-deducible within the intuitionistic functional calculus.The aim of this note is to outline a general method which permits us to establish the intuitionistic non-deducibility of many formulas and in particular of the formula (1).

1980 ◽  
Vol 45 (1) ◽  
pp. 103-120 ◽  
Author(s):  
J. V. Tucker

A natural way of studying the computability of an algebraic structure or process is to apply some of the theory of the recursive functions to the algebra under consideration through the manufacture of appropriate coordinate systems from the natural numbers. An algebraic structure A = (A; σ1,…, σk) is computable if it possesses a recursive coordinate system in the following precise sense: associated to A there is a pair (α, Ω) consisting of a recursive set of natural numbers Ω and a surjection α: Ω → A so that (i) the relation defined on Ω by n ≡α m iff α(n) = α(m) in A is recursive, and (ii) each of the operations of A may be effectively followed in Ω, that is, for each (say) r-ary operation σ on A there is an r argument recursive function on Ω which commutes the diagramwherein αr is r-fold α × … × α.This concept of a computable algebraic system is the independent technical idea of M.O.Rabin [18] and A.I.Mal'cev [14]. From these first papers one may learn of the strength and elegance of the general method of coordinatising; note-worthy for us is the fact that computability is a finiteness condition of algebra—an isomorphism invariant possessed of all finite algebraic systems—and that it serves to set upon an algebraic foundation the combinatorial idea that a system can be combinatorially presented and have effectively decidable term or word problem.


1963 ◽  
Vol 59 (2) ◽  
pp. 287-305
Author(s):  
S. N. Afriat

A normal preference system for a combination of goods is represented by an increasing function φ with convex levels. From Gossen's law, that preference and price directions coincide in equilibrium (a special consequence of his Second Law), it follows that, on the data that xr is the vector of quantities purchased at prices given by a vector pr (r = 1,…, k), the gradient gr = g(xr) of the function φ at the point xr is given byfor some positive multiplier μr;. There may be considered the class of preference functions thus satisfying Gossen's law in respect to the data, and thus with gradients taking prescribed directions at k prescribed points. In particular, there may be considered the subclass of these which are quadratic in some convex region containing the points xr. By choosing any multipliers μr, there is obtained a set of gradients gr associated with the points xr. It is asked if there exists a quadratic function which is increasing and has convex levels in a convex neighbourhood of the points xr, and whose gradient at xr is gr; also it is required to characterize the class of such functions, which, if any exist, form an infinite variety. This is the background of the questions which are going to be investigated, and which are of importance in a general method of empirical preference analysis in economics.


1949 ◽  
Vol 14 (3) ◽  
pp. 159-166 ◽  
Author(s):  
Leon Henkin

Although several proofs have been published showing the completeness of the propositional calculus (cf. Quine (1)), for the first-order functional calculus only the original completeness proof of Gödel (2) and a variant due to Hilbert and Bernays have appeared. Aside from novelty and the fact that it requires less formal development of the system from the axioms, the new method of proof which is the subject of this paper possesses two advantages. In the first place an important property of formal systems which is associated with completeness can now be generalized to systems containing a non-denumerable infinity of primitive symbols. While this is not of especial interest when formal systems are considered as logics—i.e., as means for analyzing the structure of languages—it leads to interesting applications in the field of abstract algebra. In the second place the proof suggests a new approach to the problem of completeness for functional calculi of higher order. Both of these matters will be taken up in future papers.The system with which we shall deal here will contain as primitive symbolsand certain sets of symbols as follows:(i) propositional symbols (some of which may be classed as variables, others as constants), and among which the symbol “f” above is to be included as a constant;(ii) for each number n = 1, 2, … a set of functional symbols of degree n (which again may be separated into variables and constants); and(iii) individual symbols among which variables must be distinguished from constants. The set of variables must be infinite.


1977 ◽  
Vol 9 (1-2) ◽  
pp. 203-207 ◽  
Author(s):  
K. Loimaranta

By experience rating the main problem is to estimate the credibilities. We have for the credibility αk the famous formula)but it is often troublesome to find suitable estimates for the variances and . In the present paper a general method to estimate them from the actual statistics is given.A disadvantage of the method is that good estimates require relatively extensive statistical material. If one of the variances is known, the method can be easily modified to give the other variance from statistics of moderate size.The method is based on the Maximum Likelihood principle and leads to a system of non-linear equations. The equations can be solved by an iterative process, easily programmable for computers.The mathematical model underlying the experience rating problem differs in our case lightly from the usual one.


1953 ◽  
Vol 18 (2) ◽  
pp. 115-118 ◽  
Author(s):  
John Myhill

The purpose of this paper is to present a system of arithmetic stronger than those usually employed, and to prove some syntactical theorems concerning it.We presuppose the lower functional calculus with identity and functions, and we start with three of Peano's axioms.The other two (0 ϵ N and x ϵ N .⊃. x′ ϵ N) we do not need since our variables are anyhow restricted to natural numbers. Sometimes in the interest of a uniform notation for functions, we write Sx instead of x′.Next we have two axioms for μ (the smallest number such that) as follows.A third axiom for μ must wait until we have defined ≤.Now we introduce the central feature of the system, the following rule of definition.RD. Let Φ be a previously unused symbol. Then we can introduce it by a pair of definitions of the following form (n ≥ 0),where F(x1, …, xn) is a wff in which no symbol occurs which was not previously defined (in particular, not Φ), and in which no free variables occur other than x1, …, xn (and possibly not all of these), and G(x1, …, xn, y) is a wff in which no free variables occur other than x1, …, xn, y (and possibly not all of these), and in which no symbol occurs which was not previously defined, except that Φ may occur but only if its last argument is y.


1950 ◽  
Vol 15 (2) ◽  
pp. 92-92
Author(s):  
Ruth Barcan Marcus

In a recent note Bergmann states that “nonextensional languages may contain sentences from which contextually denned predicates are not eliminable.” A restatement of his argument is as follows. Suppose L is a functional calculus of fourth order. Included among the definitions occurring in L isLet ϕ occur in A (where A represents a well-formed formula of L) without an argument. The elimination of ϕ from A in accordance with (1) requiresThe proof of (2) depends on the principle of extensionalityHence Bergmann's conclusion “no such general elimination rule can be constructed for nonextensional languages.”


1955 ◽  
Vol 7 ◽  
pp. 328-336
Author(s):  
E. Rosenthall

1. Reducible diophantine equations. The present paper will provide a general method for obtaining the complete parametric representation for the rational integer solutions of the multiplicative diophantine equation1.1 for some specified range of k, where the aijk,bijk are non-negative integers and the fki, hki are decomposable forms, that is to say they are integral irreducible homogeneous polynomials over the rational field R of degree k in k variables which can be written as the product of k linear forms.


1851 ◽  
Vol 1 (2) ◽  
pp. 9-11
Author(s):  
William Orchard

Let be the given function, then, by a well known theoremthe integral of which, since u0, δu0, δ2u0, &c., are constants, andwill bewhich differs from (A) only by the coefficients of δu0, δ2u0, &c, being shifted each one place to the left.


2017 ◽  
Vol 82 (4) ◽  
pp. 1229-1251
Author(s):  
TREVOR M. WILSON

AbstractWe prove several equivalences and relative consistency results regarding generic absoluteness beyond Woodin’s ${\left( {{\bf{\Sigma }}_1^2} \right)^{{\rm{u}}{{\rm{B}}_\lambda }}}$ generic absoluteness result for a limit of Woodin cardinals λ. In particular, we prove that two-step $\exists ^ℝ \left( {{\rm{\Pi }}_1^2 } \right)^{{\rm{uB}}_\lambda } $ generic absoluteness below a measurable limit of Woodin cardinals has high consistency strength and is equivalent, modulo small forcing, to the existence of trees for ${\left( {{\bf{\Pi }}_1^2} \right)^{{\rm{u}}{{\rm{B}}_\lambda }}}$ formulas. The construction of these trees uses a general method for building an absolute complement for a given tree T assuming many “failures of covering” for the models $L\left( {T,{V_\alpha }} \right)$ for α below a measurable cardinal.


Sign in / Sign up

Export Citation Format

Share Document