The first millisecond of the Big Bang

ACL2 functions, e.g., if, that show enter-boot-strap-mode as their defining command are in fact primitives. It is impossible for the system to display defining axioms about these symbols.

Enter-boot-strap-mode is a Common Lisp function but not an ACL2 function. It magically creates from nil an ACL2 property list world that lets us start the boot-strapping process. That is, once enter-boot-strap-mode has created its world, it is possible to process the defconsts, defuns, and defaxioms, necessary to bring up the rest of the system. Before that world is created, the attempt by ACL2 even to translate a defun form, say, would produce an error because defun is undefined.

Several ACL2 functions show enter-boot-strap-mode as their defining command. Among them are if, cons, car, and cdr. These functions are characterized by axioms rather than definitional equations -- axioms that in most cases are built into our code and hence do not have any explicit representation among the rules and formulas in the system.