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.
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.
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.
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).
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.
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.
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).
≡)¶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.
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 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.
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.
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:
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.
just : // …
| '∧e1' rNUM // And-Elimination1
X. R ∧ Q …
Z. R ∧e1 X
just : // …
| '∧e2' rNUM // And-Elimination2
X. P ∧ R …
Z. R ∧e2 X
just : // …
| '∨i1' rNUM // Or-Introduction1
X. P …
Z. P ∨ Q ∨i1 X // R ≡ P ∨ Q
just : // …
| '∨i2' rNUM // Or-Introduction2
X. Q …
Z. P ∨ Q ∨i2 X // R ≡ P ∨ Q
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).
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.
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).
just : // …
| '→i' sNUM // Implication-Introduction
X. {
X1. P assume
…
XK. Q …
…
}
Z. P → Q →i X // R ≡ P → Q
just : // …
| '→e' rNUM rNUM // Implication-Elimination
X. P → R …
Y. P …
Z. R →e X Y
just : // …
| '¬i' sNUM // Negation-Introduction
X. {
X1. P assume
…
XK. ⊥ …
…
}
Z. ¬P ¬i X // R ≡ ¬P
just : // …
| '¬e' rNUM rNUM // Negation-Elimination
X. P …
Y. ¬P …
Z. ⊥ ¬e X Y // R ≡ ⊥
just : // …
| '⊥e' rNUM // ⊥-Elimination
X. ⊥ …
Z. R ⊥e X // R can be anything
just : // …
| 'pbc' sNUM // Proof-by-Contradiction
X. {
X1. ¬R assume
…
XK. ⊥ …
…
}
Z. R pbc
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