To put it simply, what i'm looking for is a logic that models sequential circuits.
If i understood correctly, digital circuits are often categorized in two distinct categories, combinatorial and sequential, the former being a subset of the latter. Combinatorial circuits are modeled by propositional calculus, though instead of focusing on separate formulas, like propositional calculus does, it builds bigger and bigger circuits through composition of smaller ones.
More precisely, in combinatorial circuits, we are used to basically defining a set of free signals, say, A, B and C for example, and then building more complex circuits based on them, like $P = AB$, $Q = A+C$, S = (PQ)' (for the less versed in boolean algebra, simply note that there's an equivalence between these operators and the usual from propositional calculus).
This simplistic approach breaks down if applied to sequential circuits. Consider our free signals R and S. One definition of a flip-flop goes like this: Q = (R + Q_i)' and Q_i = (S + Q)' (where "$+$" is the logical "or", and "$'$" is the logical negation). If you perform a substitution you'll see a self-reference, something propositional calculus isn't equipped to work with.
The usual explanation here is to consider prior values to $Q$ and $Q_i$. The idea here is that, if $Q$ is the logical opposite of $Q_i$, and it never so happens that we set both $R$ and $S$ to 1 (in propositional calculus parlance, $R$ and $S$ both interpreted as true), then $Q$ and $Q_i$ will always be logical opposites. From there we note that setting $R$ and $S$ both to 0 mantains the current values of $Q$ and $Q_i$, while setting only one of $R$ or $S$ to 1 sets $Q_i$ or $Q$ to 1, respectively.
I believe these are some of the topics i think answers to this question could shed some light on:
- What exactly do you need to add to propositional calculus in order for it to model sequential circuits? For example, sequential circuits have to do with the notion of state, which in turn basically means that the result of setting a couple of signals can vary through time - does this means we'll have to add something to model the notion of time?
- What kind of sequential circuits can we build, anyway?
- I vaguely recall that an in-depth explanations on the subject would have to explain how delay actually works in real life circuits. Indeed, real world circuits sometimes make use of a construct called buffer; in propositional calculus terms, this is simply the unary identity function! Does this factor in our logic? How so?
- Can we compose it further with other known logics?
- I've tried to look up the answer at Wikipedia and stumbled upon an approach based on Sequentions and Venjunctions - two things which not only i had never heard about before, i also failed to find any sort of useful information about. Are these concepts really related to this problem?