A software architecture is the result of multiple decisions made by a software architect. These decisions are called architectural decisions, as they bring solutions to architectural problems. Relations between decisions can be captured in architectural decision models. Such models are then a form of reusable knowledge for software architects. Several models have been described in the literature, introducing necessary concepts and relations. These concepts and relations were usually explained using natural language. Not much work has been done so far on their formal definitions. Specifically, such a definition of an architectural decision model is still missing. The purpose of this paper is filling this gap by providing the formal definition of an architectural decision model at both syntax and semantics levels. At the syntax level, different concepts and relations that are elements of a model have been mathematically defined. At the semantics level, the meaning of a model has been defined in a form of denotational semantics. The formalization not only allows for better understanding of architectural decision models but opens the possibility to reason on such models, e.g., checking their consistency - something that is very limited for the models proposed so far. A practical example of the semantics of an architectural decision model is also presented.