Theorems · Inductive type · logic and foundations

FirstOrder.Language.Structure

FirstOrder.Language → Type w → Type (max (max u v) w)

A first-order structure on a type M consists of interpretations of all the symbols in a given language. Each function of arity n is interpreted as a function sending tuples of length n (modeled as (Fin n → M)) to M, and a relation of arity n is a function from tuples of length n to Prop.

Defined in

Mathlib.ModelTheory.Basic

Cited by

775 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms