Recursion theory and formal deducibility

1970 ◽  
Vol 35 (4) ◽  
pp. 556-558
Author(s):  
E. M. Kleinberg
Keyword(s):  
Recursion Theory ◽  
Order Logic ◽  
Negative Integer ◽  
Predicate Calculus ◽  
First Order Logic ◽  
Recursively Enumerable Set ◽  
First Order ◽  
Recursively Enumerable ◽  
Order Predicate Calculus

The enumeration, given a first-order sentence , of all sentences deducible from in the first-order predicate calculus, and the enumeration, given a non-negative integer n, of the recursively enumerable set Wn, are two well-known examples of effective processes. But are these processes really distinct? Indeed, might there not exist a Gödel numbering of the sentences of first-order logic such that for each n, if n is the number assigned to the sentence , then Wn is the set of numbers assigned to all sentences deducible from ? If this were the case, the first sort of enumeration would just be a particular instance of the second.

A weak completeness theorem for infinite valued first-order logic

1963 ◽  
Vol 28 (1) ◽  
pp. 43-50 ◽  
Author(s):  
L. P. Belluce ◽  
C. C. Chang
Keyword(s):  
Completeness Theorem ◽  
Unit Interval ◽  
Order Logic ◽  
First Order Logic ◽  
Order System ◽  
First Order ◽  
Recursively Enumerable ◽  
Weak Completeness ◽  
Truth Value

This paper contains some results concerning the completeness of a first-order system of infinite valued logicThere are under consideration two distinct notions of completeness corresponding to the two notions of validity (see Definition 3) and strong validity (see Definition 4). Both notions of validity, whether based on the unit interval [0, 1] or based on linearly ordered MV-algebras, use the element 1 as the designated truth value. Originally, it was thought by many investigators in the field that one should be able to prove that the set of valid sentences is recursively enumerable. It was first proved by Rutledge in [9] that the set of valid sentences in the monadic first-order infinite valued logic is recursively enumerable.

Resolution in type theory

1971 ◽  
Vol 36 (3) ◽  
pp. 414-432 ◽  
Author(s):  
Peter B. Andrews
Keyword(s):  
Set Theory ◽  
Type Theory ◽  
Higher Order ◽  
Order Logic ◽  
First Order Logic ◽  
Higher Order Logic ◽  
First Order ◽  
Different Types ◽  
Axiomatic Set Theory ◽  
Order Predicate Calculus

In [8] J. A. Robinson introduced a complete refutation procedure called resolution for first order predicate calculus. Resolution is based on ideas in Herbrand's Theorem, and provides a very convenient framework in which to search for a proof of a wff believed to be a theorem. Moreover, it has proved possible to formulate many refinements of resolution which are still complete but are more efficient, at least in many contexts. However, when efficiency is a prime consideration, the restriction to first order logic is unfortunate, since many statements of mathematics (and other disciplines) can be expressed more simply and naturally in higher order logic than in first order logic. Also, the fact that in higher order logic (as in many-sorted first order logic) there is an explicit syntactic distinction between expressions which denote different types of intuitive objects is of great value where matching is involved, since one is automatically prevented from trying to make certain inappropriate matches. (One may contrast this with the situation in which mathematical statements are expressed in the symbolism of axiomatic set theory.).

Translating Advanced Integrity Checking Technology to SQL

2002 ◽  
pp. 203-249 ◽  
Author(s):  
Hendrik Decker
Keyword(s):  
Natural Language ◽  
Order Logic ◽  
Predicate Calculus ◽  
Integrity Constraints ◽  
First Order Logic ◽  
First Order ◽  
Integrity Checking ◽  
Natural Language Interface ◽  
User Friendly ◽  
Declarative Specifications

The main goal of this chapter is to arrive at a coherent technology for deriving efficient SQL triggers from declarative specifications of arbitrary integrity constraints. The user may specify integrity constraints declaratively as closed queries in predicate calculus syntax (i.e., sentences in the language of first-order logic, abbr. FOL), as datalog denials, as query conditions in SQL WHERE clauses, or in some other, possibly more user-friendly manner (e.g., via a dialog-driven graphical or natural language interface which internally translates to equivalent WHERE clause conditions). As we are going to see, the triggers derived from such specifications behave such that whenever some update event would violate any of the integrity constraints, one or several of the triggers derived from that constraint are activated in order to enforce the constraint. That is, the violation is either prevented by rolling back the update or repaired instantly by subsequent further updates.

Infinitary logic and admissible sets

1969 ◽  
Vol 34 (2) ◽  
pp. 226-252 ◽  
Author(s):  
Jon Barwise
Keyword(s):  
Second Order ◽  
Order Logic ◽  
Predicate Calculus ◽  
Generalized Quantifiers ◽  
Infinitary Logic ◽  
First Order ◽  
Admissible Sets ◽  
Classical Language ◽  
Second Order Logic ◽  
Order Predicate Calculus

In recent years much effort has gone into the study of languages which strengthen the classical first-order predicate calculus in various ways. This effort has been motivated by the desire to find a language which is(I) strong enough to express interesting properties not expressible by the classical language, but(II) still simple enough to yield interesting general results. Languages investigated include second-order logic, weak second-order logic, ω-logic, languages with generalized quantifiers, and infinitary logic.

Predicate calculus

2018 ◽  
Author(s):  
Timothy Smiley
Keyword(s):  
Propositional Calculus ◽  
Second Order ◽  
Order Logic ◽  
Predicate Calculus ◽  
First Order Logic ◽  
Complex Predicates ◽  
Modern Logic ◽  
Form Complex ◽  
First Order ◽  
Second Order Logic

The predicate calculus is the dominant system of modern logic, having displaced the traditional Aristotelian syllogistic logic that had been the previous paradigm. Like Aristotle’s, it is a logic of quantifiers – words like ‘every’, ‘some’ and ‘no’ that are used to express that a predicate applies universally or with some other distinctive kind of generality, for example ‘everyone is mortal’, ‘someone is mortal’, ‘no one is mortal’. The weakness of syllogistic logic was its inability to represent the structure of complex predicates. Thus it could not cope with argument patterns like ‘everything Fs and Gs, so everything Fs’. Nor could it cope with relations, because a logic of relations must be able to analyse cases where a quantifier is applied to a predicate that already contains one, as in ‘someone loves everyone’. Remedying the weakness required two major innovations. One was a logic of connectives – words like ‘and’, ‘or’ and ‘if’ that form complex sentences out of simpler ones. It is often studied as a distinct system: the propositional calculus. A proposition here is a true-or-false sentence and the guiding principle of propositional calculus is truth-functionality, meaning that the truth-value (truth or falsity) of a compound proposition is uniquely determined by the truth-values of its components. Its principal connectives are negation, conjunction, disjunction and a ‘material’ (that is, truth-functional) conditional. Truth-functionality makes it possible to compute the truth-values of propositions of arbitrary complexity in terms of their basic propositional constituents, and so develop the logic of tautology and tautological consequence (logical truth and consequence in virtue of the connectives). The other invention was the quantifier-variable notation. Variables are letters used to indicate things in an unspecific way; thus ‘x is mortal’ is read as predicating of an unspecified thing x what ‘Socrates is mortal’ predicates of Socrates. The connectives can now be used to form complex predicates as well as propositions, for example ‘x is human and x is mortal’; while different variables can be used in different places to express relational predicates, for example ‘x loves y’. The quantifier goes in front of the predicate it governs, with the relevant variable repeated beside it to indicate which positions are being generalized. These radical departures from the idiom of quantification in natural languages are needed to solve the further problem of ambiguity of scope. Compare, for example, the ambiguity of ‘someone loves everyone’ with the unambiguous alternative renderings ‘there is an x such that for every y, x loves y’ and ‘for every y, there is an x such that x loves y’. The result is a pattern of formal language based on a non-logical vocabulary of names of things and primitive predicates expressing properties and relations of things. The logical constants are the truth-functional connectives and the universal and existential quantifiers, plus a stock of variables construed as ranging over things. This is ‘the’ predicate calculus. A common option is to add the identity sign as a further logical constant, producing the predicate calculus with identity. The first modern logic of quantification, Frege’s of 1879, was designed to express generalizations not only about individual things but also about properties of individuals. It would nowadays be classified as a second-order logic, to distinguish it from the first-order logic described above. Second-order logic is much richer in expressive power than first-order logic, but at a price: first-order logic can be axiomatized, second-order logic cannot.

Tailoring recursion for complexity

1995 ◽  
Vol 60 (3) ◽  
pp. 952-969 ◽  
Author(s):  
Erich Grädel ◽  
Yuri Gurevich
Keyword(s):  
Polynomial Time ◽  
Recursion Theory ◽  
Order Logic ◽  
First Order Logic ◽  
Complexity Classes ◽  
First Order ◽  
Logarithmic Space ◽  
Functional Analog

AbstractWe design functional algebras that characterize various complexity classes of global functions. For this purpose, classical schemata from recursion theory are tailored for capturing complexity. In particular we present a functional analog of first-order logic and describe algebras of the functions computable in nondeterministic logarithmic space, deterministic and nondeterministic polynomial time, and for the functions computable by AC1 -circuits.

Some remarks concerning theories with recursively enumerable complements

1963 ◽  
Vol 28 (1) ◽  
pp. 72-74 ◽  
Author(s):  
Alan Cobham
Keyword(s):  
Predicate Calculus ◽  
Effective Procedure ◽  
First Order ◽  
Recursively Enumerable ◽  
Decidable Theories ◽  
Mechanical Procedure ◽  
Order Predicate Calculus

A system formalized within the first order predicate calculus either with or without the identity but without predicate or function variables we call simply a theory. We say that a theory T has a recursively enumerable complement (r.e. Comp.) if the set of all sentences of T not valid in T is recursively enumerable. This is equivalent to saying that there exists an effective, purely mechanical procedure for establishing the non-validity in T of precisely those sentences of T which are in fact not theorems of T. If in addition T is recursively enumerable, that is, if there is an effective procedure for establishing the validity in T of its theorems, then T is decidable. It will be shown here that several well-known results concerning decidable theories can be extended to cover theories with r.e. comps. In this respect it should be observed that there exist theories having r.e. comps. which are not decidable. An example is the theory which has as valid sentences just those which contain a given two-place predicate and which are valid in all non-void finite universes [3], [4].

First-Order Logic Reasoning Support for the Semantic Web

2009 ◽  
Vol 19 (12) ◽  
pp. 3091-3099 ◽  
Author(s):  
Gui-Hong XU ◽  
Jian ZHANG
Keyword(s):  
Semantic Web ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Logic Reasoning

Boolean-valued structures

2018 ◽  
Author(s):  
Tim Button ◽  
Sean Walsh
Keyword(s):  
Model Theory ◽  
Order Logic ◽  
First Order Logic ◽  
Inference Rules ◽  
Mathematical Concepts ◽  
Semantic Framework ◽  
First Order ◽  
Standard Models ◽  
Boolean Valued Model ◽  
Semantic Values

Chapters 6-12 are driven by questions about the ability to pin down mathematical entities and to articulate mathematical concepts. This chapter is driven by similar questions about the ability to pin down the semantic frameworks of language. It transpires that there are not just non-standard models, but non-standard ways of doing model theory itself. In more detail: whilst we normally outline a two-valued semantics which makes sentences True or False in a model, the inference rules for first-order logic are compatible with a four-valued semantics; or a semantics with countably many values; or what-have-you. The appropriate level of generality here is that of a Boolean-valued model, which we introduce. And the plurality of possible semantic values gives rise to perhaps the ‘deepest’ level of indeterminacy questions: How can humans pin down the semantic framework for their languages? We consider three different ways for inferentialists to respond to this question.

Sign in / Sign up

Export Citation Format

Share Document