Sireum Logika Documentation — 3. The Logika Formal Input Language
3.2. Propositional Logic

3.2. Propositional Logic

Propositional Logic Input Language Grammar

propositional: sequent proof           // newlines are treated as whitespaces until start of proof

The propositional logic input language consists of two main parts: (1) a sequent, which is followed by (2) a proof of the sequent.

We will show examples later, but an example input has been shown in the Verifying Examples using Sireum CLI section.

3.2.1. Sequent

sequent     : claimList?               // premises
              '⊢'                      // turnstile ("turn-the-style"), can also use '|-' for '⊢'
              claimList                // conclusions

            | claim*                   // premises
              HLINE                    // HLINE is three or more dashes '-'
              claim+                   // conclusions

claimList   : claim ( ',' claim )*

A sequent consists of premises (optional) and conclusions that are separated either by a turnstile or a horizontal line (HLINE) of three or more dashes (-). In the former, each premises and conclusions is separated by a comma ,; the latter separates them using whitespaces (newlines are considered as whitespaces inside sequents).

Here is an example sequent written using the turnstile notation.

p → r,  q → r  ⊢  (p ∨ q) → r

An equivalent sequent to that written using the horizontal line notation is as follows.

 p → r     q → r
-----------------
   (p ∨ q) → r

Either way to express yourself is fine.

3.2.2. Proof

proof       : '{'
                proofStep+             // separated by newline(s)
              '}'

proofStep   : regularStep
            | subProof

regularStep : rNUM '.' claim just        // rNUM is NUM, distinguished for readability of just arguments later

subProof    : sNUM '.'                   // sNUM is NUM, distinguished for readability of just arguments later
              '{'
                assumeStep               // separated by newline(s)
                proofStep*               // separated by newline(s)
              '}'

assumeStep  : rNUM '.' claim 'assume'

A proof consists of a sequence of proof steps delimited by curly braces {}; the proof steps should be separated by newline(s).

Each proof step in the whole proof should be uniquely NUMbered (but can be out of order), and it is either: (a) a regular proof step (atomic), or (b) a sub-proof (composite). (Regular step number rNUM and sub-proof number sNUM are NUM literals, but distinguished here to increase readability of the justification grammar where one applies some inference rules later.)

In addition to its unique number, a regular proof step consists of a claim expression, followed by a justification – a valid application of one of propositional logic inference rules to deduce the claim. A sub-proof in the propositional logic language starts with an assumption (assume justification) that is also a regular proof step with a claim expression, followed by zero or more proof steps (they are delimited inside {} similar to a proof); the steps, including the assumption, should be separated by newline(s).

Here is an example proof of the above sequent: p r,  q r    (p q) r.

{
  1. p → r                    premise
  2. q → r                    premise
  3. {
       4. p ∨ q               assume
       5. {
            6. p              assume
            7. r              →e 1 6
          }
       8. {
            9. q              assume
           10. r              →e 2 9
          }
      11. r                   ∨e 4 5 8
     }
 12. (p ∨ q) → r              →i 3
}

Steps 1, 2, 7, 10, 11, and 12 are regular proof steps; steps 4, 6, and 9 are assumptions; and 3, 5, and 8 are sub-proofs, where 5 and 8 are nested inside 3.

3.2.3. Proof Scoping Rules

When applying an inference rule to justify a proof step, one can refer to proof step numbers preceeding it (i.e., in the order of appearance instead of by their number ordering) in the same level of {} (e.g., 11 refers to 4, 5, and 8) or at the preeceding step numbers in any of its outer {} layers (e.g., 7 refers 1). As a non-example, step 10 cannot refer to step 7 to deduce its claim.

Hence, the scoping rules are similar to variable declaration-usage scoping rules in various programming languages such as Scala or Java, where (with the exception that, again, each proof step number is unique throughout the whole proof, for clarity sake).

3.2.4. Proof Schematic Pattern

The discussion on justification and inference rules uses the following schematic pattern rule and notation.

Consider the situation at a regular proof step numbered Z whose claim expression is R, where Z applies an inference rule I to deduce R, and I requires some claim arguments that can be retrieved from other proof steps, say, numbered Y and Z. The notation is as follows:

X. …
Y. …
Z. R    I X Y

In this notation, X and Y could be the same proof step, do not have be next to each other, out of order, and/or in the same or outer scope layers of Z.

When curly braces are explicitly listed, however, it means that the scope of proof steps are the same. For example:

X. {
     X1. …
     …
     XK. …
     …
   }
Z. R    I X

In this case, X1 and XK have to be in same level and they indicate a prefix sequence of proof steps of X.

3.2.5. Claim Expression

claim       : '⊤'                        // true literal, can also use 'T' or 'true' for '⊤'            (also apply in just)
            | '⊥'                        // false literal, can also use 'F', 'false', or '_|_' for '⊥'  (also apply in just)
            | ID                         // identifier
            | '(' claim ')'              // parenthesized claim expression
            | '¬' claim                  // negation, can also use 'not', 'neg', ''!', or '~' for '¬'    (also apply in just)
            | claim '∧' claim            // conjunction/and, can also use '&', 'and', or '^' for '∧'     (also apply in just)
            | claim '∨' claim            // disjunction/or, can also use '|', 'or', or 'V' for '∨'       (also apply in just)
            | claim '→' claim            // implication, can also use '->' or 'implies' for '→'          (also apply in just)

The claim boolean expression language in propositional logic is rather small; it consists of boolean literals, variable reference (identifier), parenthesized expression, one unary expression (negation), and and/or/imply binary expressions; they are listed in decreasing order of precedence (i.e., first is highest) that is inline with the precedence ordering specified in the Operators and Literals section. Note that variables do not need to be explicitly declared nor typed (they are booleans) in the propositional input language.

3.2.5.1. Newlines in Expression

One newline separator can be inserted after a binary expression operator. For example, P Q is the same as:

P ∧
  Q

but:

P ∧

  Q

where the expressions are separated by more than one newlines, are not because they considered as two separate expressions.

However, newlines are ignored when they appear inside parenthesis. That is:

(P ∧

   Q)

is the same as P Q

These rules follow Scala’s line-orientation (follow the link to see more examples).

3.2.5.2. Expression Equivalence ()

Logika’s propositional logic reasoning mainly uses structural equivalence () that determines equality of two expressions E1 and E2 (i.e., E1 E2) based on whether they have the same structure/form.

A parenthesized expression is structurally (and semantically) equivalent to the expression it contains; it is only used as a means to override operator precedences. In other words, for any Logika expression E, E (E). This equivalence holds even for programming logic expressions.

3.2.6. Justification and Inference Rules

just        : 'premise'
            | '∧i'  rNUM rNUM            // And-Introduction
            | '∧e1' rNUM                 // And-Elimination1
            | '∧e2' rNUM                 // And-Elimination2
            | '∨i1' rNUM                 // Or-Introduction1
            | '∨i2' rNUM                 // Or-Introduction2
            | '∨e'  rNUM sNUM sNUM       // Or-Elimination
            | '→i'  sNUM                 // Implication-Introduction
            | '→e'  rNUM rNUM            // Implication-Elimination
            | '¬i'  sNUM                 // Negation-Introduction
            | '¬e'  rNUM rNUM            // Negation-Elimination
            | '⊥e'  rNUM                 // ⊥-Elimination
            | 'pbc' sNUM                 // Proof-by-Contradiction

Each regular proof step should justify the deduction that it makes to derive its claim by applying some inference rules. This section summarizes Logika’s rendition of propositional logic natural deduction rules that are intuitively described in Applications of Propositional Logic to Program Proving.

The subsequent discussion for each inference rules assumes that it is being applied at a regular proof step numbered Z and whose claim expression that it deduces is R.

3.2.6.1. Premise

just        : 'premise'

The premise justification can be used to call on one of the sequent’s premises associated with the proof. That is, R has to be one of the sequent’s premises. For example,

p,  q  ⊢  q
{
  1. q    premise
}

In this case, R is q (R q) and proof step 1 (Z 1) uses premise to deduce its claim q, which is exactly the second sequent’s premise.

The premise justification can also be used to conjure (true). For example, here is the shortest sequent proof in Logika.

⊢  ⊤
{
  1. ⊤   premise
}

In this example, Z 1 and R . There is no premise in the sequent needed to justify for ; one can always depend on to be true to its true self.

3.2.6.2. And-Introduction (∧i)

just        : // …
            | '∧i'  rNUM rNUM            // And-Introduction

The ∧i rule requires two arguments, which are regular proof step numbers (rNUMs).

Here is a schematic pattern for valid inference using ∧i:

And-Introduction (∧i) Schematic Pattern
X.  P          … // justification for P
Y.  Q          … // justification for Q
Z.  P ∧ Q      ∧i X Y      // R ≡ P ∧ Q

For example,

⊢ ⊤ ∧ ⊤
{
  2. ⊤       premise  // out of order proof step numbering is fine, which is
  1. ⊤ ∧ ⊤   ∧i 2 2   // handy to insert unforeseen proof steps in between others
}

In this case, the pattern is instantiated with X Y 2, P Q , Z 1, and R .

Another example,

p, q ⊢ p ∧ q
{
  1. q       premise
  2. p       premise
  3. p ∧ q   ∧i 2 1
}

In this example, X 2, P p, Y 1, Q q, Z 3, and R p q.

One last example,

p, q ⊢ p ∧ q
{
  1. q       premise
  2. p       premise
  3. p ∧ q   ∧i 2 1
}

In this case, X 1, P q, Y 2, Q p, Z 3, and R q p.

The rest of this section assumes that one already “groks” the basics of schematic pattern by now. Hence, the subsequent is without examples and only discusses new concepts and Logika nuances that enhance the natural deduction rules described in Applications of Propositional Logic to Program Proving.

3.2.6.3. And-Eliminations (∧e1, ∧e2)

And-Elimination1 (∧e1)

just        : // …
            | '∧e1' rNUM                 // And-Elimination1
And-Elimination1 (∧e1) Schematic Pattern
X.  R ∧ Q      …
Z.  R          ∧e1 X

And-Elimination2 (∧e2)

just        : // …
            | '∧e2' rNUM                 // And-Elimination2
And-Elimination2 (∧e2) Schematic Pattern
X.  P ∧ R      …
Z.  R          ∧e2 X

3.2.6.4. Or-Introductions (∨i1, ∨i2)

Or-Introduction1 (∨i1)

just        : // …
            | '∨i1' rNUM                 // Or-Introduction1
Or-Introduction1 (∨i1) Schematic Pattern
X.  P          …
Z.  P ∨ Q      ∨i1 X       // R ≡ P ∨ Q

Or-Introduction1 (∨i2)

just        : // …
            | '∨i2' rNUM                 // Or-Introduction2
Or-Introduction2 (∨i2) Schematic Pattern
X.  Q          …
Z.  P ∨ Q      ∨i2 X       // R ≡ P ∨ Q

3.2.6.5. Or-Elimination (∨e)

just        : // …
            | '∨e'  rNUM sNUM sNUM       // Or-Elimination

The ∨e justification requires two sub-proofs as its second and third arguments (referred by using their proof step sNUMber).

Or-Elimination (∨e) Schematic Pattern
X.  P ∨ Q      …
Y1. {
      Y11. P   assume
      …
      Y1K. R   …
      …
    }
Y2. {
      Y21. Q   assume
      …
      Y2K. R   …
      …
    }
Z.  R          ∨e X Y1 Y2

Note that in the Or-Elimination (∨e) Schematic Pattern above, assumptions Y11 and Y21 must be the first proof step in their corresponding sub-proof.

However, Y1K and Y2K do not have to be the last proof step. This allows the same sub-proofs to be used to “extract” different claims (for example, see logika-examples/src/programming/conditional-1.logika’s lines#43-44; note that “ore” is an alias for ∨e).

Justification of conditional-1.logika’s line#44 leverages the following Logika alternative pattern for ∨e.

Alternative Or-Elimination (∨e) Schematic Pattern
X.  P ∨ Q      …
Y1. {
      Y11. P   assume
      …
      Y1K. R1  …
      …
    }
Y2. {
      Y21. Q   assume
      …
      Y2K. R2  …
      …
    }
Z.  R          ∨e X Y1 Y2  // R ≡ R1,       if R1 ≡ R2
                           // R ≡ R1 ∨ R2,  otherwise

That is, the Alternative Or-Elimination (∨e) Schematic Pattern actually introduces a disjunction!

Note that this pattern is not so useful if Y11 Y1K (thus, P R1) and Y21 Y2K (thus, Q R2), because then R P Q, which is X’s claim (however, it is still a valid deduction).

3.2.6.6. Implication-Introduction (→i)

just        : // …
            | '→i'  sNUM                 // Implication-Introduction
Implication-Introduction (→i) Schematic Pattern
X.  {
      X1. P    assume
      …
      XK. Q    …
      …
    }
Z.  P → Q      →i X        // R ≡ P → Q

3.2.6.7. Implication-Elimination (→e)

just        : // …
            | '→e'  rNUM rNUM            // Implication-Elimination
Implication-Elimination (→e) Schematic Pattern
X.  P → R      …
Y.  P          …
Z.  R          →e X Y

3.2.6.8. Negation-Introduction (¬i)

just        : // …
            | '¬i'  sNUM                 // Negation-Introduction
Negation-Introduction (¬i) Schematic Pattern
X.  {
      X1. P    assume
      …
      XK. ⊥    …
      …
    }
Z.  ¬P         ¬i X        // R ≡ ¬P

3.2.6.9. Negation-Elimination (¬e)

just        : // …
            | '¬e'  rNUM rNUM            // Negation-Elimination
Negation-Elimination (¬e) Schematic Pattern
X.  P          …
Y.  ¬P         …
Z.  ⊥          ¬e X Y      // R ≡ ⊥

3.2.6.10. ⊥-Elimination (⊥e)

just        : // …
            | '⊥e'  rNUM                 // ⊥-Elimination
⊥-Elimination (⊥e) Schematic Pattern
X.  ⊥          …
Z.  R          ⊥e X        // R  can be anything

3.2.6.11. Proof-by-Contradiction (pbc)

just        : // …
            | 'pbc' sNUM                 // Proof-by-Contradiction
Proof-by-Contradiction (pbc) Schematic Pattern
X.  {
      X1. ¬R   assume
      …
      XK. ⊥    …
      …
    }
Z.  R          pbc

3.2.7. Propositional Logic Input Language Grammar

propositional: sequent proof           // newlines are treated as whitespaces until start of proof

sequent     : claimList?               // premises
              '⊢'                      // turnstile ("turn-the-style"), can also use '|-' for '⊢'
              claimList                // conclusions

            | claim*                   // premises
              HLINE                    // HLINE is three or more dashes '-'
              claim+                   // conclusions

claimList   : claim ( ',' claim )*

proof       : '{'
                proofStep+             // separated by newline(s)
              '}'

proofStep   : regularStep
            | subProof

regularStep : rNUM '.' claim just        // rNUM is NUM, distinguished for readability of just arguments later

subProof    : sNUM '.'                   // sNUM is NUM, distinguished for readability of just arguments later
              '{'
                assumeStep               // separated by newline(s)
                proofStep*               // separated by newline(s)
              '}'

assumeStep  : rNUM '.' claim 'assume'

claim       : '⊤'                        // true literal, can also use 'T' or 'true' for '⊤'            (also apply in just)
            | '⊥'                        // false literal, can also use 'F', 'false', or '_|_' for '⊥'  (also apply in just)
            | ID                         // identifier
            | '(' claim ')'              // parenthesized claim expression
            | '¬' claim                  // negation, can also use 'not', 'neg', ''!', or '~' for '¬'    (also apply in just)
            | claim '∧' claim            // conjunction/and, can also use '&', 'and', or '^' for '∧'     (also apply in just)
            | claim '∨' claim            // disjunction/or, can also use '|', 'or', or 'V' for '∨'       (also apply in just)
            | claim '→' claim            // implication, can also use '->' or 'implies' for '→'          (also apply in just)

just        : 'premise'
            | '∧i'  rNUM rNUM            // And-Introduction
            | '∧e1' rNUM                 // And-Elimination1
            | '∧e2' rNUM                 // And-Elimination2
            | '∨i1' rNUM                 // Or-Introduction1
            | '∨i2' rNUM                 // Or-Introduction2
            | '∨e'  rNUM sNUM sNUM       // Or-Elimination
            | '→i'  sNUM                 // Implication-Introduction
            | '→e'  rNUM rNUM            // Implication-Elimination
            | '¬i'  sNUM                 // Negation-Introduction
            | '¬e'  rNUM rNUM            // Negation-Elimination
            | '⊥e'  rNUM                 // ⊥-Elimination
            | 'pbc' sNUM                 // Proof-by-Contradiction