commit 650d48930c5d2cd4566a2fd1f8eff4178299ec5f
parent 05ffb1207d71862521175054f714b84934d35ca5
Author: Antoine Amarilli <a3nm@a3nm.net>
Date: Mon, 30 Mar 2026 22:10:37 +0200
commit with codex
Diffstat:
5 files changed, 26 insertions(+), 2 deletions(-)
diff --git a/decidable_fo_fragments b/decidable_fo_fragments
@@ -0,0 +1,13 @@
+# Decidable FO fragments
+
+[FO_fragments] for which [satisfiability_FO] is [decidable]
+
+cf survey [hustadt2004survey]
+- [fluted_fragment], cf [fluted_fragment_satisfiability]
+- [Maslovs_fragment] alias "K-bar"
+- [guarded_fragment], cf [guarded_fragment_satisfiability]
+- [FO2], cf [FO2_satisfiability]
+
+Up: [FO_fragments], [satisfiability_FO]
+
+Aliases: decidable FO fragment
diff --git a/fo2 b/fo2
@@ -1,4 +1,4 @@
-# Fo2
+# FO2
[FOk] with [two_variables]
@@ -11,4 +11,6 @@ FO2 on [words] with order cannot define [successor]: you need [FO3]
Does not enjoy [craig_interpolation], according to [cate2023craig], but enjoys [finite_model_property]
+For [FO_satisfiability], cf [FO2_satisfiability]
+
Up: [fok]
diff --git a/logic b/logic
@@ -76,4 +76,4 @@ Up: [mathematics], [theoretical_computer_science]
See also: [knowledge_representation], [reasoning], [logic_applications], [expressiveness], [reverse_mathematics]
-Aliases: logics
+Aliases: logics, logical
diff --git a/transitive_relation b/transitive_relation
@@ -5,3 +5,5 @@ A [relation] which satisfies [transitivity]
Up: [transitivity]
Aliases: transitive relations, transitive
+
+See also: [Transitivity_assertion]
diff --git a/transitivity_assertion b/transitivity_assertion
@@ -0,0 +1,7 @@
+# Transitivity assertion
+
+The [logical] assertion that a relation is [transitive]
+
+Up: [transitivity], [axiom]
+
+Aliases: transitivity axiom, transitivity axioms, transitivity assertions
