First-Order Logic (FOL) + bOoleans = FOOL

Boolean Terms and Formulae

• Boolean variables as formulae and Formulae (including variables) as terms
• Example: ∀X:bool ∀Y:bool (imply(X,Y) ↔ (¬X ∨ Y))

Tuples

• Tuple types and Tuple terms
• Example: (ℝ,ℝ) and (2.3,-6.6)

Conditional Expressions

• Expressions of the form if φ then s else t
• Example term: ∀X:ℤ ∀Y:ℤ (max(X,Y) = if X ≥ Y then X else Y)
• Example formula: ∀X:ℤ ∀Y:ℤ (if max(X,Y) = X then X ≥ Y else Y ≥ X)

Let Expressions

• Expressions of the form let D₁;...;D_k in t
• Example term: ∀X:ℤ ∀Y:ℤ let (max(X,Y) = if X ≥ Y then X else Y) in p(max(max(a,b),c))
• Example formula: ∀X:bool ∀Y:bool let (imply(X,Y) = ¬X ∨ Y) in (imply(a,b) ∧ imply(b,a))