unicode_fol_kit.intuitionistic_faithfulness_theory¶

unicode_fol_kit.intuitionistic_faithfulness_theory(theory_name='IntFaithfulness', formula=None)[source]¶

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

See unicode_fol_kit.hol.deepshallow.modal.modal_faithfulness_theory(); this is the intuitionistic-Kripke counterpart. With a local Isabelle/HOL it is verified end to end by unicode_fol_kit.hol.isabelle_runner.check_theory().

Parameters:

theory_name (str)
formula (Node | None)

Return type:

str