Sireum Logika Documentation — 3. The Logika Formal Input Language
3.3. Predicate Logic

# 3.3. Predicate Logic¶

The Logika predicate logic input language is a small extension of its Propositional Logic that adds the following language elements: (1) Extended Sub-Proof Assumption Step, (2) First-Order Uninterpreted Predicate and Function Applications, (3) Universally and Existensially Quantified Claims, and (4) Quantified Claim Justification and Inference Rules.

Similar to the discussion in Propositional Logic, this section only discusses Logika’s rendition of predicate logic natural deductions; the reader is referred to The Predicate-Logic Quantifiers for more intuitive and general discussion on predicate logic.

Predicate Logic Input Language Grammar

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

Logika’s predicate logic input language is similar to that of Propositional Logic, where it consists of a sequent and the sequent’s proof. Here is an example that is also a syllogism:

```∀x human(x) → mortal(x),  ∃y human(y)  ⊢  ∃z mortal(z)
{
1. ∀x human(x) → mortal(x)               premise
2. ∃y human(y)                           premise
3. {
4. a  human(a)                      assume
5. human(a) → mortal(a)             ∀e 1 a
6. mortal(a)                        →e 5 4
7. ∃z mortal(z)                     ∃i 6 a
}
8. ∃z mortal(z)                          ∃e 2 3
}
```

In the subsequent description, only language elements that are new or extend Propositional Logic are discussed. As a reference, the complete predicate logic input language is specified in Predicate Logic Input Language Grammar.

## 3.3.1. Extended Sub-Proof Assumption Step¶

```assumeStep  : rNUM '.' claim 'assume'
| rNUM '.' ID                  // ID must be "fresh" in scope; used for ForAll-Introduction
| rNUM '.' ID claim 'assume'   // ID must be "fresh"; used for Exists-Elimination
```

To support Quantified Claim Justification and Inference Rules, the sub-proof assumption form has to be enhanced.

The first highlighted enhancement is to introduce a “fresh” variable suitable for Forall-Introduction (∀i); here, “fresh” means that the identifier is not used in the scope of the variable; this form is a special one because it is not a regular proof step which has a claim associated with it.

The second highlighted form also introduces a fresh variable, but also has an associated claim assumption that refers to the fresh variable. This form is used for Exists-Elimination (∃e).

## 3.3.2. Extended 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
| ID '(' claimList? ')'        // predicate application
| '(' 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)
| ( '∀'                        // univ. quant., can also use 'forall', 'all', 'A' for '∀'      (also apply in just)
| '∃'                        // exist. quant., can also use 'exists', 'some', 'E' for '∃'    (also apply in just)
) ID ( ',' ID)* claim
```

Similar to propositional logic’s Claim Expression, the predicate logic claim expressions are untyped. One can take the view that all variables in Logika’s predicate logic language are of integer type and all predicates/functions accepts only integers and returns an integer, where zero is treated as `⊥` and non-zero as `⊤`. Integers are desirable in this context instead of booleans because it allows one to quantify over (infinitely) many objects instead of only two.

At any rate, the claim expression language in Logika’s predicate logic has two additional kinds of expression: (1) predicate/function applications, and (2) quantified claims, as highlighted above, and described next.

### 3.3.2.1. First-Order Uninterpreted Predicate and Function Applications¶

```assumeStep  : // …
| ID '(' claimList? ')'        // predicate application

claimList   : claim ( ',' claim )*
```

A predicate is a function that returns either `⊤` or `⊥`. In predicate logic, the meaning of each function is unspecified, thus, uninterpreted.

Instead of depending on function interpretations, Logika’s predicate logic reasoning uses rewriting/substitution, in addition to structural equivalence (`≡`) that is used in propositional logic. The rewriting technique depends on the inherent property that each function is pure – meaning that it produces the same result when given the same arguments regardless of how many times it is applied (invoked/called).

A function is applied by referring to its identifier followed by some ordered arguments (optional) which are separated by a comma (`,`) and delimited by a parenthesis, such as shown in the syllogism example above (and below) for `human` and `mortal`.

Functions have to always be supplied with arguments whenever referred (i.e., they have to always be applied). This makes it easy to distinguish whether an identifier is a predicate, e.g.,:

```∀x human(x) → mortal(x),  human(socrates)  ⊢  mortal(socrates)
{
1. ∀x human(x) → mortal(x)               premise
2. human(socrates)                       premise
3. human(socrates) → mortal(socrates)    ∀e 1 socrates
4. mortal(socrates)                      →e 3 2
}
```

In this popular syllogism, `socrates` is distinguishably a variable (intuitively, it points to Socrates the person, which is mechanically modeled using an integer object made up from `1`s and `0`s), but `human` and `mortal` are predicates (which intuitively, classify whether an object is a human and a mortal, respectively).

In Logika, all functions are first-order, i.e., they do not accept function values as arguments. Note that this does not preclude functions to accepts results of other functions, as illustrated in the following example:

```∀x gt(inc(x), x)     ∀x gt(x, dec(x))
-------------------------------------
∀x gt(inc(x), x)  ∧  gt(x, dec(x))
{
1. ∀x gt(inc(x), x)                      premise
2. ∀x gt(x, dec(x))                      premise
3. {
4. a
5. gt(inc(a), a)                    ∀e 1 a
6. gt(a, dec(a))                    ∀e 2 a
7. gt(inc(a), a)  ∧  gt(a, dec(a))  ∧i 5 6
}
8. ∀x gt(inc(x), x)  ∧  gt(x, dec(x))    ∀i 3
}
```

As can be observed, the `gt` predicate can accepts results of applying functions `inc` and `dec`. (By the way, the example uses uninterpreted functions/predicates to model properties of integer arithmetic operators due to the lack for algebra support in Logika’s predicate logic; instead, it is supported in programming logic later.)

Furthermore, Logika functions cannot be overloaded; each identifier is only associated with exactly one signature. In Logika’s predicate logic, the signature is only determined by the number of its arguments; hence, each function has a fixed number of arguments.

### 3.3.2.2. Universally and Existensially Quantified Claims¶

```claim       : // …
| ( '∀'                        // univ. quant., can also use 'forall', 'all', 'A' for '∀'      (also apply in just)
| '∃'                        // exist. quant., can also use 'exists', 'some', 'E' for '∃'    (also apply in just)
) ID ( ',' ID)* claim
```

Logika’s quantification form can be used to quantify over multiple variables at once (followed by the quantified claim expression), which means the same as if one quantifies over the variables one by one in the same order. For example, `∀x ∀y p(x,y)` is semantically equivalent as `∀x,y p(x,y)`; however, for simplicity, they are not considered as structurally equivalent, i.e., `¬(∀x ∀y p(x,y) ≡ ∀x,y p(x,y))` or `∀x ∀y p(x,y) ≢ ∀x,y p(x,y)`.

## 3.3.3. Well-Formed-Ness¶

For simplicity, Logika does not allow identifier “shadowing”, which means that a variable cannot be quantified more than one time in the same scope. For example, `∀x (… ∧ ∀x …)` is ill-formed in Logika, but `(∀x …)  ∧  (∀x …)` is well-formed.

In general, `x ∧ ∀x …` is well-formed, because the first variable `x` is different than the quantified variable `x`. The first `x` is a free variable because it is not defined/quantified in the expression where it is referred, while the second `x` is defined in the quantification.

However, to avoid confusion, Logika disallows such claim expression. This is because, in the context of a sequent and its proof, all free variables are actually implicitly universally-quantified (even for propositional logic). In that sense, disallowing the same identifier used for as both free and quantified is consistent with the restriction of disallowing identifier shadowing.

## 3.3.4. Abstract Notations and Substitution¶

One abstract notation that is used from now on is to express that a claim `R` that refers to some free variables (in the context of `R` itself) such as `a` and `b`, as: `R{a,b}`. In this notation, the order appearance of variables `a` and `b` do not matter. For example, one can abstract `∀x,y p(x,y))` as `∀x,y Q{x,y}` or `∀x,y Q{y,x}` because both just say that the claim `Q` refers to both `x` and `y`. Thus, in general, when defining a quantification, it is either one of the following forms: `∀a1,...,aN P{a1,...,aN}` (universal), or `∃a1,...,aN P{a1,...,aN}` (existensial), where `N > 0`.

Another notation is for expression substitution. The notation `[E2/E1]R` means all occurences of expression `E1` in `R` is replaced with `E2`; an easy way to remember which one replaces which one is to read `/` as “steps over”, thus `[E2/E1]R` reads as `E2` steps over `E1` in `R`. Here is a concrete example of a substitution, `[x/y]g(y) ≡ g(x)`. Another example, `[f(g(x))/f(y)]g(f(y), f(x)) ≡ g(f(g(x)), f(x))`.

The substitution notation is right-associative. When multiple substitutions are done on an expression at the same time, notated as: `[E2_N/E1_N]…[E2_2/E1_2][E2_1/E1_1]R`, for `N > 1` – it means, `[E2_N/E1_N] (… ([E2_2/E1_2] ([E2_1/E1_1] R)))`. For example, `[z/y][y/x]x ≡ [z/y]([y/x]x) ≡ [z/y]y ≡ z`.

## 3.3.5. Quantified Claim 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
| '∀i'  sNUM                   // Forall-Introduction
| '∀e'  rNUM claim+            // Forall-Elimination
| '∃i'  rNUM claim+            // Exists-Introduction
| '∃e'  rNUM sNUM              // Exists-Elimination
```

There are four new inference rules for Logika’s predicate logic – one introduction rule and one elimination rule for both universal and existensial quantifications.

The subsequent sections assume that each rule is being applied at a regular proof step numbered `Z` and they use the Proof Schematic Pattern to characterize valid inference rule applications.

### 3.3.5.1. Forall-Introduction (∀i)¶

```just        : // …
| '∀i'  sNUM                   // Forall-Introduction
```
Forall-Introduction (∀i) Schematic Pattern
```X. {
X1. a                                                   // variable  a  has to be fresh
…
XK. P{a}                                …
…
}
Z. ∀x P{x}                                   ∀i X            // P{x} ≡ [x/a]P{a}
```

Note that `x` cannot appear in `P{a}`; otherwise, the proof violates the Well-Formed-Ness rules (i.e., such `x` in `P{a}` can only either be a free variable or defined in an enclosing sub-proof, both of which are disallowed).

The following alternative pattern is used grouping multiple quantified variables in a single ∀-quantification.

Alternative Forall-Introduction (∀i) Schematic Pattern
```X. {
X1. a                                                   // variable  a  has to be fresh
…
XK. ∀y1,…,yN P{a}                       …               // N > 0 (otherwise the previous applies)
…
}
Z. ∀x,y1,…,yN P{x}                           ∀i X            // P{x} ≡ [x/a]P{a}
```

### 3.3.5.2. Forall-Elimination (∀e)¶

```just        : // …
| '∀e'  rNUM claim+            // Forall-Elimination
```
Forall-Elimination (∀e) Schematic Pattern
```X. ∀x P{x}                                   …
Z. [E/x]P{x}                                 ∀e X E
```

The following pattern is used for eliminating multiple quantified variables at once.

Alternative Forall-Elimination (∀e) Schematic Pattern
```X. ∀x1,…,xN P{x1,…,xN}                       …               // N > 1 (otherwise the previous applies)
Z. ∀x(K+1),…,xN [E1/x1]…[EK/xK]P{x1,…,xN}    ∀e X E1 … EK    // K <= N
```

The following can be applied for nested ∀-quantifications.

Alternative+1 Forall-Elimination (∀e) Schematic Pattern
```X. ∀x1,…,xK ∀x(K+1),…,xN P{x1,…,xN}          …
Z. ∀x(J+1),…,xN [E1/x1]…[EJ/xK]P{x1,…,xN}    ∀e X E1 … EJ    // 0 < K < J <= N
```

There are actually infinitely many of such patterns according to the level of ∀-quantification nesting that is implemented in Logika (i.e., there exists Alternative+`M` Forall-Elimination (∀e) Schematic Pattern for any positive `M`).

### 3.3.5.3. Exists-Introduction (∃i)¶

```just        : // …
| '∃i'  rNUM claim+            // Exists-Introduction
```
Exists-Introduction (∃i) Schematic Pattern
```X. [E/x]P{x}                                 …
Z. ∃x P{x}                                   ∃i X E
```
Alternative Exists-Introduction (∃i) Schematic Pattern
```X. [E1/x1]…[EK/xK]P{x}                       …
Z. ∃x1,…,xN P{x}                             ∃i X E1 … EK    // K <= N, N > 1 (otherwise the previous applies)
```
Alternative+1 Exists-Introduction (∃i) Schematic Pattern
```X. [E1/x1]…[EJ/xJ]P{x}                       …
Z. ∃x1,…,xK ∃x(K+1),…,xN P{x}                ∃i X E1 … EJ    // 0 < K < J <= N
```

### 3.3.5.4. Exists-Elimination (∃e)¶

```just        : // …
| '∃e'  rNUM sNUM              // Exists-Elimination
```
Exists-Elimination (∃e) Schematic Pattern
```X. ∃x P{x}
Y. {
X1. a  P{a}                                             // variable  a  has to be fresh
…
XK. Q                                   …
…
}
Z. Q                                         ∃e X Y          // P{x} ≡ [x/a]P{a}
```
Alternative Exists-Elimination (∃e) Schematic Pattern
```X. ∃x,y1,…,yN P{x}                                           // N > 0 (otherwise the previous applies)
Y. {
X1. a  ∃y1,…,yN P{a}                                    // variable  a  has to be fresh
…
XK. Q                                   …
…
}
…
Z. Q                                         ∃e X Y          // P{x} ≡ [x/a]P{a}
```

## 3.3.6. Predicate Logic Input Language Grammar¶

Note that extended language elements from that of the Propositional Logic Input Language Grammar are highlighted.

```predicate  : 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'
| rNUM '.' ID                  // ID must be "fresh" in scope; used for ForAll-Introduction
| rNUM '.' ID claim 'assume'   // ID must be "fresh"; used for Exists-Elimination

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
| ID '(' claimList? ')'        // predicate application
| '(' 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)
| ( '∀'                        // univ. quant., can also use 'forall', 'all', 'A' for '∀'      (also apply in just)
| '∃'                        // exist. quant., can also use 'exists', 'some', 'E' for '∃'    (also apply in just)
) ID ( ',' ID)* claim

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