logo

Weak Cardinality Theorems for First-Order Logic

Till Tantau

Fakultät für Elektrotechnik und Informatik

Technische Universität Berlin

Fundamentals of Computation Theory 2003

logo^{History  Unification by Logic  Applications  Summary}

Outline

1 History

Enumerability in Recursion and Automata Theory Known Weak Cardinality Theorem Why Do Cardinality Theorems Hold Only for Certain Models?

2 Unification by First-Order Logic

Elementary Definitions Enumerability for First-Order Logic Weak Cardinality Theorems for First-Order Logic

1 History

Enumerability in Recursion and Automata Theory Known Weak Cardinality Theorem Why Do Cardinality Theorems Hold Only for Certain Models?

2 Unification by First-Order Logic

Elementary Definitions Enumerability for First-Order Logic Weak Cardinality Theorems for First-Order Logic

logo

History  Unification by Logic  Applications  Summary

Enumerability in Recursion and Automata Theory

Motivation of Enumerability

Problem Many functions are not computable or not efficiently computable.

We are working on this picture.

Example

#SAT:

How many satisfying assignments does a formula have?

logo

History  Unification by Logic  Applications  Summary

Enumerability in Recursion and Automata Theory

Motivation of Enumerability

Problem Many functions are not computable or not efficiently computable.

We are working on this picture.

Example

For difficult languages A:

Cardinality function #_{A}^{n}:

How many input words are in A?

Characteristic function χ_{A}^{n}: Which input words are in A?

(w_{1}, w_{2}, w_{3}, w_{4}, w_{5}) in A 2 01001 #_{A}^{5} χ_{A}^{5}

logo

History  Unification by Logic  Applications  Summary

Enumerability in Recursion and Automata Theory

Motivation of Enumerability

Problem Many functions are not computable or not efficiently computable.

We are working on this picture.

Solutions Difficult functions can be

computed using probabilistic algorithms, computed efficiently on average, approximated, or enumerated.

logo

History  Unification by Logic  Applications  Summary

Enumerability in Recursion and Automata Theory

Enumerators Output Sets of Possible Function Values

output tape input tapes ⋮w_{1} w_{n} computerimage input tapes ⋮w_{1} w_{n} Definition (1987, 1989, 1994, 2001) An m-enumerator for a function f

1 reads n input words w_{1}, …, w_{n}, 2 does a computation, 3 outputs at most m values, 4 one of which is f (w_{1}, …, w_{n}).

logo

History  Unification by Logic  Applications  Summary

Enumerability in Recursion and Automata Theory

Enumerators Output Sets of Possible Function Values

output tape input tapes ⋮w_{1} w_{n} computerimage input tapes ⋮w_{1} w_{n} Definition (1987, 1989, 1994, 2001) An m-enumerator for a function f

1 reads n input words w_{1}, …, w_{n}, 2 does a computation, 3 outputs at most m values, 4 one of which is f (w_{1}, …, w_{n}).

logo

History  Unification by Logic  Applications  Summary

Enumerability in Recursion and Automata Theory

Enumerators Output Sets of Possible Function Values

output tape input tapes ⋮w_{1} w_{n} computerimage input tapes ⋮w_{1} w_{n} Definition (1987, 1989, 1994, 2001) An m-enumerator for a function f

1 reads n input words w_{1}, …, w_{n}, 2 does a computation, 3 outputs at most m values, 4 one of which is f (w_{1}, …, w_{n}).

logo

History  Unification by Logic  Applications  Summary

Enumerability in Recursion and Automata Theory

Enumerators Output Sets of Possible Function Values

output tape input tapes ⋮w_{1} w_{n} computerimage input tapes ⋮w_{1} w_{n} Definition (1987, 1989, 1994, 2001) An m-enumerator for a function f

1 reads n input words w_{1}, …, w_{n}, 2 does a computation, 3 outputs at most m values, 4 one of which is f (w_{1}, …, w_{n}).

logo

History  Unification by Logic  Applications  Summary

Enumerability in Recursion and Automata Theory

Enumerators Output Sets of Possible Function Values

output tape input tapes ⋮w_{1} w_{n} computerworkingimage input tapes ⋮w_{1} w_{n} Definition (1987, 1989, 1994, 2001) An m-enumerator for a function f

1 reads n input words w_{1}, …, w_{n}, 2 does a computation, 3 outputs at most m values, 4 one of which is f (w_{1}, …, w_{n}).

logo

History  Unification by Logic  Applications  Summary

Enumerability in Recursion and Automata Theory

Enumerators Output Sets of Possible Function Values

output tape input tapes ⋮w_{1} w_{n} computerimage input tapes ⋮w_{1} w_{n} u_{1} Definition (1987, 1989, 1994, 2001) An m-enumerator for a function f

1 reads n input words w_{1}, …, w_{n}, 2 does a computation, 3 outputs at most m values, 4 one of which is f (w_{1}, …, w_{n}).

logo

History  Unification by Logic  Applications  Summary

Enumerability in Recursion and Automata Theory

Enumerators Output Sets of Possible Function Values

output tape input tapes ⋮w_{1} w_{n} computerimage input tapes ⋮w_{1} w_{n} u_{1} u_{2} Definition (1987, 1989, 1994, 2001) An m-enumerator for a function f

1 reads n input words w_{1}, …, w_{n}, 2 does a computation, 3 outputs at most m values, 4 one of which is f (w_{1}, …, w_{n}).

logo

History  Unification by Logic  Applications  Summary

Enumerability in Recursion and Automata Theory

Enumerators Output Sets of Possible Function Values

output tape input tapes ⋮w_{1} w_{n} computerimage input tapes ⋮w_{1} w_{n} u_{1} u_{2} u_{3} Definition (1987, 1989, 1994, 2001) An m-enumerator for a function f

1 reads n input words w_{1}, …, w_{n}, 2 does a computation, 3 outputs at most m values, 4 one of which is f (w_{1}, …, w_{n}).

logo

History  Unification by Logic  Applications  Summary

Enumerability in Recursion and Automata Theory

Enumerators Output Sets of Possible Function Values

output tape input tapes ⋮w_{1} w_{n} computerimage input tapes ⋮w_{1} w_{n} u_{1} u_{2} u_{3} Definition (1987, 1989, 1994, 2001) An m-enumerator for a function f

1 reads n input words w_{1}, …, w_{n}, 2 does a computation, 3 outputs at most m values, 4 one of which is f (w_{1}, …, w_{n}).

History  Unification by Logic  Applications  Summary

Known Weak Cardinality Theorem

How Well Can the Cardinality Function Be Enumerated?

Observation For fixed n, the cardinality function #_{A}^{n}

can be 1-enumerated by Turing machines only for recursive A, but can be (n + 1)-enumerated for every language A.

Question What about 2-, 3-, 4-, …, n-enumerability?

History  Unification by Logic  Applications  Summary

Known Weak Cardinality Theorem

How Well Can the Cardinality Function Be Enumerated?

Observation For fixed n, the cardinality function #_{A}^{n}

can be 1-enumerated by Turing machines only for recursive A, but can be (n + 1)-enumerated for every language A.

Question What about 2-, 3-, 4-, …, n-enumerability?

logo

History  Unification by Logic  Applications  Summary

Known Weak Cardinality Theorem

How Well Can the Cardinality Function Be Enumerated by Turing Machines?

Cardinality Theorem (Kummer, 1992) If #_{A}^{n} is n-enumerable by a Turing machine, then A is recursive.

Weak Cardinality Theorems (1987, 1989, 1992)

1 If χ_{A}^{n} is n-enumerable by a Turing machine, then A is

recursive. 2 If #_{A}^{2} is 2-enumerable by a Turing machine, then A is

recursive. 3 If #_{A}^{n} is n-enumerable by a Turing machine that never

enumerates both 0 and n, then A is recursive.

logo

History  Unification by Logic  Applications  Summary

Known Weak Cardinality Theorem

How Well Can the Cardinality Function Be Enumerated by Turing Machines?

Cardinality Theorem (Kummer, 1992) If #_{A}^{n} is n-enumerable by a Turing machine, then A is recursive.

Weak Cardinality Theorems (1987, 1989, 1992)

1 If χ_{A}^{n} is n-enumerable by a Turing machine, then A is

recursive. 2 If #_{A}^{2} is 2-enumerable by a Turing machine, then A is

recursive. 3 If #_{A}^{n} is n-enumerable by a Turing machine that never

enumerates both 0 and n, then A is recursive.

logo

History  Unification by Logic  Applications  Summary

Known Weak Cardinality Theorem

How Well Can the Cardinality Function Be Enumerated by Turing Machines?

Cardinality Theorem (Kummer, 1992) If #_{A}^{n} is n-enumerable by a Turing machine, then A is recursive.

Weak Cardinality Theorems (1987, 1989, 1992)

1 If χ_{A}^{n} is n-enumerable by a Turing machine, then A is

recursive. 2 If #_{A}^{2} is 2-enumerable by a Turing machine, then A is

recursive. 3 If #_{A}^{n} is n-enumerable by a Turing machine that never

enumerates both 0 and n, then A is recursive.

logo

History  Unification by Logic  Applications  Summary

Known Weak Cardinality Theorem

How Well Can the Cardinality Function Be Enumerated by Turing Machines?

Cardinality Theorem (Kummer, 1992) If #_{A}^{n} is n-enumerable by a Turing machine, then A is recursive.

Weak Cardinality Theorems (1987, 1989, 1992)

1 If χ_{A}^{n} is n-enumerable by a Turing machine, then A is

recursive. 2 If #_{A}^{2} is 2-enumerable by a Turing machine, then A is

recursive. 3 If #_{A}^{n} is n-enumerable by a Turing machine that never

enumerates both 0 and n, then A is recursive.

logo

History  Unification by Logic  Applications  Summary

Known Weak Cardinality Theorem

How Well Can the Cardinality Function Be Enumerated by Finite Automata?

Conjecture If #_{A}^{n} is n-enumerable by a finite automaton, then A is regular.

Weak Cardinality Theorems (2001, 2002)

1 If χ_{A}^{n} is n-enumerable by a finite automaton, then A is

regular. 2 If #_{A}^{2} is 2-enumerable by a finite automaton, then A is

regular. 3 If #_{A}^{n} is n-enumerable by a finite automaton that never

enumerates both 0 and n, then A is regular.

logo

History  Unification by Logic  Applications  Summary

Why Do Cardinality Theorems Hold Only for Certain Models?

Cardinality Theorems Do Not Hold for All Models

Turing machines finite automataWeak cardinality theorems hold. Weak cardinality theorems hold.

logo

History  Unification by Logic  Applications  Summary

Why Do Cardinality Theorems Hold Only for Certain Models?

Cardinality Theorems Do Not Hold for All Models

Turing machines resource-bounded machines Weak cardinality theorems do not hold. finite automataWeak cardinality theorems hold. Weak cardinality theorems hold.

logo

History  Unification by Logic  Applications  Summary

Why Do Cardinality Theorems Hold Only for Certain Models?

Why?

First Explanation The weak cardinality theorems hold both for recursion and automata theory by coincidence.

Second Explanation The weak cardinality theorems hold both for recursion and automata theory, because they are instantiations of single, unifying theorems.

The second explanation is correct. The theorems can (almost) be unified using first-order logic.

logo

History  Unification by Logic  Applications  Summary

Why Do Cardinality Theorems Hold Only for Certain Models?

Why?

First Explanation The weak cardinality theorems hold both for recursion and automata theory by coincidence.

Second Explanation The weak cardinality theorems hold both for recursion and automata theory, because they are instantiations of single, unifying theorems.

The second explanation is correct. The theorems can (almost) be unified using first-order logic.

1 History

Enumerability in Recursion and Automata Theory Known Weak Cardinality Theorem Why Do Cardinality Theorems Hold Only for Certain Models?

2 Unification by First-Order Logic

Elementary Definitions Enumerability for First-Order Logic Weak Cardinality Theorems for First-Order Logic

logo

History  Unification by Logic  Applications  Summary

Elementary Definitions

What Are Elementary Definitions?

Definition A relation R is elementarily definable in a logical structure S if

1 there exists a first-order formula ϕ, 2 that is true exactly for the elements of R.

Example The set of even numbers is elementarily definable in (ℕ, +) via the formula ϕ(x) ≡ ∃z ▪ z + z = x.

Example The set of powers of 2 is not elementarily definable in (ℕ, +).

History  Unification by Logic  Applications  Summary

Elementary Definitions

Characterisation of Classes by Elementary Definitions

Theorem (Büchi, 1960) There exists a logical structure (ℕ, +, e_{2}) such that a set A ⊆ ℕ is regular iff it is elementarily definable in (ℕ, +, e_{2}).

Theorem There exists a logical structure R such that a set A ⊆ ℕ is recursively enumerable iff it is positively elementarily definable in R.

logo

History  Unification by Logic  Applications  Summary

Elementary Definitions

Characterisation of Classes by Elementary Definitions

regular sets (ℕ, +, e_{2}) resource-bounded classes none recursively enumerable sets positively in R

logo

History  Unification by Logic  Applications  Summary

Elementary Definitions

Characterisation of Classes by Elementary Definitions

Presburger arithmetic(ℕ, +) regular sets (ℕ, +, e_{2}) resource-bounded classes none recursively enumerable sets positively in R arithmetic hierarchy(ℕ, +, ·) ordinal number arithmetic(On, +, ·)

History  Unification by Logic  Applications  Summary

Enumerability for First-Order Logic

Elementary Enumerability is a Generalisation of Elementary Definability

Rx f (x) f Definition A function f is elementarily m-enumerable in a structure S if

1 its graph is contained in an

elementarily definable relation R, 2 which is m-bounded, i.e., for each x

there are at most m different y with (x, y) ∈ R.

History  Unification by Logic  Applications  Summary

Enumerability for First-Order Logic

The Original Notions of Enumerability are Instantiations

Theorem A function is m-enumerable by a finite automaton iff it is elementarily m-enumerable in (ℕ, +, e_{2}).

Theorem A function is m-enumerable by a Turing machine iff it is positively elementarily m-enumerable in R.

History  Unification by Logic  Applications  Summary

Weak Cardinality Theorems for First-Order Logic

The First Weak Cardinality Theorem

Theorem Let S be a logical structure with universe U and let A ⊆ U. If

1 S is well-orderable and

2 χ_{A}^{n} is elementarily n-enumerable in S, then A is elementarily definable in S.

logo

History  Unification by Logic  Applications  Summary

Weak Cardinality Theorems for First-Order Logic

The First Weak Cardinality Theorem

Theorem Let S be a logical structure with universe U and let A ⊆ U. If

1 S is well-orderable and

2 χ_{A}^{n} is elementarily n-enumerable in S, then A is elementarily definable in S.

Corollary If χ_{A}^{n} is n-enumerable by a finite automaton, then A is regular.

logo

History  Unification by Logic  Applications  Summary

Weak Cardinality Theorems for First-Order Logic

The First Weak Cardinality Theorem

Theorem Let S be a logical structure with universe U and let A ⊆ U. If

1 S is well-orderable and

2 χ_{A}^{n} is elementarily n-enumerable in S, then A is elementarily definable in S.

Corollary (with more effort) If χ_{A}^{n} is n-enumerable by a Turing machine, then A is recursive.

History  Unification by Logic  Applications  Summary

Weak Cardinality Theorems for First-Order Logic

The Second Weak Cardinality Theorem

Theorem Let S be a logical structure with universe U and let A ⊆ U. If

1 S is well-orderable,

2 every finite relation on U is elementarily definable in S, and 3 #_{A}^{2} is elementarily 2-enumerable in S,

then A is elementarily definable in S.

History  Unification by Logic  Applications  Summary

Weak Cardinality Theorems for First-Order Logic

The Third Weak Cardinality Theorem

Theorem Let S be a logical structure with universe U and let A ⊆ U. If

1 S is well-orderable,

2 every finite relation on U is elementarily definable in S, and 3 #_{A}^{n} is elementarily n-enumerable in S via a relation that

never ‘enumerates’ both 0 and n, then A is elementarily definable in S.

logo

History  Unification by Logic  Applications  Summary

Weak Cardinality Theorems for First-Order Logic

Relationships Between Cardinality Theorems (CT)

1st Weak CT 2nd Weak CT 3rd Weak CT 1st Weak CT 2nd Weak CT 3rd Weak CT CT 1st Weak CT 2nd Weak CT 3rd Weak CT automata theory first-order logic recursion theory

logo

History  Unification by Logic  Applications  Summary

Weak Cardinality Theorems for First-Order Logic

Relationships Between Cardinality Theorems (CT)

CT 1st Weak CT 2nd Weak CT 3rd Weak CT CT 1st Weak CT 2nd Weak CT 3rd Weak CT CT 1st Weak CT 2nd Weak CT 3rd Weak CT automata theory first-order logic recursion theory

1 History

Enumerability in Recursion and Automata Theory Known Weak Cardinality Theorem Why Do Cardinality Theorems Hold Only for Certain Models?

2 Unification by First-Order Logic

Elementary Definitions Enumerability for First-Order Logic Weak Cardinality Theorems for First-Order Logic

History  Unification by Logic  Applications  Summary

A Separability Result for First-Order Logic

A × Ā A × A Ā× Ā Theorem Let S be a well-orderable logical structure in which all finite relations are elementarily definable.

If there exist elementarily definable supersets of A × A, A × Ā, and Ā× Ā whose intersection is empty, then A is elementarily definable in S.

Note The theorem is no longer true if we add Ā× A to the list.

History  Unification by Logic  Applications  Summary

A Separability Result for First-Order Logic

A × Ā A × A Ā× Ā Theorem Let S be a well-orderable logical structure in which all finite relations are elementarily definable.

If there exist elementarily definable supersets of A × A, A × Ā, and Ā× Ā whose intersection is empty, then A is elementarily definable in S.

Note The theorem is no longer true if we add Ā× A to the list.

History  Unification by Logic  Applications  Summary

A Separability Result for First-Order Logic

A × Ā A × A Ā× Ā Theorem Let S be a well-orderable logical structure in which all finite relations are elementarily definable.

If there exist elementarily definable supersets of A × A, A × Ā, and Ā× Ā whose intersection is empty, then A is elementarily definable in S.

Note The theorem is no longer true if we add Ā× A to the list.

logo^{History  Unification by Logic  Applications  Summary}

Summary

Summary The weak cardinality theorems for first-order logic unify the weak cardinality theorems of automata and recursion theory. The logical approach yields weak cardinality theorems for other computational models. Cardinality theorems are separability theorems in disguise.

Open Problems Does a cardinality theorem for first-order logic hold? What about non-well-orderable structures like (ℝ, +, ·)?