Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-fmla Structured version   Visualization version   GIF version

Definition df-fmla 32596
Description: Define the predicate which defines the set of valid Godel formulas. The parameter 𝑛 defines the maximum height of the formulas: the set (Fmla‘∅) is all formulas of the form 𝑥𝑦 (which in our coding scheme is the set ({∅} × (ω × ω)); see df-sat 32594 for the full coding scheme), see fmla0 32633, and each extra level adds to the complexity of the formulas in (Fmla‘𝑛), see fmlasuc 32637. Remark: it is sufficient to have atomic formulas of the form 𝑥𝑦 only, because equations (formulas of the form 𝑥 = 𝑦), which are required as (atomic) formulas, can be introduced as a defined notion in terms of 𝑔, see df-goeq 32695. (Fmla‘ω) = 𝑛 ∈ ω(Fmla‘𝑛) is the set of all valid formulas, see fmla 32632. (Contributed by Mario Carneiro, 14-Jul-2013.)
Assertion
Ref Expression
df-fmla Fmla = (𝑛 ∈ suc ω ↦ dom ((∅ Sat ∅)‘𝑛))

Detailed syntax breakdown of Definition df-fmla
StepHypRef Expression
1 cfmla 32588 . 2 class Fmla
2 vn . . 3 setvar 𝑛
3 com 7583 . . . 4 class ω
43csuc 6196 . . 3 class suc ω
52cv 1535 . . . . 5 class 𝑛
6 c0 4294 . . . . . 6 class
7 csat 32587 . . . . . 6 class Sat
86, 6, 7co 7159 . . . . 5 class (∅ Sat ∅)
95, 8cfv 6358 . . . 4 class ((∅ Sat ∅)‘𝑛)
109cdm 5558 . . 3 class dom ((∅ Sat ∅)‘𝑛)
112, 4, 10cmpt 5149 . 2 class (𝑛 ∈ suc ω ↦ dom ((∅ Sat ∅)‘𝑛))
121, 11wceq 1536 1 wff Fmla = (𝑛 ∈ suc ω ↦ dom ((∅ Sat ∅)‘𝑛))
Colors of variables: wff setvar class
This definition is referenced by:  fmlafv  32631  fmla  32632  fmlasuc0  32635
  Copyright terms: Public domain W3C validator