Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

First-order logic over a relational vocabulary

Lax512892.FirstOrder · concepts/Lax512892/FirstOrder.lean · lax-512892

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    First-order terms are variables or constants. Formulas are relation atoms, equalities, negations, disjunctions, and existential quantifications. The satisfaction relation gives these constructors their usual semantics, and the quantifier rank is the greatest nesting depth of quantifiers.

    Concept map
    2 concepts; 2 descendants hidden
    100%
    Open claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax512892.RelationalStructures
    2
    3/-!
    4---
    5title: First-order logic over a relational vocabulary
    6type: definition
    7---
    8First-order terms are variables or constants. Formulas are relation atoms,
    9equalities, negations, disjunctions, and existential quantifications. The
    10satisfaction relation gives these constructors their usual semantics, and the
    11quantifier rank is the greatest nesting depth of quantifiers.
    12
    13# Formalization notes
    14
    15`Formula σ k` has exactly `k` available free variables. Variables are finite
    16levels: an existential quantifier adds the new last variable, and satisfaction
    17extends an environment with `Fin.snoc`. Consequently a sentence has type
    18`Formula σ 0`; closedness is enforced by the type rather than checked by a
    19separate predicate. Conjunction and universal quantification are definable from
    20the chosen constructors and do not need additional semantic cases.
    21-/
    22
    23namespace Lax512892.FirstOrder
    24
    25open Lax512892.RelationalStructures
    26
    27/-- Terms over `σ` with `k` available variables. -/
    28inductive Term (σ : Vocabulary) (k : ℕ) : Type
    29 /-- A variable. -/
    30 | var (i : Fin k)
    31 /-- A constant of the vocabulary. -/
    32 | const (c : σ.Constant)
    33
    34/-- First-order formulas over `σ` with `k` available free variables. -/
    35inductive Formula (σ : Vocabulary) : ℕ → Type
    36 /-- A relation atom. -/
    37 | rel {k : ℕ} (R : σ.Relation) (args : Fin (σ.arity R) → Term σ k) : Formula σ k
    38 /-- Equality of terms. -/
    39 | eq {k : ℕ} (left right : Term σ k) : Formula σ k
    40 /-- Negation. -/
    41 | not {k : ℕ} (φ : Formula σ k) : Formula σ k
    42 /-- Disjunction. -/
    43 | or {k : ℕ} (φ ψ : Formula σ k) : Formula σ k
    44 /-- Existential quantification, binding the new last variable. -/
    45 | ex {k : ℕ} (φ : Formula σ (k + 1)) : Formula σ k
    46
    47namespace Term
    48
    49/-- Interpretation of a term in a structure under an environment. -/
    50def eval {σ : Vocabulary} {M : Type*} {k : ℕ} (A : Structure σ M)
    51 (env : Fin k → M) : Term σ k → M
    52 | .var i => env i
    53 | .const c => A.constant c
    54
    55end Term
    56
    57namespace Formula
    58
    59/-- Satisfaction of a formula in a structure under an environment for its free
    60variables. -/
    61def Sat {σ : Vocabulary} {M : Type*} (A : Structure σ M) :
    62 {k : ℕ} → Formula σ k → (Fin k → M) → Prop
    63 | _, .rel R args, env => A.relation R (fun i => (args i).eval A env)
    64 | _, .eq left right, env => left.eval A env = right.eval A env
    65 | _, .not φ, env => ¬ Sat A φ env
    66 | _, .or φ ψ, env => Sat A φ env ∨ Sat A ψ env
    67 | _, .ex φ, env => ∃ x : M, Sat A φ (Fin.snoc env x)
    68
    69/-- The quantifier rank of a formula. -/
    70def quantifierRank {σ : Vocabulary} : {k : ℕ} → Formula σ k → ℕ
    71 | _, .rel _ _ => 0
    72 | _, .eq _ _ => 0
    73 | _, .not φ => quantifierRank φ
    74 | _, .or φ ψ => max (quantifierRank φ) (quantifierRank ψ)
    75 | _, .ex φ => quantifierRank φ + 1
    76
    77end Formula
    78
    79end Lax512892.FirstOrder
    80
    Formalization notes

    FormulaσkFormula σ k has exactly kk available free variables. Variables are finite levels: an existential quantifier adds the new last variable, and satisfaction extends an environment with Fin.snocFin.snoc. Consequently a sentence has type Formulaσ0Formula σ 0; closedness is enforced by the type rather than checked by a separate predicate. Conjunction and universal quantification are definable from the chosen constructors and do not need additional semantic cases.

    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…