has, and y has every property which x has. He then derives some other "laws" from this law: II. Law of Reflexivity: Everything is equal to itself: x = x. [Proven at PM ❋13.15] III. Law of Symmetry: If x = y, then y = x. [Proven at PM ❋13.16] IV. Law of Transitivity: If x = y and y = z, then x = z. [Proven at PM ❋13.17] V. If x = z and y = z, then x = y. [Proven at PM ❋13.172] Principia Mathematica defines the notion of equality as follows (in modern symbols); note that the generalization "for all" extends over predicate-functions f( ): ❋13.01. x = y =def ∀f:(f(x) → f(y)) ("This definition states that x and y are to be called identical when every predicate function satisfied by x is satisfied by y" Hilbert 1927:467 adds only two axioms of equality, the first is x = x, the second is (x = y) → ((f(x) → f(y)); the "for all f" is missing (or implied). Gödel 1930 defines equality similarly to PM :❋13.01. Kleene 1967 adopts the two from Hilbert 1927 plus two more (Kleene 1967:387). George Spencer-Brown (1969): Laws of Form George Spencer-Brown in his 1969 "Laws of Form" (LoF) begins by first taking as given that "we cannot make an indication without drawing a distinction". This, therefore, presupposes the law of excluded middle. He then goes on to define two axioms, which describe how distinctions (a "boundary") and indications (a "call") work: Axiom 1. The law of calling: The value of a call made again is the value of the call. Axiom 2. The law of crossing: The value of a (boundary) crossing made again is not the value of the crossing. These axioms bare a resemblance to the "law of identity" and the "law of non-contradiction" respectively. However, the law of identity is proven as a theorem (Theorem 4.5 in "Laws of Form") within the framework of LoF. In general, LoF can be reinterpreted as First-order logic, propositional logic, and second-order logic by assigning specific interpretations to the symbols and values of LoF. Contemporary developments All of the above "systems of logic" are considered to be "classical" meaning propositions and predicate expressions are two-valued, with either the truth value "truth" or "falsity" but not both(Kleene 1967:8 and 83). While intuitionistic logic falls into the "classical" category, it objects to