nLab
first law of thought

Contents

Idea

In philosophy, the statement that given any AA, then AA equals AA

A=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:Typerefl A:A=A. 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).

References

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

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

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

See also

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=xx = x see