scholarly journals MECHANIZING PRINCIPIA LOGICO-METAPHYSICA IN FUNCTIONAL TYPE-THEORY

2019 ◽  
Vol 13 (1) ◽  
pp. 206-218 ◽  
Author(s):  
DANIEL KIRCHNER ◽  
CHRISTOPH BENZMÜLLER ◽  
EDWARD N. ZALTA
Keyword(s):  
Type Theory ◽  
Scientific Practice ◽  
Higher Order ◽  
Functional Type ◽  
Higher Order Logic ◽  
Joint Project ◽  
Metaphysical Theory ◽  
Fresh Perspective ◽  
Computational Metaphysics ◽  
Universal Reasoning

AbstractPrincipia Logico-Metaphysica contains a foundational logical theory for metaphysics, mathematics, and the sciences. It includes a canonical development of Abstract Object Theory [AOT], a metaphysical theory (inspired by ideas of Ernst Mally, formalized by Zalta) that distinguishes between ordinary and abstract objects.This article reports on recent work in which AOT has been successfully represented and partly automated in the proof assistant system Isabelle/HOL. Initial experiments within this framework reveal a crucial but overlooked fact: a deeply-rooted and known paradox is reintroduced in AOT when the logic of complex terms is simply adjoined to AOT’s specially formulated comprehension principle for relations. This result constitutes a new and important paradox, given how much expressive and analytic power is contributed by having the two kinds of complex terms in the system. Its discovery is the highlight of our joint project and provides strong evidence for a new kind of scientific practice in philosophy, namely, computational metaphysics.Our results were made technically possible by a suitable adaptation of Benzmüller’s metalogical approach to universal reasoning by semantically embedding theories in classical higher-order logic. This approach enables one to reuse state-of-the-art higher-order proof assistants, such as Isabelle/HOL, for mechanizing and experimentally exploring challenging logics and theories such as AOT. Our results also provide a fresh perspective on the question of whether relational type theory or functional type theory better serves as a foundation for logic and metaphysics.

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.

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

Hauptsatz for higher order logic

1968 ◽  
Vol 33 (3) ◽  
pp. 452-457 ◽  
Author(s):  
Dag Prawitz
Keyword(s):  
Finite Type ◽  
Type Theory ◽  
Predicate Logic ◽  
Higher Order ◽  
Second Order ◽  
Order Logic ◽  
Simple Type ◽  
Higher Order Logic ◽  
Simple Type Theory ◽  
Second Order Logic

I shall prove in this paper that Gentzen's Hauptsatz is extendible to simple type theory, i.e., to the predicate logic obtained by admitting quantification over predicates of arbitrary finite type and generalizing the second order quantification rules to cover quantifiers of other types. (That Gentzen's Hauptsatz is extendible to this logic has been known as Takeuti's conjecture; see [4].) Gentzen's Hauptsatz has been extended to second order logic in a recent paper by Tait [3]. However, as remarked by Tait, his proof seems not to be extendible to higher orders. The present proof is rather an extension of a different proof of the Hauptsatz for second order logic that I have presented in [1].

Computational Models for Multilayered Composite Shells with Application to Tires

1996 ◽  
Vol 24 (1) ◽  
pp. 11-38 ◽  
Author(s):  
G. M. Kulikov
Keyword(s):  
Type Theory ◽  
Computational Models ◽  
Geometrical Nonlinearity ◽  
Higher Order ◽  
Stress Strain ◽  
Strain Fields ◽  
First Order ◽  
Timoshenko Type ◽  
Joint Influence ◽  
Discrete Layer

Abstract This paper focuses on four tire computational models based on two-dimensional shear deformation theories, namely, the first-order Timoshenko-type theory, the higher-order Timoshenko-type theory, the first-order discrete-layer theory, and the higher-order discrete-layer theory. The joint influence of anisotropy, geometrical nonlinearity, and laminated material response on the tire stress-strain fields is examined. The comparative analysis of stresses and strains of the cord-rubber tire on the basis of these four shell computational models is given. Results show that neglecting the effect of anisotropy leads to an incorrect description of the stress-strain fields even in bias-ply tires.

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.

Sign in / Sign up

Export Citation Format

Share Document