Predicate language (?), different logical connectives etc.

Stream: new members

[Ilmārs Cīrulis]

Greetings!

I'm reading through publicly available study materials (I hope to start math studies in September), in this case Mathematical Logic, and trying to translate it to Lean. The problem is that the specific book has few more logical connectives (implication →, conjunction ∧, disjunction ∨, negation ¬) and both quantifiers (universal quantifier ∀, existential quantifier ∃) than Mathlib has at ModelTheory.Syntax. Also equality is defined as binary relation or as part of language.

As far as I see, that there's False, equality, relations of language, implication and universal quantifier:

inductive BoundedFormula : ℕ → Type max u v u'
  | falsum {n} : BoundedFormula n
  | equal {n} (t₁ t₂ : L.Term (α ⊕ (Fin n))) : BoundedFormula n
  | rel {n l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ (Fin n))) : BoundedFormula n
  | imp {n} (f₁ f₂ : BoundedFormula n) : BoundedFormula n
  | all {n} (f : BoundedFormula (n + 1)) : BoundedFormula n

If I want to translate this book to Lean, should I write my own BoundedFormula and maybe some other definitions that use this inductive definition? Or maybe there's some other way (although probably not)?

[Ilmārs Cīrulis]

Of course, if I'm do some more serious formalization then I will use Mathlib's definition.

[Ilmārs Cīrulis]

Yes, I've decided to extract necessary parts of Mathlib and change them a bit. At the start there's not much to take.

[Notification Bot]

Ilmārs Cīrulis has marked this topic as resolved.

[Notification Bot]

Ilmārs Cīrulis has marked this topic as unresolved.

[Ilmārs Cīrulis]

Is there a way to define Term and Formula in a way that is easier for making lot's of examples (in other words, easier to enter)?

[Ilmārs Cīrulis]

For now I doing it this way:

namespace Podnieks

  structure Language where
  Functions: ℕ → Type
  Relations: ℕ → Type

  inductive preTerm (L: Language) (α: Type): Type
  | var: α → preTerm L α
  | func: ∀ {l: ℕ} (f: L.Functions l) (ts: List (preTerm L α)), preTerm L α

  def correctTerm {L α} (pt: preTerm L α): Prop :=
  match pt with
  | preTerm.var _ => True
  | @preTerm.func _ _ l _ ts => ts.length = l ∧ ∀ x ∈ ts, correctTerm x

  def Term L α := { pt: preTerm L α // correctTerm pt }

  inductive preFormula (L: Language) (α: Type): Type
  | rel {l: ℕ} (R: L.Relations l) (ts: List (Term L α)): preFormula L α
  | neg (f: preFormula L α): preFormula L α
  | imp (f1 f2: preFormula L α): preFormula L α
  | conj (f1 f2: preFormula L α): preFormula L α
  | disj (f1 f2: preFormula L α): preFormula L α
  | all (n: ℕ) (f: preFormula L α): preFormula L α
  | ex (n: ℕ) (f: preFormula L α): preFormula L α

  def correctFormula {L α} (pf: preFormula L α): Prop :=
  match pf with
  | @preFormula.rel _ _ l _ ts => ts.length = l
  | .neg f => correctFormula f
  | .imp f1 f2 => correctFormula f1 ∧ correctFormula f2
  | .conj f1 f2 => correctFormula f1 ∧ correctFormula f2
  | .disj f1 f2 => correctFormula f1 ∧ correctFormula f2
  | .all _ f => correctFormula f
  | .ex _ f => correctFormula f

  def Formula L α := { pf: preFormula L α // correctFormula pf }

end Podnieks

Of course, this could possibly make further formalization harder, but that's okay. For anything more serious I am going to use Mathlib definitions.

[Ilmārs Cīrulis]

Ouch, I see mistake in definition of correctTerm.

[Ilmārs Cīrulis]

Fixed, i hope

[Matt Diamond]

FYI Mathlib has docs#FirstOrder.Language.BoundedFormula.ex and docs#FirstOrder.Language.BoundedFormula.not