Formalization of Cost and Utility in Microeconomics

Abstract

Cost and utility modeling of economics agents based on the differential theory is fundamental to the analysis of the microeconomics models. In particular, the first and second-order derivative tests are used to specify the desired properties of the cost and utility models. Traditionally, paper-and-pencil proof methods and computer-based tools are used to investigate the mathematical properties of these models. However, these techniques do not provide an accurate analysis due to their inability to exhaustively specify and verify the mathematical properties of the cost and utility models. Additionally, these techniques cannot accurately model and analyze pure continuous behaviors of the economic agents due to the utilization of computer arithmetic. On the other hand, an accurate analysis is direly needed in many safety and cost-critical microeconomics applications, such as agriculture and smart grids. To overcome the issues pertaining to the above-mentioned techniques, in this paper, we propose a theorem proving based methodology to formally analyze and specify the mathematical properties of functions used in microeconomics modeling. The proposed methodology is primarily based on a formalization of the derivative tests and root analysis of the polynomial functions, within the sound core of the HOL-Light theorem prover. We also provide a formalization of the first-order condition, which is used to analyze the maximum of the profit function in a higher-order-logic theorem prover. We then present the formal analysis of the utility, cost and first-order condition based on the polynomial functions. To illustrate the usefulness of proposed formalization, the proposed formalization is used to formally analyze and verify the quadratic cost and utility functions, which have been used in an optimal power flow problem and demand response (DR) program, respectively.

1. Introduction

Microeconomics is the study of the economic actions of individuals (consumers) and well-defined groups of individuals (firms) [1]. The individual decision-making analysis lies at the core of the behavioral modeling in the microeconomics theory. In economics, behavioral economics [2] and rational choice theory [3] are two major approaches for modeling the choices, i.e., goods and services, of consumers and firms. In behavioral economics, the decision-making is assumed to be affected by many factors, such as cognitive capabilities, knowledge or information and preferences of a consumer or firm, whereas rational choice theory assumes the decision maker is always able to prefer and rank his given set of choices. However, the rational choice approach results in a tractable mathematical framework to conduct the analysis of the given economy and therefore is widely used to model the behavior of the underlying decision makers in microeconomics models [4]. Based on the rational choice model, consumer and firm theories are developed to analyze the consumption (demand) and production (supply) behaviors of the economy [1]. In this regard, cost and utility functions are used to quantify and analyze the affects of the decision-making by firms and consumers, respectively. Therefore, cost and utility modeling has a central role in the microeconomic analysis of an economy market.

In microeconomics, mathematical methods provide sophisticated tools to analyze the economy markets [5]. Mathematically, a cost function can be modeled using continuous, differentiable, increasing and convex function, whereas, for the utility modeling, the function should be continuous, differentiable, non-decreasing and concave [1]. In particular, differential theory allows for analytically verifying the continuity, monotonicity and convex or concave nature, using derivative tests, of a given function to model the cost and utility functions. Generally, polynomial, exponential and logarithmic function are used to model the cost and utility in microeconomics.

The cost and utility modeling allows for studying transaction prices and quantities of buyers and sellers in markets, such as electricity and agriculture. Particularly, microeconomics models and concepts have immense possibilities for applications in the energy sector [6,7], particularly in the smart grids [8], which are characterized by the information flow, along with the electric energy, and thus allow for regulating and trading electricity in the smart grid network [9,10,11,12,13,14]. In the electricity market, the cost function is used to model the cost of generating, transmitting, and distributing the electricity to end-consumers [15]. On the other hand, utility modeling plays a key role in the demand response (DR) programs [16], which are used to shape/reshape the demand of the consumers for safe and secure smart grids.

Traditional analysis techniques, such as paper-and-pencil proof methods and simulations, are used to analyze the above-mentioned properties of functions. Computer-based simulation methods are commonly employed to investigate the functional properties for many test cases. However, simulations cannot provide an exhaustive analysis due to the associated high computational cost and memory requirements. Moreover, simulation methods cannot model continuous behaviors of the cost and utility functions, due to computer-arithmetic based modeling, which results in round-off or truncation errors. Although paper-and-pencil proof methods can overcome the above-mentioned problems, these methods are prone to human error. Furthermore, the paper-and-pencil proofs are not scalable with respect to the complexity of the problem. Computer algebra systems (CAS), such as Maxima [17] and Mathematica [18], are also used to investigate the general mathematical properties of the candidate functions for the modeling and analysis of microeconomics concepts [19]. These methods are based upon symbolic manipulation and thus involve large and unverified computer-language programs. Therefore, the analysis performed using CAS cannot be guaranteed to be 100% accurate as well [20]. Moreover, the above-mentioned computer aided techniques allow for verifying the behavior or properties of a given function over the user specified domain intervals only, and, therefore, cannot ensure exhaustive verification over the complete domain of the given function. For example, a simple cubic polynomial function may behave as a convex or a concave function depending upon the specified domain. The above-mentioned shortcomings of traditional techniques can lead to inaccurate analysis results, which in turn may result in unbearable financial or human life loss especially in the case of mission or safety-critical microeconomics’ applications, such as the electricity market. In order to overcome these limitations, we propose to use theorem proving for the formal analysis of systems relying on the fundamental microeconomics concepts.

Formal methods are computer based techniques to formally specify, verify and analyze hardware and software systems [21]. These techniques use logic to express the system model, in a computer-based language, to formally verify and validate the properties of the system based on deductive reasoning. The use of mathematical logic in this process leads to the soundness and rigor for specifying and verifying the properties of the given system model.

Formal methods can be primarily classified as model checking and theorem proving techniques. Model checking allows for modeling the behavior of the system as a state transition system and the system properties are expressed in temporal logic [22]. However, the technique cannot be used to express continuous models due to its state-based nature. Moreover, it is prone to the state-space explosion problem for extremely large state-space systems. Therefore, model checking cannot be used to verify the properties of the cost and utility functions because of their continuous nature. On the other hand, theorem proving utilizes logic to model the system and its properties and the relationship is verified either automatically or interactively based on the decidability of the underlying logic. However, automatic theorem proving cannot be used to model and verify the continuous behavior of the cost and utility functions, as these details cannot be captured by the decidable propositional or semi-decidable first-order logic, whereas interactive theorem proving [23] uses highly expressive higher-order logic for the purpose of modeling, analysis, and verification of the given system and therefore is capable of analyzing the continuous aspects pertaining to the functions used in the mathematical behavioral modeling in microeconomics. Therefore, we propose to use the interactive theorem proving to formalize the behavioral modeling in microeconomics.

Formal methods techniques have been widely adopted for the formal analysis and verification in the energy sector [24]. Markovian models of smart grid components, along with back-up protection, are proposed for the reliability assessment using a PRISM model checker [25]. In [26], smart grid components are formally specified using Z formal specification language. Formal verification of smart grid applications based on distributed intelligence has been conducted using the symbolic model verifier (SMV) model checker [27]. In theorem proving, a degradation strategy is formalized as a satisfiability modulo theories (SMT) problem and analyzed using the Z3 SMT-solver [28]. Petri-nets have also been employed to formally analyze the reliability [29], cost reduction [30], failure detection [31], performance [32,33], and possible security breaches [34] in smart grids. To the best of our knowledge, microeconomics concepts have never been formalized using theorem proving, which are essential to formally analyze the economy of the electricity markets.

In microeconomic studies, differential and convex theories are central mathematical concepts which are used for the behavioral modeling. Many interactive theorem provers, such as HOL-Light [35], HOL4 [36], and Isabelle [37], support the differential analysis; however, besides multivariate differential theory, HOL-Light provides extensive support for convex analysis. In addition to the convex theory, HOL-Light theorem prover is endowed with the root analysis for polynomials up to the fourth order [38], which is the foremost requirement to conduct the formal analysis of the first-order condition based upon the polynomial type of the mathematical functions. Therefore, in this paper, we utilize the HOL-Light theorem prover to formalize the mathematical behavioral modeling and property verification of the these models.

The primary objective of this paper is to develop a logical framework for the behavioral modeling in microeconomics. The logical framework enables formally specifying and reasoning about the cost, utility, and first-order condition models within the sound core of the HOL-Light theorem prover. A formal analysis of these models in higher-order logic results in the certified and mechanized formal proofs of given models. As a case study, we provide the formal modeling and analysis of the behavioral modeling in the electricity market based upon the polynomial functions, up to the fourth order. The formally verified results, for the behavioral modeling of electricity market, provide necessary conditions on the functions to accurately model the cost, utility and first-order condition. Finally, we utilize this behavioral modeling to formally verify the applications of cost, utility and profit–maximization models in economic dispatch and dynamic-pricing problems in the electricity market.

The rest of the paper is organized as follows: Section 2 describes some preliminaries related to mathematical modeling in microeconomics, HOL-Light theorem prover, and related formalization that are essential for the understanding of the rest of the paper. Section 3 presents the proposed methodology and, based on this, Section 4 provides the formalization of second-order derivative test for strict convexity or concavity, cost, utility, and first-order condition models in higher-order-logic theorem prover. Section 5 utilizes the basic logical framework to formally specify and verify the mathematical behavioral modeling in DR programs for a polynomial type of modeling functions. Finally, Section 6 concludes the paper.

2. Mathematical Modeling in Microeconomics

Generally, any continuous, differentiable, non-decreasing and concave or strictly concave function can be used to model the utility function, i.e., satisfaction or happiness of a consumer for consuming the goods or services. The continuity and differentiability ensure that consumer preferences to consume goods and services never vanish abruptly. The non-decreasing property ensures that the preferences of a consumer are rational, whereas rationality further imposes conditions such as completeness and transitivity. The rationality assumption ensures that the consumer is always able to prefer each and every good or service, and can rank his preference of goods or services. On the other hand, concavity or strict concavity is due to the law of diminishing marginal utility, which states that every extra unit of consumption leads to a reduced satisfaction or happiness for the consumer.

Similarly, a continuous, differentiable, increasing and convex or strict convex function can be used to model the cost function, i.e., total cost accrued in producing a unit of goods or services. The product theory models the production of goods or services by using a product set, which contains all possible feasible plans for the production process. To model a given production process, it is assumed that the product set satisfies certain properties, e.g., non-emptiness, convexity, and non-decreasing returns to scale e.t.c. These assumptions mainly relate the input and output of the feasible production process. Consequently, the assumptions on the relationship between inputs and outputs are translated to the aforementioned mathematical properties of the cost function. For example, the monotonicity and convexity properties are based on the assumptions of convex technology and ensure the marginal non-decreasing returns with respect to the production of goods or services, whereas continuity and differentiability ensure the existence of the solution for the cost minimization problem and also allow for expressing the concepts of average and marginal costs using the total cost function.

Microeconomics modeling is primarily based upon the mathematical theories of continuity, differentiation, and convexity. Specifically, derivative tests involving first-order and second-order derivatives are fundamental in assessing the monotonicity and convexity or concavity of a given function [39]. The first-order derivative of any given function is used to investigate the increasing or decreasing behavior of the given function, i.e., monotonicity. Moreover, the first-order derivative of functions are also used to find the stationary or critical points, i.e.,

$$\frac{df(x)}{dx}=0.$$

(1)

Equation (1) is also known as the first-order condition and is used for the analysis of the profit–maximization problem in microeconomics [1], whereas the second-order derivative is used to test the convexity or concavity, which are the most desired properties of the functions to qualify for the modeling of the cost and utility. For a convex function, the second-order derivative test is non-negative, i.e.,

$$0\le \frac{d^{2}f(x)}{d{x}^2}.$$

(2)

On the contrary, the second-order derivative is negative for a concave function. Strict-convex and concave functions have positive and negative derivatives, respectively, but the corresponding converse relationships are not true. The derivative tests for the strict-convexity and concavity are formally stated as implications, i.e.,

$$\begin{array}{c}\hfill \mathit{strict-convexity}\Rightarrow 0<\frac{d^{2}f(x)}{d{x}^2}.\end{array}$$

(3a)

$$\begin{array}{c}\hfill \mathit{strict-convcavity}\Rightarrow \frac{d^{2}f(x)}{d{x}^2}<0.\end{array}$$

(3b)

Therefore, the derivative tests play a vital role in specifying the mathematical properties of the modeling functions in microeconomics.

3. Foundational Formalization for Microeconomics Models

This section provides a brief introduction to the HOL-Light theorem prover and its formalization of real convex and polynomial root analysis theories to facilitate the understanding of the rest of the paper.

3.1. HOL-Light Theorem Prover

HOL-Light [35] is an interactive theorem prover that allows its users to develop new mechanized theories, proofs, and inference rules with the support of many automated tools and pre-proved mathematical theories, such as arithmetic, set, and real theories. It has been widely-used for some significant industrial-scale verification applications [40,41].

A variant of the strongly typed functional programming language, i.e., Objective CAML (OCaml), is used to implement higher-order logic in the HOL-Light theorem prover. HOL-Light provides a secure and sound platform for the formal verification and specification of the systems. Sound theorem proving is ensured by the small core that consists of only 1500 lines, including 10 primitive inference rules, such as modus ponens and reflexivity, whereas soundness is ascertained due to the convergence of all the mechanized proofs to these inference rules. HOL-Light supports backward and forward proof strategies. In the backward proof strategy, a theorem is formally verified using inference rules, whereas, in the forward proof strategy, the given theorem is broken down into subgoals using HOL-Light tactics. A tactic is a special ML function used to divide the main goal into subgoals.

We used the HOL-Light theorem prover for the proposed work as it is endowed with the library of the real convex theory and polynomial root analysis to facilitate the formalization of the mathematical modeling of the DR programs.

Table 1. HOL-Light symbols and functions.

HOL Symbol	Standard Symbol	Meaning
∧	$and$	Logical $and$
∨	$or$	Logical $or$
¬	$not$	Logical $negation$
∀	$forall$	Universal quantifier
∃	$thereexists$	Existential quantifier
$\lambda \mathtt{x}.\mathtt{t}$	$\lambda x.t$	Function that maps x to $t(x)$
$\mathtt{real}$	All Real numbers	Real data type
$\mathtt{x}\mathtt{pow}\mathtt{n}$	$x^n$	Power with integer exponent

presents some of the frequently used HOL-Light functions and symbols in this paper to facilitate the understanding of the formalization and verification.

3.2. Real Convex Analysis Theory

The multivariate real analysis theory of the HOL-Light supports the convex analysis for real-valued functions. This theory, in conjunction with multivariate differential and integral theories, provides support for the convex analysis of the real-valued functions. In particular, the theory can be used to conduct the second-order derivative test to determine the convexity of the given function, which in turn is utilized for the formalization and verification of the utility function in this paper.

A real convex function is defined in higher-order logic as:

Definition 1.

Real convex function

⊢∀ s f. f real_convex_on s = (∀ x y u v. x ∈ s ∧ y ∈ s ∧ &0 ≤ u ∧ &0 ≤ v ∧ u + v = &1 ⇒ f (u ∗ x + v ∗ y) ≤ u ∗ f x + v ∗ f y).

In Definition 1, real_convex_on is a higher-order-logic function that accepts a real-valued function, f:$\mathtt{real}$→$\mathtt{real}$, defined over an interval s:$\mathtt{real}$→$\mathtt{bool}$, whereas s is a set theoretic definition of the real interval that represents all subintervals possible for a given real interval. The function is convex if for any two points x and y, within the real interval s, the value of the function f ( u ∗ x + u ∗ y) lies below the line segment defined by the function values at f(x) and f(y). The variables u and v, of $\mathtt{real}$ data type, together provide all possible lines for the graph of the function between f(x) and f(y).

The second-order derivative test is widely used to analytically verify the convexity or concavity of a given function. The second-order test for the convexity of a function, i.e., Equation (2), has been verified in multivariate real analysis theory as:

Theorem 1.

Second-order derivative of real convex function

⊢∀ $\mathtt{f}$ ${\mathtt{f}}^{\prime }$ ${\mathtt{f}}^{″}$ $\mathtt{s}$.

• A1: ¬(∃$\mathtt{a}$.$\mathtt{s}$ $=$ $\left\{\mathtt{a}\right\}$) ∧
• A2: (∀ $\mathtt{x}$. $\mathtt{x}$ ∈ $\mathtt{s}$ ⇒($\mathtt{f}$ $\mathtt{has}\_\mathtt{vector}\_\mathtt{derivative}$ ${\mathtt{f}}^{\prime }$ $\mathtt{x}$)($\mathtt{atreal}$ $\mathtt{x}$ $\mathtt{within}$ $\mathtt{x}$))
• A3: (∀ $\mathtt{x}$. $\mathtt{x}$∈$\mathtt{s}$⇒(${\mathtt{f}}^{\prime }$ $\mathtt{has}\_\mathtt{vector}\_\mathtt{derivative}$ ${\mathtt{f}}^{″}$ $\mathtt{x}$)($\mathtt{atreal}$ $\mathtt{x}$ $\mathtt{within}$ $\mathtt{x}$))
         ⇒$\mathtt{f}$ $\mathtt{real}\_\mathtt{convex}\_\mathtt{on}$ $\mathtt{s}$=(∀ $\mathtt{x}.$ $\mathtt{x}$∈$\mathtt{s}$⇒&$\mathtt{0}$≤${\mathtt{f}}^{″}$)

In the above theorem, $\mathtt{f}$, ${\mathtt{f}}^{\prime }$, and ${\mathtt{f}}^{″}$ represent a real-valued function, and its first-order and second-order derivatives, respectively, defined over an arbitrary interval, s. Assumption A1 excludes all real subintervals, of a given interval, with a single element to satisfy the differentiability of the given function subject to the open intervals. Assumptions A2 and A3 ensure that the first-order and second-order derivatives of the given function exist within the given interval $\mathtt{s}$, whereas $\mathtt{has}\_\mathtt{vector}\_\mathtt{derivative}$ is the definition of the real derivative in HOL-Light in the relational form. Finally, the theorem concludes the equivalence of the convexity of a given function and its positive second-order derivative, i.e., $\mathtt{0}$ ≤ ${\mathtt{f}}^{″}$.

In this paper, Definition 1 and Theorem 1 are utilized to formally model and reason about the convexity and concavity properties of the mathematical functions in microeconomics.

3.3. Root Analysis Theory

We have already developed formal reasoning support for the formal root analysis for the polynomials up to fourth order [38]. This formal analysis allows finding zeros of the polynomial functions and further provides an exhaustive set of assumption for the stable roots of the polynomials.

The roots of the second order polynomial are formally verified as:

Theorem 2.

Quadratic Roots

⊢∀ $\mathtt{a}$ $\mathtt{b}$ $\mathtt{c}$ $\mathtt{x}$.

       A1: $\mathtt{a}$ ≠ $\mathtt{0}$

    ⇒$\mathtt{Cx}\mathtt{a}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{2}$ $+$ $\mathtt{Cx}\mathtt{b}$ $\ast$ $\mathtt{x}$ $+$ $\mathtt{Cx}\mathtt{c}$ $=\mathtt{Cx}\mathtt{0}$

     $\mathtt{x}$ = $\frac{-\mathtt{Cx}\mathtt{b}+\sqrt{\mathtt{Cx}\mathtt{b}\mathtt{pow}\mathtt{2}-\mathtt{Cx}\mathtt{4}\ast \mathtt{Cx}\mathtt{a}\ast \mathtt{Cx}\mathtt{c}}}{\mathtt{Cx}\mathtt{2}\ast \mathtt{Cx}\mathtt{a}}$∨

     $\mathtt{x}$ = $\frac{-\mathtt{Cx}\mathtt{b}-\sqrt{\mathtt{Cx}\mathtt{b}\mathtt{pow}\mathtt{2}-\mathtt{Cx}\mathtt{4}\ast \mathtt{Cx}\mathtt{a}\ast \mathtt{Cx}\mathtt{c}}}{\mathtt{Cx}\mathtt{2}\ast \mathtt{Cx}\mathtt{a}}$

In the above theorem, the variables $\mathtt{a}$, $\mathtt{b}$, and $\mathtt{c}$ represent real coefficients, whereas $\mathtt{x}$ is a complex variable. Assumption A1 ensures that the order of the polynomial is 2 as it can be reduced if the leading term coefficient is zero. The conclusion of the theorem formally verifies the two roots of the quadratic polynomial, whereas Cx is a higher-order-logic function, which maps a real number into an equivalent complex number.

The polynomials of higher-order are formally verified by factorizing them into linear and quadratic factors and then utilizing the above theorem on the factored polynomials for the verification of their roots. The factorization of cubic and quartic polynomial are verified as:

Theorem 3.

Cubic Factors

⊢∀ $\mathtt{a}$ $\mathtt{b}\mathtt{1}$ $\mathtt{c}\mathtt{1}$ $\mathtt{d}\mathtt{1}$ $\mathtt{r}$ $\mathtt{x}$.

       A1: $\mathtt{Cx}\mathtt{b}$ = $\mathtt{Cx}\mathtt{b}\mathtt{1}$ + $\mathtt{Cx}\mathtt{a}$ ∗ $\mathtt{Cx}\mathtt{r}$∧

       A2: $\mathtt{Cx}\mathtt{c}$ = $\mathtt{Cx}\mathtt{c}\mathtt{1}$ + $\mathtt{Cx}\mathtt{b}\mathtt{1}$ ∗ $\mathtt{Cx}\mathtt{r}$

       A3: $\mathtt{Cx}\mathtt{d}$ = $\mathtt{Cx}\mathtt{c}\mathtt{1}$ ∗ $\mathtt{Cx}\mathtt{r}$∧

     ⇒ $\mathtt{Cx}\mathtt{a}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{3}$ $+$ $\mathtt{Cx}\mathtt{b}$ $\ast$ $\mathtt{xpow}\mathtt{2}$ $+$ $\mathtt{Cx}\mathtt{c}$ $\ast$ $\mathtt{x}$ $+$ $\mathtt{Cx}\mathtt{d}$=

        $(\mathtt{x}$ $+$ $\mathtt{Cx}\mathtt{r})$ ∗ $(\mathtt{Cx}\mathtt{a}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{2}$ $+$ $\mathtt{Cx}\mathtt{b}\mathtt{1}$ $\ast$ $\mathtt{x}$ $+$ $\mathtt{Cx}\mathtt{c}\mathtt{1}).$

In the above theorem, $\mathtt{a}$, $\mathtt{b}\mathtt{1}$, $\mathtt{c}\mathtt{1}$, and $\mathtt{r}$ are real coefficients corresponding to the linear and quadratic factors of the cubic polynomial. Assumptions A1–A3 relate the coefficients of the cubic polynomial to its factored polynomials, whereas $\mathtt{x}$ is a complex variable. The conclusion formally verifies the factorization of the cubic polynomial for the given coefficients.

Theorem 4.

Quartic Factors

⊢∀ $\mathtt{a}\mathtt{1}$ $\mathtt{b}\mathtt{1}$ $\mathtt{c}\mathtt{1}$ $\mathtt{a}\mathtt{2}$ $\mathtt{b}\mathtt{2}$ $\mathtt{c}\mathtt{2}$ $\mathtt{x}$.

       A1: $\mathtt{Cx}\mathtt{a}$ = $\mathtt{Cx}\mathtt{a}\mathtt{1}$ ∗ $\mathtt{Cx}\mathtt{a}\mathtt{2}$∧

       A2: $\mathtt{Cx}\mathtt{b}$ = $\mathtt{Cx}\mathtt{a}\mathtt{1}$ ∗ $\mathtt{Cx}\mathtt{b}\mathtt{2}$ + $\mathtt{Cx}\mathtt{a}\mathtt{2}$ ∗ $\mathtt{Cx}\mathtt{b}\mathtt{1}$∧

       A3: $\mathtt{Cx}\mathtt{c}$ = $\mathtt{Cx}\mathtt{a}\mathtt{1}$ ∗ $\mathtt{Cx}\mathtt{c}\mathtt{2}$ + $\mathtt{Cx}\mathtt{b}\mathtt{1}$ ∗ $\mathtt{Cx}\mathtt{b}\mathtt{2}$ + $\mathtt{Cx}\mathtt{a}\mathtt{2}$ ∗ $\mathtt{Cx}\mathtt{c}\mathtt{1}$∧

       A4: $\mathtt{Cx}\mathtt{d}$ = $\mathtt{Cx}\mathtt{b}\mathtt{1}$ ∗ $\mathtt{Cx}\mathtt{c}\mathtt{2}$ + $\mathtt{Cx}\mathtt{b}\mathtt{2}$ ∗ $\mathtt{Cx}\mathtt{c}\mathtt{1}$∧

       A5: $\mathtt{Cx}\mathtt{e}$ = $\mathtt{Cx}\mathtt{c}\mathtt{1}$ ∗ $\mathtt{Cx}\mathtt{c}\mathtt{2}$

  ⇒$(\mathtt{Cx}\mathtt{a}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{4}$ $+$ $\mathtt{Cx}\mathtt{b}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{3}$ $+$ $\mathtt{Cx}\mathtt{c}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{2}$ $+$ $\mathtt{Cx}\mathtt{d}$ $\ast$ $\mathtt{x}$

    $+$ $\mathtt{Cx}\mathtt{e}$)=

    $($ $(\mathtt{Cx}\mathtt{a}\mathtt{1}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{2}$ $+$ $\mathtt{Cx}\mathtt{b}\mathtt{1}$ $\ast$ $\mathtt{x}$ $+$ $\mathtt{Cx}\mathtt{c}\mathtt{1})$ $\ast$

     $(\mathtt{Cx}\mathtt{a}\mathtt{2}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{2}$ $+$ $\mathtt{Cx}\mathtt{b}\mathtt{2}$ $\ast$ $\mathtt{x}$ $+$ $\mathtt{Cx}\mathtt{c}\mathtt{2})$ $)$

In the above theorem, $\mathtt{a}\mathtt{1}$, $\mathtt{b}\mathtt{1}$, $\mathtt{c}\mathtt{1}$, $\mathtt{a}\mathtt{2}$, $\mathtt{b}\mathtt{2}$, and $\mathtt{c}\mathtt{2}$ are real coefficients corresponding to the two quadratic factors of the quartic polynomial. Based on the Assumptions A1–A5, Theorem 4 verifies the factorization of the given quartic polynomial.

The cubic and quartic polynomial roots are formally verified as:

Theorem 5.

Cubic Roots

⊢∀ $\mathtt{a}$ $\mathtt{b}\mathtt{1}$ $\mathtt{c}\mathtt{1}$ $\mathtt{d}\mathtt{1}$ $\mathtt{r}$ $\mathtt{x}$.

    A1: $\mathtt{a}$ ≠ $\mathtt{0}$∧

    A2: $\mathtt{Cx}\mathtt{b}$ = $\mathtt{Cx}\mathtt{b}\mathtt{1}$ + $\mathtt{Cx}\mathtt{a}$ ∗ $\mathtt{Cx}\mathtt{r}$∧

    A3: $\mathtt{Cx}\mathtt{c}$ = $\mathtt{Cx}\mathtt{c}\mathtt{1}$ + $\mathtt{Cx}\mathtt{b}\mathtt{1}$ ∗ $\mathtt{Cx}\mathtt{r}$∧

    A4: $\mathtt{Cx}\mathtt{d}$ = $\mathtt{Cx}\mathtt{c}\mathtt{1}$ ∗ $\mathtt{Cx}\mathtt{r}$

 ⇒$(\mathtt{Cx}\mathtt{a}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{3}$ $+$ $\mathtt{Cx}\mathtt{b}$ $\ast$ $\mathtt{xpow}\mathtt{2}$ $+$ $\mathtt{Cx}\mathtt{c}$ $\ast$ $\mathtt{x}$ $+$ $\mathtt{Cx}\mathtt{d}$ = $\mathtt{Cx}$ $\mathtt{0})$

   = $($ $\mathtt{x}$ = $\mathtt{Cx}\mathtt{r}$ ∨ $\mathtt{x}$ = $\frac{-\mathtt{Cx}\mathtt{b}\mathtt{1}+\sqrt{\mathtt{Cx}\mathtt{b}\mathtt{1}\mathtt{pow}\mathtt{2}-\mathtt{Cx}\mathtt{4}\ast \mathtt{Cx}\mathtt{a}\ast \mathtt{Cx}\mathtt{c}\mathtt{1}}}{\mathtt{Cx}\mathtt{2}\ast \mathtt{Cx}\mathtt{a}}$∨

            $\mathtt{x}$ = $\frac{-\mathtt{Cx}\mathtt{b}\mathtt{1}-\sqrt{\mathtt{Cx}\mathtt{b}\mathtt{1}\mathtt{pow}\mathtt{2}-\mathtt{Cx}\mathtt{4}\ast \mathtt{Cx}\mathtt{a}\ast \mathtt{Cx}\mathtt{c}\mathtt{1}}}{\mathtt{Cx}\mathtt{2}\ast \mathtt{Cx}\mathtt{a}}$ $)$

In the above theorem, Assumption A1 ensures that the order of the given polynomial is 3. Assumptions A2–A4 provide the relationship between the coefficients of the cubic polynomial and their factors. The theorem gives formally verified results for the three roots of a cubic polynomial. Similarly, the roots of the fourth order polynomial are formally verified as:

Theorem 6.

Quartic Roots

⊢∀ $\mathtt{a}\mathtt{1}$ $\mathtt{b}\mathtt{1}$ $\mathtt{c}\mathtt{1}$ $\mathtt{a}\mathtt{2}$ $\mathtt{b}\mathtt{2}$ $\mathtt{c}\mathtt{2}$ $\mathtt{x}$.

  A1: $\mathtt{a}$ ≠ $\mathtt{0}$ ∧ A2:$\mathtt{Cx}\mathtt{a}$ = $\mathtt{Cx}\mathtt{a}\mathtt{1}$ ∗ $\mathtt{Cx}\mathtt{a}\mathtt{2}$∧

  A3: $\mathtt{Cx}\mathtt{b}$ = $\mathtt{Cx}\mathtt{a}\mathtt{1}$ ∗ $\mathtt{Cx}\mathtt{b}\mathtt{2}$ + $\mathtt{Cx}\mathtt{a}\mathtt{2}$ ∗ $\mathtt{Cx}\mathtt{b}\mathtt{1}$∧

  A4: $\mathtt{Cx}\mathtt{c}$ = $\mathtt{Cx}\mathtt{a}\mathtt{1}$ ∗ $\mathtt{Cx}\mathtt{c}\mathtt{2}$ + $\mathtt{Cx}\mathtt{b}\mathtt{1}$ ∗ $\mathtt{Cx}\mathtt{b}\mathtt{2}$ + $\mathtt{Cx}\mathtt{a}\mathtt{2}$ ∗ $\mathtt{Cx}\mathtt{c}\mathtt{1}$∧

  A5: $\mathtt{Cx}\mathtt{d}$ = $\mathtt{Cx}\mathtt{b}\mathtt{1}$ ∗ $\mathtt{Cx}\mathtt{c}\mathtt{2}$ + $\mathtt{Cx}\mathtt{b}\mathtt{2}$ ∗ $\mathtt{Cx}\mathtt{c}\mathtt{1}$∧

  A6: $\mathtt{Cx}\mathtt{e}$ = $\mathtt{Cx}\mathtt{c}\mathtt{1}$ ∗ $\mathtt{Cx}\mathtt{c}\mathtt{2}$

  ⇒$(\mathtt{Cx}\mathtt{a}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{4}$ $+$ $\mathtt{Cx}\mathtt{b}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{3}$ $+$ $\mathtt{Cx}\mathtt{c}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{2}$ $+$ $\mathtt{Cx}\mathtt{d}$ $\ast$ $\mathtt{x}$

    $+$ $\mathtt{Cx}\mathtt{e}$ = $\mathtt{Cx}\mathtt{0})$=

    $($ $\mathtt{x}$ = $\frac{-\mathtt{Cx}\mathtt{b}\mathtt{1}+\sqrt{\mathtt{Cx}\mathtt{b}\mathtt{1}\mathtt{pow}\mathtt{2}-\mathtt{Cx}\mathtt{4}\ast \mathtt{Cx}\mathtt{a}\mathtt{1}\ast \mathtt{Cx}\mathtt{c}\mathtt{1}}}{\mathtt{Cx}\mathtt{2}\ast \mathtt{Cx}\mathtt{a}\mathtt{1}}$∨

              $\mathtt{x}$ = $\frac{-\mathtt{Cx}\mathtt{b}\mathtt{1}-\sqrt{\mathtt{Cx}\mathtt{b}\mathtt{1}\mathtt{pow}\mathtt{2}-\mathtt{Cx}\mathtt{4}\ast \mathtt{Cx}\mathtt{a}\mathtt{1}\ast \mathtt{Cx}\mathtt{c}\mathtt{1}}}{\mathtt{Cx}\mathtt{2}\ast \mathtt{Cx}\mathtt{a}\mathtt{1}}$∨

    $\mathtt{x}$ = $\frac{-\mathtt{Cx}\mathtt{b}\mathtt{2}+\sqrt{\mathtt{Cx}\mathtt{b}\mathtt{2}\mathtt{pow}\mathtt{2}-\mathtt{Cx}\mathtt{4}\ast \mathtt{Cx}\mathtt{a}\mathtt{2}\ast \mathtt{Cx}\mathtt{c}\mathtt{2}}}{\mathtt{Cx}\mathtt{2}\ast \mathtt{Cx}\mathtt{a}\mathtt{2}}$∨

              $\mathtt{x}$ = $\frac{-\mathtt{Cx}\mathtt{b}\mathtt{2}-\sqrt{\mathtt{Cx}\mathtt{b}\mathtt{2}\mathtt{pow}\mathtt{2}-\mathtt{Cx}\mathtt{4}\ast \mathtt{Cx}\mathtt{a}\mathtt{2}\ast \mathtt{Cx}\mathtt{c}\mathtt{2}}}{\mathtt{Cx}\mathtt{2}\ast \mathtt{Cx}\mathtt{a}\mathtt{2}}$ $)$

In this paper, Theorems 2–6 are used to formally analyze the first and second-order derivatives of the cost, utility and first-order condition formal models.

Definition 1 and Theorems 1–6 provide support for the property verification of the cost and utility modeling in the HOL-Light theorem prover. Definition 1 allows for formally verifying the convexity or concavity of a given function, whereas Theorems 1–6 facilitate conducting formal algebraic manipulation in verifying maxima, minima or the inflection points of the given function using derivative tests, i.e., Equations (1)–(3), in higher-order logic theorem proving. However, the framework does not support the formal analysis of the strict convexity or concavity that is presented in Section 5.

4. Proposed Methodology

In this section, we present the main steps of the proposed methodology, shown in Figure 1, for conducting the formal modeling and analysis of cost, utility functions for consumers or firms and first-order condition for profit maximization problems.

• As a first step, we formally model a real strict convex or concave function in higher-order logic. Then, we formally conduct the second-order derivative test to formally determine the strict convexity or concavity of a real function. The results are formally verified using the formal model of the strictly convex function, differential, convex and real analysis theories of HOL-Light.
• In the second step, the above-mentioned formalization is used to formally model the cost and utility functions in higher-order logic. We also formally model the first-order condition for profit maximization problems using differential theory of HOL-Light. These formalizations allow us to formally reason and verify the properties of the given functions within the sound core of HOL-Light theorem prover.
• Finally, we utilize the formalization from Steps 1 and 2 to formally verify the cost, utility, and first-order condition modeling based on the polynomial functions. We use the formalization to formally verify the behavioral modeling employed in the electricity market, for electricity dispatch and DR economic problems.

5. Formalization of Microeconomics Concepts

In this section, we present a higher-order-logic formalization of the second-order derivative test for the strict convexity or concavity of a real function. These formally verified results are further employed to formally model the cost and utility functions in microeconomics. We also present formal modeling of the first-order condition in the HOL-Light theorem prover.

Formalization of Strict-Convexity and Concavity

We formally define a real strict convex function in HOL-Light as:

Definition 2.

Real strict convex function

⊢∀ s f. f real_strict_convex_on s = (∀ x y u v. x ∈ s ∧ y ∈ s ∧ &0 < u ∧ &0 < v ∧ u + v < &1 ⇒ f (u ∗ x + v ∗ y) < u ∗ f x + v ∗ f y).

In the above definition, f:$\mathtt{real}$→$\mathtt{real}$ represents a real function and s:$\mathtt{real}$→$\mathtt{bool}$ represents a real interval. The above definition differs from Definition 1 by a strict inequality.

Based on Definition 2, we formally verify the scalar multiplication and addition of the two strictly convex functions in HOL-Light, as:

Lemma 1.

constant multiplier property

⊢∀ $\mathtt{f}$ $\mathtt{s}$ $\mathtt{c}$.

       A1: $\mathtt{0}$ < $\mathtt{c}$ ∧ A2:$\mathtt{f}$$\mathtt{real}\_\mathtt{strict}\_\mathtt{convex}\_\mathtt{on}$$\mathtt{s}$

    ⇒($\lambda$ $\mathtt{x}$.$\mathtt{c}$ ∗ $\mathtt{f}$ $\mathtt{x}$ $\mathtt{real}\_\mathtt{strict}\_\mathtt{convex}\_\mathtt{on}$ $\mathtt{s}$ $).$

In the above lemma, Assumptions A1–A2 ensure that the constant multiplier is positive and the given function is strictly convex. Under these conditions, the multiplication does not affect the strict convexity of the given function.

Similarly, we formally verify that the addition of the two strict convex functions results in a real strict convex behavior as:

Lemma 2.

Addition property

⊢∀ $\mathtt{f}$ $\mathtt{s}$ $\mathtt{g}$.

  A1: $\mathtt{f}$$\mathtt{real}\_\mathtt{strict}\_\mathtt{convex}\_\mathtt{on}$$\mathtt{s}$       A2:$\mathtt{g}$$\mathtt{real}\_\mathtt{strict}\_\mathtt{convex}\_\mathtt{on}$$\mathtt{s}$

    ⇒($\lambda$ $\mathtt{x}$.$\mathtt{f}$ $\mathtt{x}$ + $\mathtt{g}$ $\mathtt{x}$ $\mathtt{real}\_\mathtt{strict}\_\mathtt{convex}\_\mathtt{on}$ $\mathtt{s}$)

Now, we formally verify the second-order derivative test for the real strict functions, i.e., Equation (3a), in HOL-Light, as:

Theorem 7.

Second-order derivative for real strict convex function

⊢∀ $\mathtt{f}$ ${\mathtt{f}}^{\prime }$ ${\mathtt{f}}^{″}$ $\mathtt{s}$.

    A1: ¬(∃$\mathtt{a}$.$\mathtt{s}$ $=$ $\left\{\mathtt{a}\right\}$) ∧

    A2: (∀ $\mathtt{x}$. $\mathtt{x}$∈$\mathtt{s}$⇒($\mathtt{f}$ $\mathtt{has}\_\mathtt{vector}\_\mathtt{derivative}$ ${\mathtt{f}}^{\prime }$ $\mathtt{x}$)($\mathtt{atreal}$ $\mathtt{x}$ $\mathtt{within}$ $\mathtt{x}$))

    A3: (∀ $\mathtt{x}$. $\mathtt{x}$∈$\mathtt{s}$⇒(${\mathtt{f}}^{\prime }$ $\mathtt{has}\_\mathtt{vector}\_\mathtt{derivative}$ ${\mathtt{f}}^{″}$ $\mathtt{x}$)($\mathtt{atreal}$ $\mathtt{x}$ $\mathtt{within}$ $\mathtt{x}$))

    A4: $\mathtt{f}$$\mathtt{real}\_\mathtt{strict}\_\mathtt{convex}\_\mathtt{on}$$\mathtt{s}$

    ⇒(${\mathtt{f}}^{″}<\mathtt{0}$)

The above theorem is verified using the mean-value theorem along with the definition of the strict convexity. Assumptions A2–A3 ensure that the function is twice differentiable over the given interval and Assumption A4 ensures that the function is strictly convex. The conclusion of the theorem formally verifies that the second-derivative of the function is positive.

We utilize the strict convexity formalization to formally verify the strict concavity of any given function. It is possible due to the mathematical relationship between two concepts, i.e., the negative of a strictly convex function is strictly concave. The second order derivative test for strict concavity, i.e., Equation (3b), is verified in HOL-Light, as:

Theorem 8.

Second-order derivative for real strict concave function

⊢∀ $\mathtt{f}$ ${\mathtt{f}}^{\prime }$ ${\mathtt{f}}^{″}$ $\mathtt{s}$.

  A1: ¬(∃$\mathtt{a}$.$\mathtt{s}$ $=$ $\left\{\mathtt{a}\right\}$) ∧

  A2: (∀ $\mathtt{x}$. $\mathtt{x}$∈$\mathtt{s}$⇒($\mathtt{f}$ $\mathtt{has}\_\mathtt{vector}\_\mathtt{derivative}$ ${\mathtt{f}}^{\prime }$ $\mathtt{x}$)($\mathtt{atreal}$ $\mathtt{x}$ $\mathtt{within}$ $\mathtt{x}$))

  A3: (∀ $\mathtt{x}$. $\mathtt{x}$∈$\mathtt{s}$⇒(${\mathtt{f}}^{\prime }$ $\mathtt{has}\_\mathtt{vector}\_\mathtt{derivative}$ ${\mathtt{f}}^{″}$ $\mathtt{x}$)($\mathtt{atreal}$ $\mathtt{x}$ $\mathtt{within}$ $\mathtt{x}$))

  A4: $-\mathtt{f}$$\mathtt{real}\_\mathtt{strict}\_\mathtt{convex}\_\mathtt{on}$$\mathtt{s}$

    ⇒(${\mathtt{f}}^{″}<\mathtt{0}$)

Theorem 8 is formally verified by using the definition of the strict convexity and second-order derivative in HOL-Light. In Assumption A4, we utilize the mathematical relationship between the strict convex and strict concave functions, i.e., the negative of a strict convex function is a strict concave function. The conclusion is the formally verified result for the second-order derivative of the given strictly concave function, i.e., second-order derivative of a strictly concave function is negative. We adopted a similar approach for verifying the variants of Lemmas 1 and 2 for strictly concave functions in our formalization.

Now, we formally model the mathematical properties, i.e., continuity, differentiability, monotonicity and convexity or concavity, of the cost and utility functions in HOL-Light. The cost function is modeled in higher-order logic as:

Definition 3.

Convex Cost function

⊢∀ f x.convex_cost_func f s x =

( f real_continuous_on s ) ∧ ( f real_differentiable_on s ) ∧

 ( ∀ x y. ( x ∈ s ) ∧ ( y ∈ s ) ∧ ( x ≤ y ) ⇒ ( f x ≤ f y ) ) ∧

 ( f real_convex_on s ) )

Definition 4.

Strictly Convex Cost function

⊢∀ f x. strict_convex_cost_func f s x =

( f real_continuous_on s ) ∧ ( f real_differentiable_on s ) ∧

 ( ∀ x y. ( x ∈ s ) ∧ ( y ∈ s ) ( x < y ) ⇒ ( f x < f y ) ∧

 ( f real_strict_convex_on s ) )

Similarly, the utility function is modeled as:

Definition 5.

Concave Utility function

⊢∀ f x. concave_utility_func f s x =

( f real_continuous_on s ) ∧ ( f real_differentiable_on s ) ∧

 ( ∀ x y. ( x ∈ s ) ∧ ( y ∈ s ) ∧ ( f x ≤ f y ) ) ∧

 ( -f real_convex_on s )

Definition 6.

Strictly Concave Utility function

⊢∀ f x. strict_concave_utility_func f s x =

( f real_continuous_on s ) ∧ ( f real_differentiable_on s ) ∧

 ( ∀ x y. ( x ∈ s ) ∧ ( y ∈ s ) ∧ ( f x < f y ) ) ∧

 ( -f real_strict_convex_on s )

Finally, we formally model the first-order condition, described by Equation (1), in HOL-Light, as:

Definition 7.

First-order Condition

⊢∀ f x. first_order_cond f x = ( real_derivative f x = &0 )

In Definition 7, first_order_cond is a higher-order-logic function, which accepts a real valued function, f, and variable x, whereas real_derivative is a higher-order-logic function representing mathematical derivative of the given real function.

The formalization in this section provides the necessary logical framework to formally verify the cost, utility and first-order condition models within the sound core of the HOL-Light theorem prover.

6. Case Study: Formal Behavioral Modeling Based on Polynomial Functions

Polynomial functions are commonly used in microeconomics models [1,5,42]. We provide formal analysis of the cost and utility modeling based on the polynomial type of functions up to the fourth order. Additionally, we formally verify the first-order condition for the profit functions, which are based on the polynomial type of cost utility functions.

6.1. Polynomial Type of Cost Functions

We formally verify the quadratic cost function as:

Theorem 9.

Quadratic Cost Function

⊢∀ $\mathtt{x}$ $\mathtt{s}$ $\mathtt{a}$ $\mathtt{b}$ $\mathtt{c}$.

  A1: ($\mathtt{is}\_\mathtt{realinterval}$ $\mathtt{s}$)    ∧A2:($\mathtt{real}\_\mathtt{open}$ $\mathtt{s}$)    ∧       A3:¬(∃$\mathtt{a}\mathtt{1}$.$\mathtt{s}$ $=$ $\left\{\mathtt{a}\mathtt{1}\right\}$) ∧

  A4: $\mathtt{strict}\_\mathtt{convex}\_\mathtt{cost}\_\mathtt{func}$($\lambda$$\mathtt{x}.$$\mathtt{Cx}\mathtt{a}$$\ast$$\mathtt{x}\mathtt{pow}\mathtt{2}$$+$$\mathtt{Cx}\mathtt{b}$$\ast$$\mathtt{x}$$+$$\mathtt{Cx}\mathtt{c}$) ∧

  A5: ($\mathtt{x}$∈$\mathtt{s}$) ∧A6:($-\frac{\mathtt{b}}{\mathtt{2}\mathtt{a}}$ < $\mathtt{x}$)    A7:($\mathtt{0}$ < $\mathtt{a}$) ∧

 ⇒$\mathtt{0}$ < $\mathtt{real}\_\mathtt{derivative}$($\lambda$ $\mathtt{x}.$ $\mathtt{Cx}\mathtt{a}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{2}$ $+$ $\mathtt{Cx}\mathtt{b}$ $\ast$ $\mathtt{x}$ $+$ $\mathtt{Cx}\mathtt{c}$) ∧

  $\mathtt{0}$ < $\mathtt{real}\_\mathtt{derivative}$($\mathtt{real}\_\mathtt{derivative}$($\lambda$ $\mathtt{x}.$ $\mathtt{Cx}\mathtt{a}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{2}$ $+$ $\mathtt{Cx}\mathtt{b}$ $\ast$ $\mathtt{x}$ $+$ $\mathtt{Cx}\mathtt{c}$))

In the above theorem, Assumptions A1–A3 represent the conditions on the given interval, i.e., s is a real, open, and non-singular interval. Assumption A4 ensures that the given function satisfies the necessary conditions to model the utility by using Definition 4. Assumption A5 ensures that function is defined over the given interval, whereas Assumptions A6–A7 represent the conditions on the domain of the given function, $-\frac{\mathtt{b}}{\mathtt{2}\mathtt{a}}$ < $\mathtt{x}$, and on the leading coefficient, $\mathtt{0}$ < $\mathtt{a}$, to formally verify the increasing first and second-order derivatives of the quadratic function in the conclusion.

Next, we formally verify the cubic cost function modeling, in the HOL-Light theorem prover, as:

Theorem 10.

Cubic Cost Function

⊢∀ $\mathtt{x}$ $\mathtt{s}$ $\mathtt{a}$ $\mathtt{b}$ $\mathtt{c}$ $\mathtt{d}$.

  A1: ($\mathtt{is}\_\mathtt{realinterval}$ $\mathtt{s}$)    ∧A2:($\mathtt{real}\_\mathtt{open}$ $\mathtt{s}$)    ∧A3:¬(∃$\mathtt{a}\mathtt{1}$.$\mathtt{s}$ $=$ $\left\{\mathtt{a}\mathtt{1}\right\}$)

  A4: $\mathtt{strict}\_\mathtt{convex}\_\mathtt{cost}\_\mathtt{func}$($\lambda$$\mathtt{x}.$$\mathtt{Cx}\mathtt{a}$$\ast$$\mathtt{x}\mathtt{pow}\mathtt{3}$$+$$\mathtt{Cx}\mathtt{b}$$\ast$$\mathtt{xpow}\mathtt{2}$$+$$\mathtt{Cx}\mathtt{c}$$\ast$$\mathtt{x}$$+$$\mathtt{Cx}\mathtt{d}$)

  A5: ($\mathtt{x}$∈$\mathtt{s}$)    ∧

  A6: ($-\frac{\mathtt{b}}{\mathtt{3}\mathtt{a}}$ < $\mathtt{x}$))    ∧A7:($\frac{-\mathtt{b}-\sqrt{{\mathtt{b}}^{\mathtt{2}}+\mathtt{3}\ast \mathtt{a}\ast \mathtt{c}}}{\mathtt{3}\mathtt{a}}$ < $\mathtt{x}$)    ∨    ($\frac{-\mathtt{b}+\sqrt{{\mathtt{b}}^{\mathtt{2}}+\mathtt{3}\ast \mathtt{a}\ast \mathtt{c}}}{\mathtt{3}\mathtt{a}}$ < $\mathtt{x}$)

  ⇒$\mathtt{0}$ < $\mathtt{real}\_\mathtt{derivative}$($\lambda$ $\mathtt{x}.$ $\mathtt{Cx}\mathtt{a}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{3}$ $+$ $\mathtt{Cx}\mathtt{b}$ $\ast$ $\mathtt{xpow}\mathtt{2}$ $+$ $\mathtt{Cx}\mathtt{c}$ $\ast$ $\mathtt{x}$ $+$ $\mathtt{Cx}\mathtt{d}$

                       $\mathtt{Cx}\mathtt{c}$ $\ast$ $\mathtt{x}$ $+$ $\mathtt{Cx}\mathtt{d}$))∧

       $\mathtt{0}$ < $\mathtt{real}\_\mathtt{derivative}$($\mathtt{real}\_\mathtt{derivative}$($\lambda$ $\mathtt{x}.$ $\mathtt{Cx}\mathtt{a}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{3}$ $+$ $\mathtt{Cx}\mathtt{b}$ $\ast$ $\mathtt{xpow}\mathtt{2}$ $+$

                       $\mathtt{Cx}\mathtt{c}$ $\ast$ $\mathtt{x}$ $+$ $\mathtt{Cx}\mathtt{d}$)))

In the above theorem, Assumptions A6–A7 are conditions on the domain, $\mathtt{x}$, of the cubic cost function to formally verify the properties of the increasing first and second-order derivatives in the conclusion.

Theorem 11.

Quartic Cost Function

⊢∀ $\mathtt{x}$ $\mathtt{s}$ $\mathtt{a}$ $\mathtt{b}$ $\mathtt{c}$ $\mathtt{d}$ $\mathtt{e}$.

  A1: ($\mathtt{is}\_\mathtt{realinterval}$ $\mathtt{s}$)    ∧A2:($\mathtt{real}\_\mathtt{open}$ $\mathtt{s}$)    ∧A3:¬(∃$\mathtt{a}\mathtt{1}$.$\mathtt{s}$ $=$ $\left\{\mathtt{a}\mathtt{1}\right\}$)

  A4: $\mathtt{strict}\_\mathtt{convex}\_\mathtt{cost}\_\mathtt{func}$($\lambda$$\mathtt{x}.$$\mathtt{Cx}\mathtt{a}$$\ast$$\mathtt{x}\mathtt{pow}\mathtt{4}$$+$$\mathtt{Cx}\mathtt{b}$$\ast$$\mathtt{x}\mathtt{pow}\mathtt{3}$$+$$\mathtt{Cx}\mathtt{c}$$\ast$$\mathtt{x}\mathtt{pow}\mathtt{2}$$+$

       $\mathtt{Cx}\mathtt{d}$ $\ast$ $\mathtt{x}$ $+$ $\mathtt{Cx}\mathtt{e}$)

  A5: ($\mathtt{x}$∈$\mathtt{s}$) ∧    A6:(${\mathtt{a}}_{\mathtt{1}}$ = $\mathtt{4}\ast \mathtt{a}$) ∧

  A7: (${\mathtt{b}}_{\mathtt{1}}+{\mathtt{a}}_{\mathtt{1}}\ast \mathtt{r}$ = $\mathtt{3}\ast \mathtt{b}$)    ∧A8: (${\mathtt{c}}_{\mathtt{1}}+{\mathtt{b}}_{\mathtt{1}}\ast \mathtt{r}$ = $\mathtt{2}\ast \mathtt{c}$)    ∧A9: (−$\mathtt{r}\ast {\mathtt{c}}_{\mathtt{1}}$ = $\mathtt{d}$) ∧

  A10: ($-\mathtt{r}$≤$\mathtt{x}$    ∨    $\frac{{\mathtt{b}}_{\mathtt{1}}-\sqrt{{\mathtt{b}}_{\mathtt{1}}^{\mathtt{2}}-\mathtt{4}\ast {\mathtt{a}}_{\mathtt{1}}\ast {\mathtt{c}}_{\mathtt{1}}}}{\mathtt{2}{\mathtt{a}}_{\mathtt{1}}}$≤$\mathtt{x}$    ∨    $\frac{{\mathtt{b}}_{\mathtt{1}}+\sqrt{{\mathtt{b}}_{\mathtt{1}}^{\mathtt{2}}-\mathtt{4}\ast {\mathtt{a}}_{\mathtt{1}}\ast {\mathtt{c}}_{\mathtt{1}}}}{\mathtt{2}{\mathtt{a}}_{\mathtt{1}}}$≤$\mathtt{x}$) ∧

  A11: ($\frac{\mathtt{3}\ast \mathtt{b}-\sqrt{\mathtt{9}\ast {\mathtt{b}}^{\mathtt{2}}+\mathtt{24}\ast \mathtt{a}\ast \mathtt{c}}}{\mathtt{12}\mathtt{a}}$ < $\mathtt{x}$∨    $\frac{\mathtt{3}\ast \mathtt{b}+\sqrt{\mathtt{9}\ast {\mathtt{b}}^{\mathtt{2}}+\mathtt{24}\ast \mathtt{a}\ast \mathtt{c}}}{\mathtt{12}\mathtt{a}}$ < $\mathtt{x}$)

    ⇒$\mathtt{0}$ < $\mathtt{real}\_\mathtt{derivative}$($\lambda$ $\mathtt{x}.$ $\mathtt{Cx}\mathtt{a}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{4}$ $+$ $\mathtt{Cx}\mathtt{b}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{3}$ $+$ $\mathtt{Cx}\mathtt{c}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{2}$ $+$ $\mathtt{Cx}\mathtt{d}$ $\ast$ $\mathtt{x}$

      $+$ $\mathtt{Cx}\mathtt{e}$))    ∧

      $\mathtt{0}$ < $\mathtt{real}\_\mathtt{derivative}$($\mathtt{real}\_\mathtt{derivative}$($\lambda$ $\mathtt{x}.$ $\mathtt{Cx}\mathtt{a}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{4}$ $+$ $\mathtt{Cx}\mathtt{b}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{3}$ $+$

      $\mathtt{Cx}\mathtt{c}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{2}$ $+$ $\mathtt{Cx}\mathtt{d}$ $\ast$ $\mathtt{x}$ $+$ $\mathtt{Cx}\mathtt{e}$)

In the above theorem, Assumptions A6–A9 provide the relationship between the coefficients of the given quartic polynomial and coefficients of its quadratic factor. Assumptions A10–11 impose conditions on the domain, $\mathtt{x}$, of the given polynomial in terms of the coefficients of the linear and quadratic factors of the given quartic cost function, to formally verify the increasing first and second-order derivatives in the conclusion of the theorem.

Theorems 9–11 are formally verified results for the quadratic, cubic and quartic cost functions, mainly, based on Definition 4, Lemma 1, Lemma 2, and Theorem 7, whereas Theorems 2–6 are used to formally specify the domain, of the given polynomials, in which the desired properties of the cost models are satisfied.

6.2. Utility Function

We formally verify the utility functions modeled using the polynomial functions of up to the fourth order, in higher-order logic, as:

Theorem 12.

Quadratic Utility Function

⊢∀ $\mathtt{f}$ $\mathtt{x}$ $\mathtt{s}$ $\mathtt{a}$.

  A1: ($\mathtt{is}\_\mathtt{realinterval}$ $\mathtt{s}$)    ∧A2:($\mathtt{real}\_\mathtt{open}$ $\mathtt{s}$) ∧

  A3: ¬(∃$\mathtt{a}$.$\mathtt{s}$ $=$ $\left\{\mathtt{a}\right\}$)    ∧A4: ($\mathtt{x}$∈$\mathtt{s}$) ∧

  A5: (∀ $\mathtt{x}$.$\mathtt{concave}\_\mathtt{utility}\_\mathtt{func}$($\lambda$ $\mathtt{x}.$($\mathtt{Cx}\mathtt{a}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{2}$ $+$ $\mathtt{Cx}\mathtt{b}$ $\ast$ $\mathtt{x}$ $+$ $\mathtt{Cx}\mathtt{c}$))∧

  A6: ($-\frac{\mathtt{b}}{\mathtt{2}\mathtt{a}}$≤$\mathtt{x}$) ∧    A7: ($\mathtt{a}$ < $\mathtt{0}$)

        ⇒  $\mathtt{0}$≤$\mathtt{real}\_\mathtt{derivative}$($\lambda$ $\mathtt{x}.$ $\mathtt{Cx}\mathtt{a}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{2}$ $+$ $\mathtt{Cx}\mathtt{b}$ $\ast$ $\mathtt{x}$ $+$ $\mathtt{Cx}\mathtt{c}$) ∧

         $\mathtt{real}\_\mathtt{derivative}$($\lambda$ $\mathtt{x}.$ $\mathtt{real}\_\mathtt{derivative}$($\lambda$ $\mathtt{x}.$ $\mathtt{Cx}\mathtt{a}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{2}$ $+$

                                      c $\mathtt{Cx}\mathtt{b}$ $\ast$ $\mathtt{x}$ $+$ $\mathtt{Cx}\mathtt{c}$))≤$\mathtt{0}$

In the above theorem, Assumption A5 models the necessary conditions for utility modeling by using Definition 5. Assumption A6 ensures that the domain of the given quadratic polynomial, i.e., variable x, is greater than $-\frac{\mathtt{b}}{\mathtt{2}\mathtt{a}}$ to satisfy the increasing property of utility modeling. Assumption A6 ensures that the leading coefficient is negative, which in turn ascertains the concavity of the given quadratic polynomial. These assumptions ensure the formal verification of the increasing first-order derivate and decreasing second-order derivatives in the conclusion of the theorem.

Theorem  13.

Cubic Utility Function

⊢∀ $\mathtt{f}$ $\mathtt{x}$ $\mathtt{s}$ $\mathtt{a}$ $\mathtt{b}$ $\mathtt{c}$ $\mathtt{d}$.

  A1: ($\mathtt{is}\_\mathtt{realinterval}$ $\mathtt{s}$)    ∧A2: ($\mathtt{real}\_\mathtt{open}$ $\mathtt{s}$) ∧

  A3: ¬(∃$\mathtt{a}\mathtt{1}$.$\mathtt{s}$ $=$ $\left\{\mathtt{a}\mathtt{1}\right\}$) ∧A4:($\mathtt{x}$∈$\mathtt{s}$)    ∧

  A5: (∀ $\mathtt{x}$.$\mathtt{concave}\_\mathtt{utility}\_\mathtt{func}$($\lambda$ $\mathtt{x}.$ $(\mathtt{Cx}\mathtt{a}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{3}$ $+$ $\mathtt{Cx}\mathtt{b}$ $\ast$ $\mathtt{xpow}\mathtt{2}$ $+$

   $\mathtt{Cx}\mathtt{c}$ $\ast$ $\mathtt{x}$ $+$ $\mathtt{Cx}\mathtt{d}$) ∧       A6:($\frac{\mathtt{b}-\sqrt{{\mathtt{b}}^{\mathtt{2}}+\mathtt{3}\ast \mathtt{a}\ast \mathtt{c}}}{\mathtt{3}\mathtt{a}}$≤$\mathtt{x}$)    ∨    ($\frac{\mathtt{b}+\sqrt{{\mathtt{b}}^{\mathtt{2}}+\mathtt{3}\ast \mathtt{a}\ast \mathtt{c}}}{\mathtt{3}\mathtt{a}}$≤$\mathtt{x}$)

  A7: ($\mathtt{x}$≤$-\frac{\mathtt{b}}{\mathtt{3}\mathtt{a}}$)

  ⇒($\mathtt{0}$≤$\mathtt{real}\_\mathtt{derivative}$($\lambda$ $\mathtt{x}.$ $(\mathtt{Cx}\mathtt{a}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{3}$ $+$ $\mathtt{Cx}\mathtt{b}$ $\ast$ $\mathtt{xpow}\mathtt{2}$ $+$ $\mathtt{Cx}\mathtt{c}$ $\ast$ $\mathtt{x}$ $+$ $\mathtt{Cx}\mathtt{d}$))

  ∧  $\mathtt{real}\_\mathtt{derivative}$($\lambda$ $\mathtt{x}.$ $\mathtt{real}\_\mathtt{derivative}$($\lambda$ $\mathtt{x}.$ $(\mathtt{Cx}\mathtt{a}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{3}$ $+$ $\mathtt{Cx}\mathtt{b}$ $\ast$ $\mathtt{xpow}\mathtt{2}$ $+$

                 $\mathtt{Cx}\mathtt{c}$ $\ast$ $\mathtt{x}$ $+$ $\mathtt{Cx}\mathtt{d}$) ≤$\mathtt{0}$)

Assumptions A6 and A7 impose conditions on the real variable, x, which is the domain of the cubic utility function for positive first-order derivative and negative second-order derivative tests.

Next, we formally verify the quartic utility function in higher-order logic as:

Theorem 14.

Quartic Utility Function

⊢∀ $\mathtt{f}$ $\mathtt{x}$ $\mathtt{s}$ $\mathtt{a}$ $\mathtt{b}$ $\mathtt{c}$ $\mathtt{d}$.

    A1: ($\mathtt{is}\_\mathtt{realinterval}$ $\mathtt{s}$)    ∧A2:($\mathtt{real}\_\mathtt{open}$ $\mathtt{s}$) ∧    A3:¬(∃$\mathtt{a}$.$\mathtt{s}$ $=$ $\left\{\mathtt{a}\right\}$) ∧

    A4: ($\mathtt{x}$∈$\mathtt{s}$)    ∧A5:(∀ $\mathtt{x}$.$\mathtt{concave}\_\mathtt{utility}\_\mathtt{func}$($\lambda$ $\mathtt{x}.$ $(\mathtt{Cx}\mathtt{a}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{4}$ $+$

   $\mathtt{Cx}\mathtt{b}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{3}$ $+$ $\mathtt{Cx}\mathtt{c}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{2}$ $+$ $\mathtt{Cx}\mathtt{d}$ $\ast$ $\mathtt{x}$ $+$ $\mathtt{Cx}\mathtt{e}$))∧A6:(${\mathtt{a}}_{\mathtt{1}}$ = $\mathtt{4}\ast \mathtt{a}$) ∧

    A7: (${\mathtt{b}}_{\mathtt{1}}+{\mathtt{a}}_{\mathtt{1}}\ast \mathtt{r}$ = $\mathtt{3}\ast \mathtt{b}$)    ∧A8:(${\mathtt{c}}_{\mathtt{1}}+{\mathtt{b}}_{\mathtt{1}}\ast \mathtt{r}$ = $\mathtt{2}\ast \mathtt{c}$)    ∧A9:(−$\mathtt{r}\ast {\mathtt{c}}_{\mathtt{1}}$ = $\mathtt{d}$) ∧

    A10: ($-\mathtt{r}$≤$\mathtt{x}$    ∨    $\frac{{\mathtt{b}}_{\mathtt{1}}-\sqrt{{\mathtt{b}}_{\mathtt{1}}^{\mathtt{2}}-\mathtt{4}\ast {\mathtt{a}}_{\mathtt{1}}\ast {\mathtt{c}}_{\mathtt{1}}}}{\mathtt{2}{\mathtt{a}}_{\mathtt{1}}}$≤$\mathtt{x}$    ∨    $\frac{{\mathtt{b}}_{\mathtt{1}}+\sqrt{{\mathtt{b}}_{\mathtt{1}}^{\mathtt{2}}-\mathtt{4}\ast {\mathtt{a}}_{\mathtt{1}}\ast {\mathtt{c}}_{\mathtt{1}}}}{\mathtt{2}{\mathtt{a}}_{\mathtt{1}}}$≤$\mathtt{x}$) ∧

    A11: ($\mathtt{x}$≤$\frac{\mathtt{3}\ast \mathtt{b}-\sqrt{\mathtt{9}\ast {\mathtt{b}}^{\mathtt{2}}+\mathtt{24}\ast \mathtt{a}\ast \mathtt{c}}}{\mathtt{12}\mathtt{a}}$    ∨    $\mathtt{x}$≤$\frac{\mathtt{3}\ast \mathtt{b}+\sqrt{\mathtt{9}\ast {\mathtt{b}}^{\mathtt{2}}+\mathtt{24}\ast \mathtt{a}\ast \mathtt{c}}}{\mathtt{12}\mathtt{a}}$)

    ⇒( 0 ≤$\mathtt{real}\_\mathtt{derivative}$ $\lambda$ $\mathtt{x}.$ $(\mathtt{Cx}\mathtt{a}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{4}$ $+$ $\mathtt{Cx}\mathtt{b}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{3}$ $+$

    $\mathtt{Cx}\mathtt{c}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{2}$ $+$ $\mathtt{Cx}\mathtt{d}$ $\ast$ $\mathtt{x}$ $+$ $\mathtt{Cx}\mathtt{e}$))∧

      $\mathtt{real}\_\mathtt{derivative}$($\lambda$ $\mathtt{x}.$ $\mathtt{real}\_\mathtt{derivative}$($\lambda$ $\mathtt{x}.$ $(\mathtt{Cx}\mathtt{a}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{4}$ $+$ $\mathtt{Cx}\mathtt{b}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{3}$ $+$

      $\mathtt{Cx}\mathtt{c}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{2}$ $+$ $\mathtt{Cx}\mathtt{d}$ $\ast$ $\mathtt{x}$ $+$ $\mathtt{Cx}\mathtt{e}$))≤$\mathtt{0}$

Assumptions A6–A9 relate the coefficients of the linear and quadratic factors of the quartic polynomial coefficients. These conditions formally specify the factorization of the quartic polynomial based on Theorem 3. Assumptions A10 and A11 provide allowable ranges of the domain, x, of the given function to formally verify the positive first-order derivative and negative second-order derivative in the conclusion of the above theorem.

Theorems 12–14 are formally verified using Theorem 1 and Definition 5. Theorem 1 is used to verify the concavity of the polynomial utility functions, whereas, factoring theorems, i.e., Theorems 2–6, are used to formally specify the conditions on the domain of the polynomial type of the utility functions.

6.3. First-Order Condition

Finally, we present formally verified results for the real stationary or critical points for the profit functions designed using polynomial functions. We use Definition 7 to model the first-order condition for the profit function, where $\mathtt{f}(\mathtt{x})=\mathtt{R}(\mathtt{x})-\mathtt{C}(\mathtt{x})$ is used to model the real function. We use linear revenue function, i.e., $\mathtt{R}(\mathtt{x})$ = $\mathtt{r}$ ∗ $\mathtt{x}$, in which $\mathtt{r}$ is the rate of the electricity for the amount of consumed electricity, i.e., $\mathtt{x}$. For the cost function, $\mathtt{C}(\mathtt{x})$, modeling, we consider quadratic, cubic, and quartic polynomial based behavioral models one by one.

In this regard, profit function based on the quadratic cost or utility function is verified as:

Theorem 15.

First-order condition for quadratic cost function

⊢∀ $\mathtt{a}$ $\mathtt{b}$ $\mathtt{c}$ $\mathtt{x}$.

  A1: $\mathtt{a}$ ≠ $\mathtt{0}$∧

  A2: $\mathtt{x}$ = $\frac{\mathtt{r}-\mathtt{b}}{\mathtt{2}\mathtt{a}}$

    ⇒$\mathtt{first}\_\mathtt{order}\_\mathtt{cond}$($\lambda x.$ $\mathtt{r}$ ∗ $\mathtt{x}$−($\mathtt{a}$ ∗ $\mathtt{x}\mathtt{pow}\mathtt{2}$ $+$ $\mathtt{b}$ $\ast$ $\mathtt{x}$ $+$ $\mathtt{c}$))$\mathtt{x}$

In the above theorem, Assumption A1 ensures that the leading coefficient of the quadratic type of the cost or utility function is not zero. This assumption avoids the possibility of the reduced order case of the polynomial. Assumption A2 specifies the critical point of the given profit function in terms of the rate of electricity, $\mathtt{r}$, and coefficients of the given quadratic cost function.

Theorem 15 is formally verified by taking the derivative of the profit function. This allows for formally verifying the above theorem using Assumption A2, which is the critical point of the given function.

Similarly, the profit function based on the cubic type of cost or utility function is formally verified as:

Theorem 16.

First-order condition for cubic cost function

⊢∀ $\mathtt{a}$ $\mathtt{b}$ $\mathtt{c}$ $\mathtt{d}$ $\mathtt{x}$.

    A1: $\mathtt{a}$ ≠ $\mathtt{0}$∧

    A2: $\mathtt{0}$ < $\mathtt{b}\mathtt{pow}\mathtt{2}$ − $\mathtt{3}$ ∗ $\mathtt{a}$ ∗ ($\mathtt{c}$ − $\mathtt{r}$) ∧

        $($ $\mathtt{a}$ < $\mathtt{0}$∧$($ $\mathtt{b}$< $\sqrt{\mathtt{b}\mathtt{pow}\mathtt{2}-\mathtt{3}\ast \mathtt{a}\ast (\mathtt{c}-\mathtt{r})}$∨

                 $\sqrt{\mathtt{b}\mathtt{pow}\mathtt{2}-\mathtt{3}\ast \mathtt{a}\ast (\mathtt{c}-\mathtt{r})}$< - $\mathtt{b}$ $)$∨

        $($ $\mathtt{0}$ < $\mathtt{a}$∧$($ $\sqrt{\mathtt{b}\mathtt{pow}\mathtt{2}-\mathtt{3}\ast \mathtt{a}\ast (\mathtt{c}-\mathtt{r})}$ < $\mathtt{b}$∨

                 - $\mathtt{b}$ < $\sqrt{\mathtt{b}\mathtt{pow}\mathtt{2}-\mathtt{3}\ast \mathtt{a}\ast (\mathtt{c}-\mathtt{r})}$ $)$

   ⇒$\mathtt{first}\_\mathtt{order}\_\mathtt{cond}$($\lambda x.$ $\mathtt{r}$ ∗ $\mathtt{x}$−($\mathtt{a}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{3}$ $+$ $\mathtt{b}$ $\ast$ $\mathtt{xpow}\mathtt{2}$ $+$ $\mathtt{c}$ $\ast$ $\mathtt{x}$ $+$ $\mathtt{d})$)$\mathtt{x}$

In the above theorem, Assumption A2 provides the relationship between variable, $\mathtt{x}$, and coefficients of the given function to ensure real critical or stationary points.

Finally, we formally verify the first-order condition for profit function, when the cost or utility function is a quartic polynomial, in higher-order logic, as:

Theorem 17.

First-order condition for quartic cost function

⊢∀ $\mathtt{a}$ $\mathtt{b}$ $\mathtt{c}$ $\mathtt{d}$ $\mathtt{e}$ $\mathtt{x}$.

    A1: $\mathtt{a}$ ≠ $\mathtt{0}$∧A2:$\mathtt{a}\mathtt{1}$ = $\mathtt{4}\mathtt{a}$∧

    A3: $\mathtt{b}\mathtt{1}$ + $\mathtt{a}\mathtt{1}$ ∗ $\mathtt{r}$ = $\mathtt{3}\mathtt{b}$∧ A4:$\mathtt{c}\mathtt{1}$ + $\mathtt{b}\mathtt{1}$ ∗ $\mathtt{r}$ = $\mathtt{2}\mathtt{c}$

    A5: $\mathtt{c}\mathtt{1}$ + $\mathtt{b}\mathtt{1}$ ∗ $\mathtt{r}$ = $\mathtt{2}\mathtt{c}$    A6:$\mathtt{d}$ − $\mathtt{r}$ = $\mathtt{c}\mathtt{1}$ ∗ $\mathtt{r}$

    A7: $\mathtt{0}$ < $\mathtt{b}\mathtt{1}\mathtt{pow}\mathtt{2}$ − $\mathtt{4}$ ∗ $\mathtt{a}\mathtt{1}$ ∗ $\mathtt{c}\mathtt{1}$∧

        $($ $\mathtt{a}\mathtt{1}$ < $\mathtt{0}$∧$($ $\mathtt{b}\mathtt{1}$< $\sqrt{\mathtt{b}\mathtt{1}\mathtt{pow}\mathtt{2}-\mathtt{4}\ast \mathtt{a}\mathtt{1}\ast \mathtt{c}\mathtt{1}}$∨

               $\sqrt{\mathtt{b}\mathtt{1}\mathtt{pow}\mathtt{2}-\mathtt{4}\ast \mathtt{a}\mathtt{1}\ast \mathtt{c}\mathtt{1}}$< - $\mathtt{b}\mathtt{1}$ $)$∨

        $($ $\mathtt{0}$ < $\mathtt{a}\mathtt{1}$∧$($ $\sqrt{\mathtt{b}\mathtt{1}\mathtt{pow}\mathtt{2}-\mathtt{4}\ast \mathtt{a}\mathtt{1}\ast \mathtt{c}\mathtt{1}}$ < $\mathtt{b}\mathtt{1}$∨

            − $\mathtt{b}\mathtt{1}$ < $\sqrt{\mathtt{b}\mathtt{1}\mathtt{pow}\mathtt{2}-\mathtt{4}\ast \mathtt{a}\mathtt{1}\ast \mathtt{c}\mathtt{1}}$ $)$

   ⇒$\mathtt{first}\_\mathtt{order}\_\mathtt{cond}$($\lambda x.$ $\mathtt{Cx}\mathtt{a}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{4}$ $+$ $\mathtt{Cx}\mathtt{b}$ $\ast$ $\mathtt{xpow}\mathtt{3}$ $+$ $\mathtt{Cx}\mathtt{c}$ $\ast$ $\mathtt{xpow}\mathtt{2}$ $+$ $\mathtt{Cx}\mathtt{d}$ $\ast$ $\mathtt{x}$ $+$ $\mathtt{Cx}\mathtt{e})$ $\mathtt{x}$

In the above theorem, first-order derivative reduces the given fourth order quartic polynomial to the corresponding third-order polynomial. Assumptions A2–A6 represent the relationship among the coefficients of the cubic ordered profit function and its factors, i.e., linear and quadratic. Assumption A7 gives the relationship between variable x and coefficients for the real stationary points of the profit function.

The proposed foundational formalization of the derivative tests allowed us to formally specify and verify the microeconomics based behavioral modeling of the smart grid entities in DR programs. Theorems 9–17 represent universally quantified results, which unlike traditional techniques, also contain exact and exhaustive set of the assumptions to model the behavior of the given entities. These results give very useful insights about the behavior of the modeling function, with respect to its domain, to satisfy the desired mathematical properties. For example, the assumptions in Theorems 9–14 provide explicit conditions on the domain of the commonly used polynomial type of the cost and utility functions in DR programs [42,43,44,45,46,47]. Similarly, the assumptions of Theorems 15–17 provide a priori information regarding the effect of the values of the coefficients of the given profit function on the maximum possible profit. In the case of real profit function, the assumptions of Theorem 15–17 facilitate choosing the values of the coefficients of the profit function for the real maximum of the given profit function.

The proposed formalization is generic and can be readily employed to formally verify and specify any microeconomics model based on the different mathematical functions, such as exponential and logarithmic. The main challenges faced in the proposed formalization were to provide formally verified theorems related to strict convexity or concavity and associated properties of such functions to enable the formalization of the microeconomics concepts. Besides the development of the fundamental logical framework, the formal verification of the case study involved considerable effort due to the rigorous formal reasoning required to accomplish the task using theorem proving. The corresponding proof script, which is available for download at [48], has 2000 lines of HOL-Light code and required about 250 man hours of development time.

7. Electricity Market Applications

In this section, we formally verify the quadratic cost [49] and utility [44] models, which have been used in the optimal power flow [50] and DR programs [44] in the electricity market. In optimal power flow, polynomial functions are used to find the economic dispatch, which ensures reduced electricity generation cost, whereas DR programs are used to change the demand behavior of the consumers to ensure the safe and secure smart grid operations. In this regard, incentive and time based programs are employed to change the electricity usage behavior of the smart grids.

7.1. Quartic Polynomial Cost Function for Thermal Power Plants

We formally verify the quadratic polynomial cost function for thermal power plants using the results of Section 6. A metahuristic algorithm in [49], called the ABC algorithm, has been utilized for estimating the coefficients of the quadratic type of the cost function for the economic dispatch problem, which is used in the operation economics to reduce the cost of electricity generation. In the economic dispatch problem, distributed generators are used to produce electricity to reduce the total operational cost and regulation issues in an electricity market. The mathematical form for the quartic cost function is:

$$F{C}_j(P_{G_j})=a_{oj}+a_{1j}{P}_{G_j}+a_{2j}{P}_{G_j}^2+r_j.$$

(4)

where $F{C}_j$, $P_{G_j}$, $a_{oj}$, $a_{1j}$, $a_{2j}$, and $r_j$ represent the cost function for electricity generation, amount of the power generated, coefficients, and error associated with the j-th generator. Equation (4) is used to estimate the parameters for three different thermal power plants with fuels such as coal, oil, and gas [49]. Each power plant consists of five generating units with 10, 20, 30, 40, and 50 MW. The estimation is performed on the actual data [51] and presented in

Table 2. Estimated coefficients of cubic cost function using the ABC algorithm.

Coefficients	${\mathit{a}}_{\mathbf{0}}$	${\mathit{a}}_{\mathbf{1}}$	${\mathit{a}}_{\mathbf{2}}$
Estimated values (coal)	0.0414	7.5874	96.6046
Estimated values (oil)	0.0442	7.8779	101.5360
Estimated values (gas)	0.0439	8.0991	101.8179

.

We formally verify the mathematical properties of the cost function, in HOL-Light, as:

Theorem 18.

Quadratic Cost Function for Economic Dispatch

⊢∀ $\mathtt{x}$.

  A1: ($\mathtt{x}$∈$(\mathtt{0},\mathtt{150})$)

  ⇒$\mathtt{0}$ < $\mathtt{real}\_\mathtt{derivative}$($\mathtt{Cx}\mathtt{0.0414}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{2}$ $+$ $\mathtt{Cx}\mathtt{7.5874}$ $\ast$ $\mathtt{x}$ $+$ $\mathtt{Cx}\mathtt{96.6046}$) ∧

  $\mathtt{0}$ < $\mathtt{real}\_\mathtt{derivative}$($\mathtt{real}\_\mathtt{derivative}$($\lambda$ $\mathtt{x}.$ $\mathtt{Cx}\mathtt{0.0414}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{2}$ $+$ $\mathtt{Cx}\mathtt{7.5874}$ $\ast$ $\mathtt{x}$ $+$

              $\mathtt{Cx}\mathtt{96.6046}$) ∧

  $\mathtt{0}$ < $\mathtt{real}\_\mathtt{derivative}$($\mathtt{Cx}\mathtt{0.0442}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{2}$ $+$ $\mathtt{Cx}\mathtt{7.8779}$ $\ast$ $\mathtt{x}$ $+$ $\mathtt{Cx}\mathtt{101.5360}$) ∧

  $\mathtt{0}$ < $\mathtt{real}\_\mathtt{derivative}$($\mathtt{real}\_\mathtt{derivative}$($\lambda$ $\mathtt{x}.$ $\mathtt{Cx}\mathtt{0.0442}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{2}$ $+$ $\mathtt{Cx}\mathtt{7.8779}$ $\ast$ $\mathtt{x}$ $+$

              $\mathtt{Cx}\mathtt{101.5360}$) ∧

  $\mathtt{0}$ < $\mathtt{real}\_\mathtt{derivative}$($\mathtt{Cx}\mathtt{0.0439}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{2}$ $+$ $\mathtt{Cx}\mathtt{8.0991}$ $\ast$ $\mathtt{x}$ $+$ $\mathtt{Cx}\mathtt{101.8179}$) ∧

  $\mathtt{0}$ < $\mathtt{real}\_\mathtt{derivative}$($\mathtt{Cx}\mathtt{0.0439}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{2}$ $+$ $\mathtt{Cx}\mathtt{8.0991}$ $\ast$ $\mathtt{x}$ $+$

              $\mathtt{Cx}\mathtt{101.8179}$)

In the above theorem, the quadratic cost function for coal, oil, and gas power plants is formally verified using Theorem 9. Thanks to our foundational formalization, the proof of Theorem 18 just required a few lines of HOL-Light code. The formally verified results ensure that all the mathematical properties, in Definition 4, for modeling the cost function are satisfied by the estimated quadratic polynomial cost functions.

7.2. Quadratic Utility Function for Smart Grids

We formally verify a quadratic utility function, using our proposed formalization in Section 6, which is used in [44] to find the optimal energy consumption levels for the smart grid users. The proposed algorithm in [44] relies on the real-time pricing for DR management by exploiting the utility maximization concept of microeconomics. The algorithm considers a smart grid environment that is equipped with smart meters and communication network for interacting among energy provider and end-users in the smart grid network. The quadratic utility function is defined as [44]:

$$U(\omega ,x)=\left\{\begin{array}{c}\omega x-\frac{\alpha }{2}{x}^{2}0\le x\le \frac{\omega }{\alpha }\hfill \\ \frac{\omega }{\alpha }\frac{\omega }{\alpha }<x\hfill \end{array}\right..$$

(5)

The function $U(\omega ,x)$ represents utility function for different users in the smart grid network, where $\omega$ varies among the electricity users in the network to differentiate users, such as industrial or household, and $\alpha$ is a predetermined parameter. The utility for a particular consumer is a function of its electricity consumption, i.e., x.

Furthermore, the utility function is also employed to design the welfare objective function, $W(\omega ,x)$, of an individual consumer, as:

$$W(\omega ,x)=U(\omega ,x)-Px.$$

(6)

where P is the price of the x(MW) amount of the electricity consumption of a user. The welfare objective function is maximized using the first-order condition,

$$\frac{d}{dx}W(\omega ,x)=0.$$

(7)

We formally verify the behavior of the quadratic utility function, i.e., Equation (5), and utility maximization problem, i.e., Equation (6), for $\omega =4$ and $\alpha =0.5$ for a single consumer in $(0,\frac{\omega }{\alpha })$ interval, as:

Theorem 19.

Quadratic utility function for the real-time algorithm

⊢∀ $\mathtt{x}$.

  A1: ($\mathtt{x}$∈$(\mathtt{0},\mathtt{8})$)

  ⇒$\mathtt{0}$≤$\mathtt{real}\_\mathtt{derivative}$($\lambda$ $\mathtt{x}.$ $-\mathtt{Cx}\mathtt{0.25}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{2}$ $+$ $\mathtt{Cx}\mathtt{8}$ $\ast$ $\mathtt{x}$ )∧

  $\mathtt{real}\_\mathtt{derivative}$($\mathtt{real}\_\mathtt{derivative}$($\lambda$ $\mathtt{x}.$ $-\mathtt{Cx}\mathtt{0.25}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{2}$ $+$ $\mathtt{Cx}\mathtt{8}$ $\ast$ $\mathtt{x}$≤$\mathtt{0}$)

The above theorem is formally verified using Theorem 12. Assumption A1 ensures that the electricity demand of an individual consumer is within the allowed consumption levels. Moreover, assumptions of Theorem 12 are also verified to accomplish the verification of the given utility function.

Similarly, the first-order condition for the welfare objective is formally verified as:

Theorem 20.

First-order condition for Welfare objective function

⊢∀ $\mathtt{P}$ $\mathtt{x}$.

  A1: ($\mathtt{x}$ = $\mathtt{2}$ ∗ $\mathtt{P}$−$\mathtt{8}$)

  ⇒($\mathtt{real}\_\mathtt{derivative}$($\mathtt{P}$ ∗ $\mathtt{x}$−($-\mathtt{Cx}\mathtt{0.25}$ $\ast$ $\mathtt{x}\mathtt{pow}\mathtt{2}$ $+$ $\mathtt{Cx}\mathtt{8}$ $\ast$ $\mathtt{x}$))=$\mathtt{0}$)

The above theorem is formally verified using Theorem 15. Assumption A1 is the necessary condition for the profit maximization of the welfare function in terms of the electricity price, P, and maximum electricity consumption level. Again, the proof of Theorems 19 and 20 just required a few lines of HOL-Light code, which illustrates the usefulness and practical effectiveness of the proposed formalization of foundational theories. Theorem 19 ensures that utility function satisfies the mathematical properties of Definition 6, whereas Theorem 20 gives explicit conditions for the maximization of the welfare function.

8. Conclusions

In this paper, we presented a formal methodology to conduct the formal behavioral modeling and analysis of microeconomics concepts. The derivative tests are primary mathematical techniques to specify and verify the desired properties, such as monotonicity and convexity, of the modeling functions in microeconomics. To formally model the microeconomics concepts, we formally verified second-order derivative tests for strict convexity or concavity, and, based on these results, we provided the formal models of the cost and utility functions. Additionally, we also developed the formal modeling of the first order condition, which is based on the first-order derivative, to formally analyze the profit functions for profit maximization problems. As a case study, the formalization is employed for the formal behavioral modeling and analysis of the cost and utility modeling based on the polynomial function. Finally, the quadratic cost and utility functions for the economic dispatch problem and DR program are formally verified using the proposed formalization. The distinguishing features of the proposed analysis work include its accurate results due to the involvement of sound theorem proving and the availability of an exhaustive set of assumptions that are required for the validity of the results.

The proposed formalization can be readily employed to formally specify and verify the microeconomics models, such as exponential and logarithmic functions, for any underlying market agent. Moreover, the formalization is based upon the second-order derivative tests, which are abundantly used in the convex theory. Thus, the formalization is also beneficial for a wide range applications of the convex theory [52,53]. The reported formalization supports real analysis with single variable only and thus can be extended to multivariate analysis, which is supported by HOL-Light theorem prover. Moreover, linking conventional analysis tools, such as Maxima [17], with a theorem prover, such as HOL-Light, is also an interesting direction for facilitating formal non-experts to conduct highly reliable and accurate microeconomics analysis of economy markets, using the proposed formalization.