scholarly journals IBN SĪNĀ’S APPROACH TO EQUALITY AND UNITY

2014 ◽  
Vol 24 (2) ◽  
pp. 297-307 ◽  
Author(s):  
Shahid Rahman ◽  
Johan Georg Granström ◽  
Zaynab Salloum

AbstractAristotle did not develop the quantification of the predicate, but, as shown in a recent paper by Hasnawi, Ibn Sīnā did. In fact, assuming the Aristotelian subject-predicate structure, Ibn Sīnā qualifies those propositions that carry a quantified predicate as deviating (muḥarrafa) propositions. A consequence of Ibn Sīnā’s approach is that the second quantification is absorbed by the predicate term. The clear differentiation between a quantified subject, that settles the domain of quantification, and a predicative part, that builds a proposition over this domain, corresponds structurally to the distinction, made in constructive type theory, between the type of sets and the type of propositions.Neither did Aristotle combine his logical analysis of quantification with his ontological theory of relations or equality. But Ibn Sīnā makes use of syllogisms that require a logic of equality, and considered cases where quantification combines via equality with singular terms. Moreover these reflections provide the basis for his theory of numbers that is based on the interplay between the One and the Many. If we combine Ibn Sīnā’s metaphysical theory of equality with his work on the quantification of the predicate, a logic of equality comes out naturally. Indeed, the interaction between quantification of the predicate and equality can be applied to Ibn Sīnā’s own examples of syllogisms involving these notions. By using the formal instruments provided Martin-Löf's constructive type theory, the present paper establishes links between Ibn Sīnā’s metaphysics and his logical work: links that have been discussed in relation to other topics by Thom and Street. Ibn Sīnā did not develop a logic of identity, but he did develop the conceptual means to do so.

Author(s):  
Ernesto Copello ◽  
Nora Szasz ◽  
Álvaro Tasistro

Abstarct We formalize in Constructive Type Theory the Lambda Calculus in its classical first-order syntax, employing only one sort of names for both bound and free variables, and with α-conversion based upon name swapping. As a fundamental part of the formalization, we introduce principles of induction and recursion on terms which provide a framework for reproducing the use of the Barendregt Variable Convention as in pen-and-paper proofs within the rigorous formal setting of a proof assistant. The principles in question are all formally derivable from the simple principle of structural induction/recursion on concrete terms. We work out applications to some fundamental meta-theoretical results, such as the Church–Rosser Theorem and Weak Normalization for the Simply Typed Lambda Calculus. The whole development has been machine checked using the system Agda.


1989 ◽  
pp. 369-410 ◽  
Author(s):  
PRAKASH PANANGADEN ◽  
PAUL MENDLER ◽  
MICHAEL I. SCHWARTZBACH

1997 ◽  
Vol 62 (4) ◽  
pp. 1315-1332 ◽  
Author(s):  
Sara Negri ◽  
Silvio Valentini

In this paper we give a constructive proof of the pointfree version of Tychonoff's theorem within formal topology, using ideas from Coquand's proof in [7]. To deal with pointfree topology Coquand uses Johnstone's coverages. Because of the representation theorem in [3], from a mathematical viewpoint these structures are equivalent to formal topologies but there is an essential difference also. Namely, formal topologies have been developed within Martin Löf's constructive type theory (cf. [16]), which thus gives a direct way of formalizing them (cf. [4]).The most important aspect of our proof is that it is based on an inductive definition of the topological product of formal topologies. This fact allows us to transform Coquand's proof into a proof by structural induction on the last rule applied in a derivation of a cover. The inductive generation of a cover, together with a modification of the inductive property proposed by Coquand, makes it possible to formulate our proof of Tychonoff s theorem in constructive type theory. There is thus a clear difference to earlier localic proofs of Tychonoff's theorem known in the literature (cf. [9, 10, 12, 14, 27]). Indeed we not only avoid to use the axiom of choice, but reach constructiveness in a very strong sense. Namely, our proof of Tychonoff's theorem supplies an algorithm which, given a cover of the product space, computes a finite subcover, provided that there exists a similar algorithm for each component space.


2011 ◽  
pp. 609-638 ◽  
Author(s):  
Steve Awodey ◽  
Richard Garner ◽  
Per Martin-Löf ◽  
Vladimir Voevodsky

Author(s):  
AARON STUMP

AbstractModern constructive type theory is based on pure dependently typed lambda calculus, augmented with user-defined datatypes. This paper presents an alternative called the Calculus of Dependent Lambda Eliminations, based on pure lambda encodings with no auxiliary datatype system. New typing constructs are defined that enable induction, as well as large eliminations with lambda encodings. These constructs are constructor-constrained recursive types, and a lifting operation to lift simply typed terms to the type level. Using a lattice-theoretic denotational semantics for types, the language is proved logically consistent. The power of CDLE is demonstrated through several examples, which have been checked with a prototype implementation called Cedille.


Sign in / Sign up

Export Citation Format

Share Document