commit bb478db58dbe8f2587a1a72d168a961cecb32b26
parent 34021cd85ce54287174b7fa978131720591ae105
Author: Antoine Amarilli <a3nm@a3nm.net>
Date: Mon, 6 Oct 2025 19:05:41 +0200
commit with codex
Diffstat:
3 files changed, 15 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,7 +16,7 @@
- [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]
@@ -22,4 +24,4 @@
Up: [first_order_logic]
-See also: [two_variables]
+See also: [two_variables], [pebble_game]
