wiki_research

commit 05ffb1207d71862521175054f714b84934d35ca5
parent 1c2d0dc44b1240c39828849112f9cb24df36cf6c
Author: Antoine Amarilli <a3nm@a3nm.net>
Date:   Mon, 30 Mar 2026 17:30:35 +0200

commit with codex

Diffstat:
binary_relation
 | 
7
+++++++
buchis_theorem
 | 
2
+-
equality_generating_dependency
 | 
2
++
fo2
 | 
2
+-
fo3
 | 
7
+++++++
fok
 | 
3
++-
preorder
 | 
9
+++++++++
quantifier
 | 
1
+
reflexive_relation
 | 
5
+++++
relation
 | 
9
+++++++++
satisfiability
 | 
2
+-
satisfiability_finite
 | 
10
++++++++++
symmetric_relation
 | 
5
+++++
transitive_relation
 | 
7
+++++++
tseytin_transformation
 | 
2
++

15 files changed, 69 insertions(+), 4 deletions(-)
diff --git a/binary_relation b/binary_relation
@@ -0,0 +1,7 @@
+# Binary relation
+
+A [relation] of [arity] two
+
+Up: [relation]
+
+See also: [FO2], [unary_relation]
diff --git a/buchis_theorem b/buchis_theorem
@@ -6,6 +6,6 @@ Equivalence of [monadic_second_order_logic] and of [regular_languages] for [logi
 
 Up: [theorem] in [formal_language_theory]
 
-See also: [Büchi_automaton]
+See also: [Büchi_automaton], [trakhtenbrot's_theorem]
 
 Aliases: Büchi Elgot Trakhtenbrot theorem
diff --git a/equality_generating_dependency b/equality_generating_dependency
@@ -7,3 +7,5 @@ A [database_dependency] in which the head is an [equality] [atom]
 Up: [database_dependency], [first_order_logic]
 
 Aliases: EGD, EGDs
+
+See also: [equality_relation]
diff --git a/fo2 b/fo2
@@ -6,7 +6,7 @@ extensions:
 - [c2] with [counting_quantifier]
 - [gc2] with [guarded_fragment] quantification
 
-FO2 on [words] with order cannot define [successor]: you need [fo3]
+FO2 on [words] with order cannot define [successor]: you need [FO3]
 - with [successor], it defines a variety of [semigroups]
 
 Does not enjoy [craig_interpolation], according to [cate2023craig], but enjoys [finite_model_property]
diff --git a/fo3 b/fo3
@@ -0,0 +1,7 @@
+# FO3
+
+[first_order_logic] with three variables
+
+Up: [fok]
+
+See also: [FO2]
diff --git a/fok b/fok
@@ -6,7 +6,8 @@ Also called "finite variable logics" in the [survey] [grohe1998finite]
 
 ## Fragments
 
-- [fo2]
+- [FO2]
+- [FO3]
 
 ## Extensions
 
diff --git a/preorder b/preorder
@@ -0,0 +1,9 @@
+# Preorder
+
+https://en.wikipedia.org/wiki/Preorder
+
+A [binary_relation] which is [transitive] and [reflexive] but not necessarily [antisymmetric]
+
+May be [total_relation] or not, if it is total then it is a [total_order] except that there are "ties"
+
+Up: [ddal_seminar_vincent]
diff --git a/quantifier b/quantifier
@@ -4,6 +4,7 @@
 - [universal_quantifier]
 
 - [quantifier_rank]
+- [quantifier_prefix]
 
 Up: [logic]
 
diff --git a/reflexive_relation b/reflexive_relation
@@ -0,0 +1,5 @@
+# Reflexive relation
+
+A [relation] which satisfies [reflexivity]
+
+Up: [relation]
diff --git a/relation b/relation
@@ -1,6 +1,15 @@
 # Relation
 
 - [equivalence_relation]
+- [preorder]
 - [word_relation]
+- [binary_relation]
+- [unary_relation]
+
+Axioms:
+- [transitive_relation]
+- [reflexive_relation]
+- [symmetric_relation]
+- [antisymmetric_relation]
 
 Up: [mathematics]
diff --git a/satisfiability b/satisfiability
@@ -10,6 +10,6 @@ The *satisfiability problem* is a [decision_problem] in [logic]: given a [logica
 
 Tools: [sat_solver]
 
-See also: [strong_exponential_time_hypothesis], [satisfiability_boolean], [tautology], [automaton_emptiness], [satisfiability_modulo_theory], [equisatisfiability], [enumeration_valuations]
+See also: [strong_exponential_time_hypothesis], [satisfiability_boolean], [tautology], [automaton_emptiness], [satisfiability_modulo_theory], [equisatisfiability], [enumeration_valuations], [satisfiability_finite]
 
 Up: [computational_problem]
diff --git a/satisfiability_finite b/satisfiability_finite
@@ -0,0 +1,10 @@
+# Finite satisfiability
+
+Like [satisfiability] but deciding whether a [logic_formula] has a [finite_model]
+
+- [finite_model_property]
+- [finite_controllability]
+
+Up: [satisfiability]
+
+Aliases: finite satisfiability, finsat
diff --git a/symmetric_relation b/symmetric_relation
@@ -0,0 +1,5 @@
+# Symmetric relation
+
+A [binary_relation] which is symmetric, i.e., forall x y R(x, y) -> R(y, x)
+
+Up: [relation]
diff --git a/transitive_relation b/transitive_relation
@@ -0,0 +1,7 @@
+# Transitive relation
+
+A [relation] which satisfies [transitivity]
+
+Up: [transitivity]
+
+Aliases: transitive relations, transitive
diff --git a/tseytin_transformation b/tseytin_transformation
@@ -7,3 +7,5 @@ Transform a [Boolean_circuit] into [equisatisfiable] [CNF], by adding some addit
 Up: [circuit]
 
 Aliases: Tseytin transform
+
+See also: [scott_normal_form]