Propositional Calculus and "Lazy evaluation"?

Question

I want to formalize a system, and currently I don't know, if I can use propositional calculus in my case. At first, I though that I need a simple conjunction.

$A \wedge B$

However, there is a problem. In order to "evaluate" $B$ (there are some formulas behind) some calculations are required which depend on $A$, i.e. these calculations can only be performed, if $A$ is true.

I am not an expert in maths (maybe moderate), but computer science. In regular, imperative programming lanugages (not very formal, I know), we have "lazy evaluation". This means that the system does not care about $B$, if $A$ already evaluates to $false$. As I said, in this case $B$ cannot even be evaluated - the application would crash.

Well, I guess that there is no "lazy evaluation" in the propositional calculus. Therefore, I assume that my definition $A \wedge B$ is wrong.

1. Is my assumption correct?
2. What to do? Is there another calculus I have to use?
3. Alternativly, can I use some standardized phrases (prose) in order to define what I mean?

I already digged into temporal logic. First, it's very hard for me to understand. Second, I don't know if I am off the track. Would be nice if you can provide a solution for my problem (easy, right?) and give me some hint which calculus or theory could be important for me. I am willing to learn more...

[Edit]

After a nice try for solving my problem, I have to give another example.

Given:

$A(x) =$ very complex predicate based on x

$f(x) = \begin{cases} x + 10 & A(x) = true \\ undef. & \text{otherwise} \end{cases}$

Now, I cannot simply write: $A(x) \wedge (f(x) > 20)$

Further note: I cannot write expressions like "if $f(x)$ is $undef$" or use $dom(f)$ or whatever. In my case $f$ is a complex transformation and (by definition) this transformation is $applicable$, iff $A(x)$ is $true$.

[/Edit]

Answer 1

As a practical matter there is nothing wrong with writing something like $$ x > 0 ~\land~ \sin(\sqrt x) < \frac 1x $$ I understand your unease -- coming from a programming background it is natural to view mathematical formulas as a language for instructing some imagined machine which might break down or explode if it were to try to evaluate $\sin(\sqrt x)$ and $x$ happened to be negative. However, mathematical formulas are not about instructing a machine -- they are about communicating your ideas to a real, live, flesh-and-blood reader who is capable of independent thought. That reader will certainly understand what this formula is meant to convey, and as such it has served its purpose. In most contexts you can even get away with writing simply $$ \sin(\sqrt x) < \frac 1x $$ thus leaving implicit the condition that both comparands have to be defined.

Now what's the point of these practical considerations when you explicitly asked for a formalization? It is this: the details of a formalization are a matter of choice, but we have a duty to ourselves and our readers to try to make the formalization match everyday communicative usage as much as possible. Otherwise the formalization will be misleading rather than enlightening, and therefore useless. So when we're deciding on a formalization, our first task is to understand which intuition it is we want to formalize.

---

Now there are several avenues to take for formalizing terms. The first and most intuitively appealing one is to to consider that the value of an expression or variable can always be some exceptional "undefined" value. Then "undefined" will dominate every arithmetic operator and most other operators such that the result is always undefined when one or more of the operands is undefined. However the logical connectives that we use to build conditions will need to take a more subtle approach: $$ \begin{array}{c|ccc} \land & T & ? & F \\ \hline T & T & ? & F \\ ? & ? & ? & F \\ F & F & F & F \end{array} \qquad \begin{array}{c|ccc} \lor & T & ? & F \\ \hline T & T & T & T \\ ? & T & ? & ? \\ F & T & ? & F \end{array} $$ (Note that whereas programming usually considers boolean just one of many types an "expression" can have, mathematical notation has a tradition for distinguishing more strictly between "expressions" (or "terms" in the jargon of formal logic) which denote mathematical objects, and "formulas" which have truth values).

Since even formalized mathematics is still not instructions for a machine that is at risk of exploding, we're free not to fix any particular "order of evaluation" for these extended connectives -- we can let a $F$ on either side of the $\land$ win as long as we're sure it's there. And we can then decide that the formulas we're really interested in -- such as the $\phi$ in set builder notation $\{x\mid \phi(x)\}$ must be one that we can prove never take the "undefined" value (even though some of its subformulas may), or the value of the set itself would be "undefined".

We can choose to extend this special treatment to comparison operators such as $<$ ("predicates" in formal-logic jargon), such that "undefined" compared to anything, or anything compared to "undefined" both produce "false" rather than "undefined". Again, because there is no machine that we must prevent from exploding, we can define things to mean what is most convenient for us. Then the expression $$\sin(\sqrt x) < \frac1x$$ will be good and equally false for $x=-42$ as for $x=2$.

---

Reasoning about "undefined" makes good sense for most everyday reasoning, but there is a second approach to the problem which is usually favored in rigorous metamathematics because it is technically simpler, though conceptually somewhat removed from everyday intuition:

According to this interpretation there is no undefined. Every expression always means something, and every formula is always either true or false once we're given values for all the variables -- but we may not know which -- the axioms we're working with may not allow us to prove anything about it.

When we're thinking in this mode, the expression $\frac 1x$ denotes some mathematical object even when $x=0$. It will even be convenient to assume that the mathematical object $\frac 10$ is some number, but which number is not going to be important, because the only way we can use $\frac 1x$ is by appealing to an axiom saying something like $$ \forall x\Bigl[ x\ne 0 \Longrightarrow x\times\frac1x=1 \Bigr] $$ Likewise, $\sqrt x$ is always some number, but the only thing we know about this number is $$ \forall x\Bigl[ x\ge 0 \Longrightarrow \sqrt x \times \sqrt x = x\land \sqrt x \ge 0 \Bigr] $$ Thus if we want to prove something about an expression that involves $\frac 1x$ or $\sqrt x$, we had better make sure we already have proof that $x$ is neither zero nor negative -- otherwise the axioms about reciprocals and square roots will do us no good. We can satisfy that obligation by adding a guard formula $$ x > 0 ~\land~ \sin(\sqrt x) < \frac 1x $$ which will allow us to prove things about the entire formula by case analysis: the values of $x$ that make the axioms useless on the right-hand side will be taken care of by the left-hand side.

In this way "can't prove anything about" ends up serving the same end purpose as "undefined" does in the more everyday approach above, but without requiring us to add specific support for it in the rules of formal logic that define what is a valid proof or a valid model.

This technical simpliciation is usually considered worth it in formal metamathematics, where one needs to reason about things like the set of all valid proofs, and it is therefore a priority that the rules of the proof system are as lean and simple as possible. When this is not the case, it is usually better (and certainly more intuitive) to imagine that there is some underlying concept of "undefined".

One doesn't often find completely rigorous formalizations of the "undefined" solution, because the situations where one wants completely rigorous formalizations of formulas tend to coincide with situations where the conceptual price of using "can'r prove anything about it" instead is worth paying. About the only prominent exception to this general trend is when formally defining the semantics of a programming language. As you well know, programming languages often have explicit exceptional values at various levels -- from NaN in floating-point arithmetic to the throwing of exceptions -- because there we do have an actual machine to worry about.

Answer 2

I believe you're concerned about expressions like the predicate

$x$ is a real number satisfying $x \neq 0$ and $1/x = 2$

In typical formal grammars, this is a grammatically incorrect proposition: one is only allowed to divide by a non-zero value, but $x$ is a real variable, not a non-zero real variable.

But it "morally" makes sense, because we are only interested in the division in the particular case that $x$ is nonzero.

The way to fix it without changing logic is to translate into something like

$x$ is a real number satisfying $x \neq 0$ and (there exists a nonzero real number $y$ such that $x = y$ and $1/y = 2$)

One could define a formal logic that had short-circuited Boolean expressions. This would make things rather complicated for the typical purposes of studying formal theories, but it would make things simpler for expressing things as a formal theories.

---

If one bases syntax on the notion of partial function rather than function, then the expression $1/x$ is fine for a real variable $x$: it is simply a partial function on the reals. Depending on the finer details of how you interpret the logical symbols, the predicate

$x$ is a real number satisfying $x \neq 0$ and $1/x = 2$

could be a well-defined relation true for 1/2 and false for all other values of $x$. Or, it could be a partial relation, true for 1/2, false for 2, but undefined at 0.