Deduction systems for propositional logic given by their rules, and proofs checked with them.
A system is a list of rules written as schemas, so that each exercise can say which rules may be used:
rule ∧I : A, B ⊢ A ∧ B
rule →I : [A] B ⊢ A → B
rule ∨E : A ∨ B, [A] C, [B] C ⊢ C
rule RAA : [¬A] ⊥ ⊢ A
axiom A1 : A → (B → A)In a schema, a capital letter (A, B, C1...) stands for any formula. A premise [A] B is a subproof that
assumes A and ends in B; the rule closes it. ⊢ can be written |-, and the connectives as in the formulas of the
library (&, |, ->, <->, ¬, !F, !T). The systems of LogicUS.PL.DeductionSystems are written in this way.
A proof is written in the style of Fitch, a line per formula, with bars for the subproofs:
1 p → q premise
2 q → r premise
3 | p assumption
4 | q →E 1, 3
5 | r →E 2, 4
6 p → r →I 3-5Lines are cited by their number, and closed subproofs by their first and last lines (3-5). A line can cite the lines
above it that are not inside a closed subproof. An assumption opens a new subproof; a line with fewer bars closes the
subproofs deeper than it. The line numbers at the beginning are optional (lines are numbered by their position), and
% can separate the formula from its justification. premise and assumption can also be written premisa/P and
supuesto/A/hyp. The formulas are read with the syntax of LogicUS.PL.SyntaxSemantics.
The module also gives hints: the rules of the system that can be applied at the end of a proof (to its lines, to its closed subproofs or closing the current one) and those that would give a target formula.
LogicUS.FOL.Deduction (package logicus-fol) extends all this to first-order logic, with the same syntax for rules and
proofs.
An exercise that only allows the rules of the implication, a proof with one wrong line, and what can be done next:
import LogicUS.PL.Deduction as D
rules =
"rule →I : [A] B ⊢ A → B\nrule →E : A → B, A ⊢ B"
proof =
"p -> q premise\nq -> r premise\n| p assumption\n| r ->E 2, 3"
exercise =
{ premises = List.filterMap (Result.toMaybe << D.readFormula) [ "p -> q", "q -> r" ]
, goal = Result.toMaybe (D.readFormula "p -> r")
}
case D.readSystem rules of
Ok sys ->
( D.checkProof sys exercise (D.readProof proof)
, D.hints sys exercise (D.readProof proof) Nothing 5
)
Err e ->
...The report says that line 4 is wrong ("→E (A → B, A ⊢ B) does not give this formula from 2, 3") and that the proof
is not complete; among the hints, →E 1, 3 gives q. A rule that is not valid, such as rule bad : A → B, B ⊢ A, is
still accepted by readSystem (an exercise may want to show why it is wrong), and ruleCounterexample says why it
is not valid.
A premise of a rule: a formula, or a subproof from an assumption to a formula.
A rule: its name, its premises and its conclusion. An axiom is a rule without premises.
A deduction system: the rules that can be used.
It reads a system: a rule per line (rule NAME : premises ⊢ conclusion, or axiom NAME : formula). Empty lines
and lines starting with # or -- are ignored. The errors say the line.
readSystem "rule →E : A → B, A ⊢ B"
== Ok [ { name = "→E", premises = [ PFormula (SImp (SMeta "A") (SMeta "B")), PFormula (SMeta "A") ], conclusion = SMeta "B" } ]It writes a rule as readSystem reads it.
ruleToString { name = "→I", premises = [ PSubproof (SMeta "A") (SMeta "B") ], conclusion = SImp (SMeta "A") (SMeta "B") }
== "rule →I : [A] B ⊢ A → B"It writes a system as readSystem reads it.
It finds a rule of a system by its name. The name can use the ASCII forms of the connectives (->I for →I),
and upper and lower case are not distinguished.
A valuation of the letters of a rule under which its premises are true and its conclusion is false (a subproof
[A] B counts as A → B), if there is one. There is none exactly when the rule is valid in classical logic: then
every step made with it goes from true lines to a true line. Rules that are only valid classically (¬¬E, RAA)
have no counterexample, even in an intuitionistic system.
-- rule bad : A → B, B ⊢ A
ruleCounterexample bad == Just [ ( "A", False ), ( "B", True ) ]It reads a formula in the syntax of LogicUS.PL.SyntaxSemantics (p -> q, ¬p & q_{1}, !F).
It writes a formula (with fplToString).
It writes a formula in the syntax that readFormula reads.
A line of a proof: its depth (the number of open subproofs it is in), its formula, its rule (premise,
assumption or the name of a rule) and the lines it cites ("1, 3", "3-5").
An exercise: its premises and the formula to prove (if any).
The verdict on a line: its number, its formula (if it could be read) and whether it is correct, with an explanation.
The verdict on a proof: a report per line, whether the proof is complete (every line is correct and the last one is the goal, out of every subproof) and a sentence that sums it up.
It reads a proof written as text, a line per formula (see the beginning of the module).
readProof "1 p → q premise\n2 | p assumption\n3 | q →E 1, 2"
== [ { depth = 0, formula = "p → q", rule = "premise", refs = "" }
, { depth = 1, formula = "p", rule = "assumption", refs = "" }
, { depth = 1, formula = "q", rule = "→E", refs = "1, 2" }
]It writes a proof as text, with its line numbers and bars.
It checks a proof with the rules of a system. The premises of the proof must be premises of the problem (if it has any), and the proof is complete when it ends with the goal.
checkProof sys { premises = [ p → q, q → r ], goal = Just (p → r) } (readProof proof)A hint: the rule, the lines it uses (refs), the formula it gives (result), the same formula in the syntax of
the proofs (input), for backward hints what is still needed (unknown parts are written ?A) and the assumptions of
the subproofs it needs (in the syntax of the proofs, when they are known), and a sentence that explains it.
The kind of a hint: a rule applied to the accessible lines and subproofs, a rule that closes the current subproof, or a rule that would give the target.
The rules of the system that can be used at the end of a proof:
CloseSubproof: a rule that closes the subproof that is open at the end, using it;Backward: a rule whose conclusion is the target (or the goal of the problem, when no subproof is open), with
what it still needs; the parts of the premises that are lines of the proof are taken from them;Forward: a rule whose premises are lines and closed subproofs that can be cited there, when its result is
useful: part of the target or of a cited line, or ⊥.Only the correct lines are used. Rules that only copy a line, and results that are already lines that can be cited,
are left out. At most limit hints of each kind are given.
A formula schema.
SMeta "A"stands for any formula.