The general doctrine that all mathematics is deduction by logical principles from logical principles was strongly advocated by Leibniz, who urged constantly that axioms ought to be proved and that all except a few fundamental notions ought to be defined. But owing partly to a faulty logic, partly to a belief in the logical necessity of Euclidean Geometry, he was led into hopeless errors in the endeavour to carry out in detail a view which, in its general outline, is now known to be correct^[1]. The actual propositions of Euclid, for example, do not follow from the principles of logic alone; and the perception of this fact led Kant to his innovations in the theory of knowledge. But since the growth of non-Euclidean Geometry, it has appeared that pure mathematics has no concern with the question whether the axioms and propositions of Euclid hold of actual space or not: this is a question for applied mathematics, to be decided, so far as any decision is possible, by experiment and observation. What pure mathematics asserts is merely that the Euclidean propositions follow from the Euclidean axioms--i.e. it asserts an implication: any space which has such and such properties has also such and such other properties. Thus, as dealt with in pure mathematics, the Euclidean and non-Euclidean Geometries are equally true: in each nothing is affirmed except implications. All propositions as to what actually exists, like the space we live in, belong to experimental or empirical science, not to mathematics; when they belong to applied mathematics, they arise from giving to one or more variables in a proposition of pure mathematics some constant value satisfying the hypothesis, and thus enabling us, for that value of the variable, actually to assert both hypothesis and consequent instead of asserting merely the implication. We assert always in mathematics that if a certain assertion p is true of any entity x, or of any set of entities x, y, z, ..., then some other assertion q is true of those entities; but we do not assert either p or q separately of our entities. We assert a relation between the assertions p and q, which I shall call formal implication.(§ 5 ¶ 1)