Typing:

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α

.
ok_text Right! f_nodes 5 /* Thank you for trying! */ 2 / sin 2 al=(2(sin^2 al + cos² al))/(2 sin al cos al) = (sin al) / cos l + (cos al) / sin al = tan al + cot al + 0
or

The alphabet is {a, b}. Write a grammar for the strings that contain equally many as as bs, in arbitrary order.
ok_text Right! CFG_set X ::= "" | aXbX | bXaX ; CFG_set2 ban ambiguity
X ::= "" | aAbX | bBaX A ::= "" | aAbA B ::= "" | bBaX ;CFG_compare
or

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

Solve 2x + 3y = 6 ∧ y − x = 7.
ok_text Right! real_logic f_nodes 8 solve_all 2x + 3y = 6 ∧ y − x = 7<=> 2x+3y = 6 /\ 2y-2x = 2*7 <=> 2x+3y = 6 /\ 2x+3y + 2y-2x = 6 + 14 <=> 2x+3y = 6 /\ 5y = 20 <=> 2x+3*4 = 6 /\ y = 4 <=> x = -3 /\ y = 4
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

 .
ok_text This entry has been designed to illustrate that undefined expressions are a problem. It has no better answer than the original input, I am sorry. arithmetic f_nodes 11 (r^2+r-6)/(r-2) = r+3
or

Write a formula saying that the contents of the array A[1…n] constitute a palindrome.
ok_text Right! fail_text This one you can fix! array_claim A[1...n] AA i; 1 <= i <= n: A[i] = A[n+1-i] === AA i; 1 <= i <= n: A[i] = A[n-i]
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

They advocated this:

r ≠ 2 ∧

r 2 + r − 6

r − 2

= 8
⇔  r ≠ 2 ∧ r ² + 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 ∧ r ² + 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)
ok_text Right! AA x: AA y; x < y: EE z: x < z < y
or

ok_text Right! real_logic 1/x >= 0 <=> x > 0 real_logic 1/x < 0 <=> !(1/x >= 0) <=> !(x > 0) <=> x <= 0 real_logic !(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 U ⇔ F !

	1 x ≥ 0	x > 0
x < 0	F	F
x = 0	U	F
x > 0	T	T

⇔ 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
  ok_text Right! real_logic x > 1 ==> x > 0 ==> x > 1 real_logic x > 1 --> x > 0 --> x > 1
  or
  What do the the expression trees look like?
  ok_text Right! tree_compare x > 1 ==> x > 0 ==> x > 1 ; x > 1 --> x > 0 --> x > 1
  or
• logical connectives cannot be applied to them
  ok_text Right! real_logic !(x > 1 ==> x > 0)
  or
• context information can be exploited
  ok_text Seems weird but is correct! real_logic assume x < 0; |x| = 4 ==> x = -4 real_logic assume x < -1 /\ x >= y /\ y = |y|; 1 > 0 ==> 0 = 1
  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:  P → Q  ≡  ¬P ∨ Q
• Jan Łukasiewicz:
  • U ↠ U  ≡  T
  • otherwise  P ↠ Q  ≡  P → Q

You may try propositional formulas and reasoning here.
U is not used
U is used
ok_text Right! (P ->> Q) /\ (P \/ !P \/ Q \/ !Q) === P --> Q ==> P ->> Q <=> P --> Q
or

Variable and constant symbols are never undefined.

Each function symbol f (x₁, …, x_n) has an associated formula ⌊ f (x₁, …, x_n) ⌉ 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.
• To declare that f is a total function, choose T as ⌊ f ⌉.
• ⌊…⌉ 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

• Add √  to the signature.
• 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 (t₁, …, t_n) is undefined if and only if

• at least one t_i is undefined, or
• ⌊ f ⌉ (t₁, …, t_n)  ≡  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 (t₁, …, t_n) ⌉  ≡  ⌊ t₁ ⌉ ∧ … ∧ ⌊ t_n ⌉ ∧ ⌊ f ⌉(t₁, …, t_n)
• examples
  • ⌊ √f  ⌉  ≡  ⌊ f ⌉ ∧ f ≥ 0
  • ⌊ 

    f

    g

     ⌉  ≡  ⌊ f ⌉ ∧ ⌊ g ⌉ ∧ g ≠ 0
• ⌊ R(t₁, …, t_n) ⌉  ≡  ⌊ t₁ ⌉ ∧ … ∧ ⌊ t_n ⌉
• ⌊ ¬φ ⌉  ≡  ⌊ φ ⌉
• ⌊ φ ∧ ψ ⌉  ≡  ⌊ φ ⌉ ∧ ⌊ ψ ⌉ ∨ ⌊ φ ⌉ ∧ ¬φ ∨ ⌊ ψ ⌉ ∧ ¬ψ
• …

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
• P → P and P ↔ P are not always T
• P ∨ ¬P ∧ Q is not always P ∨ Q
  • But it is the “or” of many programming languages!
  • It crashes if and only if P crashes or P ≡ F and Q crashes
• P ∧ (¬P ∨ Q) is not always P ∧ Q
  • it is the “and” of many programming languages

An observation

• In two-valued logic, φ ⇒ ψ if and only if Γ ⊨ φ → ψ.
• In our logic, U ⇒ F but U → F  ≡  U ↠ F  ≡  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.

Negation is regular, because ¬U ≡ U.

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 U ↠ U ≡ T and T ↠ U ≡ U.

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
ok_text Right! real_logic solve_all 1/|x| <= 1/x + 1 === x < 0 /\ 1/(-x) <= 1/x + 1 \/ x >= 0 /\ 1/x <= 1/x + 1 === x < 0 /\ -1 >= 1 + x \/ x >= 0 /\ 1/x - 1/x <= 1 === x <= -2 \/ x >= 0 /\ 1/x - 1/x <= 1 <=> x <= -2 \/ x >= 0 /\ 0 <= 1 <=> x <= -2 \/ x >= 0 /\ #(x != 0 /\ 0 <= 1#) === x <= -2 \/ x > 0
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
ok_text Right! real_logic solve_all !(1/|x| > 1/x + 1) === x < 0 /\ !(1/(-x) > 1/x + 1) \/ x >= 0 /\ !(1/x > 1/x + 1) === x < 0 /\ !(-1 < 1 + x) \/ x >= 0 /\ !(1/x - 1/x > 1) === x <= -2 \/ x >= 0 /\ !(1/x - 1/x > 1) <=> x <= -2 \/ x >= 0 /\ !(x != 0 /\ 0 > 1) === x <= -2 \/ x >= 0 <=> x <= -2 \/ x >= 0 /\ !(!(x != 0) \/ 0 > 1) === x <= -2 \/ x >= 0 /\ !(!(x != 0)) === x <= -2 \/ x > 0
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 also allows → and ↔, 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
ok_text Right! real_logic solve_all (|3x|-15)/(x-5) = 2 <=> |3x|-15 = 2(x-5) ==> |3x|-15 = 2(x-5) subproof /*The case `3x < 0`*/ -3x-15 = 2x-10 === 5x = -5 === x = -1 ==> 3x = -3 < 0 subend subproof /*The case `3x >= 0`*/ 3x-15 = 2x-10 === x = 5 ==> 3x = 15 >= 0 subend original <=> x=-1
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

• Let  *P  ≡  ¬ (P ↠ ¬ P) ∨ ¬ (¬ P ↠ P).

  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!