“Definition” was probably a wrong word to use. Since we are talking in the context of provability, I meant “a short string of text that replaces a longer string of text for ease of human reader, but is parsed as a longer string of text when you actually work with it”. Impredicative definitions are indeed quite common, but they go hand in hand with proofs of their consistency, like proof that a functional equation have a solution, or example of a group to prove that group axioms are consistent, or more generally a model of some axiom system.
Sadly I am not familiar with Haskell, so your link is of limited use to me. But it seems to contain a lot of code and no proofs, so it is probably not what I am looking for anyway.
What I am looking for probably looks like a proof of “GL⊢(∃f∀g(f(g)=□g(f)))”. I am in many ways uncertain about whether this is the right formula (is GL a right system to use here (does it even support quantifiers over functional symbols? if not then there should be an extension that does support it); is “does f exist” the right question to be asking here; does “f(g)=□g(f)” correctly describe what we want rom FairBot). But some proof of that kind should exists, overwise why should we think that such FairBot exists/is consistent?
“Definition” was probably a wrong word to use. Since we are talking in the context of provability, I meant “a short string of text that replaces a longer string of text for ease of human reader, but is parsed as a longer string of text when you actually work with it”. Impredicative definitions are indeed quite common, but they go hand in hand with proofs of their consistency, like proof that a functional equation have a solution, or example of a group to prove that group axioms are consistent, or more generally a model of some axiom system.
Sadly I am not familiar with Haskell, so your link is of limited use to me. But it seems to contain a lot of code and no proofs, so it is probably not what I am looking for anyway.
What I am looking for probably looks like a proof of “GL⊢(∃f ∀g (f(g)=□ g(f)))”. I am in many ways uncertain about whether this is the right formula (is GL a right system to use here (does it even support quantifiers over functional symbols? if not then there should be an extension that does support it); is “does f exist” the right question to be asking here; does “f(g)=□g(f)” correctly describe what we want rom FairBot). But some proof of that kind should exists, overwise why should we think that such FairBot exists/is consistent?