Typing:

propositional

symbol | type | comment |
---|---|---|

∧ | /\ | |

∨ | \/ | |

¬ | ! | |

F | FF | |

T | TT | |

U | UU | |

→ | --> | |

↔ | <-> | |

&& | && | short-circuit and |

|| | || | short-circuit or |

↠ | ->> | Łukasiewicz implication |

quantifiers

(Between ; and :, not all operators are available)

symbol | type |
---|---|

∀ 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

A global assumption (i.e., axiom) may be added to the front, e.g.:
`assume x > 3 \/ x = y;`

symbol | type | comment |
---|---|---|

⇒ | ==> | |

⇐ | <== | |

⇔ | <=> | unifies U and
F |

≡ | === | does not unify U
and F |

subproof | starts a sub-reasoning | |

subend | ends a sub-reasoning | |

original | refers to the first formula of the (sub-)reasoning |

arithmetic

symbol | type | ||
---|---|---|---|

< | < | ||

≤ | <= | ||

= | = | ||

≠ | != | ||

≥ | >= | ||

> | > | ||

+ | + | ||

− | - | ||

3y | 3y | ||

y ⋅ 3 | y*3 | ||

|2x − 5| | |2x-5| | ||

| (x+1)/6 | ||

2
| 2 3/4 | ||

(3 + 4)(x + 5) | (3+4)(x+5) |

**Antti Valmari**

University of Jyväskylä

2020-10-09

- Background
- The Logic
- Propositional Reasoning
- Intro to the Rest
- Regularity
- Replacing an Undefined Term by a Defined Term
- A Unidirectional Replacement Theorem
- Replacement of a sub-formula
- Concluding Remarks

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

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

Undefined expressions are everywhere!

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

= 8

r^{2}+r− 6r− 2

They advocated this:

r≠ 2 ∧= 8

r^{2}+r− 6r− 2

⇔r≠ 2 ∧r^{2}+r− 6 = 8(r− 2) ⇔ …

⇔r≠ 2 ∧ (r= 2 ∨r= 5)

⇔r= 5

But I was taught at school to do this:

= 8

r^{2}+r− 6r− 2

⇔r≠ 2 ∧r^{2}+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.

We should have

≥ 0 ⇔ *x* > 0

1 |

x |

How about

< 0 ⇔ ¬(

≥ 0) ⇔ ¬(*x* > 0) ⇔ *x* ≤ 0 ?

1 |

x |

1 |

x |

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** !

≥ 0

1 xx> 0x< 0FFx= 0UFx> 0TT

⇔ 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
- logical connectives cannot be applied to them
- context information can be exploited
- ⇒ resembles a bit
*Γ*⊨ or*Γ*⊢

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

⇒ FUTF✓ ✓ ✓ U✓ ✓ ✓ T✓

⇔ FUTF✓ ✓ U✓ ✓ T✓

≡ FUTF✓ U✓ T✓

These arise very naturally:

¬ FTUUTF

∧ FUTFFFFUFUUTFUT

∨ FUTFFUTUUUTTTTT

Implication has two natural choices:

- S.C. Kleene:
*P*→*Q*≡ ¬*P*∨*Q* - Jan Łukasiewicz:
**U**↠**U**≡**T**- otherwise
*P*↠*Q*≡*P*→*Q*

Variable and constant symbols are never undefined.

Each function symbol *f* (*x*_{1}, …,
*x _{n}*) has an associated formula ⌊

- 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.

- For instance,
- 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

- 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*_{1}, …,
*t _{n}*) is undefined if and only if

- at least one
*t*is undefined, or_{i} - ⌊
*f*⌉ (*t*_{1}, …,*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 and
*x*≥1 0 are undefined for every*x*<1 0 *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

- ⌊
*f*(*t*_{1}, …,*t*) ⌉ ≡ ⌊_{n}*t*_{1}⌉ ∧ … ∧ ⌊*t*⌉ ∧ ⌊_{n}*f*⌉(*t*_{1}, …,*t*)_{n} - examples
- ⌊ √
*f*⌉ ≡ ⌊*f*⌉ ∧*f*≥ 0 - ⌊

⌉ ≡ ⌊*f**g**f*⌉ ∧ ⌊*g*⌉ ∧*g*≠ 0

- ⌊
*R*(*t*_{1}, …,*t*) ⌉ ≡ ⌊_{n}*t*_{1}⌉ ∧ … ∧ ⌊*t*⌉_{n} - ⌊ ¬
*φ*⌉ ≡ ⌊*φ*⌉ - ⌊
*φ*∧*ψ*⌉ ≡ ⌊*φ*⌉ ∧ ⌊*ψ*⌉ ∨ ⌊*φ*⌉ ∧ ¬*φ*∨ ⌊*ψ*⌉ ∧ ¬*ψ* - …

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)

φ(x) ⇒ ⌊φ(x) ⌉

- For instance, √
*x*− 3 < 7 ⇒*x*− 3 ≥ 0

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.

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*)

- If ↠ is dropped, then

The only remaining issue needs a long story!

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

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 ¬**U** ≡ **U**.

Conjunction is regular:

∧ FUTFFFFUFUUTFUT

- 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**.

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**.

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,
may be replaced by 0.

−1 *x*1 *x*

Assumptions of the theorem:

*t*is a term- for instance,
*t*=

−1 *x*1 *x*

- for instance,
*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*

= 01 *x*

- that is, ⌊
*R*(…) is a relation- for instance,
*R*(…) ≡ … ≤ 1

- for instance,
*φ*(*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*

≤ 11 *x* - this rules out ↠

- for instance,
*χ*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

- for instance,

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*

≤ 11 *x*⇔ *x*≤ − 2 ∨*x*≥ 0 ∧ (*x*≠ 0 ∧ 0 ≤ 1)

- for instance,
- If
*R*(*t*) is within the scope of an odd number of negations, then*φ*(*R*(*t*) ) ⇔*φ*( ¬*χ*∨*R*(*t*′) )

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*) ).

- If

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.

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*′) ) .

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* PFTUFTT

- Let
*φ*(*R*(*t*) ) be ¬ *(*x*= 0). - We have ¬ *(but

−1 0

= 0) ≡1 0 **T**¬ *(0 = 0) ≡.**F**

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

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

- 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.

- → 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!