** متابعات ثقافية متميزة ** Blogs al ssadh
هل تريد التفاعل مع هذه المساهمة؟ كل ما عليك هو إنشاء حساب جديد ببضع خطوات أو تسجيل الدخول للمتابعة.

** متابعات ثقافية متميزة ** Blogs al ssadh

موقع للمتابعة الثقافية العامة
 
Natural Numbers I_icon_mini_portalالرئيسيةالأحداثالمنشوراتأحدث الصورالتسجيلدخول



مدونات الصدح ترحب بكم وتتمنى لك جولة ممتازة

وتدعوكم الى دعمها بالتسجيل والمشاركة

عدد زوار مدونات الصدح

إرسال موضوع جديد   إرسال مساهمة في موضوع
 

 Natural Numbers

اذهب الى الأسفل 
كاتب الموضوعرسالة
free men
فريق العمـــــل *****
free men


التوقيع : رئيس ومنسق القسم الفكري

عدد الرسائل : 1500

الموقع : center d enfer
تاريخ التسجيل : 26/10/2009
وســــــــــام النشــــــــــــــاط : 6

Natural Numbers Empty
11032016
مُساهمةNatural Numbers

Natural Numbers Ouo_0010
As in Peano arithmetic the natural numbers are generated by 0 and the successor operation [ltr]ss[/ltr]. The elimination rule states that these are the only possible ways to generate a natural number.
We write [ltr]f(c)=R(c,d,xy.e)f(c)=R(c,d,xy.e)[/ltr] for the function which is defined by primitive recursion on the natural number [ltr]cc[/ltr] with base case [ltr]dd[/ltr] and step function [ltr]xy.exy.e[/ltr] (or alternatively [ltr]λxy.eλxy.e[/ltr]) which maps the value [ltr]yy[/ltr] for the previous number [ltr]x:Nx:N[/ltr] to the value for [ltr]s(x)s(x)[/ltr]. Note that [ltr]RR[/ltr] is a new variable-binding operator: the variables [ltr]xx[/ltr] and [ltr]yy[/ltr] become bound in [ltr]ee[/ltr].
[ltr]NN[/ltr]-formation.
[ltr]Γ⊢NΓ⊢N[/ltr]

[ltr]NN[/ltr]-introduction.
[ltr]Γ⊢0:NΓ⊢a:NΓ⊢s(a):NΓ⊢0:NΓ⊢a:NΓ⊢s(a):N[/ltr]

[ltr]NN[/ltr]-elimination.

[ltr]Γ,x:N⊢CΓ⊢c:NΓ⊢d:C[x:=0]Γ,y:N,z:C[x:=y]⊢e:C[x:=s(y)]Γ⊢R(c,d,yz.e):C[x:=c]Γ,x:N⊢CΓ⊢c:NΓ⊢d:C[x:=0]Γ,y:N,z:C[x:=y]⊢e:C[x:=s(y)]Γ⊢R(c,d,yz.e):C[x:=c][/ltr]

[ltr]NN[/ltr]-equality (under appropriate premises).
[ltr]R(0,d,yz.e)R(s(a),d,yz.e)=d:C[x:=0]=e[y:=a,z:=R(a,d,yz.e)]:C[x:=s(a)]R(0,d,yz.e)=d:C[x:=0]R(s(a),d,yz.e)=e[y:=a,z:=R(a,d,yz.e)]:C[x:=s(a)][/ltr]

The rule of [ltr]NN[/ltr]-elimination simultaneously expresses the type of a function defined by primitive recursion and, under the Curry-Howard interpretation, the rule of mathematical induction: we prove the property [ltr]CC[/ltr] of a natural number [ltr]xx[/ltr] by induction on [ltr]xx[/ltr].
Gödel’s System [ltr]TT[/ltr] is essentially intuitionistic type theory with only the type formers [ltr]NN[/ltr] and [ltr]A→BA→B[/ltr] (the type of functions from [ltr]AA[/ltr] to [ltr]BB[/ltr], which is the special case of [ltr](Πx:A)B(Πx:A)B[/ltr] where [ltr]BB[/ltr]does not depend on [ltr]x:Ax:A[/ltr]). Since there are no dependent types in System [ltr]TT[/ltr] the rules can be simplified.

3.6 The Universe of Small Types

Martin-Löf’s first version of type theory (Martin-Löf 1971a) had an axiom stating that there is a type of all types. This was proved inconsistent by Girard who found that the Burali-Forti paradox could be encoded in this theory.
To overcome this pathological impredicativity, but still retain some of its expressivity, Martin-Löf introduced in 1972 a universe [ltr]UU[/ltr] of small types closed under all type formers of the theory, except that it does not contain itself (Martin-Löf 1998 [1972]). The rules are:
[ltr]UU[/ltr]-formation.
[ltr]Γ⊢UΓ⊢U[/ltr]

[ltr]UU[/ltr]-introduction.
[ltr]Γ⊢∅:UΓ⊢1:UΓ⊢∅:UΓ⊢1:U[/ltr]


[ltr]Γ⊢A:UΓ⊢B:UΓ⊢A+B:UΓ⊢A:UΓ⊢B:UΓ⊢A×B:UΓ⊢A:UΓ⊢B:UΓ⊢A+B:UΓ⊢A:UΓ⊢B:UΓ⊢A×B:U[/ltr]

[ltr]Γ⊢A:UΓ⊢B:UΓ⊢A→B:UΓ⊢A:UΓ⊢B:UΓ⊢A→B:U[/ltr]

[ltr]Γ⊢A:UΓ,x:A⊢B:UΓ⊢Σx:A.B:UΓ⊢A:UΓ,x:A⊢B:UΓ⊢Πx:A.B:UΓ⊢A:UΓ,x:A⊢B:UΓ⊢Σx:A.B:UΓ⊢A:UΓ,x:A⊢B:UΓ⊢Πx:A.B:U[/ltr]

[ltr]Γ⊢N:UΓ⊢N:U[/ltr]
[ltr]UU[/ltr]-elimination.
[ltr]Γ⊢A:UΓ⊢AΓ⊢A:UΓ⊢A[/ltr]

Since [ltr]UU[/ltr] is a type, we can use [ltr]NN[/ltr]-elimination to define small types by primitive recursion. For example, if [ltr]A:UA:U[/ltr], we can define the type of [ltr]nn[/ltr]-tuples of elements in [ltr]AA[/ltr] as follows:

[ltr]A[size=13]n=R(n,1,xy.A×y):UAn=R(n,1,xy.A×y):U[/ltr][/size]
This type-theoretic universe [ltr]UU[/ltr] is analogous to a Grothendieck universe in set theory which is a set of sets closed under all the ways sets can be constructed in Zermelo-Fraenkel set theory. The existence of a Grothendieck universe cannot be proved from the usual axioms of Zermelo-Fraenkel set theory but needs a new axiom.
In Martin-Löf (1975) the universe is extended to a countable hierarchy of universes

[ltr]U[size=13]0:U1:U2:⋯.U0:U1:U2:⋯.[/ltr][/size]
In this way each type has a type, not only each small type.

3.7 Propositional Identity

Above, we introduced the equality judgment

[ltr]Γ⊢a=a[size=13]′:A.(4)(4)Γ⊢a=a′:A.[/ltr][/size]
This is usually called a “definitional equality” because it can be decided by normalizing the terms [ltr]aa[/ltr] and [ltr]a[size=13]′a′[/ltr] and checking whether the normal forms are identical. However, this equality is a judgment and not a proposition (type) and we thus cannot prove such judgmental equalities by induction. For this reason we need to introduce propositional identity types. For example, the identity type for natural numbers [ltr]I(N,m,n)I(N,m,n)[/ltr] can be defined by [ltr]UU[/ltr]-valued primitive recursion. We can then express and prove the Peano axioms. Moreover, extensional equality of ufnctions can be defined by[/size]

[ltr]I(N→N,f,f[size=13]′)=Πx:N.I(N,fx,fx).I(N→N,f,f′)=Πx:N.I(N,fx,f′x).[/ltr][/size]

3.8 The Axiom of Choice is a Theorem

The following form of the axiom of choice is an immediate consequence of the BHK-interpretation of the intuitionistic quantifiers, and is easily proved in intuitionistic type theory:

[ltr](Πx:A.Σy:B.C)→Σf:(Πx:A.B).C[y:=fx](Πx:A.Σy:B.C)→Σf:(Πx:A.B).C[y:=fx][/ltr]
The reason is that [ltr]Πx:A.Σy:B.CΠx:A.Σy:B.C[/ltr] is the type of functions which map elements [ltr]x:Ax:A[/ltr] to pairs [ltr](y,z)(y,z)[/ltr] with [ltr]y:By:B[/ltr] and [ltr]z:Cz:C[/ltr]. The choice function [ltr]ff[/ltr] is obtained by returning the first component [ltr]y:By:B[/ltr]of this pair.
It is perhaps surprising that intuitionistic type theory directly validates an axiom of choice, since this axiom is often considered problematic from a constructive point of view. A possible explanation for this state of affairs is that the above is an axiom of choice for types, and that types are not in general appropriate constructive approximations of sets in the classical sense. For example, we can represent a real number as a Cauchy sequence in intuitionistic type theory, but the set of real numbers is not the type of Cauchy sequences, but the type of Cauchy sequences up to equiconvergence. More generally, a set in Bishop’s constructive mathematics is represented by a type (commonly called “preset”) together with an equivalence relation.
If [ltr]AA[/ltr] and [ltr]BB[/ltr] are equipped with equivalence relations, there is of course no guarantee that the choice function, [ltr]ff[/ltr] above, is extensional in the sense that it maps equivalent element to equivalent elements. This is the failure of the extensional axiom of choice, see Martin-Löf (2009) for an analysis.

4. Extensions

4.1 The Logical Framework

The above completes the description of a core version of intuitionistic type theory close to that of (Martin-Löf 1998 [1972]).
In 1986 Martin-Löf proposed a reformulation of intuitionistic type theory; see Nordström, Peterson and Smith (1990) for an exposition. The purpose was to give a more compact formulation, where [ltr]λλ[/ltr] and [ltr]ΠΠ[/ltr] are the only variable binding operations. It is nowadays considered the main version of the theory. It is also the basis for the Agda proof assistant. The 1986 theory has two parts:

  • the theory of types (the logical framework);

  • the theory of sets (small types).


Remark 4.1. Note that the word “set” in the logical framework does not coincide with the way it is used in Bishop’s constructive mathematics. To avoid this confusion, types together with equivalence relations are usually called “setoids” or “extensional sets” in intuitionistic type theory.
The logical framework has only two type formers: [ltr]Πx:A.BΠx:A.B[/ltr] (usually written [ltr](x:A)B(x:A)B[/ltr] or [ltr](x:A)→B(x:A)→B[/ltr] in the logical framework formulation) and [ltr]UU[/ltr] (usually called [ltr]SetSet[/ltr]). The rules for [ltr]Πx:A.BΠx:A.B[/ltr] ([ltr](x:A)→B(x:A)→B[/ltr]) are the same as given above (including [ltr]ηη[/ltr]-conversion). The rules for [ltr]UU[/ltr] ([ltr]SetSet[/ltr]) are also the same, except that the logical framework only stipulates closure under [ltr]ΠΠ[/ltr]-type formation.
The other small type formers (“set formers”) are introduced in the theory of sets. In the logical framework formulation each formation, introduction, and elimination rule can be expressed as the typing of a new constant. For example, the rules for natural numbers become

[ltr]N0sR:Set,:N,:N→N,:(C:N→Set)→C0→((x:N)→Cx→C(sx))→(c:N)→Cc.N:Set,0:N,s:N→N,R:(C:N→Set)→C0→((x:N)→Cx→C(sx))→(c:N)→Cc.[/ltr]

where we have omitted the common context [ltr]ΓΓ[/ltr], since the types of these constants are closed. Note that the recursion operator [ltr]RR[/ltr] has a first argument [ltr]C:N→SetC:N→Set[/ltr] unlike in the original formulation.
Moreover, the equality rules can be expressed as equations

[ltr]RCde0RCde(sa)=d:C0=ea(RCdea):C(sa)RCde0=d:C0RCde(sa)=ea(RCdea):C(sa)[/ltr]
under suitable assumptions.
In the sequel we will present several extensions of type theory. To keep the presentation uniform we will however not use the logical framework presentation of type theory, but will use the same notation as in section 2.

4.2 A General Identity Type Former

As we mentioned above, identity on natural numbers can be defined by primitive recursion. Identity relations on other types can also be defined in the basic version of intuitionistic type theory presented in section 2.
However, Martin-Löf (1975) extended intuitionistic type theory with a uniform primitive identity type former [ltr]II[/ltr] for all types. The rules for [ltr]II[/ltr] express that the identity relation is inductively generated by the proof of reflexivity, a canonicial constant called [ltr]rr[/ltr]. (Note that [ltr]rr[/ltr] was coded by the number 0 in the introductory presentation of proof-objects in 2.3. The elimination rule for the identity type is a generalization of identity elimination in predicate logic and introduces an elimination constant [ltr]JJ[/ltr]. (We here show the formulation due to Paulin-Mohring (1993) rather than the original formulation of Martin-Löf (1975).) The inference rules are the following.
[ltr]II[/ltr]-formation.
[ltr]Γ⊢AΓ⊢a:AΓ⊢a[size=13]′:AΓ⊢I(A,a,a)Γ⊢AΓ⊢a:AΓ⊢a′:AΓ⊢I(A,a,a′)[/ltr][/size]

[ltr]II[/ltr]-introduction.
[ltr]Γ⊢AΓ⊢a:AΓ⊢r:I(A,a,a)Γ⊢AΓ⊢a:AΓ⊢r:I(A,a,a)[/ltr]

[ltr]II[/ltr]-elimination.

[ltr]Γ,x:A,y:I(A,a,x)⊢CΓ⊢b:AΓ⊢c:I(A,a,b)Γ⊢d:C[x:=a,y:=r]Γ⊢J(c,d):C[x:=b,y:=c]Γ,x:A,y:I(A,a,x)⊢CΓ⊢b:AΓ⊢c:I(A,a,b)Γ⊢d:C[x:=a,y:=r]Γ⊢J(c,d):C[x:=b,y:=c][/ltr]

[ltr]II[/ltr]-equality (under appropriate assumptions).

[ltr]J(r,d)=dJ(r,d)=d[/ltr]
By constructing a model of type theory where types are interpreted as groupoids (categories where all arrows are isomorphisms) Hofmann and Streicher (1998) showed that it cannot be proved in intuitionistic type theory that all proofs of [ltr]I(A,a,b)I(A,a,b)[/ltr] are identical. This may seem as an incompleteness of the theory and Streicher suggested a new axiom [ltr]KK[/ltr] from which it follows that all proofs of [ltr]I(A,a,b)I(A,a,b)[/ltr] are identical to [ltr]rr[/ltr].
The [ltr]I[/ltr]
[ltr]I[/ltr]-type is often called the intensional identity type, since it does not satisfy the principle of function extensionality. Intuitionistic type theory with the intensional identity type is also often called intensional intuitionistic type theory to distinguish it from extensional intuitionistic type theory which will be presented in section 7.1.
الرجوع الى أعلى الصفحة اذهب الى الأسفل
مُشاطرة هذه المقالة على: reddit

Natural Numbers :: تعاليق

free men
رد: Natural Numbers
مُساهمة الجمعة مارس 11, 2016 12:03 pm من طرف free men

 Well-Founded Trees

A type of well-founded trees of the form [ltr]Wx:A.BWx:A.B[/ltr] was introduced in Martin-Löf 1982 (and in a more restricted form by Scott 1970). Elements of [ltr]Wx:A.BWx:A.B[/ltr] are trees of varying and arbitrary branching: varying, because the branching type [ltr]BB[/ltr] is indexed by [ltr]x:Ax:A[/ltr] and arbitrary because [ltr]BB[/ltr] can be arbitrary. The type is given by a generalized inductive definition since the well-founded trees may be infinitely branching. We can think of [ltr]Wx:A.BWx:A.B[/ltr] as the free term algebra, where each [ltr]a:Aa:A[/ltr]represents a term constructor [ltr]supasupa[/ltr] with (possibly infinite) arity [ltr]B[x:=a]B[x:=a][/ltr].
[ltr]WW[/ltr]-formation.
[ltr]Γ⊢AΓ,x:A⊢BΓ⊢Wx:A.BΓ⊢AΓ,x:A⊢BΓ⊢Wx:A.B[/ltr]

[ltr]WW[/ltr]-introduction.
[ltr]Γ⊢a:AΓ,y:B[x:=a]⊢b:Wx:A.BΓ⊢sup(a,y.b):Wx:A.BΓ⊢a:AΓ,y:B[x:=a]⊢b:Wx:A.BΓ⊢sup(a,y.b):Wx:A.B[/ltr]

We omit the rules of [ltr]WW[/ltr]-elimination and [ltr]WW[/ltr]-equality.
Adding well-founded trees to intuitionistic type theory increases its proof-theoretic strength significantly (Setzer (1998)).

4.4 Iterative Sets and CZF

An important application of well-founded trees is Aczel’s (1978) construction of a type-theoretic model of Constructive Zermelo Fraenkel Set Theory. To this end he defines the type of iterative sets as
[ltr]V=Wx:U.x.V=Wx:U.x.[/ltr]
Let [ltr]A:UA:U[/ltr] be a small type, and [ltr]x:A⊢Mx:A⊢M[/ltr] be an indexed family of iterative sets. Then [ltr]sup(A,x.M)sup(A,x.M)[/ltr], or with a more suggestive notation [ltr]{M∣x:A}{M∣x:A}[/ltr], is an iterative set. To paraphrase: an iterative set is a set of iterative sets.
Note that an iterative set is a data-structure in the sense of functional programming: a possibly infinitely branching well-founded tree. Different trees may represent the same set. We therefore need to define a notion of extensional equality between iterative sets which disregards repetition and order of elements. This definition is formally similar to the definition of bisimulation of processes in process algebra. The type [ltr]VV[/ltr] up to extensional equality can be viewed as a constructive type-theoretic model of the cumulative hierarchy, see the entry on set theory: constructive and intuitionistic ZF for further information about CZF.

4.5 Inductive Definitions

The notion of an inductive definition is fundamental in intuitionistic type theory. It is a primitive notion and not, as in set theory, a derived notion where an inductively defined set is defined impredicatively as the smallest set closed under some rules. However, in intuitionistic type theory inductive definitions are considered predicative: they are viewed as being built up from below.
The inductive definability of types is inherent in the meaning explanations of intuitionistic type theory which we shall discuss in the next section. In fact, intuitionistic type theory can be described briefly as a theory of inductive, recursive, and inductive-recursive definitions based on a framework of lambda calculus with dependent types.
We have already seen the type of natural numbers and the type of well-founded trees as examples of types given by inductive definitions; the natural numbers is an example of an ordinary finitary inductive definition and the well-founded trees of a generalized possibly infinitary inductive definition. The introduction rules describe how elements of these types are inductively generated and the elimination and equality rules describe how functions from these types can be defined by structural recursion on the way these elements are generated. According to the propositions as types principle, the elimination rules are simultaneously rules for proof by structural induction on the way the elements are generated.
The type formers [ltr]0,1,+,×,→,Σ,0,1,+,×,→,Σ,[/ltr] and [ltr]ΠΠ[/ltr] which interpret the logical constants for intuitionistic predicate logic are examples of degenerate inductive definitions. Even the identity type (in intensional intuitionistic type theory) is inductively generated; it is the type of proofs generated by the reflexivity axiom. Its elimination rule expresses proof by pattern matching on the proof of reflexivity.
The common structure of the rules of the type formers can be captured by a general schema for inductive definitions (Dybjer 1991). This general schema has many useful instances, for example, the type [ltr]List(A)List(A)[/ltr] of lists with elements of type [ltr]AA[/ltr] has the following introduction rules:
[ltr]Γ⊢nil:List(A)Γ⊢a:AΓ⊢as:List(A)Γ⊢cons(a,as):List(A)Γ⊢nil:List(A)Γ⊢a:AΓ⊢as:List(A)Γ⊢cons(a,as):List(A)[/ltr]
Other useful instances are types of binary trees and other trees such as the infinitely branching trees of the Brouwer ordinals of the second and higher number classes.
The general schema does not only cover inductively defined types, but also inductively defined families of types, such as the identity relation. The above mentioned type [ltr]A[size=13]nAn[/ltr] of [ltr]nn[/ltr]-tuples of type [ltr]AA[/ltr] was defined above by primitive recursion on [ltr]nn[/ltr]. It can also be defined as an inductive family with the following introduction rules[/size]
[ltr]Γ⊢nil:A[size=13]0Γ⊢a:AΓ⊢as:AnΓ⊢cons(a,as):AsnΓ⊢nil:A0Γ⊢a:AΓ⊢as:AnΓ⊢cons(a,as):Asn[/ltr][/size]
The schema for inductive types and families is a type-theoretic generalization of a schema for iterated inductive definitions in predicate logic (formulated in natural deduction) presented by Martin-Löf (1971b). This paper immediately preceded Martin-Löf’s first version of intuitionistic type theory. It is both conceptually and technically a forerunner to the development of the theory.
It is an essential feature of proof assistants such as Agda and Coq that it enables users to define their own inductive types and families by listing their introduction rules (the types of their constructors). This is much like in typed functional programming languages such as Haskell and the different dialects of ML. However, unlike in these programming languages the schema for inductive definitions in intuitionistic type theory enforces a restriction amounting to well-foundedness of the elements of the defined types.

4.6 Inductive-Recursive Definitions

We already mentioned that there are two main definition principles in intuitionistic type theory: the inductive definition of types (sets) and the (primitive, structural) definition of functions by recursion on the way the elements of such types are inductively generated. Usually, the inductive definition of a set comes first: the formation and introduction rules make no reference to the elimination rule. However, there are definitions in intuitionistic type theory for which this is not the case and we simultaneously inductively generate a type and a function from that type defined by structural recursion. Such definitions are simultaneously inductive-recursive.
The first example of such an inductive-recursive definition is an alternative formulation à la Tarski of the universe of small types. Above we presented the universe formulated à la Russell, where there is no notational distinction between the element [ltr]A:UA:U[/ltr] and the corresponding type [ltr]AA[/ltr]. For a universe à la Tarski there is such a distinction, for example, between the element [ltr]N^:UN^:U[/ltr] and the corresponding type [ltr]NN[/ltr]. The element [ltr]N^N^[/ltr] is called the code for [ltr]NN[/ltr].
The elimination rule for [ltr]UU[/ltr] à la Tarski is:
[ltr]Γ⊢a:UΓ⊢T(a)Γ⊢a:UΓ⊢T(a)[/ltr]
This expresses that there is a function [ltr]TT[/ltr] which maps a code [ltr]aa[/ltr] to its corresponding type [ltr]T(a)T(a)[/ltr]. The equality rules define this correspondence. For example,
[ltr]T(N^)=N.T(N^)=N.[/ltr]
We see that [ltr]UU[/ltr] is inductively generated with one introduction rule for each small type former, and[ltr]TT[/ltr] is defined by recursion on these small type formers. The simultaneous inductive-recursive nature of this definition becomes apparent in the rules for [ltr]ΠΠ[/ltr] for example. The introduction rule is
[ltr]Γ⊢a:UΓ,x:T(a)⊢b:UΓ⊢Π^x:a.b:UΓ⊢a:UΓ,x:T(a)⊢b:UΓ⊢Π^x:a.b:U[/ltr]
and the corresponding equality rule is
[ltr]T(Π^x:a.b)=Πx:T(a).T(b)T(Π^x:a.b)=Πx:T(a).T(b)[/ltr]
Note that the introduction rule for [ltr]UU[/ltr] refers to [ltr]TT[/ltr], and hence that [ltr]UU[/ltr] and [ltr]TT[/ltr] must be defined simultaneously.
There are a number of other universe constructions which are defined inductive-recursively: universe hierarchies, superuniverses (Palmgren 1998; Rathjen, Griffor, and Palmgren 1998), and Mahlo universes (Setzer 2000). These universes are analogues of certain large cardinals in set theory: inaccessible, hyperinaccessible, and Mahlo cardinals.
Other examples of inductive-recursive definitions include an informal definition of computability predicates used by Martin-Löf in an early normalization proof of intuitionistic type theory (Martin-Löf 1998 [1972]). There are also many natural examples of “small” inductive-recursive definitions, where the recursively defined (decoding) function returns an element of a type rather than a type.

A large class of inductive-recursive definitions, including the above, can be captured by a general schema (Dybjer 2000) which extends the schema for inductive definitions mentioned above. As shown by Setzer, intuitionistic type theory with this class of inductive-recursive definitions is very strong proof-theoretically (Dybjer and Setzer 2003). However, as proposed in recent unpublished work by Setzer, it is possible to increase the strength of the theory even further and define universes such as an autonomous Mahlo universe which are analogues of even larger cardinals.
free men
رد: Natural Numbers
مُساهمة الجمعة مارس 11, 2016 12:04 pm من طرف free men
http://plato.stanford.edu/new.html



Ontological Arguments (Graham Oppy) [REVISED: February 12, 2016]
 

Natural Numbers

الرجوع الى أعلى الصفحة 

صفحة 1 من اصل 1

 مواضيع مماثلة

-
»  Natural Kinds
»  From the American Museum of Natural History:
» حالة طبيعيّة (Natural State)
» Natural disasters as seen from outer space
»  Reexamination of Parallel Evolution in Diurnal Neotropical Moths Appears in Bulletin of The American Museum of Natural History

صلاحيات هذا المنتدى:تستطيع الرد على المواضيع في هذا المنتدى
** متابعات ثقافية متميزة ** Blogs al ssadh :: Pensée-
إرسال موضوع جديد   إرسال مساهمة في موضوعانتقل الى: