commit 94ecab0d142f4d8ed1e4b43f5f064d2c0bcf2ad8
parent 3cb2e81ae073313388243972ca62e1d14bbc7dd2
Author: Antoine Amarilli <a3nm@a3nm.net>
Date: Wed, 8 Oct 2025 11:44:10 +0200
Merge branch 'master' of a3nm.net:git/wiki_research
Diffstat:
3 files changed, 17 insertions(+), 20 deletions(-)
diff --git a/ehrenfeucht_fraisse_game b/ehrenfeucht_fraisse_game
@@ -1,18 +0,0 @@
-# EF-game
-
-Spoiler plays in [structure] A by marking a [vertex], Duplicator answers in [structure] B
-
-The structures induced by the [pebbles] must be [isomorphic]
-
-- Number of rounds necessary to distinguish both [structures]
- - connections to types nombre de rounds nécessaires pour distinguer les deux structures ([quantifier_rank])
-- Number of [pebbles] needed
- - connection to [FOk]
-
-[MSO] EF-game: the players can pebble sets
-
-Up: [logic], [games]
-
-See also: [bisimulation], [homomorphic_equivalence], [prover_verifier_game]
-
-Aliases: EF game, EF games
diff --git a/first_order_positive b/first_order_positive
@@ -0,0 +1,11 @@
+# Positive first order
+
+[FO] without [negation] but with [universal_quantification]
+
+Should be distinguished from [existential_positive_FO] which also disallows [universal_quantification]
+
+Discussed in [berkholz2019compiling] and in [bova2014complexity]
+
+Up: [first_order_logic]
+
+Aliases: positive FO, positive first order
diff --git a/fok b/fok
@@ -2,6 +2,8 @@
[first_order_logic] with k variables, or [first_order_logic_width] k
+Also called "finite variable logics" in the [survey] [grohe1998finite]
+
## Fragments
- [fo2]
@@ -14,12 +16,14 @@
- [satisfiability] of FO^2 etc., cf "kings" [gradel1997decision]
-- [first_order_model_checking_fok]
+- [model_checking]: [first_order_model_checking_fok]
- special case: [first_order_model_checking_fo2]
- connections to [yannakakis_algorithm]
- finding the best k: [fok_rewriting]
+
+- [fok_quantifier_rank]
Up: [first_order_logic]
-See also: [two_variables]
+See also: [two_variables], [pebble_game]
