unicode_fol_kit.modal_faithfulness_theory¶

unicode_fol_kit.modal_faithfulness_theory(theory_name='ModalFaithfulness', formula=None)[source]¶

Emit the self-contained modal deep/maximal/minimal + faithfulness theory.

The returned string is a full theory <theory_name> imports Main begin ... end containing the three embeddings and the five faithfulness theorems, each closed by Isabelle. With a local Isabelle/HOL it is verified end to end by unicode_fol_kit.hol.isabelle_runner.check_theory().

Parameters:

theory_name (str) – the Isabelle theory / file name (a legal identifier).
formula (Node | None) – an optional propositional modal formula. When given, its deep encoding is appended as definition example :: pml (with consts for its atoms), so the certificate is grounded in a concrete formula and the faithfulness theorems specialise to it.

Returns:

The theory text (newline-terminated).

Return type:

str