Typing:
propositional
symbol  type comment
/\
\/
¬!
FFF
TTT
UUU
-->
<->
&&&&short-circuit and
||||short-circuit or
->>Łukasiewicz implication
quantifiers
symboltype
x:AA x:
x; 0 ≤ x < y:     AA x; 0 <= x < y:
x:EE x:
x; x + 2 ≠ z: EE x; x+2 != z:

(Between ; and :, not all operators are available)
reasoning
symbol  type comment
==>
<==
<=>unifies U and F
===does not unify U and F
subproofstarts a sub-reasoning
subendends a sub-reasoning
originalrefers to the first formula of the (sub-)reasoning
A global assumption (i.e., axiom) may be added to the front, e.g.: assume x > 3 \/ x = y;
arithmetic
symboltype
<<
<=
==
!=
>=
>>
++
-
3y3y
y ⋅ 3y*3
|2x − 5||2x-5|
 x + 1 6
(x+1)/6
2
 3 4
2 3/4
(3 + 4)(x + 5)    (3+4)(x+5)

# Undefined Terms in Practical Mathematical Reasoning

Antti Valmari
University of Jyväskylä
2020-10-09

## Background

I have been developing a tool for giving students feedback on math, logic and TCS exercises. Feel free to try the interactive material in this talk! You may modify given answers as much as you want.

http://users.jyu.fi/~ava/practical_logic3.html

Simplify
 2 sin 2α
.

or

The alphabet is {a, b}. Write a grammar for the strings that contain equally many as as bs, in arbitrary order.
ban ambiguity

or

To promote thinking skills, the tool should allow different approaches to a problem.

Solve 2x + 3y = 6 ∧ y − x = 7.

or

Try also this (paint, copy, drop):
==> y = x+7
original ==> 2x+3(x+7) = 6 <=> 5x = -15 <=> x = -3
original ==> y = -3+7 = 4
original <=> x = -3 /\ y = 4

Undefined expressions are everywhere!

Simplify
 r 2 + r − 6 r − 2
.

or

Write a formula saying that the contents of the array A[1…n] constitute a palindrome.

or

To make my tool work, I needed a first-order logic that deals with undefined expressions. Unfortunately, what I found in the literature was unsuitable. Consider solving

 r 2 + r − 6 r − 2
= 8

r ≠ 2 ∧
 r 2 + r − 6 r − 2
= 8
⇔  r ≠ 2 ∧ r2 + r − 6 = 8(r − 2)  ⇔  …
⇔  r ≠ 2 ∧ (r = 2 ∨ r = 5)
⇔  r = 5

But I was taught at school to do this:

 r 2 + r − 6 r − 2
= 8
⇔  r ≠ 2 ∧ r2 + r − 6 = 8(r − 2)  ⇔  …
⇔  r = 5

Indeed, that 2 must be rejected, should not be given by the teacher but found out by the student.

So I became a Raider of the Lost School Logic.

## The Logic

Should be applicable to any domain of discourse in the usual sense.
ℝ, +, −, ⋅, /, |…| (only linear)
ℕ, +, ⋅, div c, mod c (only linear)

or
We should have

 1 x
≥ 0  ⇔  x > 0

 1 x
< 0  ⇔  ¬(
 1 x
≥ 0)  ⇔  ¬(x > 0)  ⇔  x ≤ 0
?

or

Intuitively, the negation of undefined is undefined. So we use three truth values:

• T true
• F false
• U undefined

To use the logic for solving (in)equations, we need UF !

 1 x
≥ 0
x > 0
x < 0 FF
x = 0 UF
x > 0 TT

and are not logical connectives but reasoning operators

• we mimic their informal use in everyday math
• they do not yield truth values, but denote semantically correct or incorrect reasoning steps
• they are neither left nor right associative, but conjunctional

or
What do the the expression trees look like?

or
• logical connectives cannot be applied to them

or
• context information can be exploited

or
• resembles a bit Γ or Γ

When U must be distinguished from F, we use instead of .

 ⇒ F U T F ✓ ✓ ✓ U ✓ ✓ ✓ T ✓

 ⇔ F U T F ✓ ✓ U ✓ ✓ T ✓

 ≡ F U T F ✓ U ✓ T ✓

These arise very naturally:

 ¬ F T U U T F

 ∧ F U T F F F F U F U U T F U T

 ∨ F U T F F U T U U U T T T T T

Implication has two natural choices:

• S.C. Kleene:  PQ  ≡  ¬PQ
• Jan Łukasiewicz:
• UU  ≡  T
• otherwise  PQ  ≡  PQ

You may try propositional formulas and reasoning here.
U is not used
U is used

or

Variable and constant symbols are never undefined.

Each function symbol f (x1, …, xn) has an associated formula ⌊ f (x1, …, xn) ⌉ that tells when it is defined.

• For instance, ⌊ x ⌉ is
• x ≥ 0 on .
• y: y ⋅ y = x on .
• ⌊ f ⌉ may not use non-total function symbols.
• For instance, x ≥ 0 uses no function symbols at all.
• Therefore, every ⌊ f ⌉ is defined everywhere.
• If f is a total function, then ⌊ f ⌉ is T.
• ⌊…⌉ is not a symbol in the logic!
• ⌊ x ⌉ cannot be written as such in the logic.
• x ≥ 0 can.
• ⌊ x ⌉ in metalanguage refers to x ≥ 0 in the logic.

Example: adding x to first-order real closed fields

• Say that ⌊ x ⌉ is x ≥ 0.
• Add  x ≥ 0 → x ≥ 0 ∧ x ⋅ x = x  to the axioms.
• (Drop the standard square root axiom.)

A function call f (t1, …, tn) is undefined if and only if

• at least one ti is undefined, or
• ⌊ f ⌉ (t1, …, tn)  ≡  F .

A relation yields U if and only if at least one of its arguments is undefined.

• for instance,
 1 0
=  1 0
≡  U
• for instance, both
x ≥  1 0
and
x <  1 0
are undefined for every x ∈ ℝ
• no loss of generality, simplifies technicalities

x: φ(x) yields

• F, if φ(x) yields F for at least one x
• T, if φ(x) yields T for every x
• U, otherwise

x: φ(x) yields

• T, if φ(x) yields T for at least one x
• F, if φ(x) yields F for every x
• U, otherwise
Given the ⌊ f ⌉, there is a straightforward algorithm for computing ⌊ t ⌉ and ⌊ φ ⌉ such that ¬⌊ φ ⌉ holds if and only if φU.
• ⌊ f (t1, …, tn) ⌉  ≡  ⌊ t1 ⌉ ∧ … ∧ ⌊ tn ⌉ ∧ ⌊ f ⌉(t1, …, tn)
• examples
• ⌊ f ⌉  ≡  ⌊ f ⌉ ∧ f ≥ 0
• ⌊  f g
⌉  ≡  ⌊ f ⌉ ∧ ⌊ g ⌉ ∧ g ≠ 0
• ⌊ R(t1, …, tn) ⌉  ≡  ⌊ t1 ⌉ ∧ … ∧ ⌊ tn ⌉
• ⌊ ¬φ ⌉  ≡  ⌊ φ ⌉
• ⌊ φψ ⌉  ≡  ⌊ φ ⌉ ∧ ⌊ ψ ⌉ ∨ ⌊ φ ⌉ ∧ ¬φ ∨ ⌊ ψ ⌉ ∧ ¬ψ

## Propositional Reasoning

The most novel issues are on predicate side, so we must not stay here too long.

The law of the excluded middle has been replaced by the law of the excluded fourth.

x: φ(x) ∨ ¬φ(x) ∨ ¬⌊ φ(x) ⌉
• For instance,
x: x − 3 < 7 ∨ ¬( x − 3 < 7 ) ∨ ¬(x − 3 ≥ 0)
Whatever is true, is defined.
φ(x)  ⇒  ⌊ φ(x) ⌉
• For instance,  x − 3 < 7  ⇒  x − 3 ≥ 0
These imply that in a consistent theory, for any x, precisely one of φ(x), ¬φ(x) and ¬⌊ φ(x) ⌉ holds. The law of contraposition adopts many forms, including
If  φ  ⇒  ψ  then  ¬ψ ∨ ¬⌊ ψ ⌉  ⇒  ¬φ ∨ ¬⌊ φ ⌉  .

In addition to the above, in a long textbook list of laws, only the following have to be dropped:

• P ∧ ¬P is not always F
• PP and PP are not always T
• P ∨ ¬PQ is not always PQ
• But it is the “or” of many programming languages!
• It crashes if and only if P crashes or PF and Q crashes
• P ∧ (¬PQ) is not always PQ
• it is the “and” of many programming languages

An observation

• In two-valued logic, φψ if and only if Γφψ.
• In our logic, UF but UF  ≡  UF  ≡  U.
• Therefore, not every instance of φψ can be derived by modus ponens.
• As a consequence, has minor role in our logic.

## Intro to the Rest

A relation is undefined if and only if at least one argument is

• many familiar laws remain valid, e.g.,  ¬( f(t) > g(t) ) ≡ f(t) ≤ g(t) ≡ f(t) < g(t) ∨ f(t) = g(t)
• t = t must be restricted to defined terms

Not much changes in a long list of quantifier laws

• If t is free for x in φ, then ⌊ t ⌉ ∧ ∀ x: φ(x)  ⇒  φ(t)
• If t is free for x in φ, then ⌊ t ⌉ ∧ φ(t)  ⇒  ∃ x: φ(x)
• If is dropped, then  φ(t)  ⇒  ∃ x: φ(x)

The only remaining issue needs a long story!

• substitution of a term or sub-formula by an equivalent term or formula

## Regularity

S.C. Kleene introduced it for propositional formulas. It is assumed by important laws, so we need to grasp it.

A propositional formula φ(P) is regular if and only if for each truth value combination of other propositions than P
• φ(U) ≡ U  or
• φ(F) ≡ φ(U) ≡ φ(T).

Negation is regular, because ¬UU.

Conjunction is regular:

 ∧ F U T F F F F U F U U T F U T
• the first row is constant F
• the other rows have U in the U-column
• a similar argument holds for the columns

If a propositional formula is composed only using regular connectives, then it is regular.

Any propositional formula composed only using ¬, , , Kleene implication , and/or Kleene equivalence is regular.

Łukasiewicz implication is not regular, because UUT and TUU.

Let denote any undefined term. A first-order formula φ(x) is regular if and only if for each value combination of other free variables than x,
• φ(⊥) ≡ U  or
• x: φ(x) ≡ φ(⊥).

Any first-order formula composed only using ¬, , , , , and/or is regular.

The following lemma is useful.

Let φ(…) be a formula that contains no other logical symbols than ¬, , , and . Assume that is within the scope of an even number of negations. Either φ(ψ) does not depend on ψ or φ(ψ) ⇒ ψ.

Proof

• Assume that φ(ψ) depends on ψ.
• By regularity φ(U) ≡ U.
• By even number of negations, φ(F) ≡ F or φ(F) ≡ U.
• Thus if φ(ψ) ≡ T, then ψT.

## Replacing an Undefined Term by a Defined Term

Throughout Sections 6 to 8 we assume that no free variable becomes bound nor the other way round in the substitutions.

With the theorem in this section, reasoning can proceed towards terms that are defined everywhere.

• For instance,
 1 x
−  1 x
may be replaced by 0.

An example

or

Assumptions of the theorem:

• t is a term
• for instance,  t =
 1 x
−  1 x
• t is a term, which yields the same value as t whenever t is defined
• that is,  ⌊t⌉  ⇒  t = t
• for instance,  t = 0
• indeed
x ≠ 0  ⇒   1 x
−  1 x
= 0
• R(…) is a relation
• for instance,  R(…)  ≡  … ≤ 1
• φ( R(t) ) is a formula, where t occurs as an argument of R, and where no other logical symbols than ¬, , , and occur
• for instance,
φ( R(t) )  ≡
x ≤ − 2 ∨ x ≥ 0 ∧  1 x
−  1 x
≤ 1
• this rules out
• χ is a formula such that  ⌊t⌉  ⇒  χ  ⇒  ⌊t⌉ ∨ ¬⌊t′⌉
• for instance,  χ  ≡  x ≠ 0
• χ holds whenever t is defined, and in a user-chosen collection of situations where neither term is defined

Claims of the theorem:

• If R(t) is within the scope of an even number of negations, then
φ( R(t) )  ⇔  φ( χR(t′) )
• for instance,
x ≤ − 2  ∨  x ≥ 0  ∧   1 x
−  1 x
≤ 1
⇔   x ≤ − 2  ∨  x ≥ 0  ∧  (x ≠ 0 ∧ 0 ≤ 1)
• If R(t) is within the scope of an odd number of negations, then
φ( R(t) )  ⇔  φ( ¬χR(t′) )

An example

or

Proof in the even case

• If φ(…) does not depend on , then the claim is obvious.
• Otherwise, because of regularity, φ(U) ≡ U.
• If φ( R(t) ) then R(t) and t, thus χ and R(t′), so φ( χR(t′) ).
• If φ( χR(t′) ) then χ and R(t′) and t′⌉, thus t, so φ( R(t) ).

The odd case reduces to the even case by replacing ¬R(t) by χ ∧ ¬R(t′) in φ( ¬¬R(t) ).

The theorem is useful even if t and t are the same!

• The choice χ ≡ ⌊t makes the sub-formula defined everywhere, facilitating familiar two-valued thinking.

## A Unidirectional Replacement Theorem

This law is easy to use and allows all logical symbols, but the validity of the roots must be checked at the end.

If  ⌊t⌉  ⇒  t = t′  and φ( R(…) ) is regular, then  φ( R(t) )  ⇒  φ( R(t′) ) .

An example

or

Proof

• If t, then t = t, R(t) ≡ R(t′) and φ( R(t) ) ≡ φ( R(t′) ).
• If ¬ ⌊t, then R(t) ≡ U. Because of regularity, either φ(…) does not depend on , implying φ( R(t) ) ≡ φ( R(t′) ); or φ( R(t) ) ≡ φ(U) ≡ Uφ( R(t′).

A counter-example if φ is not regular

 P *P F T U F T T
• Let φ( R(t) ) be ¬ *(x = 0).
• We have
¬ *( 1 0
−  1 0
= 0)  ≡  T
but
¬ *(0 = 0)  ≡  F
.

## Replacement of a sub-formula

Let φ(…) be a formula that contains no other logical symbols than ¬, , , and . Assume that is within the scope of an even number of negations. If ψ ⇒ ψ then φ(ψ) ⇒ φ(ψ′).

Proof

• If φ(…) does not depend on , then the claim is obvious.
• Otherwise, because of regularity, φ(U) ≡ U. Thus if φ(ψ), then ψ, ψ and φ(ψ′).

Corollary:

If φ(…) is like above, then φ(ψ) ⇒ φ( ⌊ψ⌉ ∧ ψ ).

Example:

 … ∨ √x < 3 ∧ … ⇒ … ∨ (x ≥ 0 ∧ √x < 3) ∧ …

To deal with an odd number of negations, replace ¬ψ in φ(¬¬ψ).

Finally we mention that

φψ  ≡  ¬φψ ∨ ¬( ⌊ φ ⌉ ∨ ⌊ ψ ⌉ )

## Concluding Remarks

Key ideas
• Reasoning operators are clearly distinguished from logical connectives, and from .
• Variables are never undefined, terms may be.
• In laws, ⌊ φ ⌉ is used instead of U.
• Regularity underlies many laws.
Observations
• loses its significance.
• The most dramatic differences to reasoning in traditional logic are in substitutions.
• Programming language “and” and “or” are obtained naturally.

Implementations

• (ℝ, +, −, ⋅, /, |…|) (only linear)
• decidable, but horrible problem complexity
• atomic formulas are inequalities
• formulas are in DNF
• Fourier–Motzkin quantifier elimination
• |…| are converted to individual cases
• division by a linear term is allowed, if multiplying it out makes the relation linear
• non-trivial trickery to delay run time explosion
• also general polynomials are decidable, but does not look promising
• future dream: very liberal expressions for one free variable by semi-numerical methods
• (ℕ, +, ⋅, div c, mod c) (only linear)
• decidable, but horrible problem complexity
• deterministic finite automata
• numbers are in binary, with arbitrary many leading 0s, LSB first
• each DFA represents a set of tuples of numbers, interleaved
• direct compilation of relation to DFA when div and mod are not used
• fast brief practical DFA minimization

Thank you for attention!