Deduction systems for first-order logic given by their rules, and proofs checked with them. It extends
LogicUS.PL.Deduction (package logicus-pl) with quantifiers and equality: the rules and the proofs are written in the
same way.
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 ∀I : A[x/a] ⊢ ∀x A if a fresh
rule ∀E : ∀x A ⊢ A[x/t]
rule =E : t = s, A[x/t] ⊢ A[x/s]
axiom A1 : A → (B → A)In a schema, a capital letter (A, B, C1...) stands for any formula; after a quantifier or before / in a
substitution, a lower-case name (x, y) stands for any variable; elsewhere a lower-case name (t, s, a) stands
for any term. A[x/t] is the formula A with the free occurrences of x replaced by t (the replacement must not
capture variables). A premise [A] B is a subproof that assumes A and ends in B; the rule closes it. The side
conditions are a fresh (a is a variable or a constant that does not occur in the conclusion, in the formula A of
A[x/a], in the premises of the proof nor in its open assumptions) and x not free in A. ⊢ can be written |-,
and the connectives as in the formulas of the library (&, |, ->, <->, ¬, !A, !E, !F, !T).
A proof is written in the style of Fitch, a line per formula, with bars for the subproofs:
1 !E[X]P(X) premise
2 !A[X](P(X) -> Q(X)) premise
3 | P(a) assumption
4 | P(a) -> Q(a) ∀E 2
5 | Q(a) →E 4, 3
6 | !E[X]Q(X) ∃I 5
7 !E[X]Q(X) ∃E 1, 3-6Lines are cited by their number, and closed subproofs by their first and last lines (3-6). 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.FOL.SyntaxSemantics (!A[X](P(X) -> Q(X)), a = b).
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.
A term in a schema: a variable (TVar "x", bound by a quantifier of the schema) or any term (TMeta "t").
A premise of a rule: a formula, or a subproof from an assumption to a formula.
A side condition of a rule.
A rule: its name, its premises, its conclusion and its side conditions. 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 [if conditions], or
axiom NAME : formula). Empty lines and lines starting with # or -- are ignored. The errors say the line.
It writes a rule as readSystem reads it.
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.
It reads a formula in the syntax of LogicUS.FOL.SyntaxSemantics.
It writes a formula (with ffolToString).
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"). It is the same as in
LogicUS.PL.Deduction.
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). It is
LogicUS.PL.Deduction.readProof.
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.
A hint: the rule, the lines it uses (refs), the formula it gives (result; unknown parts are written ?A,
?t), the same formula in the syntax of the proofs (input, empty when it has unknown parts), for backward hints
what is still needed 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,SAll "x" sfor∀x s(xstands for any variable) andSSubst s "x" tfors[x/t].