Arithmetic hierarchy of propositions in Lean

Stream: general

[Joseph Tooby-Smith]

Is it possible to talk about the arithmetic hierarchy of propositions in Lean, or more generally associate with a proposition some formal notion of complexity which can be proved?

[Johan Commelin]

You can do this, but not with random terms of Prop.
You'll have to define your own PropExpr (or reuse parts from ModelTheory/).
You can then define PropExpr.toProp : PropExpr -> Prop. The hierarchy can be defined on PropExpr.

[Joseph Tooby-Smith]

Ok, thanks, this makes sense. I will explore what is available in ModelTheory and go from there.

[Dexin Zhang]

FFL has a nice formalization of arithmetic hierarchy.

[SnO2WMaN]

Dexin Zhang said:

FFL has a nice formalization of arithmetic hierarchy.

Mention that this is not strict: https://github.com/FormalizedFormalLogic/Foundation/issues/707

FYI: @Palalansoukî

[Palalansoukî]

How about defining using computability theoretic notion?

import Mathlib

inductive SigmaPi
| sigma
| pi

inductive ArithmeticalHierarchy : SigmaPi → ℕ → (ℕ → Prop) → Prop
| delta0 : PrimrecPred p → ArithmeticalHierarchy Γ 0 p
| exists : ArithmeticalHierarchy .pi s p → ArithmeticalHierarchy .sigma (s + 1) fun x ↦ ∃ y, p (x.pair y)
| forall : ArithmeticalHierarchy .sigma s p → ArithmeticalHierarchy .pi (s + 1) fun x ↦ ∀ y, p (x.pair y)

Of course, this can only be used for predicates of natural numbers (or type which is Primrcodable), but I don't think meaningful definitions can be made for other type of predicates.