scholarly journals Identity, equality, nameability and completeness. Part II

2018 ◽  
Vol 47 (3) ◽  
Author(s):  
María Manzano ◽  
Manuel Crescencio Moreno
Keyword(s):  
Modal Logic ◽  
Binary Relation ◽  
Type Theory ◽  
Formal Language ◽  
Higher Order ◽  
Order Logic ◽  
The Other ◽  
Higher Order Logic ◽  
Points Of View ◽  
Definition Of

This article is a continuation of our promenade along the winding roads of identity, equality, nameability and completeness. We continue looking for a place where all these concepts converge. We assume that identity is a binary relation between objects while equality is a symbolic relation between terms. Identity plays a central role in logic and we have looked at it from two different points of view. In one case, identity is a notion which has to be defined and, in the other case, identity is a notion used to define other logical concepts. In our previous paper, [16], we investigated whether identity can be introduced by definition arriving to the conclusion that only in full higher-order logic with standard semantics a reliable definition of identity is possible. In the present study we have moved to modal logic and realized that here we can distinguish in the formal language between two different equality symbols, the first one shall be interpreted as extensional genuine identity and only applies for objects, the second one applies for non rigid terms and has the characteristic of synonymy. We have also analyzed the hybrid modal logic where we can introduce rigid terms by definition and can express that two worlds are identical by using the nominals and the @ operator. We finish our paper in the kingdom of identity where the only primitives are lambda and equality. Here we show how other logical concepts can be defined in terms of the identity relation. We have found at the end of our walk a possible point of convergence in the logic Equational Hybrid Propositional Type Theory (EHPTT), [14] and [15].

scholarly journals Identity, Equality, Nameability and Completeness

2017 ◽  
Vol 46 (3/4) ◽  
Author(s):  
María Manzano ◽  
Manuel Crescencio Moreno
Keyword(s):  
Binary Relation ◽  
Order Logic ◽  
The Other ◽  
Higher Order Logic ◽  
First Case ◽  
General Semantics ◽  
Relevant Role ◽  
Definition Of ◽  
Relationship Of ◽  
The Relationship

This article is an extended promenade strolling along the winding roads of identity, equality, nameability and completeness, looking for places where they converge. We have distinguished between identity and equality; the first is a binary relation between objects while the second is a symbolic relation between terms. Owing to the central role the notion of identity plays in logic, you can be interested either in how to define it using other logical concepts or in the opposite scheme. In the first case, one investigates what kind of logic is required. In the second case, one is interested in the definition of the other logical concepts (connectives and quantifiers) in terms of the identity relation, using also abstraction. The present paper investigates whether identity can be introduced by definition arriving to the conclusion that only in full higher-order logic a reliable definition of identity is possible. However, the definition needs the standard semantics and we know that with this semantics completeness is lost. We have also studied the relationship of equality with comprehension and extensionality and pointed out the relevant role played by these two axioms in Henkin’s completeness method. We finish our paper with a section devoted to general semantics, where the role played by the nameable hierarchy of types is the key in Henkin’s completeness method.

scholarly journals Closed Structure

2021 ◽  
Author(s):  
Peter Fritz ◽  
Harvey Lederman ◽  
Gabriel Uzquiano
Keyword(s):  
Formal Language ◽  
Syntactic Structure ◽  
Natural Extension ◽  
Propositional Attitudes ◽  
Higher Order ◽  
Order Logic ◽  
Bertrand Russell ◽  
Structured Propositions ◽  
Higher Order Logic ◽  
Closed Structure

AbstractAccording to the structured theory of propositions, if two sentences express the same proposition, then they have the same syntactic structure, with corresponding syntactic constituents expressing the same entities. A number of philosophers have recently focused attention on a powerful argument against this theory, based on a result by Bertrand Russell, which shows that the theory of structured propositions is inconsistent in higher order-logic. This paper explores a response to this argument, which involves restricting the scope of the claim that propositions are structured, so that it does not hold for all propositions whatsoever, but only for those which are expressible using closed sentences of a given formal language. We call this restricted principle Closed Structure, and show that it is consistent in classical higher-order logic. As a schematic principle, the strength of Closed Structure is dependent on the chosen language. For its consistency to be philosophically significant, it also needs to be consistent in every extension of the language which the theorist of structured propositions is apt to accept. But, we go on to show, Closed Structure is in fact inconsistent in a very natural extension of the standard language of higher-order logic, which adds resources for plural talk of propositions. We conclude that this particular strategy of restricting the scope of the claim that propositions are structured is not a compelling response to the argument based on Russell’s result, though we note that for some applications, for instance to propositional attitudes, a restricted thesis in the vicinity may hold some promise.

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.).

scholarly journals POLYMORPHISM AND THE OBSTINATE CIRCULARITY OF SECOND ORDER LOGIC: A VICTIMS’ TALE

2018 ◽  
Vol 24 (1) ◽  
pp. 1-52
Author(s):  
PAOLO PISTONE
Keyword(s):  
Type Theory ◽  
Order Type ◽  
Higher Order ◽  
Second Order ◽  
Order Logic ◽  
Higher Order Logic ◽  
Related Notion ◽  
Foundational Research ◽  
The One ◽  
Second Order Logic

AbstractThe investigations on higher-order type theories and on the related notion of parametric polymorphism constitute the technical counterpart of the old foundational problem of the circularity (or impredicativity) of second and higher-order logic. However, the epistemological significance of such investigations has not received much attention in the contemporary foundational debate.We discuss Girard’s normalization proof for second order type theory or System F and compare it with two faulty consistency arguments: the one given by Frege for the logical system of the Grundgesetze (shown inconsistent by Russell’s paradox) and the one given by Martin-Löf for the intuitionistic type theory with a type of all types (shown inconsistent by Girard’s paradox).The comparison suggests that the question of the circularity of second order logic cannot be reduced to Russell’s and Poincaré’s 1906 “vicious circle” diagnosis. Rather, it reveals a bunch of mathematical and logical ideas hidden behind the hazardous idea of impredicative quantification, constituting a vast (and largely unexplored) domain for foundational research.

Predicative vs. Impredicative Abstraction

2018 ◽  
Author(s):  
Øystein Linnebo
Keyword(s):  
Higher Order ◽  
Order Logic ◽  
The Other ◽  
Abstract Objects ◽  
Higher Order Logic ◽  
Abstraction Principle ◽  
Two Sides

According to Frege and many of his followers, there is no “metaphysical distance” between the two sides of an acceptable abstraction principle. How should this attractive idea be understood? An analysis is developed in terms of the existence of a translation from the language concerned with the relevant abstract objects to a language not committed to such objects, such that this translation maps one side of the abstraction principle to the other. Next, two different notions of predicativity are distinguished: one pertaining to the background higher-order logic, and another associated with the abstraction principle itself. Finally, it is shown that only abstraction which is predicative in the latter sense satisfies our explication of the attractive idea about no “metaphysical distance”. This provides a reason to favor a conception of abstraction which is predicative in this sense.

A realizability interpretation of Church's simple theory of types

2016 ◽  
Vol 27 (8) ◽  
pp. 1364-1385
Author(s):  
ULRICH BERGER ◽  
TIE HOU
Keyword(s):  
Lambda Calculus ◽  
Higher Order ◽  
Order Logic ◽  
Simple Theory ◽  
Formal Proofs ◽  
Higher Order Logic ◽  
Mathematical Structures ◽  
Inductive Definitions ◽  
Definition Of ◽  
Intuitionistic Version

We give a realizability interpretation of an intuitionistic version of Church's Simple Theory of Types (CST) which can be viewed as a formalization of intuitionistic higher-order logic. Although definable in CST we include operators for monotone induction and coinduction and provide simple realizers for them. Realizers are formally represented in an untyped lambda–calculus with pairing and case-construct. The purpose of this interpretation is to provide a foundation for the extraction of verified programs from formal proofs as an alternative to type-theoretic systems. The advantages of our approach are that (a) induction and coinduction are not restricted to the strictly positive case, (b) abstract mathematical structures and results may be imported, (c) the formalization is technically simpler than in other systems, for example, regarding the definition of realizability, which is a simple syntactical substitution, and the treatment of nested and simultaneous (co)inductive definitions.

scholarly journals Embedding of Quantified Higher-Order Nominal Modal Logic into Classical Higher-Order Logic

10.29007/dzc2 ◽  
2018 ◽  
Author(s):  
Max Wisniewski ◽  
Alexander Steen
Keyword(s):  
Modal Logic ◽  
Higher Order ◽  
Order Logic ◽  
Tense Logic ◽  
Theorem Prover ◽  
Higher Order Logic ◽  
First Order ◽  
Automated Theorem Prover ◽  
Nominal Logic ◽  
The Moment

In this paper, we present an embedding of higher-order nominal modal logicinto classical higher-order logic, and study its automation. There exists no automated theorem prover for first-order or higher-order nominal logic at the moment, hence, this is the first automation for this kind of logic.In our work, we focus on nominal tense logic and have successfully proven some first theorems.

scholarly journals A HOL Basis for Reasoning about Functional Programs

1994 ◽  
Vol 1 (44) ◽  
Author(s):  
Sten Agerholm
Keyword(s):  
Higher Order ◽  
Partial Orders ◽  
Order Logic ◽  
Domain Theory ◽  
Higher Order Logic ◽  
Unification Algorithm ◽  
Recursive Functions ◽  
Bottom Element ◽  
Definition Of ◽  
Primitive Recursive

Domain theory is the mathematical theory underlying denotational semantics. This thesis presents a formalization of domain theory in the Higher Order Logic (HOL) theorem proving system along with a mechanization of proof functions and other tools to support reasoning about the denotations of functional programs. By providing a fixed point operator for functions on certain domains which have a special undefined (bottom) element, this extension of HOL supports the definition of recursive functions which are not also primitive recursive. Thus, it provides an approach to the long-standing and important problem of defining non-primitive recursive functions in the HOL system.<br /> <br />Our philosophy is that there must be a direct correspondence between elements of complete partial orders (domains) and elements of HOL types, in order to allow the reuse of higher order logic and proof infrastructure already available in the HOL system. Hence, we are able to mix domain theoretic reasoning with reasoning in the set theoretic HOL world to advantage, exploiting HOL types and tools directly. Moreover, by mixing domain and set theoretic reasoning, we are able to eliminate almost all reasoning about the bottom element of complete partial orders that makes the LCF theorem prover, which supports a first order logic of domain theory, difficult and tedious to use. A thorough comparison with LCF is provided.<br /> <br />The advantages of combining the best of the domain and set theoretic worlds in the same system are demonstrated in a larger example, showing the correctness of a unification algorithm. A major part of the proof is conducted in the set theoretic setting of higher order logic, and only at a late stage of the proof domain theory is introduced to give a recursive definition of the algorithm, which is not primitive recursive. Furthermore, a total well-founded recursive unification function can be defined easily in pure HOL by proving that the unification algorithm (defined in domain theory) always terminates; this proof is conducted by a non-trivial well-founded induction. In such applications, where non-primitive recursive HOL functions are defined via domain theory and a proof of termination, domain theory constructs only appear temporarily.

Williamson on necessitism

2016 ◽  
Vol 46 (4-5) ◽  
pp. 613-639 ◽  
Author(s):  
Jeremy Goodman
Keyword(s):  
Modal Logic ◽  
Higher Order ◽  
Order Logic ◽  
Higher Order Logic ◽  
Way Of Thinking

AbstractI critically discuss some of the main arguments of Modal Logic as Metaphysics, present a different way of thinking about the issues raised by those arguments, and briefly discuss some broader issues about the role of higher-order logic in metaphysics.

Sign in / Sign up

Export Citation Format

Share Document