First-Order Formulas and the Classes Σ_t and Π_t

Lax496464.WH_B2_FirstOrder · concepts/Lax496464/WH_B2_FirstOrder.lean · lax-496464

definition

Loading review…

Natural Language Statement

Definition

First-order formulas over a relational vocabulary, with equality and one free relation variable $X$ ; their satisfaction in a structure; their free variables; and the syntactic classes that define the hierarchies [FG06, Section 4.2]:

$\Sigma_0 = \Pi_0$ is the class of quantifier-free formulas; $\Sigma_{t+1}$ consists of the formulas $\exists x_1 \dots \exists x_k\,\varphi$ with $\varphi \in \Pi_t$ , and $\Pi_{t+1}$ of the formulas $\forall x_1 \dots \forall x_k\,\varphi$ with $\varphi \in \Sigma_t$ ;
a formula is positive if it contains no negation symbol, as in $\Sigma_1^+$ ;
a formula is at most $u$ -ary if every relation symbol in it has arity at most $u$ , as in $\Sigma_1[2]$ .

Concept map

2 concepts; 18 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

1	import Lax496464.WH_B1_Structures
2
3	/-!
4	---
5	title: First-Order Formulas and the Classes Σ_t and Π_t
6	type: definition
7	---
8	First-order formulas over a relational vocabulary, with equality and one free relation variable
9	$X$ ; their satisfaction in a structure; their free variables; and the syntactic classes that define
10	the hierarchies [FG06, Section 4.2]:
11
12	* $\Sigma_0 = \Pi_0$ is the class of quantifier-free formulas; $\Sigma_{t+1}$ consists of the
13	formulas $\exists x_1 \dots \exists x_k\,\varphi$ with $\varphi \in \Pi_t$ , and $\Pi_{t+1}$ of the
14	formulas $\forall x_1 \dots \forall x_k\,\varphi$ with $\varphi \in \Sigma_t$ ;
15	* a formula is positive if it contains no negation symbol, as in $\Sigma_1^+$ ;
16	* a formula is at most $u$ -ary if every relation symbol in it has arity at most $u$ , as in
17	$\Sigma_1[2]$ .
18
19	# Formalization Notes
20
21	Syntax. Variables and relation symbols are numbers: `rel i xs` is the atom
22	$R_i\,x_{a_1}\dots x_{a_r}$ for symbol $i$ and the variables listed in `xs`, and `setVar xs` is the
23	atom $X x_{a_1}\dots x_{a_s}$ . The connectives are negation, conjunction and disjunction;
24	$\varphi \to \psi$ abbreviates $\neg\varphi \vee \psi$ (`Formula.imp`).
25
26	Semantics. A formula is evaluated under an assignment of numbers to variables and an
27	interpretation $S$ of $X$ as a set of tuples; quantifiers range over the universe. A formula fits
28	a vocabulary if every symbol it mentions belongs to the vocabulary and is applied to the right
29	number of arguments, and every atom of $X$ has the declared arity $s$ . The problems built on
30	formulas treat a formula that does not fit as false.
31
32	Free variables and sentences are syntactic (`Formula.freeVars`, `IsSentence`), so whether a
33	concrete formula is a sentence is decided by computation.
34
35	The classes. Quantifier blocks may be empty, so $\Sigma_t \cup \Pi_t \subseteq \Sigma_{t+1} \cap \Pi_{t+1}$
36	. Atoms of the relation variable are quantifier-free.
37
38	Size and words. $\|\varphi\|$ counts symbols: an atom counts one plus its number of arguments, an
39	equation three, a connective one, a quantifier two; this is within a constant factor of the length
40	of $\varphi$ as a string. The word of a formula (`Formula.encode`) is in prefix notation and
41	self-delimiting, so a formula may be followed by further entries.
42	-/
43
44	namespace Lax496464.WH_B2_FirstOrder
45
46	open Lax496464.WH_B1_Structures
47
48	/-- First-order formulas, with atoms for the vocabulary's relation symbols and for one free relation
49	variable. -/
50	inductive Formula
51	/-- The atom `R_i x_{a_1} … x_{a_r}`. -/
52	\| rel (i : ℕ) (xs : List ℕ)
53	/-- The atom `X x_{a_1} … x_{a_s}` of the free relation variable. -/
54	\| setVar (xs : List ℕ)
55	/-- The equation `x = y`. -/
56	\| eq (x y : ℕ)
57	/-- Negation. -/
58	\| neg (φ : Formula)
59	/-- Conjunction. -/
60	\| and (φ ψ : Formula)
61	/-- Disjunction. -/
62	\| or (φ ψ : Formula)
63	/-- Existential quantification. -/
64	\| ex (x : ℕ) (φ : Formula)
65	/-- Universal quantification. -/
66	\| all (x : ℕ) (φ : Formula)
67
68	/-- The implication `φ → ψ`, an abbreviation of `¬φ ∨ ψ`. -/
69	def Formula.imp (φ ψ : Formula) : Formula := .or (.neg φ) ψ
70
71	/-- An assignment of universe elements to variables. -/
72	abbrev Assignment := ℕ → ℕ
73
74	/-- The assignment `ρ` changed to send `x` to `a`. -/
75	def Assignment.update (ρ : Assignment) (x a : ℕ) : Assignment :=
76	fun y => if y = x then a else ρ y
77
78	/-- Satisfaction. The formula holds in `A`, with the relation variable interpreted as `S`,
79	under the assignment `ρ`. -/
80	def Sat (A : Structure) (S : Set (List ℕ)) : Formula → Assignment → Prop
81	\| .rel i xs, ρ => xs.map ρ ∈ A.rel i
82	\| .setVar xs, ρ => xs.map ρ ∈ S
83	\| .eq x y, ρ => ρ x = ρ y
84	\| .neg φ, ρ => ¬ Sat A S φ ρ
85	\| .and φ ψ, ρ => Sat A S φ ρ ∧ Sat A S ψ ρ
86	\| .or φ ψ, ρ => Sat A S φ ρ ∨ Sat A S ψ ρ
87	\| .ex x φ, ρ => ∃ a, a < A.size ∧ Sat A S φ (ρ.update x a)
88	\| .all x φ, ρ => ∀ a, a < A.size → Sat A S φ (ρ.update x a)
89
90	/-- The free (individual) variables of a formula. -/
91	def Formula.freeVars : Formula → Finset ℕ
92	\| .rel _ xs => xs.toFinset
93	\| .setVar xs => xs.toFinset
94	\| .eq x y => {x, y}
95	\| .neg φ => φ.freeVars
96	\| .and φ ψ => φ.freeVars ∪ ψ.freeVars
97	\| .or φ ψ => φ.freeVars ∪ ψ.freeVars
98	\| .ex x φ => φ.freeVars.erase x
99	\| .all x φ => φ.freeVars.erase x
100
101	/-- The formula is a sentence: it has no free individual variables (the relation variable may
102	occur). -/
103	def IsSentence (φ : Formula) : Prop := φ.freeVars = ∅
104
105	/-- The formula fits the vocabulary `arities`, and uses the relation variable at arity `s`. -/
106	def Formula.Fits (arities : List ℕ) (s : ℕ) : Formula → Prop
107	\| .rel i xs => i < arities.length ∧ xs.length = arities.getD i 0
108	\| .setVar xs => xs.length = s
109	\| .eq _ _ => True
110	\| .neg φ => φ.Fits arities s
111	\| .and φ ψ => φ.Fits arities s ∧ ψ.Fits arities s
112	\| .or φ ψ => φ.Fits arities s ∧ ψ.Fits arities s
113	\| .ex _ φ => φ.Fits arities s
114	\| .all _ φ => φ.Fits arities s
115
116	/-- The formula does not use the relation variable. -/
117	def Formula.NoSetVar : Formula → Prop
118	\| .setVar _ => False
119	\| .rel _ _ => True
120	\| .eq _ _ => True
121	\| .neg φ => φ.NoSetVar
122	\| .and φ ψ => φ.NoSetVar ∧ ψ.NoSetVar
123	\| .or φ ψ => φ.NoSetVar ∧ ψ.NoSetVar
124	\| .ex _ φ => φ.NoSetVar
125	\| .all _ φ => φ.NoSetVar
126
127	/-- The formula is quantifier-free. -/
128	def Formula.IsQF : Formula → Prop
129	\| .ex _ _ => False
130	\| .all _ _ => False
131	\| .neg φ => φ.IsQF
132	\| .and φ ψ => φ.IsQF ∧ ψ.IsQF
133	\| .or φ ψ => φ.IsQF ∧ ψ.IsQF
134	\| _ => True
135
136	/-- The formula is positive: it contains no negation symbol. -/
137	def Formula.IsPositive : Formula → Prop
138	\| .neg _ => False
139	\| .and φ ψ => φ.IsPositive ∧ ψ.IsPositive
140	\| .or φ ψ => φ.IsPositive ∧ ψ.IsPositive
141	\| .ex _ φ => φ.IsPositive
142	\| .all _ φ => φ.IsPositive
143	\| _ => True
144
145	/-- Every relation symbol occurring in the formula is applied to at most `u` variables. -/
146	def Formula.ArityAtMost (u : ℕ) : Formula → Prop
147	\| .rel _ xs => xs.length ≤ u
148	\| .neg φ => φ.ArityAtMost u
149	\| .and φ ψ => φ.ArityAtMost u ∧ ψ.ArityAtMost u
150	\| .or φ ψ => φ.ArityAtMost u ∧ ψ.ArityAtMost u
151	\| .ex _ φ => φ.ArityAtMost u
152	\| .all _ φ => φ.ArityAtMost u
153	\| _ => True
154
155	/-- A block of existential quantifiers over the variables `xs`. -/
156	def Formula.exBlock (xs : List ℕ) (φ : Formula) : Formula := xs.foldr Formula.ex φ
157
158	/-- A block of universal quantifiers over the variables `xs`. -/
159	def Formula.allBlock (xs : List ℕ) (φ : Formula) : Formula := xs.foldr Formula.all φ
160
161	/-- `Alt true t φ` is `φ ∈ Σ_t` and `Alt false t φ` is `φ ∈ Π_t`: `t` alternating blocks of
162	quantifiers, the first existential or universal respectively, in front of a quantifier-free
163	formula. -/
164	def Alt : Bool → ℕ → Formula → Prop
165	\| _, 0, φ => φ.IsQF
166	\| true, t + 1, φ => ∃ xs ψ, φ = Formula.exBlock xs ψ ∧ Alt false t ψ
167	\| false, t + 1, φ => ∃ xs ψ, φ = Formula.allBlock xs ψ ∧ Alt true t ψ
168
169	/-- `φ ∈ Σ_t`. -/
170	abbrev IsSigma (t : ℕ) (φ : Formula) : Prop := Alt true t φ
171
172	/-- `φ ∈ Π_t`. -/
173	abbrev IsPi (t : ℕ) (φ : Formula) : Prop := Alt false t φ
174
175	/-- The size `\|φ\|` of a formula: the number of its symbols. -/
176	def Formula.size : Formula → ℕ
177	\| .rel _ xs => xs.length + 1
178	\| .setVar xs => xs.length + 1
179	\| .eq _ _ => 3
180	\| .neg φ => φ.size + 1
181	\| .and φ ψ => φ.size + ψ.size + 1
182	\| .or φ ψ => φ.size + ψ.size + 1
183	\| .ex _ φ => φ.size + 2
184	\| .all _ φ => φ.size + 2
185
186	/-- The word of a formula, in prefix notation. -/
187	def Formula.encode : Formula → List ℕ
188	\| .rel i xs => 0 :: i :: xs.length :: xs
189	\| .setVar xs => 1 :: xs.length :: xs
190	\| .eq x y => [2, x, y]
191	\| .neg φ => 3 :: φ.encode
192	\| .and φ ψ => 4 :: (φ.encode ++ ψ.encode)
193	\| .or φ ψ => 5 :: (φ.encode ++ ψ.encode)
194	\| .ex x φ => 6 :: x :: φ.encode
195	\| .all x φ => 7 :: x :: φ.encode
196
197	end Lax496464.WH_B2_FirstOrder
198

Formalization Notes

Syntax. Variables and relation symbols are numbers: $rel i xs$ is the atom $R_i\,x_{a_1}\dots x_{a_r}$ for symbol $i$ and the variables listed in $xs$ , and $setVar xs$ is the atom $X x_{a_1}\dots x_{a_s}$ . The connectives are negation, conjunction and disjunction; $\varphi \to \psi$ abbreviates $\neg\varphi \vee \psi$ ( $Formula.imp$ ).

Semantics. A formula is evaluated under an assignment of numbers to variables and an interpretation $S$ of $X$ as a set of tuples; quantifiers range over the universe. A formula fits a vocabulary if every symbol it mentions belongs to the vocabulary and is applied to the right number of arguments, and every atom of $X$ has the declared arity $s$ . The problems built on formulas treat a formula that does not fit as false.

Free variables and sentences are syntactic ( $Formula.freeVars$ , $IsSentence$ ), so whether a concrete formula is a sentence is decided by computation.

The classes. Quantifier blocks may be empty, so $\Sigma_t \cup \Pi_t \subseteq \Sigma_{t+1} \cap \Pi_{t+1}$ . Atoms of the relation variable are quantifier-free.

Size and words. $|\varphi|$ counts symbols: an atom counts one plus its number of arguments, an equation three, a connective one, a quantifier two; this is within a constant factor of the length of $\varphi$ as a string. The word of a formula ( $Formula.encode$ ) is in prefix notation and self-delimiting, so a formula may be followed by further entries.

Builds on

Lax496464.WH_B1_Structures

Used by

Lax496464.WH_B3_LogicProblems

From Mathlib

none

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

First-Order Formulas and the Classes Σ_t and Π_t

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments