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

  1. Background
  2. The Logic
  3. Propositional Reasoning
  4. Intro to the Rest
  5. Regularity
  6. Replacing an Undefined Term by a Defined Term
  7. A Unidirectional Replacement Theorem
  8. Replacement of a sub-formula
  9. Concluding Remarks

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
r2 + 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

r2 + r − 6
r − 2
= 8

They advocated this:

r ≠ 2 ∧
r2 + 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:

r2 + 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
How about
 
1
x
< 0  ⇔  ¬(
1
x
≥ 0)  ⇔  ¬(x > 0)  ⇔  x ≤ 0
?


or

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

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

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:

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.

Example: adding x to first-order real closed fields

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

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

x: φ(x) yields

x: φ(x) yields

Given the ⌊ f ⌉, there is a straightforward algorithm for computing ⌊ t ⌉ and ⌊ φ ⌉ such that ¬⌊ φ ⌉ holds if and only if φU.

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) ⌉
Whatever is true, is defined.
φ(x)  ⇒  ⌊ φ(x) ⌉
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:

An observation

Intro to the Rest

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

Not much changes in a long list of quantifier laws

The only remaining issue needs a long story!

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

Negation is regular, because ¬UU.

Conjunction is regular:

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

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,

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

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.

An example

or

Assumptions of the theorem:

Claims of the theorem:

An example

or

Proof in the even case

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!

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

A counter-example if φ is not regular

P  *P
F  T
U  F
T  T

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

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 Observations

Implementations

Thank you for attention!