nLab first law of thought

Idea

In philosophy, the statement that given any $A$, then $A$ equals $A$

$$A = A$$

(i.e. reflexivity) has been called (see the references below) the first law of thought.

In terms of type theory this is the judgement that exhibits the term introduction for the reflector in an identity type

$$A \colon Type \;\vdash\; refl_A \;\colon A = A\; \,.$$

In fact, identity types may be regarded as inductive types generated by just this reflector (Licata 11, Shulman 12, slide 35, see there).

Related concepts

• ontology

References

In Gottfried Leibniz‘s unpublished but famous manuscript on logic (from some time in 1683-1716), reproduced in the Latin original in

• K. Gerhard (ed.), Section XIX, p. 228 in: Die philosophischen Schriften von Gottfried Wilhelm Leibniz, Siebenter Band, Weidmannsche Buchhandlung (1890) [archive.org]

and English translation in

• Clarence I. Lewis, Appendix (p. 373) of: A Survey of Symbolic Logic, University of California (1918) [pdf]

it says, after statement of the identity of indiscernibles and then the indiscernibility of identicals, that

$A$ and $A$ are, of course, said to be the same

Later,

• Johann Fichte, Grundlage der gesamten Wissenschaftslehre (1794)

calls “$A = A$” “den ersten, schlechthin unbedingent Grundsatz” hence the “absolutely imperative principle”. (In fact Fichte there highlights the importance of the antecedent $A \colon Type$ to arrive at the consequent $A = A$.)

• Georg Hegel, Science of Logic 1812,

in its §875 calls it the first original law of thought:

The first original law of thought (WdL §875): everything is identical with itself (WdL §863), no two things are like each other (WdL §903).

• Thomas Hughes, The Ideal Theory of Berkeley and the Real World, (1865) Part II, Section XV,

in Footnote, p. 38 calls it the first of the four primary laws of thought.

See also

• Wikipedia, Law of thought – Four laws,

which gives quotes by Arthur Schopenhauer to the same extent.

For the understanding of identity types as inductive types genrated just by the reflector $x = x$ see

• Dan Licata, Understanding Identity Elimination in Homotopy Type Theory, 2011

• Mike Shulman, around slide 35 of Inductive types and identity types, 2012 (pdf)