A logic module can define a language for writing formulas.

To define operators or other formula types, define formula classes in the module.

In Flip, every formula and subformula is an instance of a class. In particular, there is a class for each logical operator. For example, consider the formula And(p,Or(q,r)). Here And is a class. This whole formula is an instance of the And class; in fact, it is the constructor expression for that instance. Here also, Or is a class, the subformula Or(q,r) is an instance of the Or class, and p, q, and r are instances of the Letter class.

We define a language for a logic by defining a class for each kind of formula or subformula that can occur. For example, here is the definition of the class And:

class And(InfixLogical):
  """
  And(a,b) means a & b in Kaye. Capitalize And, distinguish from Python keyword
  """
  def __init__(self, *args):
    InfixLogical.__init__(self, *args)
    self.symbol = '&'

This is the entire class definition. Most of its work is done in the base class InfixLogical. We usually define classes by subclassing base classes from the formula module, especially these:

Function, Relation, InfixRelation, PrefixLogical, InfixLogical, Quantifier

A logic module can define inference rules for deriving new formulas from given formulas.

To define rules, put a dictionary named _rules in the module. Each rule is an entry in this dictionary, where the key is the rule name and the value is the rule itself.

In Flip, every inference rule is a list of formulas, with the premises first and the conclusion last. The formulas in an inference rule may contain placeholders that can be matched against formulas from a proof. For example, here is the dictionary entry for a simple inference rule, And-Introduction (which we abbreviate ai):

  ai :  [ m1, m2, And(m1,m2) ]

This rule says that from premises m1 and m2, we can conclude And(m1,m2). The premises m1 and m2 are placeholders that match any formula, and the conclusion And(m1,m2) uses these placeholders. When a proof is checked, m1 and m2 are bound to the actual premises cited in the proof, and the conclusion in the proof is checked against And(m1,m2) with those bindings for m1 and m2 substituted in their places.

An axiom is just an inference rule with no premises. For example, Reflexivity (of Equality, refl) is an axiom:

  refl :  [ Equal(t1,t1) ]

Here is a rule that uses a subproof. Implication-Introduction (impli):

  impli :  [[ m1, m2], Impl(m1,m2) ]

This rule says we need a subproof with premise m1 and conclusion m2. From that subproof, we can conclude the implication Impl(m1,m2). Notice how the subproof is indicated by a nested list.

Here is a rule that illustrates substitution, named Substitution (sub):

  sub :  [ Equal(t1,s1), S1(t1), S1({t1:s1}) ]

From the premise Equal(t1,s1), and from another premise S1 possibly containing the term t1, we can conclude S1 where zero or more occurrences of t1 have been replaced by the term s1. The placeholder S1 indicates a formula where optional substitutions may be performed. The substitution is described here by a Python dictionary with a single key t1 (the source of the substitution) associated with value s1 (the replacement).

Here is a rule that has a subproof with substitutions. Exists-Elimination (Ee):

  Ee :  [ E(v1, P1(v1)), [Let(v2,P1({v1:v2})), Q1({v2:None})], Q1({v2:None}) ]

This rule describes how to eliminate the existential quantifier that appears in E(v1, P1(v1)). We need a subproof that begins with the formula P1 from the body of the quantifier, where all occurrences of the bound variable v1 are replaced by the new free variable v2. The Let formula introduces the new variable, and the placeholder P1 indicates a formula where the substitution must be performed on every occurrence. The subproof concludes with the placeholder Q1({v2:None}), which indicates a formula where the variable v2 does not occur free. From this subproof, we can conclude the formula Q1.

Much of the information in the inference rules is carried by the placeholders. Flip defines these placeholders. Each placeholder (on the left) matches an instance of the class (on the right) that satisfies the given condition.

m1, m2	Formula
v1, v2	Variable
t1, t2, s1	Term (including Variable)
S1(t1)	Formula, may contain term t1
S1({t1:s1})	Formula, where some (zero or more) occurrences of t1 may be replaced by term s1
P1(t1)	Formula, may contain t1
P1({t1:s1})	Formula, where all occurrences of t1 must be replaced by s1
Q1({v2:None})	Formula, where variable v2 does not occur free

In the S1 and P1 patterns, the source, replacement, or both can be restricted to variables by {v1:t1}, {t1:v1}, or {v1:v2}. Flip checks side conditions on substitution: neither the source nor the replacement can contain a variable that is bound in the scope where the substitution occurs.

Flip checks additional side conditions when variable placeholders occur in these formulas:

New(v1)	Variable v1 must not already appear free in the proof
Let(v1, P1(v1))	v1 must not already appear free

A logic module is a Python module that contains formula class definitions and/or inference rules. To use a logic in proofs, we must also provide a session module that loads the logic into the checker and makes its identifiers available in a proof session.

The flip/poset directory demonstrates the recommended way to organize the modules. The logic and session modules should go in the same Python package, which is just a directory that contains those modules, and an __init__.py module -- so poset is a package, not just a directory. The tests for poset go into a test package (subdirectory) in the poset package. (Logics added before version 1.2 do not use this organization. All of those logic modules and session modules are in one flip.logic package, and all their tests are in a separate flip.test package. From now on, no more modules will be added to those packages.)

Imitate existing modules: examine the contents of fol and fol_session, and the several prop (propositional) logic and session modules. But be sure to use the package organization of the new flip.poset packge, and imitate the import statements in the modules in that package.

The classes and rules used in a single proof session are usually divided among several logic modules. This allows different logics to be configured without duplication. For example, prop_session imports from prop_classic and prop_common, while prop_constructive_session imports from prop_constructive and prop_common. The fol_session module imports from fol, prop_classic, and prop_common.

Some logic modules define inference rules but no formula classes; they just use operators defined elsewhere. This is the usual way to add axioms and derived rules. For example, prop_classic, prop_constructive, and prop_derived each define different inference rules, but they all use the operators defined in prop_common.