Documentation

MathematicalLogic.SecondOrder.Syntax

inductive List.Fin {α : Type u} :

List α → α → Type u

fz {α : Type u} {a : α} {l : List α} : (a :: l).Fin a
fs {α : Type u} {l : List α} {a b : α} : l.Fin a → (b :: l).Fin a

Instances For

instance instOfNatFinConsOfNatNat {α✝ : Type u_1} {a : α✝} {l : List α✝} :

OfNat ((a :: l).Fin a) 0

Equations

instOfNatFinConsOfNatNat = { ofNat := List.Fin.fz }

instance instOfNatFinConsOfNatNat_1 {α✝ : Type u_1} {a b : α✝} {l : List α✝} :

OfNat ((a :: b :: l).Fin b) 1

Equations

instOfNatFinConsOfNatNat_1 = { ofNat := List.Fin.fz.fs }

instance instOfNatFinConsOfNatNat_2 {α✝ : Type u_1} {a b c : α✝} {l : List α✝} :

OfNat ((a :: b :: c :: l).Fin c) 2

Equations

instOfNatFinConsOfNatNat_2 = { ofNat := List.Fin.fz.fs.fs }

instance instOfNatFinConsOfNatNat_3 {α✝ : Type u_1} {a b c d : α✝} {l : List α✝} :

OfNat ((a :: b :: c :: d :: l).Fin d) 3

Equations

instOfNatFinConsOfNatNat_3 = { ofNat := List.Fin.fz.fs.fs.fs }

instance instOfNatFinConsOfNatNat_4 {α✝ : Type u_1} {a b c d e : α✝} {l : List α✝} :

OfNat ((a :: b :: c :: d :: e :: l).Fin e) 4

Equations

instOfNatFinConsOfNatNat_4 = { ofNat := List.Fin.fz.fs.fs.fs.fs }

structure SecondOrder.Language :

Func : ℕ → Type
Rel : ℕ → Type

Instances For

inductive SecondOrder.Ty :

var : Ty
func : ℕ → Ty
rel : ℕ → Ty

Instances For

inductive SecondOrder.Language.Term (L : Language) :

List Ty → Type

var {L : Language} {l : List Ty} : l.Fin Ty.var → L.Term l
fconst {L : Language} {n : ℕ} {l : List Ty} : L.Func n → (Fin n → L.Term l) → L.Term l
fvar {L : Language} {n : ℕ} {l : List Ty} : l.Fin (Ty.func n) → (Fin n → L.Term l) → L.Term l

Instances For

def SecondOrder.Language.«term#_» :

Lean.ParserDescr

Equations

SecondOrder.Language.«term#_» = Lean.ParserDescr.node `SecondOrder.Language.«term#_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#") (Lean.ParserDescr.cat `term 1024))

Instances For

def SecondOrder.Language.«term_⬝ᶠ_» :

Lean.TrailingParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

def SecondOrder.Language.«term_⬝ᶠᵛ_» :

Lean.TrailingParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

inductive SecondOrder.Language.Formula (L : Language) :

List Ty → Type

rconst {L : Language} {n : ℕ} {l : List Ty} : L.Rel n → (Fin n → L.Term l) → L.Formula l
rvar {L : Language} {n : ℕ} {l : List Ty} : l.Fin (Ty.rel n) → (Fin n → L.Term l) → L.Formula l
eq {L : Language} {l : List Ty} : L.Term l → L.Term l → L.Formula l
false {L : Language} {l : List Ty} : L.Formula l
imp {L : Language} {l : List Ty} : L.Formula l → L.Formula l → L.Formula l
all {L : Language} {l : List Ty} : L.Formula (Ty.var :: l) → L.Formula l
allf {L : Language} {l : List Ty} (n : ℕ) : L.Formula (Ty.func n :: l) → L.Formula l
allr {L : Language} {l : List Ty} (n : ℕ) : L.Formula (Ty.rel n :: l) → L.Formula l

Instances For

def SecondOrder.Language.Formula.«term_⬝ʳ_» :

Lean.TrailingParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

def SecondOrder.Language.Formula.«term_⬝ʳᵛ_» :

Lean.TrailingParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

def SecondOrder.Language.Formula.«term_≐_» :

Lean.TrailingParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

instance SecondOrder.Language.Formula.instClassicalPropNotation {L : Language} {l : List Ty} :

ClassicalPropNotation (L.Formula l)

Equations

SecondOrder.Language.Formula.instClassicalPropNotation = { false := SecondOrder.Language.Formula.false, imp := SecondOrder.Language.Formula.imp }

def SecondOrder.Language.Formula.«term∀'_» :

Lean.ParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

def SecondOrder.Language.Formula.«term∀ᶠ[_]_» :

Lean.ParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

def SecondOrder.Language.Formula.«term∀ʳ[_]_» :

Lean.ParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

def SecondOrder.Language.Formula.ex {L : Language} {l : List Ty} (p : L.Formula (Ty.var :: l)) :

Equations

∃' p = ~ ∀' (~ p)

Instances For

def SecondOrder.Language.Formula.exf {L : Language} {l : List Ty} (n : ℕ) (p : L.Formula (Ty.func n :: l)) :

Equations

∃ᶠ[n]p = ~ ∀ᶠ[n](~ p)

Instances For

def SecondOrder.Language.Formula.exr {L : Language} {l : List Ty} (n : ℕ) (p : L.Formula (Ty.rel n :: l)) :

Equations

∃ʳ[n]p = ~ ∀ʳ[n](~ p)

Instances For

def SecondOrder.Language.Formula.«term∃'_» :

Lean.ParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

def SecondOrder.Language.Formula.«term∃ᶠ[_]_» :

Lean.ParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

def SecondOrder.Language.Formula.«term∃ʳ[_]_» :

Lean.ParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem SecondOrder.Language.Formula.false_eq {L : Language} {l : List Ty} :

@[simp]

theorem SecondOrder.Language.Formula.imp_eq {L✝ : Language} {a✝ : List Ty} {p q : L✝.Formula a✝} :

p.imp q = p ⇒ q

@[reducible, inline]

abbrev SecondOrder.Language.Sentence (L : Language) :

Equations

L.Sentence = L.Formula []

Instances For

@[reducible, inline]

abbrev SecondOrder.Language.Theory (L : Language) :

Equations

L.Theory = Set L.Sentence

Instances For