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.
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).
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.
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 1s and 0s), 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.
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).
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.
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.
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
| '∀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.
just : // …
| '∀i' sNUM // Forall-Introduction
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.
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}
just : // …
| '∀e' rNUM claim+ // Forall-Elimination
X. ∀x P{x} …
Z. [E/x]P{x} ∀e X E
The following pattern is used for eliminating multiple quantified variables at once.
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.
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).
just : // …
| '∃i' rNUM claim+ // Exists-Introduction
X. [E/x]P{x} …
Z. ∃x P{x} ∃i X E
X. [E1/x1]…[EK/xK]P{x} …
Z. ∃x1,…,xN P{x} ∃i X E1 … EK // K <= N, N > 1 (otherwise the previous applies)
X. [E1/x1]…[EJ/xJ]P{x} …
Z. ∃x1,…,xK ∃x(K+1),…,xN P{x} ∃i X E1 … EJ // 0 < K < J <= N
just : // …
| '∃e' rNUM sNUM // Exists-Elimination
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}
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}
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
| 'pbc' sNUM // Proof-by-Contradiction
| '∀i' sNUM // Forall-Introduction
| '∀e' rNUM claim+ // Forall-Elimination
| '∃i' rNUM claim+ // Exists-Introduction
| '∃e' rNUM sNUM // Exists-Elimination