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 `NUM`bered (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 `X` and `Y`. 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 immediately inside `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`

### 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
```

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 Propositional Logic.

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 or some proved claims in earlier steps. That is, `R` has to be one of the sequent’s premises or previously proved claims. 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 (`rNUM`s).

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 Propositional Logic.

### 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 `sNUM`ber).

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
```

```just        : // …
```
```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