 Logics may be represented in various ways. Axiom systems, natural deduction systems and trees (or, equivalently, tableaux) are among the most common. This section presents all three for the bivalent inclusive form of free logic known as Positive Free Logic (PFL) and mentions some variants. (For the meaning of the term “positive” in this context see  Section 3.2).  PFL is formulated in a first-order language \(\bL\) without sentence letters or function symbols, whose primitive logical operators are negation (not) ‘\({\sim}\)’, the conditional (if-then) ‘\(\rightarrow\)’, the universal quantifier (for all) ‘\(\forall\)’, identity ‘=’ and ‘E!’, the others being defined as usual. We assume for the sake of definiteness that the formulas of \(\bL\) are closed (contain no unquantified variables) and that they may be vacuously quantified (have the form \(\forall xA\) or \(\exists xA\), where \(x\) does not occur free in \(A)\). An occurrence of a variable is quantified if it lies within the scope of an operator such as ‘\(\forall\)’ or ‘\(\exists\)’ that binds that variable; otherwise it is free.