# FO[Infinite]¶

**Goal**
The goal of FO[Infinite] is to allow quantification over infinite domains.
This extension extends FO[Int] and/or FO[Real].

**Syntax**

FO[Infinite] does not introduce new syntactic rules.

**Well-formedness**

Contrary to FO[Core], constructors can be recursive in FO[Infinite]: a

`NAME_T`

occurring as argument of a`CONSTRUCTOR`

does not have to be*previously*declared (but it has to be declared). As a result, a constructed type may have an infinite domain.Contrary to FO[Int], quantification over infinite types (ℤ, ℝ, Date) are allowed in FO[Infinite]. This also applies to binary quantifications using predicates over infinite domains (FO[Sugar].

**Semantics**

The formal semantics of a formula quantified over an infinite domain is a conjunction (or disjunction) of infinite length.

**Example**

The type for “lists of integers” can be declared as follows:

```
type List := constructed from { nil, cons(ℤ, List)}
```

`cons(1, cons(2, nil))`

represents the list `[1,2]`

.

Here is a quantification over integers:

```
∀ x ∈ ℤ: 0 ≤ x^2.
```