For many, 2020 was a depressing year.

When my church was closed for a period of time by our governor, however, I found some valuable things to hold onto. I discovered a theory of catastrophic plate tectonics, and learned that it explained many of the puzzles prevalent among those who believe in an ancient earth. I discovered Jay Smith’s presentation on the origins of Islam. I also discovered this video of Dr. Lisle presenting his “Ultimate Proof of Creation,” and found it so fascinating that I then bought his book. In his book, he presents the idea of ultimate logic. I found this idea so interesting and fascinating, I wanted to share it here.

For those with a Christian background, much of Lisle’s argument follows from Prov 1:7,

The fear of the LORD is the beginning of knowledge: but fools despise wisdom and instruction. (Prov 1:7)

Contrary to popular belief, knowledge does not come from an education. It doesn’t come from the best schools, the right newspapers, or the right social media feeds. The “fear of the LORD” is the beginning of knowledge. (I also found this video of Derek Prince presenting what the fear of the LORD is in the first place during the COVID lockdowns, but I digress.) For those who would argue that science forms the basis for knowledge, I watched what science did this year with certain studies of COVID and hydroxychloroquine. These observations confirmed that science itself is founded upon honesty. Science cannot prove the necessity of honesty, and so science cannot be the beginning of knowledge.

For those who are not Christians, the rest of the discussion focuses more on the idea of and development of ultimate logic in the first place.

A Quick Background

Let’s start out by defining some terms used when describing logic. In logic, premises are presented and used to draw a conclusion. The progression from premises to conclusion is called an argument. A picture might help, so let’s consider Fig. 1.

Fig 1. The form of an argument

When working with SymbiYosys, the assumptions within your logic file form the premises and the various assertions form the logical conclusions we wish to draw. The solver then works from the premises to either prove the conclusion, or to come up with an example that proves the conclusion invalid.

The entire process is important for understanding this idea of ultimate logic, but to get there I need to first point out that this background discussion isn’t really complete since we haven’t listed all of the assumptions required for such a proof.

Digging deeper into the assumptions

Did you notice any of the missing assumptions? Here are some assumptions that we typically miss when building a formal proof of hardware correctness:

  • The RTL logic within the design itself constitutes a set of assumptions in addition to the explicit ones. This makes sense, but it’s not normally something we think about.

  • We also assume that Yosys accurately translates our logic and formal statements without error into something the solver can handle. This is a great assumption, until it isn’t true.

  • We assume the formal solver works. That is, when the formal solver proves something, no counter examples exist. None.

    A corollary assumption that when the solver declares a proof invalid that it truly is invalid isn’t typically as critical. In that case, the solver is required to provide an example proving that the proof is invalid and such examples are easily dealt with. The result, on a good day, will be a bug report in solver that will then get fixed.

  • Here’s a tricky underlying assumption as well: A valid proof today of the logic within our design will remain a valid proof until the assumptions change.

While Lisle focuses on this last assumption, he goes deeper as well. How do we know that the assumptions of any given proof are valid in the first place?

Fig 2. Assumptions get verified when you verify the second module

In digital design, many assumptions can be validated in a straightforward fashion as shown in Fig. 2. First, when any two components interact, any properties of the inputs to the one will be assumed and the outputs will be asserted. Then, when verifying the module it interacts with, that module will have its inputs assumed and its outputs asserted. By swapping the assumptions on the inputs of the one to be assertions on the outputs of the other, the assumptions can be proven. This ultimately forms a proof of our assumptions.

As a caution, let me remind you to verify only one module at a time. As we’ve discovered earlier, if you make assumptions about things within a module you might void the proof.

That deals with some of the formal assumptions within logic design, but what about the others?

Modus Ponens and the Invalid Proof of the Ultimate

Modus Ponens is a Latin name for a specific argument that, in my mind, helps explain the need for an ultimate premise. The argument is fairly basic: P|->Q (P implies Q), P (P is true), therefore Q (our conclusion) must be true as well.

Fig 3. Modus Ponens

A common, but related, fallacy is one where P|->Q and then Q, and so P is concluded. This fallacy is called Affirming the Consequent.

Fig 4. Affirming the Consequent

How common is this fallacy? Well, if you think about it, is this not the entire basis of the scientific method? The scientist considers the evidence before him and makes a theory about the world. He then forms an experiment that will have a particular outcome if his theory is true. In formal form, P would be the theory and Q a favorable outcome from the experiment. If the experiment comes out as he predicts, this does not confirm his hypothesis. It cannot. At best, all the scientific method can do is reject hypotheses which do not match the evidence. It cannot confirm or prove a hypothesis because it matches the evidence because to do so would be the fallacy of affirming the consequent.

Let’s back up to Modus Ponens, however, and ask ourselves, how do we know that P is true in the first place? Perhaps because a more fundamental premise is true, P0, and because P0 is true therefore we know that P is true. But what about P0? How shall we know that P0 is true? Because it depends upon P1?

Fig 5. Modus Ponens to Absurdity

We could repeat this logic and repeat this logic and repeat this logic and the result would be that we would never truly prove anything. There must be a first premise. This we shall call the Ultimate premise.

The Ultimate Premise

Lisle then asks, what about the rules of logic themselves? How shall logic itself be proven? Why should we accept that Modus Ponens is a valid argument? Likewise, if Modus Ponens is valid today, will it remain valid again tomorrow? If so, why?

In math, I learned to handle such arguments using axioms. An axiom is something that isn’t otherwise proven. We just accept them as true. For example, two axioms I remember include 1) there exists a zero and 2) every integer has a successor. The problem with just accepting axioms as true is that doing so is arbitrary. In other words, why should I accept your axioms as true and not someone else’s?

As a good example of this, how often have you heard a statement such as, “My [insert favorite politician] is honest, but [the opposition party] is not”? Another good example would be that parallel lines never cross. Such statements are made as axioms with no argument offered as their basis.

Fig 6. Circular logic is known as Begging the question

Such logic is arbitrary, and therefore proves nothing. How then shall the truth of competing axioms be weighed against each other to know which are in fact true?

A better definition of an axiom would be a “self-evident” truth. This is Mirriam-Websters’s second meaning of the word, and perhaps the best one for this context.

Unfortunately, declaring something to be true because it is true is a known fallacy called “begging the question”, or circular reasoning.

Proving the Ultimate Premise

Ultimate proofs, Lisle argues, have the form of A therefore A yet without being either circular or fallatious.

As an example of this, Lisle presents an existence proof for whether or not such ultimate arguments could be even exist.

  1. Premise: Rules of logic apply
  2. Conclusion: Rules of logic apply

This proof is not circular because to argue otherwise would render you unable to draw any conclusion at all, leading to complete foolishness. Indeed, you cannot argue against the rules of logic without first using the rules of logic to make your argument. This therefore is a proof of the rules of logic based upon those same rules yet without being circular.

How shall we know, however, that the rules of logic that apply today shall apply again tomorrow in the same fashion? Here again, the proof follows from an ultimate premise.

  1. God is true and unchanging. (The ultimate premise, drawn from the Bible (See Mal 3:6 and John 3:33)
  2. Rules of logic follow from God’s nature.
  3. Therefore, the rules of logic will remain unchanged again tomorrow.

Worldviews that are not founded upon God as their ultimate premise cannot make this argument.

Conclusion

Lisle makes several other claims as well which cannot be explained by a secular world view. For example, if there are no ultimate moral standards then by what standard would you judge my conduct right or wrong? If you cannot judge the conduct of another as either right or wrong, then upon what basis is justice founded? What basis would you then have for requiring one action or another of someone else? On the other hand, if there are absolute standards of right and wrong, then what is their basis?

His book, however, is really about the ultimate proof of creation: the conclusion that God made the world in six days and rested on the seventh, and that He did so roughly six thousand years ago. Any science attempting to prove otherwise, Lisle argues, must be based upon the premise that the natural processes we observe today have continued unchanging from the past to the present. This conclusion, however, is arbitrary and without basis. Just because we see nothing but natural processes today doesn’t mean that supernatural processes never existed. A separate conclusion, made on the basis of recorded observations throughout human history, is also available to us. According to recorded history, God did in fact create the world as He said He did, and further that His record is true and accurate. This record includes supernatural events which cannot be refuted today apart from resorting to arbitrary or even circular logic. (i.e., the supernatural cannot happen therefore it didn’t. But why couldn’t it have taken place? Because.)