From Undecidability.FOL Require Import FullSyntax.
From FOL Require Import Arithmetics.
From FOL Require Import Arithmetics.
Definition inv {X Y: Type} (f: Y -> X) (g: X -> Y) := forall x, x = f (g x).
Definition dec (X: Type) := (X + (X -> False))%type.
Definition decider {X: Type} (p: X -> Type) := forall x, dec (p x).
Definition dec (X: Type) := (X + (X -> False))%type.
Definition decider {X: Type} (p: X -> Type) := forall x, dec (p x).
Gödelisation of formulas
Class goedelisation {ops: operators} {ff: falsity_flag} {fns: funcs_signature} {prs: preds_signature}:=
{g: form -> nat; f: nat -> form; inv_fg: inv f g}.
{g: form -> nat; f: nat -> form; inv_fg: inv f g}.
The numeral of a formula's Gödel number
Definition quine_quote {göd: goedelisation} φ := num (g φ).
Lemma qq_closed {göd: goedelisation} A:
bounded_t 0 (quine_quote A).
Proof.
unfold quine_quote. apply num_bound.
Qed.
Lemma qq_closed {göd: goedelisation} A:
bounded_t 0 (quine_quote A).
Proof.
unfold quine_quote. apply num_bound.
Qed.