Deduction systems for first-order logic ready to use with LogicUS.FOL.Deduction, as text that can be edited:
rules can be removed, renamed or added before reading it with readSystem. The rules of the connectives are those of
LogicUS.PL.DeductionSystems (package logicus-pl).
The systems of this module. They have the same names as their propositional versions in
LogicUS.PL.DeductionSystems.
The system of a preset, by name.
Classical natural deduction for first-order logic with equality: the rules of the connectives (intuitionistic and classical), and those of the quantifiers and of equality.
The rules of the quantifiers. In ∀I and ∃E the term a must be new (a variable or a constant that does not
occur in the open assumptions nor in the conclusion).
Reflexivity and Leibniz law (substitution of equals).
Rules that can be derived from the others, for exercises that allow them: those of LogicUS.PL.DeductionSystems
(MT, DS, HS, ¬¬I, LEM, De Morgan laws) and the negation of the quantifiers.
The axiomatic system of LogicUS.PL.DeductionSystems extended to first-order logic: two axiom schemes of the
universal quantifier and the generalization rule.
A system with a name and a short description.