Building digital logic ICs using Quantificational Logic: An Exclusive Uniqueness Existential Quantifier (Quantificational Logic)

Keywords: Discrete Mathematics - Quantificational Logic - Predicate Logic - Model Theory - Digital Logic Design - KiCad - Formal Languages.

Warning

This an early-version article, and is still subjected to core changes.
This article is not written using one of the fancy AI tools; therefore, pay respect to time spent to deliver this true knowledge.
Unlike fake content, this is true knowledge!
AI (ChatGPT) is used to derive the notation for the Semantical Definition section.

The following article attempts to introduce a new quantificational operator (i.e., $$\exists^{\oplus}$$) by defining a new quantificational logic quantifier operator within the formal language grammar. A quantifier maps to a predicate function that tests all of the values from a particular domain of discourse (i.e., universe) against another predicate function by evaluating it using the values from the domain as independent variables. Then, the article introduces a maneuver that attempts to build a digital logic circuitry out of this new quantificational operator.

Table of content:

Preface
Existential Quantifier
- 2.1 Reverse Engineering Semantics
- 2.2 Definitions in the Symbolic Table (i.e., Grammar)
Universal Quantifier
- 3.1 Reverse Engineering Semantics
- 3.2 Definitions in the Symbolic Table (i.e., Grammar)
De Morgan's Theorem application
- 4.1 Defining Equivalent quantifiers using equivalent semantics
Uniqueness Quantifier
- 5.1 Syntatical Definition
- 5.2 Grammatical Extension
- 5.3 Semantical Definition
- 5.4 Examples
Digital Logic Circuitry
- 6.1 Building a logic circuit satisfying the uniqueness formula (i.e., $$\exists^{\oplus}$$).
- 6.2 Liasing with truth table and tautology.
GNU/C99 Examples using the Electrostatic-Sandbox SDK
- 7.1 Basic Library for digital switching.

1. Preface

Quantificational operators are defined within the grammer of the first-order language (i.e., $$\Sigma$$) as symbolic operators. These symbolic operators test the satisfiability of a particular property (or predicate function) over a specific domain known as the domain of discourse or the universe of that property.

Quantificational operations are nothing, but repeated predicate evaluations of a predicate function against members from a domain. Those evaluations are then appended together using one of the n-tuple propositional operations (e.g., Logical OR, Logical AND, Logical XOR, Logical NAND, Logical NXOR, and Logical NOR).

By reverse engineering the already defined quantificational operators (e.g., $$\forall$$ and $$\exists$$), one will be able to identify and obtain some of the steps that could be used to define new operations to the Grammer of the formal languages.

Formal languages are defined as triplets $$L = \{\Sigma, R, O\}$$; such that $$\Sigma$$ represents the set of grammer (i.e., the symbolic table), $$R$$ is the set of rules that provide explicit instructions about how to form valid combinations of the elements of $$\Sigma$$, and $$O$$ is a set of extra-linguistic objects that are denoted and represented by the elements of the language L.

Introducing a new operator (or a term) requires the modification of the syntatical terms $$\Sigma$$, and the syntatical rules guiding their compositions.

2. The Existential Quantifier

2.1 Reverse Engineering Semantics: The existential quantifier operator evaluates a predicate function against all the members from within the domain of discourse in a disjunctive normal form postulate (DNF). In which satisfiability necessitates that the predicate evaluation (i.e., $$\Phi{x}$$) must hold for at least one of the members from within the domain or the universe of discourse, otherwise, the statement will be false.

$$ \begin{align*} \exists(x).\Phi{x} \equiv \bigvee_{i = 0}^N \Phi{(x_{i})} = \Phi{(x_{0})} \vee \Phi{(x_{1})} \vee \Phi{(x_{2})} ... \vee \Phi{(x_{N-1})} \vee \Phi{(x_{N})} \end{align*} $$

2.2 Definitions in the Symbolic Table and the semantical definition of the existential quantifier:

$$ \begin{align*} \Sigma_{L1} = \Sigma_{L1} \cup \{\exists(x).\Phi{x}\} \\ \exists(x).\Phi{x} \triangleq \bigvee_{i = 0}^N \Phi{(x_{i})} \\ \end{align*} $$

3. The Universal Quantifier

3.1 Reverse Engineering Semantics: The universal quantifier operator evaluates a predicate function against all the members from within the domain of discourse in a conjunctive normal form postulate (CNF). In which satisfiability necessitates that the predicate evaluation (i.e., $$\Phi{x}$$) must hold for every member from within the domain or the universe of discourse, otherwise, the statement will be false.

$$ \begin{align*} \forall(x).\Phi{x} \equiv \bigwedge_{i = 0}^N \Phi{(x_{i})} = \Phi{(x_{0})} \land \Phi{(x_{1})} \land \Phi{(x_{2})} ... \land \Phi{(x_{N-1})} \land \Phi{(x_{N})} \end{align*} $$

3.2 Definitions in the Symbolic Table and the semantical definition of the universal quantifier:

$$ \begin{align*} \Sigma_{L1} = \Sigma_{L1} \cup \{\forall(x).\Phi{x}\} \\ \forall(x).\Phi{x} \triangleq \bigwedge_{i = 0}^N \Phi{(x_{i})} \\ \end{align*} $$

5. The Uniqueness Existential Quantifier (EXOR Existential Quantification)

5.1 Syntatical Definition: The uniqueness quantifier operator is a specialized type of the existential operators that evaluates a predicate function against all the members from within the domain of discourse in a disjunctive normal form postulate (CNF). In which satisfiability necessitates that the predicate evaluation (i.e., $$\Phi{x}$$) must hold for at most one member (i.e., only ONE member) from within the domain or the universe of discourse, otherwise, the statement will be false (i.e., Not Satisfiable).

$$ \begin{aligned} &\text{Let } X \text{ be the domain of discourse such that } X = \{x_0, x_1, x_2, \ldots, x_n\}, \\ &\text{where } i, j, n \in \mathbb{N}; \text{ hence } x_i, x_j, x_n \in X. \\ &\therefore\ \exists^{\oplus}x.,\Phi(x) \triangleq \bigoplus_{i=0}^{n} \Phi(x_i) \end{aligned} $$

Note

Further Expansion to the formula:

$$ \begin{align*} &\because\quad \bigoplus_{i = 0}^n \Phi{x_i} \equiv \bigvee_{i = 0}^n \left[\bigwedge_{j = 0}^n \left( (i = j) \Rightarrow \Phi{x_i} \iff \neg(i = j) \Rightarrow \neg \Phi{x_j} \right)\right] \\ &\because\quad \left( (i = j) \Rightarrow \Phi{x_i} \right) \iff \left( \neg(i = j) \Rightarrow \neg \Phi{x_j} \right) \equiv \neg \left( \left((i = j) \Rightarrow \Phi{x_i}\right) \oplus \left(\neg(i = j) \Rightarrow \neg \Phi{x_j}\right) \right) \\ &\therefore\quad \exists^{\oplus}(x).\Phi{x} \triangleq \bigvee_{i = 0}^N \left[\bigwedge_{j = 0}^N \neg \left( \left((i = j) \Rightarrow \Phi{x_i}\right) \oplus \left(\neg(i = j) \Rightarrow \neg \Phi{x_j}\right) \right)\right] \\ &\text{The EXOR quantificational formula can also be explained using a far more straightforward formula} \\ &\text{by embedding the conditional statement into the series counter:} \\ &\exists^{\oplus}x.,\Phi(x) \triangleq \bigvee_{i = 0}^n \left[\Phi{x_i} \land \bigwedge_{\substack{j \ne i}}^n \neg\Phi{x_j} \right] \end{align*} $$

5.2 Grammatical Extension:

$$ \begin{align*} \Sigma_{L1} = \Sigma_{L1} \cup \{\exists^{\oplus}(x).\Phi{x}\} \\ \exists^{\oplus}(x).\Phi{x} \triangleq \bigvee_{i = 0}^N \left[\bigwedge_{j = 0}^N \neg (((i = j) \implies \Phi{x_i}) \oplus (\neg(i = j) \implies \neg \Phi{x_j})) \right] \end{align*} $$

5.3 Semantical Definition:

$$ [ \mathcal{M}, s \models \exists^{\oplus} x. \Phi(x) \iff \exists d \in D \text{ such that } \mathcal{M}, s[x \mapsto d] \models \Phi(x) \land \forall d' \in D,, (\mathcal{M}, s[x \mapsto d'] \models \Phi(x) \Rightarrow d = d') ] $$

5.4 Examples:

Example 1: Domain with 2 Elements Let the domain of discourse be $$X = \{x_1, x_2\}$$

$$\exists^{\oplus} x. \Phi{x}\ \text{is true iff}\ \Phi{x}\ \text{holds for exactly one x}\ \in X$$

$$ \begin{array}{|c|c||c|} \hline \Phi(x_1) & \Phi(x_2) & \exists^{\oplus} x.\ \Phi(x) \\ \hline F & F & F \\ F & T & T \\ T & F & T \\ T & T & F \\ \hline \end{array} $$

Example 2: Domain with 4 Elements: Let the domain of discourse be $$X = \{x_1, x_2, x_3, x_4\}$$

$$\exists^{\oplus} x. \Phi{x}\ \text{is true iff}\ \Phi{x}\ \text{holds for exactly one x}\ \in X$$

$$ \begin{array}{|c|c|c|c|c|} \hline \Phi(x_1) & \Phi(x_2) & \Phi(x_3) & \Phi(x_4) & \exists^{\oplus} x.\ \Phi(x) \\ \hline T & F & F & F & T\\ F & T & F & F & T\\ F & F & T & F & T\\ F & F & F & T & T\\ \\ F & F & F & F & F\\ T & T & T & T & F\\ \\ F & T & T & T & F\\ T & F & T & T & F\\ T & T & F & T & F\\ T & T & T & F & F\\ \\ F & F & T & T & F\\ T & F & F & T & F\\ T & T & F & F & F\\ F & T & T & F & F\\ T & F & T & F & F\\ F & T & F & T & F\\ \hline \end{array} $$

Digital Logic Circuitry

Preface: Building digital circuitry is one of the fundamentals of designing Printed Circuit Boards (i.e., PCBs) for microcontrollers and development boards. Development Boards therefore are utilized in switching and control applications (e.g., Railway Traffic Control (Track Blocks) - Medical Alarming Systems). However, designing digital components blindly from digital logic itself is overwhelming due to the high complexity of digital logic; therefore, designing based on a FOL and a model theorem is favorable.

Structural Components: A digital logic circuitry asserting uniqueness would likely depend on the primitive digital components (i.e., AND, OR, and NOT ICs). However, incorporation of combinatorial logic gates (e.g., XOR, XAND, and NAND) could be attained to simplify wiring the switching circuit.

Digital logic design: An XOR digital IC with $$n$$ number of inputs $$I$$, a single digital output $$Q$$, a $$V_{cc}$$, and a $$GND$$ rails would suffice for this type of operation. Quantification would take place over the input domain $$I$$. The internals of this digital logic component could instantiated from the quantificational formula (i.e., $$\exists^{\oplus} x. \Phi(x)$$).

$$ \begin{aligned} \because\quad &\exists^{\oplus}(x).\Phi{x} \triangleq \bigvee_{i = 0}^N \left[ \bigwedge_{j = 0}^N \neg \left( ((i = j) \implies \Phi{x_i}) \oplus (\neg(i = j) \implies \neg \Phi{x_j}) \right) \right] \\ \therefore\quad &\exists^{\oplus}(x).\Phi{x} \triangleq (\Phi{x_i} \land \neg \Phi{x_{i + 1}} \land \neg \Phi{x_{i + 2}} \land \cdots \land \neg \Phi{x_n}) \\ &\quad \vee (\neg \Phi{x_i} \land \Phi{x_{i + 1}} \land \neg \Phi{x_{i + 2}} \land \cdots \land \neg \Phi{x_n}) \\ &\quad \vee \cdots \\ &\quad \vee (\neg \Phi{x_i} \land \neg \Phi{x_{i + 1}} \land \neg \Phi{x_{i + 2}} \land \cdots \land \Phi{x_n}) \end{aligned} $$

Switching Algebra and Uniqueness Quantificational Logic:

Based on the quantificational logic formula; the following components are required for circuit design (Structural Components):
1. OR Logic Gates x 1.
2. AND Logic Gates x {n}.
3. NOT Logic Gates x {n}.
Components' Layout: As per circuitry layout, it is advised to follow these steps:
1. Start with the domain and co-domain relations (i.e., define the number of inputs and the number of outputs).
2. Find a relationship between the domain and the co-domain (i.e., a mathematical relation defining the number of outputs from the number of inputs).
3. Write the required truth table using the correct number of inputs and outputs (See Table-1).
4. Derive the switching algebra formula that satisfies this truth table; such that it attains consistency with up-scaling and down-scaling the domain and the co-domain.
5. Switching Algebra Formulas are better written using Quantificational-Logic-first approach.
6. Start building the digital circuitry into decomposed components based on the precedence of evaluating the logical quantifiers stated in the quantification formula; such that between every 2 components, there exists a wired or otherwise a wireless interface
7. In the case of $$\exists^{\oplus}$$; the precedence will follow in a disjunctive normal form fashion; such that the following steps could be attained:
  1. Start by wiring an OR Gate at the output as a final component (See Fig-1.1).
  2. Proceed by wiring multiple AND Gates of number $$n$$ with the input of the last OR Gate; such that the number of inputs to each AND Gate is $$n$$ (See Fig-1.2).
  3. Proceed by constructing multiple NOT Gates of number $$n$$ out of the input domain (i.e., Negate the input); thus the number of input rails would be twice (See Fig-1.3).
  4. Wire the input rails to the AND Gates components; such that each AND Gate would receive $$n$$ number of input; in which all the input rails are the negated rails except the corresponding input to this AND Gate, it will receive a non-negated rail (See Fig-1.4).

Tip

The precedence of evaluating the logical quantifiers means the rank or the order of evaluating the quantifiers. The highest rank to the lowest rank is the NOT > AND > OR (among its other formats. e.g., XOR).
In this case, building a digital circuit would involve recognizing this precedence, and mapping it to an order that could be used to place the combinatorial components in which data is obtained from the highest precedence and is transmitted to the lowest precedence.
This creates a general-purpose digital design systematic structure that could be followed from just a Quantificational Formula.
Using constructive proof methodologies, one could construct new quantificational formulas, that are based on the logical combinations among basic propositional operators, to be used in digital circuit design.

7. GNU/C99 Examples using the Electrostatic-Sandbox SDK

The last section in this article introduces a code example using GNU/C99 for Arithmos Library on the Electrostatic-Sandbox SDK.

7.1 A Basic Library for digital switching:

[switching.h]

//
// A header file for switching algebra operations.
// Author: pavl_g.
//

#ifndef _SWITCHING_ALGEBRA_H_
#define _SWITCHING_ALGEBRA_H_

#include <stddef.h>
#include <stdint.h>
#include <sys/types.h>
#include <electrostatic/electronetsoft/util/utilities.h>

#ifdef __cplusplus
extern "C" {
#endif

#if !defined(SWITCHING_TYPE)
#define SWITCHING_TYPE uint8_t
#endif

status_code switching_bitwise_xor(SWITCHING_TYPE **inputs, SWITCHING_TYPE *output);

#ifdef __cplusplus
}
#endif

#endif

[switching_xor.c]

#include <electrostatic/electronetsoft/arithmos/algebra/switching.h>

status_code switching_bitwise_xor(SWITCHING_TYPE **inputs, SWITCHING_TYPE *output) {
	// pre-processor automata -- Input Validation
	if (rvalue(inputs) == NULL || rvalue(output) == NULL) {
		return EUNDEFINEDBUFFER;
	}	
	SWITCHING_TYPE __cnf;

	// processing automata -- Incremental XORing
	// Prenex Normal Form (PNF)
	// Disjunctive Normal Form (DNF)
	for (int i = 0; rvalue(input[i]) != NULL; i++) {
		// Conjunctive Normal Form (CNF)
		for (int j = 0; rvalue(input[j]) != NULL; j++) {
			if (j != i) {
				__cnf &= ~(*input[j]);
				continue;
			} 
			__cnf &= *input[j];
		}
		*output = *output | __cnf;
	}
	// post-processing automata
	return PASS;
}

pavly-gerges/uniqueness-quantifier.md