Second- and higher-order logics

2018 ◽  
Author(s):  
Shaughan Lavine
Keyword(s):  
Predicate Logic ◽  
Higher Order ◽  
Second Order ◽  
Order Logic ◽  
First Order Logic ◽  
Third Order ◽  
First Order ◽  
Proof Systems ◽  
The Universe ◽  
Second Order Logic

In first-order predicate logic there are symbols for fixed individuals, relations and functions on a given universe of individuals and there are variables ranging over the individuals, with associated quantifiers. Second-order logic adds variables ranging over relations and functions on the universe of individuals, and associated quantifiers, which are called second-order variables and quantifiers. Sometimes one also adds symbols for fixed higher-order relations and functions among and on the relations, functions and individuals of the original universe. One can add third-order variables ranging over relations and functions among and on the relations, functions and individuals on the universe, with associated quantifiers, and so on, to yield logics of even higher order. It is usual to use proof systems for higher-order logics (that is, logics beyond first-order) that include analogues of the first-order quantifier rules for all quantifiers. An extensional n-ary relation variable in effect ranges over arbitrary sets of n-tuples of members of the universe. (Functions are omitted here for simplicity: remarks about them parallel those for relations.) If the set of sets of n-tuples of members of a universe is fully determined once the universe itself is given, then the truth-values of sentences involving second-order quantifiers are determined in a structure like the ones used for first-order logic. However, if the notion of the set of all sets of n-tuples of members of a universe is specified in terms of some theory about sets or relations, then the universe of a structure must be supplemented by specifications of the domains of the various higher-order variables. No matter what theory one adopts, there are infinitely many choices for such domains compatible with the theory over any infinite universe. This casts doubt on the apparent clarity of the notion of ‘all n-ary relations on a domain’: since the notion cannot be defined categorically in terms of the domain using any theory whatsoever, how could it be well-determined?

Higher‐order Logic

2009 ◽  
Author(s):  
Stewart Shapiro
Keyword(s):  
Philosophy Of Mathematics ◽  
Higher Order ◽  
Second Order ◽  
Order Logic ◽  
First Order Logic ◽  
Higher Order Logic ◽  
First Order ◽  
Deductive Systems ◽  
Second Order Logic

The philosophical literature contains numerous claims on behalf of and numerous claims against higher-order logic. Virtually all of the issues apply to second-order logic (vis-à-vis first-order logic), so this article focuses on that. It develops the syntax of second-order languages and present typical deductive systems and model-theoretic semantics for them. This will help to explain the role of higher-order logic in the philosophy of mathematics. It is assumed that the reader has at least a passing familiarity with the theory and metatheory of first-order logic.

scholarly journals Strong Logics of First and Second Order

2010 ◽  
Vol 16 (1) ◽  
pp. 1-36 ◽  
Author(s):  
Peter Koellner
Keyword(s):  
Set Theory ◽  
Large Cardinal ◽  
Second Order ◽  
Order Logic ◽  
First Order Logic ◽  
Close Correspondence ◽  
First Order ◽  
Second Order Logic

AbstractIn this paper we investigate strong logics of first and second order that have certain absoluteness properties. We begin with an investigation of first order logic and the strong logics ω-logic and β-logic, isolating two facets of absoluteness, namely, generic invariance and faithfulness. It turns out that absoluteness is relative in the sense that stronger background assumptions secure greater degrees of absoluteness. Our aim is to investigate the hierarchies of strong logics of first and second order that are generically invariant and faithful against the backdrop of the strongest large cardinal hypotheses. We show that there is a close correspondence between the two hierarchies and we characterize the strongest logic in each hierarchy. On the first-order side, this leads to a new presentation of Woodin's Ω-logic. On the second-order side, we compare the strongest logic with full second-order logic and argue that the comparison lends support to Quine's claim that second-order logic is really set theory in sheep's clothing.

scholarly journals Formalization of Linear Space Theory in the Higher-Order Logic Proving System

2013 ◽  
Vol 2013 ◽  
pp. 1-6 ◽  
Author(s):  
Jie Zhang ◽  
Danwen Mao ◽  
Yong Guan
Keyword(s):  
Linear Space ◽  
Theorem Proving ◽  
Predicate Logic ◽  
Higher Order ◽  
Order Logic ◽  
First Order Logic ◽  
Space Theory ◽  
Higher Order Logic ◽  
First Order ◽  
Important Approach

Theorem proving is an important approach in formal verification. Higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and stronger semantics. Higher-order logic is more expressive. This paper presents the formalization of the linear space theory in HOL4. A set of properties is characterized in HOL4. This result is used to build the underpinnings for the application of higher-order logic in a wider spectrum of engineering applications.

scholarly journals Using hybrid logic for querying dependency treebanks

2012 ◽  
Vol 7 ◽  
Author(s):  
Anders Søgaard ◽  
Søren Lind Kristiansen
Keyword(s):  
General Purpose ◽  
Second Order ◽  
Logic Model ◽  
Order Logic ◽  
Hybrid Logic ◽  
First Order Logic ◽  
Model Checker ◽  
First Order ◽  
Second Order Logic ◽  
Monadic Second Order Logic

Existing logic-based querying tools for dependency treebanks use first order logic or monadic second order logic. We introduce a very fast model checker based on hybrid logic with operators ↓, @ and A and show that it is much faster than an existing querying tool for dependency treebanks based on first order logic, and much faster than an existing general purpose hybrid logic model checker. The querying tool is made publicly available.

scholarly journals Local Normal Forms for First-Order Logic with Applications to Games and Automata

1999 ◽  
Vol Vol. 3 no. 3 ◽  
Author(s):  
Thomas Schwentick ◽  
Klaus Barthelmann
Keyword(s):  
Normal Forms ◽  
Winning Strategy ◽  
Expressive Power ◽  
Second Order ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Relational Structures ◽  
Second Order Logic ◽  
Monadic Second Order Logic

International audience Building on work of Gaifman [Gai82] it is shown that every first-order formula is logically equivalent to a formula of the form ∃ x_1,...,x_l, \forall y, φ where φ is r-local around y, i.e. quantification in φ is restricted to elements of the universe of distance at most r from y. \par From this and related normal forms, variants of the Ehrenfeucht game for first-order and existential monadic second-order logic are developed that restrict the possible strategies for the spoiler, one of the two players. This makes proofs of the existence of a winning strategy for the duplicator, the other player, easier and can thus simplify inexpressibility proofs. \par As another application, automata models are defined that have, on arbitrary classes of relational structures, exactly the expressive power of first-order logic and existential monadic second-order logic, respectively.

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.

Structures and first-order logic

2004 ◽  
Author(s):  
Shawn Hedman
Keyword(s):  
Propositional Logic ◽  
Function Symbol ◽  
Second Order ◽  
Order Logic ◽  
First Order Logic ◽  
Ternary Relation ◽  
Specific Element ◽  
First Order ◽  
Lower Case ◽  
Second Order Logic

First-order logic is a richer language than propositional logic. Its lexicon contains not only the symbols ∧, ∨, ￢, →, and ↔ (and parentheses) from propositional logic, but also the symbols ∃ and ∀ for “there exists” and “for all,” along with various symbols to represent variables, constants, functions, and relations. These symbols are grouped into five categories. • Variables. Lower case letters from the end of the alphabet (. . . x, y, z) are used to denote variables. Variables represent arbitrary elements of an underlying set. This, in fact, is what “first-order” refers to. Variables that represent sets of elements are called second-order. Second-order logic, discussed in Chapter 9, is distinguished by the inclusion of such variables. • Constants. Lower case letters from the beginning of the alphabet (a, b, c, . . .) are usually used to denote constants. A constant represents a specific element of an underlying set. • Functions. The lower case letters f, g, and h are commonly used to denote functions. The arguments may be parenthetically listed following the function symbol as f(x1, x2, . . . , xn). First-order logic has symbols for functions of any number of variables. If f is a function of one, two, or three variables, then it is called unary, binary, or ternary, respectively. In general, a function of n variables is called n-ary and n is referred to as the arity of the function. • Relations. Capital letters, especially P, Q, R, and S, are used to denote relations. As with functions, each relation has an associated arity. We have an infinite number of each of these four types of symbols at our disposal. Since there are only finitely many letters, subscripts are used to accomplish this infinitude. For example, x1, x2, x3, . . . are often used to denote variables. Of course, we can use any symbol we want in first-order logic. Ascribing the letters of the alphabet in the above manner is a convenient convention. If you turn to a random page in this book and see “R(a, x, y),” you can safely assume that R is a ternary relation, x and y are variables, and a is a constant.

Abstraction Logic

2021 ◽  
Author(s):  
Steven Obua
Keyword(s):  
Binding Constants ◽  
Second Order ◽  
Order Logic ◽  
First Order Logic ◽  
Algebraic Semantics ◽  
Variable Binding ◽  
First Order ◽  
Free Variables ◽  
Direct Support ◽  
Second Order Logic

Abstraction Logic is introduced as a foundation for Practical Types and Practal. It combines the simplicity of first-order logic with direct support for variable binding constants called abstractions. It also allows free variables to depend on parameters, which means that first-order axiom schemata can be encoded as simple axioms. Conceptually abstraction logic is situated between first-order logic and second-order logic. It is sound with respect to an intuitive and simple algebraic semantics. Completeness holds for both intuitionistic and classical abstraction logic, and all abstraction logics in between and beyond.

scholarly journals A Resolution Calculus for Second-order Logic with Eager Unification

10.29007/zpg2 ◽  
2018 ◽  
Author(s):  
Alexander Leitsch ◽  
Tomer Libal
Keyword(s):  
Higher Order ◽  
Second Order ◽  
Order Logic ◽  
Higher Order Logic ◽  
Unification Algorithm ◽  
Efficient Search ◽  
First Order ◽  
Unification Algorithms ◽  
Second Order Logic ◽  
Resolution Calculus

The efficiency of the first-order resolution calculus is impaired when lifting it to higher-order logic. The main reason for that is the semi-decidability and infinitary natureof higher-order unification algorithms, which requires the integration of unification within the calculus and results in a non-efficient search for refutations.We present a modification of the constrained resolution calculus (Huet'72) which uses an eager unification algorithm while retaining completeness. Thealgorithm is complete with regard to bounded unification only, which for many cases, does not pose a problem in practice.

Sign in / Sign up

Export Citation Format

Share Document