- $p$ è fbf;
- Se $\varphi$ è una fbf allora $\neg\varphi$ è una fbf;
- Se $\varphi$ e $\psi$ sono fbf allora pure $\varphi \wedge \psi$ è una fbf:
- nient'altro è una fbf:
Se è vero che le fbf si fanno nel metalinguaggio è corretto affermare che, introducendo nell'alfabeto di quest'ultimo le (meta)variabili indicate con le lettere greche, i vari connettivi logici (quelli fondamentali come l'et ed il not dai quali si ricavano per def tutti gli altri), la definizione per ricorsione sopra è un predicato del metalinguaggio (chiamiamolo con fbf()) che va descritto tramite il connettivo "se e e solo se" del metalinguaggio? Ho un'idea vaga e fumosa di come introdurlo ma non oso scriverlo perchè c'è un miscuglio con le variabili e dei connettivi del linguaggio oggetto. Sostanzialmente usando un vel (del metalinguaggio) posso incorporare le prime tre clausole e poi definire fbf() con un se e solo se (del metalinguaggio) ponendo a destra del "$\leftrightarrow$" tale composizione dei diversi vel. In particolar modo il "$\leftarrow$" corrisponderebbe alla clausola d).
Qual è il metodo rigoroso per introdurre la definizione per rcorsione?